search_sat.h

Go to the documentation of this file.

/*****************************************************************************/
/*!
 *\file search_sat.h
 *\brief Search engine that uses an external SAT engine
 *
 * Author: Clark Barrett
 *
 * Created: Mon Dec  5 17:52:05 2005
 *
 * <hr>
 * Copyright (C) 2005 by the Board of Trustees of Leland Stanford
 * Junior University and by New York University. 
 *
 * License to use, copy, modify, sell and/or distribute this software
 * and its documentation for any purpose is hereby granted without
 * royalty, subject to the terms and conditions defined in the \ref
 * LICENSE file provided with this distribution.  In particular:
 *
 * - The above copyright notice and this permission notice must appear
 * in all copies of the software and related documentation.
 *
 * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES,
 * EXPRESSED OR IMPLIED.  USE IT AT YOUR OWN RISK.
 * 
 * <hr>
 * 
 */
/*****************************************************************************/

#ifndef _cvcl__include__search_sat_h_
#define _cvcl__include__search_sat_h_

#include <vector>
#include "search.h"
#include "smartcdo.h"
#include "cdlist.h"
#include "cnf_manager.h"
#include "expr.h"
#include "dpllt.h"
#include "theory_core.h"

namespace CVCL {

//! Search engine that connects to a generic SAT reasoning module
/*! \ingroup SE */
class SearchSat :public SearchEngine {

  //! Name of search engine
  std::string d_name;

  //! Bottom scope for current query
  CDO<int> d_bottomScope;

  //! Last expr checked for validity
  CDO<Expr> d_lastCheck;

  /*! @brief Theorem from the last successful checkValid call.  It is
    used by getProof and getAssumptions. */
  CDO<Theorem> d_lastValid;

  //! List of all user assumptions
  CDList<Theorem> d_userAssumptions;

  //! List of all internal assumptions
  CDList<Theorem> d_intAssumptions;

  //! Index to where unprocessed assumptions start
  CDO<unsigned> d_idxUserAssump;

  TheoryCore::CoreSatAPI* d_coreSatAPI;

  //! Pointer to DPLLT implementation
  SAT::DPLLT* d_dpllt;

  //! Implementation of TheoryAPI for DPLLT
  SAT::DPLLT::TheoryAPI* d_theoryAPI;

  //! Implementation of Decider for DPLLT
  SAT::DPLLT::Decider* d_decider;

  //! Store of theorems for expressions sent to DPLLT
  CDMap<Expr, Theorem> d_theorems;

  //! Manages CNF formula and its relationship to original Exprs and Theorems
  SAT::CNF_Manager *d_cnfManager;

  //! Cached values of variables
  std::vector<SmartCDO<SAT::Var::Val> > d_vars;

  //! Whether we are currently in a call to dpllt->checkSat
  bool d_inCheckSat;

  //! CNF Formula used for theory lemmas
  SAT::CD_CNF_Formula d_lemmas;

  //! Current position in d_lemmas
  CDO<unsigned> d_lemmasNext;

  //! Vector of CNF literals which represent Exprs with no fanouts
  CDList<SAT::Lit> d_rootLits;

  //! Last Var registered with core theory
  CDO<unsigned> d_lastRegisteredVar;

  //! Whether it's OK to call DPLLT solver from the current scope
  CDO<bool> d_dplltReady;

  CDO<unsigned> d_nextImpliedLiteral;

  //! Helper class for resetting DPLLT engine
  /*! We need to be notified when the scope goes below the scope from
   *  which the last invalid call to checkValid originated.  This helper class
   *  ensures that this happens.
   */
  friend class Restorer;
  class Restorer :public ContextNotifyObj {
    SearchSat* d_ss;
    public:
      Restorer(Context* context, SearchSat* ss)
        : ContextNotifyObj(context), d_ss(ss) {}
    void notifyPre()
    { if (!d_ss->d_inCheckSat && d_context->level() == d_ss->getBottomScope())
      d_ss->restoreDPLLT(); }
  };
  //! Instance of Restorer class
  Restorer d_restorer;

private:

