search_impl_base.h

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file search_impl_base.h
 * \brief Abstract API to the proof search engine
 * 
 * Author: Clark Barrett, Vijay Ganesh (Clausal Normal Form Converter)
 * 
 * Created: Fri Jan 17 13:35:03 2003
 *
 * <hr>
 *
 * 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.
 * 
 * <hr>
 * 
 */
/*****************************************************************************/

#ifndef _cvc3__include__search_impl_base_h_
#define _cvc3__include__search_impl_base_h_

#include "search.h"
#include "theory_core.h"
#include "variable.h"
#include "formula_value.h"

namespace CVC3 {

class SearchEngineRules;
class VariableManager;

  //! API to to a generic proof search engine (a.k.a. SAT solver) 
  /*! \ingroup SE */
class SearchImplBase :public SearchEngine {
  friend class DecisionEngine;
protected:
  /*! \addtogroup SE 
   * @{
   */
  //! Variable manager for classes Variable and Literal
  VariableManager* d_vm;

  /*! @brief The bottom-most scope for the current call to checkSAT (where conflict
    clauses are still valid).
  */
  CDO<int> d_bottomScope;

  TheoryCore::CoreSatAPI* d_coreSatAPI_implBase;

  //! Representation of a DP-suggested splitter
  class Splitter {
    Literal d_lit;
  public:
    // int priority;
    //! Constructor
    Splitter(const Literal& lit);
    //! Copy constructor
    Splitter(const Splitter& s);
    //! Assignment
    Splitter& operator=(const Splitter& s);
    //! Descructor
    ~Splitter();
    operator Literal() { return d_lit; }
    //! The order is descending by priority ("reversed", highest first)
//     friend bool operator<(const Splitter& s1, const Splitter& s2) {
//       return (s1.priority > s2.priority
//        || (s1.priority == s2.priority && s1.expr > s2.expr));
//     }
  };
  //! Backtracking ordered set of DP-suggested splitters
  CDList<Splitter> d_dpSplitters;

  /*! @brief Theorem from the last successful checkValid call.  It is
    used by getProof and getAssumptions. */
  Theorem d_lastValid;
  /*! @brief Assumptions from the last unsuccessful checkValid call.
    These are used by getCounterExample. */
  ExprHashMap<bool> d_lastCounterExample;
  /*! @brief Maintain the list of current assumptions (user asserts and
   splitters) for getAssumptions(). */
  CDMap<Expr,Theorem> d_assumptions;

  //! Backtracking cache for the CNF generator
  CDMap<Expr, Theorem> d_cnfCache;
  //! Backtracking set of new variables generated by CNF translator
  /*! Specific search engines do not have to split on these variables */
  CDMap<Expr, bool> d_cnfVars;
  //! Command line flag whether to convert to CNF
  const bool* d_cnfOption;
  //! Flag: whether to convert term ITEs into CNF
  const bool* d_ifLiftOption;
  //! Flag: ignore auxiliary CNF variables when searching for a splitter
  const bool* d_ignoreCnfVarsOption;
  //! Flag: Preserve the original formula with +cnf (for splitter heuristics)
  const bool* d_origFormulaOption;

  /*!
   * \name CNF Caches 
   *
   * These caches are for subexpressions of the translated formula
   * phi, to avoid expanding phi into a tree.  We cannot use
   * d_cnfCache for that, since it is effectively non-backtracking,
   * and we do not know if a subexpression of phi was translated at
   * the current level, or at some other (inactive) branch of the
   * decision tree.
   * @{
   */
  //! Cache for enqueueCNF()
  CDMap<Expr,bool> d_enqueueCNFCache;
  //! Cache for applyCNFRules()
  CDMap<Expr,bool> d_applyCNFRulesCache;
  //! Cache for replaceITE()
  CDMap<Expr,Theorem> d_replaceITECache;
  /*@}*/ // End of CNF Caches

  //! Construct a Literal out of an Expr or return an existing one
  Literal newLiteral(const Expr& e) { return Literal(d_vm, e); }

  /*! @brief Our version of simplifier: take Theorem(e), apply
    simplifier to get Theorem(e==e'), return Theorem(e') */
  Theorem simplify(const Theorem& e)
    { return d_core->iffMP(e, d_core->simplify(e.getExpr())); }

  //! Notify the search engine about a new literal fact.
  /*! It should be called by SearchEngine::addFact() only.
   *  Must be implemented by the subclasses of SearchEngine.
   *
   * IMPORTANT: do not call addFact() from this function; use
   * enqueueFact() or setInconsistent() instead.
   */
  virtual void addLiteralFact(const Theorem& thm) = 0;
  //! Notify the search engine about a new non-literal fact.
  /*! It should be called by SearchEngine::addFact() only.
   *  Must be implemented by the subclasses of SearchEngine.
   *
   * IMPORTANT: do not call addFact() from this function; use
   * enqueueFact() or setInconsistent() instead.
   */
  virtual void addNonLiteralFact(const Theorem& thm) = 0;
  //! Add a new fact to the search engine bypassing CNF converter
  /*! Calls either addLiteralFact() or addNonLiteralFact()
   * appropriately, and converts to CNF when d_cnfOption is set.  If
   * fromCore==true, this fact already comes from the core, and
   * doesn't need to be reported back to the core.
   */
  void addCNFFact(const Theorem& thm, bool fromCore=false);

 public:

  int getBottomScope() { return d_bottomScope; }

  //! Check if e is a clause (a literal, or a disjunction of literals)
  bool isClause(const Expr& e);