  //! Tell DPLLT object to go back to state before last satisfiable check
  void restoreDPLLT() { d_dpllt->returnFromSat(); }

  friend class SearchSatCoreSatAPI;
  //! Core theory callback which adds a new lemma from the core theory
  void addLemma(const Theorem& thm);
  //! Core theory callback which asks for the bottom scope for current query
  int getBottomScope() { return d_bottomScope; }
  //! Core theory callback which suggests a splitter
  void addSplitter(const Expr& e, int priority);

  friend class SearchSatTheoryAPI;
  //! DPLLT callback to inform theory that a literal has been assigned
  void assertLit(SAT::Lit l);
  //! DPLLT callback to ask if theory has detected inconsistency.
  SAT::DPLLT::ConsistentResult checkConsistent(SAT::Clause& c,bool fullEffort);
  //! DPLLT callback to get theory propagations.
  SAT::Lit getImplication();
  //! DPLLT callback to explain a theory propagation.
  void getExplanation(SAT::Lit l, SAT::Clause& c);
  //! DPLLT callback to get more general theory clauses.
  bool getNewClauses(SAT::CNF_Formula& cnf);

  friend class SearchSatDecider;
  //! DPLLT callback to decide which literal to split on next
  SAT::Lit makeDecision();

  //! Recursively traverse DAG looking for a splitter
  /*! Returns true if a splitter is found, false otherwise.  The splitter is
   * returned in lit (lit should be set to true).  Nodes whose current value is
   * fully justified are marked by calling setFlag to avoid searching them in
   * the future.
   */
  bool findSplitterRec(SAT::Lit lit, SAT::Var::Val value,
                       SAT::Lit* litDecision);

  //! Get the value of a CNF Literal
  SAT::Var::Val getValue(SAT::Lit c) {
    DebugAssert(!c.isVar() || unsigned(c.getVar()) < d_vars.size(),
                "Lit out of bounds in getValue");
    return c.isFalse() ? SAT::Var::FALSE : c.isTrue() ? SAT::Var::TRUE :
      c.isInverted() ? SAT::Var::invertValue(d_vars[c.getVar()]) :
      d_vars[c.getVar()]; }

  //! Set the value of a variable
  void setValue(SAT::Var v, SAT::Var::Val val) {
    DebugAssert(!v.isNull(), "expected non-null Var");
    DebugAssert(unsigned(v) < d_vars.size(), "Var out of bounds in getValue");
    d_vars[v] = val; }

  //! Check whether this variable's value is justified
  bool checkJustified(SAT::Var v)
    { return d_cnfManager->concreteLit(v).isJustified(); }

  //! Mark this variable as justified
  void setJustified(SAT::Var v)
    { d_cnfManager->concreteLit(v).setJustified(); }

  //! Main checking procedure shared by checkValid and restart
  Theorem check(const Expr& e, bool isRestart = false);

public:

  //! Constructor
  SearchSat(TheoryCore* core);

  //! Destructor
  virtual ~SearchSat();

  // Implementation of virtual SearchEngine methods
  virtual const std::string& getName() { return d_name; }
  virtual void registerAtom(const Expr& e);
  virtual Theorem getImpliedLiteral();
  virtual Theorem checkValid(const Expr& e) { return check(e); }
  virtual Theorem restart(const Expr& e) { return check(e, true); }
  virtual void returnFromCheck();
  virtual Theorem lastThm() { return d_lastValid; }
  virtual Theorem newUserAssumption(const Expr& e, int scope = -1);
  virtual void getUserAssumptions(std::vector<Expr>& assumptions);
  virtual void getInternalAssumptions(std::vector<Expr>& assumptions);
  virtual void getAssumptions(std::vector<Expr>& assumptions);
  virtual bool isAssumption(const Expr& e);
  virtual void getCounterExample(std::vector<Expr>& assertions,
                                 bool inOrder = true);
  virtual Proof getProof();

};

}

#endif

---