  //! Check if e is a propositional clause
  /*! \sa isPropAtom() */
  bool isPropClause(const Expr& e);
  //! Check whether e is a fresh variable introduced by the CNF converter
  /*! Search engines do not need to split on those variables in order
   * to be complete
   */
  bool isCNFVar(const Expr& e) { return (d_cnfVars.count(e) > 0); }
  //! Check if a splitter is required for completeness
  /*! Currently, it checks that 'e' is not an auxiliary CNF variable */
  bool isGoodSplitter(const Expr& e);

 private:

  //! Translate theta to CNF and enqueue the new clauses
  void enqueueCNF(const Theorem& theta);
  //! Recursive version of enqueueCNF()
  void enqueueCNFrec(const Theorem& theta);
  //! FIXME: write a comment
  void applyCNFRules(const Theorem& e);
  
  //! Cache a theorem phi <=> v by phi, where v is a literal.
  void addToCNFCache(const Theorem& thm);

  //! Find a theorem phi <=> v by phi, where v is a literal.
  /*! \return Null Theorem if not found. */
  Theorem findInCNFCache(const Expr& e);

  //! Replaces ITE subexpressions in e with variables
  Theorem replaceITE(const Expr& e);
  
protected:

  //! Return the current scope level (for convenience)
  int scopeLevel() { return d_core->getCM()->scopeLevel(); }

public:
  //! Constructor
  SearchImplBase(TheoryCore* core);
  //! Destructor
  virtual ~SearchImplBase();

  virtual void registerAtom(const Expr& e)
    { d_core->theoryOf(e)->registerAtom(e, Theorem()); }
  virtual Theorem getImpliedLiteral() { return d_core->getImpliedLiteral(); }
  virtual void push() { d_core->getCM()->push(); }
  virtual void pop() { d_core->getCM()->pop(); }

  ///////////////////////////////////////////////////////////////////////////
  // checkValid() is the method that subclasses must implement.
  ///////////////////////////////////////////////////////////////////////////

  //! Checks the validity of a formula in the current context
  /*! The method that actually calls the SAT solver (implemented in a
    subclass).  It should maintain d_assumptions (add all asserted
    splitters to it), and set d_lastValid and d_lastCounterExample
    appropriately before exiting. */
  virtual QueryResult checkValidInternal(const Expr& e) = 0;
  //! Similar to checkValidInternal(), only returns Theorem(e) or Null
  virtual QueryResult checkValid(const Expr& e, Theorem& result);
  //! Reruns last check with e as an additional assumption
  virtual QueryResult restartInternal(const Expr& e) = 0;
  //! Reruns last check with e as an additional assumption
  virtual QueryResult restart(const Expr& e, Theorem& result);
  void returnFromCheck()
    { Theorem thm; restart(d_core->falseExpr(), thm); }
  virtual Theorem lastThm() { return d_lastValid; }

  ///////////////////////////////////////////////////////////////////////////
  // The following methods are provided by the base class, and in most
  // cases should be sufficient.  However, they are virtual so that
  // subclasses can add functionality to them if needed.
  ///////////////////////////////////////////////////////////////////////////

  /*! @brief Generate and add a new assertion to the set of assertions
    in the current context.  This should only be used by class VCL in
    assertFormula(). */
  Theorem newUserAssumption(const Expr& e);
  //! Add a new internal asserion
  virtual Theorem newIntAssumption(const Expr& e);
  //! Helper for above function
  void newIntAssumption(const Theorem& thm);
  //! Get all assumptions made in this and all previous contexts.
  /*! \param assumptions should be an empty vector which will be filled \
    with the assumptions */
  void getUserAssumptions(std::vector<Expr>& assumptions);
  void getInternalAssumptions(std::vector<Expr>& assumptions);
  virtual void getAssumptions(std::vector<Expr>& assumptions);
  //! Check if the formula has been assumed
  virtual bool isAssumption(const Expr& e);

  //! Add a new fact to the search engine from the core
  /*! It should be called by TheoryCore::assertFactCore(). */
  void addFact(const Theorem& thm);

  //! Suggest a splitter to the SearchEngine
  /*! The higher is the priority, the sooner the SAT solver will split
   * on it.  It can be positive or negative (default is 0).
   *
   * The set of suggested splitters is backtracking; that is, a
   * splitter is "forgotten" once the scope is backtracked.
   *
   * This method can be used either to change the priority
   * of existing splitters, or to introduce new splitters that DPs
   * consider relevant, even though they do not appear in existing
   * formulas.
   */
  virtual void addSplitter(const Expr& e, int priority);
  
  virtual void getCounterExample(std::vector<Expr>& assertions, bool inOrder = true);

  // The following two methods should be called only after a checkValid
  // which returns true.  In any other case, they return Null values.

  //! Returns the proof term for the last proven query
  /*! It should be called only after a checkValid which returns true.
    In any other case, it returns Null. */
  virtual Proof getProof();
  /*! @brief Returns the set of assumptions used in the proof.  It
    should be a subset of getAssumptions(). */
  /*! It should be called only after a checkValid which returns true.
    In any other case, it returns Null. */
  virtual const Assumptions& getAssumptionsUsed();

  //! Process result of checkValid
  void processResult(const Theorem& res, const Expr& e);

  //:ALEX:
  inline virtual FormulaValue getValue(const CVC3::Expr& e) {
    FatalAssert(false, "not implemented");
    return UNKNOWN_VAL;
  }

  /* @} */ // end of group SE

};


}

#endif