Search Engine
[Validity Checker]

Collaboration diagram for Search Engine:

Modules

• Fast Search Engine
• Simple Search Engine
• Decision Engine

  Decision Engine, used by Search Engine.
  

• Proof Rules for the Search Engines

Classes

• class CVCL::SearchEngine

  API to to a generic proof search engine. More...
  

• class CVCL::SearchImplBase

  API to to a generic proof search engine (a.k.a. SAT solver). More...
  

• class CVCL::SearchImplBase::Splitter

  Representation of a DP-suggested splitter. More...
  

• class CVCL::SearchSat

  Search engine that connects to a generic SAT reasoning module. More...
  

Functions

• SearchEngineRules * CVCL::SearchEngine::createRules ()

  Create the trusted component.
  

• CVCL::SearchEngine::SearchEngine (TheoryCore *core)

  Constructor.
  

• virtual CVCL::SearchEngine::~SearchEngine ()

  Destructor.
  

• virtual const std::string & CVCL::SearchEngine::getName ()=0

  Name of this search engine.
  

• TheoryCore * CVCL::SearchEngine::theoryCore ()

  Accessor for TheoryCore.
  

• virtual void CVCL::SearchEngine::registerAtom (const Expr &e)=0

  Register an atomic formula of interest.
  

• virtual Theorem CVCL::SearchEngine::getImpliedLiteral ()=0

  Return next literal implied by last assertion. Null Expr if none.
  

• virtual Theorem CVCL::SearchEngine::checkValid (const Expr &e)=0

  Checks the validity of a formula in the current context.
  

• virtual Theorem CVCL::SearchEngine::restart (const Expr &e)=0

  Reruns last check with e as an additional assumption.
  

• virtual void CVCL::SearchEngine::returnFromCheck ()=0

  Returns to context immediately before last call to checkValid.
  

• virtual Theorem CVCL::SearchEngine::lastThm ()=0

  Returns the result of the most recent valid theorem.
  

• virtual Theorem CVCL::SearchEngine::newUserAssumption (const Expr &e, int scope=-1)=0

  Generate and add an assumption to the set of assumptions in the current context.
  

• virtual void CVCL::SearchEngine::getUserAssumptions (std::vector< Expr > &assumptions)=0

  Get all user assumptions made in this and all previous contexts.
  

• virtual void CVCL::SearchEngine::getInternalAssumptions (std::vector< Expr > &assumptions)=0

  Get assumptions made internally in this and all previous contexts.
  

• virtual void CVCL::SearchEngine::getAssumptions (std::vector< Expr > &assumptions)=0

  Get all assumptions made in this and all previous contexts.
  

• virtual bool CVCL::SearchEngine::isAssumption (const Expr &e)=0

  Check if the formula has already been assumed previously.
  

• virtual void CVCL::SearchEngine::getCounterExample (std::vector< Expr > &assertions, bool inOrder=true)=0

  Will return the set of assertions which make the queried formula false.
  

• virtual Proof CVCL::SearchEngine::getProof ()=0

  Returns the proof term for the last proven query.
  

• void CVCL::SearchEngine::getConcreteModel (ExprMap< Expr > &m)

  Build a concrete Model (assign values to variables), should only be called after an invalid query.
  

Variables

• TheoryCore * CVCL::SearchEngine::d_core

  Access to theory reasoning.
  

• CommonProofRules * CVCL::SearchEngine::d_commonRules

  Common proof rules.
  

• SearchEngineRules * CVCL::SearchEngine::d_rules

  Proof rules for the search engine.
  

• VariableManager * CVCL::SearchImplBase::d_vm

  Variable manager for classes Variable and Literal.
  

• CDO< int > CVCL::SearchImplBase::d_bottomScope

  The bottom-most scope for the current call to checkSAT (where conflict clauses are still valid).
  

• TheoryCore::CoreSatAPI * CVCL::SearchImplBase::d_coreSatAPI_implBase
• CDList< Splitter > CVCL::SearchImplBase::d_dpSplitters

  Backtracking ordered set of DP-suggested splitters.
  

• Theorem CVCL::SearchImplBase::d_lastValid

  Theorem from the last successful checkValid call. It is used by getProof and getAssumptions.
  

• ExprHashMap< bool > CVCL::SearchImplBase::d_lastCounterExample

  Assumptions from the last unsuccessful checkValid call. These are used by getCounterExample.
  

• CDMap< Expr, Theorem > CVCL::SearchImplBase::d_assumptions

  Maintain the list of current assumptions (user asserts and splitters) for getAssumptions().
  

• CDMap< Expr, Theorem > CVCL::SearchImplBase::d_cnfCache

  Backtracking cache for the CNF generator.
  

• CDMap< Expr, bool > CVCL::SearchImplBase::d_cnfVars

  Backtracking set of new variables generated by CNF translator.
  

• const bool * CVCL::SearchImplBase::d_cnfOption

  Command line flag whether to convert to CNF.
  

• const bool * CVCL::SearchImplBase::d_ifLiftOption

  Flag: whether to convert term ITEs into CNF.
  

• const bool * CVCL::SearchImplBase::d_ignoreCnfVarsOption

  Flag: ignore auxiliary CNF variables when searching for a splitter.
  

• const bool * CVCL::SearchImplBase::d_origFormulaOption

  Flag: Preserve the original formula with +cnf (for splitter heuristics).
  

---

Detailed Description

The search engine includes Boolean reasoning and coordinates with theory reasoning. It consists of a generic abstract API (class SearchEngine) and subclasses implementing concrete instances of search engines.

---

Function Documentation

SearchEngineRules * SearchEngine::createRules (   )  [protected, inherited]

Create the trusted component. This function is defined in search_theorem_producer.cpp Definition at line 50 of file search_theorem_producer.cpp. References CVCL::SearchEngine::d_core, and CVCL::TheoryCore::getTM(). Referenced by CVCL::SearchEngine::SearchEngine().

SearchEngine::SearchEngine (  TheoryCore *  core  )  [inherited]

Constructor. Definition at line 42 of file search.cpp. References CVCL::SearchEngine::createRules(), and CVCL::SearchEngine::d_rules.

SearchEngine::~SearchEngine (   )  [virtual, inherited]

Destructor. Definition at line 51 of file search.cpp. References CVCL::SearchEngine::d_rules.

virtual const std::string& CVCL::SearchEngine::getName (   )  [pure virtual, inherited]

Name of this search engine. Implemented in CVCL::SearchEngineFast, CVCL::SearchSat, and CVCL::SearchSimple. Referenced by CVCL::VCL::reprocessFlags().

TheoryCore* CVCL::SearchEngine::theoryCore (   )  [inline, inherited]

Accessor for TheoryCore. Definition at line 88 of file search.h. References CVCL::SearchEngine::d_core.

virtual void CVCL::SearchEngine::registerAtom (  const Expr &  e  )  [pure virtual, inherited]

Register an atomic formula of interest. Registered atoms are tracked by the decision procedures. If one of them is deduced to be true or false, it is added to a list of implied literals. Implied literals can be retrieved with the getImpliedLiteral function Implemented in CVCL::SearchImplBase, and CVCL::SearchSat. Referenced by CVCL::VCL::registerAtom().

virtual Theorem CVCL::SearchEngine::getImpliedLiteral (   )  [pure virtual, inherited]

Return next literal implied by last assertion. Null Expr if none. Returned literals are either registered atomic formulas or their negation Implemented in CVCL::SearchImplBase, and CVCL::SearchSat. Referenced by CVCL::VCL::getImpliedLiteral().

virtual Theorem CVCL::SearchEngine::checkValid (  const Expr &  e  )  [pure virtual, inherited]

Checks the validity of a formula in the current context. If the query is valid, it returns a theorem and the scope and context should be the same as when called. If the query is invalid, it returns a NULL theorem and the context will be one which falsifies the query. Implemented in CVCL::SearchImplBase, and CVCL::SearchSat. Referenced by CVCL::VCL::assertFormula(), CVCL::SearchEngine::getConcreteModel(), CVCL::VCL::query(), and CVCL::VCL::simplifyThm().

virtual Theorem CVCL::SearchEngine::restart (  const Expr &  e  )  [pure virtual, inherited]

Reruns last check with e as an additional assumption. This method should only be called after a query which is invalid. Implemented in CVCL::SearchImplBase, and CVCL::SearchSat. Referenced by CVCL::VCL::checkContinue(), and CVCL::VCL::restart().

virtual void CVCL::SearchEngine::returnFromCheck (   )  [pure virtual, inherited]

Returns to context immediately before last call to checkValid. This method should only be called after a query which is invalid. Implemented in CVCL::SearchImplBase, and CVCL::SearchSat. Referenced by CVCL::VCL::returnFromCheck().

virtual Theorem CVCL::SearchEngine::lastThm (   )  [pure virtual, inherited]

Returns the result of the most recent valid theorem. Returns Null Theorem if last call was not valid Implemented in CVCL::SearchImplBase, and CVCL::SearchSat. Referenced by CVCL::SearchEngine::getConcreteModel().

virtual Theorem CVCL::SearchEngine::newUserAssumption (  const Expr &  e, int  scope = -1 )  [pure virtual, inherited]

Generate and add an assumption to the set of assumptions in the current context. By default, the assumption is added at the current scope. The default can be overridden by specifying the scope parameter. Implemented in CVCL::SearchImplBase, and CVCL::SearchSat. Referenced by CVCL::VCL::assertFormula().

virtual void CVCL::SearchEngine::getUserAssumptions (  std::vector< Expr > &  assumptions  )  [pure virtual, inherited]

Get all user assumptions made in this and all previous contexts. User assumptions are created either by calls to newUserAssumption or a call to checkValid. In the latter case, the negated query is added as an assumption. Parameters: assumptions  should be empty on entry. Implemented in CVCL::SearchImplBase, and CVCL::SearchSat.

virtual void CVCL::SearchEngine::getInternalAssumptions (  std::vector< Expr > &  assumptions  )  [pure virtual, inherited]

Get assumptions made internally in this and all previous contexts. Internal assumptions are literals assumed by the sat solver. Parameters: assumptions  should be empty on entry. Implemented in CVCL::SearchImplBase, and CVCL::SearchSat.

virtual void CVCL::SearchEngine::getAssumptions (  std::vector< Expr > &  assumptions  )  [pure virtual, inherited]

Get all assumptions made in this and all previous contexts. Parameters: assumption  should be an empty vector which will be filled \ with the assumption Implemented in CVCL::SearchImplBase, and CVCL::SearchSat. Referenced by CVCL::SearchEngine::getConcreteModel().

virtual bool CVCL::SearchEngine::isAssumption (  const Expr &  e  )  [pure virtual, inherited]

Check if the formula has already been assumed previously. Implemented in CVCL::SearchEngineFast, CVCL::SearchImplBase, and CVCL::SearchSat.

virtual void CVCL::SearchEngine::getCounterExample (  std::vector< Expr > &  assertions, bool  inOrder = true )  [pure virtual, inherited]

Will return the set of assertions which make the queried formula false. This method should only be called after an invalid query It will try to return the simplest possible set of assertions which are sufficient to make the queried expression false. Parameters: assertions  should be empty on entry. inOrder  if true, returns the assertions in the order they were asserted. This is slightly more expensive than inOrder = false. Implemented in CVCL::SearchImplBase, and CVCL::SearchSat. Referenced by CVCL::VCL::checkContinue().

virtual Proof CVCL::SearchEngine::getProof (   )  [pure virtual, inherited]

Returns the proof term for the last proven query. It should be called only after a valid query. In any other case, it returns Null. Implemented in CVCL::SearchImplBase, and CVCL::SearchSat. Referenced by CVCL::VCL::getProof().

void SearchEngine::getConcreteModel (  ExprMap< Expr > &  m  )  [inherited]

Build a concrete Model (assign values to variables), should only be called after an invalid query. Definition at line 57 of file search.cpp. References CVCL::TheoryCore::buildModel(), CVCL::SearchEngine::checkValid(), CVCL::TheoryCore::collectBasicVars(), CVCL::SearchEngine::d_core, CVCL::Theory::falseExpr(), CVCL::SearchEngine::getAssumptions(), CVCL::TheoryCore::getCM(), CVCL::Theory::getEM(), CVCL::Theorem::getLeafAssumptions(), CVCL::TheoryCore::inconsistentThm(), CVCL::Theorem::isNull(), CVCL::SearchEngine::lastThm(), CVCL::ContextManager::popto(), CVCL::ContextManager::push(), CVCL::RAW_LIST, CVCL::TheoryCore::refineCounterExample(), CVCL::ContextManager::scopeLevel(), CVCL::Expr::toString(), and CVCL::TRACE. Referenced by CVCL::VCL::getConcreteModel().

---

Variable Documentation

TheoryCore* CVCL::SearchEngine::d_core [protected, inherited]

Access to theory reasoning. Definition at line 64 of file search.h. Referenced by CVCL::SearchImplBase::addCNFFact(), CVCL::SearchSat::addLemma(), CVCL::SearchEngineFast::addNonLiteralFact(), CVCL::SearchImplBase::addToCNFCache(), CVCL::SearchEngineFast::analyzeUIPs(), CVCL::SearchSat::assertLit(), CVCL::SearchEngineFast::bcp(), CVCL::SearchSat::check(), CVCL::SearchSimple::checkValidInternal(), CVCL::SearchEngineFast::checkValidInternal(), CVCL::SearchSimple::checkValidMain(), CVCL::SearchEngineFast::checkValidMain(), CVCL::SearchSimple::checkValidRec(), CVCL::SearchEngineFast::commitFacts(), CVCL::SearchEngine::createRules(), CVCL::SearchImplBase::findInCNFCache(), CVCL::SearchEngineFast::findSplitter(), CVCL::SearchImplBase::getAssumptionsUsed(), CVCL::SearchEngine::getConcreteModel(), CVCL::SearchSat::getImplication(), CVCL::SearchSat::getImpliedLiteral(), CVCL::SearchImplBase::getImpliedLiteral(), CVCL::SearchImplBase::getProof(), CVCL::SearchSat::newUserAssumption(), CVCL::SearchImplBase::newUserAssumption(), CVCL::Circuit::propagate(), CVCL::SearchSat::registerAtom(), CVCL::SearchImplBase::registerAtom(), CVCL::SearchImplBase::replaceITE(), CVCL::SearchSimple::restartInternal(), CVCL::SearchEngineFast::restartInternal(), CVCL::SearchSat::returnFromCheck(), CVCL::SearchImplBase::returnFromCheck(), CVCL::SearchImplBase::scopeLevel(), CVCL::SearchEngineFast::setInconsistent(), CVCL::SearchImplBase::simplify(), CVCL::SearchEngineFast::split(), and CVCL::SearchEngine::theoryCore().

CommonProofRules* CVCL::SearchEngine::d_commonRules [protected, inherited]

Common proof rules. Definition at line 67 of file search.h. Referenced by CVCL::SearchEngineFast::addLiteralFact(), CVCL::SearchSimple::addNonLiteralFact(), CVCL::SearchEngineFast::addNonLiteralFact(), CVCL::SearchImplBase::addToCNFCache(), CVCL::SearchImplBase::applyCNFRules(), CVCL::SearchSat::assertLit(), CVCL::SearchEngineFast::bcp(), CVCL::SearchSat::check(), CVCL::SearchImplBase::checkValid(), CVCL::SearchSimple::checkValidMain(), CVCL::SearchEngineFast::checkValidMain(), CVCL::SearchSimple::checkValidRec(), CVCL::SearchImplBase::enqueueCNFrec(), CVCL::SearchImplBase::findInCNFCache(), CVCL::SearchEngineFast::fixConflict(), CVCL::SearchImplBase::newIntAssumption(), CVCL::SearchSat::newUserAssumption(), CVCL::SearchImplBase::newUserAssumption(), CVCL::SearchImplBase::processResult(), CVCL::SearchEngineFast::recordFact(), CVCL::SearchImplBase::replaceITE(), CVCL::SearchSimple::SearchSimple(), and CVCL::SearchEngineFast::split().

SearchEngineRules* CVCL::SearchEngine::d_rules [protected, inherited]

Proof rules for the search engine. Definition at line 70 of file search.h. Referenced by CVCL::SearchEngineFast::addNonLiteralFact(), CVCL::SearchEngineFast::analyzeUIPs(), CVCL::SearchImplBase::applyCNFRules(), CVCL::SearchSimple::checkValidRec(), CVCL::SearchImplBase::enqueueCNFrec(), CVCL::SearchImplBase::processResult(), CVCL::SearchEngineFast::propagate(), CVCL::Circuit::propagate(), CVCL::SearchEngine::SearchEngine(), CVCL::SearchImplBase::SearchImplBase(), CVCL::SearchEngineFast::unitPropagation(), and CVCL::SearchEngine::~SearchEngine().

VariableManager* CVCL::SearchImplBase::d_vm [protected, inherited]

Variable manager for classes Variable and Literal. Definition at line 59 of file search_impl_base.h. Referenced by CVCL::SearchEngineFast::addNonLiteralFact(), CVCL::SearchEngineFast::analyzeUIPs(), CVCL::Circuit::Circuit(), CVCL::SearchImplBase::newLiteral(), CVCL::SearchImplBase::SearchImplBase(), and CVCL::SearchImplBase::~SearchImplBase().

CDO<int> CVCL::SearchImplBase::d_bottomScope [protected, inherited]

The bottom-most scope for the current call to checkSAT (where conflict clauses are still valid). Definition at line 64 of file search_impl_base.h. Referenced by CVCL::SearchImplBase::addToCNFCache(), CVCL::SearchEngineFast::analyzeUIPs(), CVCL::SearchSimple::checkValidInternal(), CVCL::SearchEngineFast::checkValidInternal(), CVCL::SearchEngineFast::checkValidMain(), CVCL::SearchEngineFast::fixConflict(), CVCL::SearchImplBase::getBottomScope(), CVCL::SearchSimple::restartInternal(), CVCL::SearchEngineFast::restartInternal(), and CVCL::SearchEngineFast::traceConflict().

TheoryCore::CoreSatAPI* CVCL::SearchImplBase::d_coreSatAPI_implBase [protected, inherited]

Definition at line 66 of file search_impl_base.h. Referenced by CVCL::SearchImplBase::SearchImplBase(), and CVCL::SearchImplBase::~SearchImplBase().

CDList<Splitter> CVCL::SearchImplBase::d_dpSplitters [protected, inherited]

Backtracking ordered set of DP-suggested splitters. Definition at line 89 of file search_impl_base.h. Referenced by CVCL::SearchImplBase::addSplitter(), and CVCL::SearchEngineFast::addSplitter().

Theorem CVCL::SearchImplBase::d_lastValid [protected, inherited]

Theorem from the last successful checkValid call. It is used by getProof and getAssumptions. Definition at line 93 of file search_impl_base.h. Referenced by CVCL::SearchImplBase::checkValid(), CVCL::SearchSimple::checkValidMain(), CVCL::SearchEngineFast::checkValidMain(), CVCL::SearchImplBase::getAssumptionsUsed(), CVCL::SearchImplBase::getProof(), CVCL::SearchImplBase::lastThm(), CVCL::SearchImplBase::processResult(), and CVCL::SearchImplBase::restart().

ExprHashMap<bool> CVCL::SearchImplBase::d_lastCounterExample [protected, inherited]

Assumptions from the last unsuccessful checkValid call. These are used by getCounterExample. Definition at line 96 of file search_impl_base.h. Referenced by CVCL::SearchSimple::checkValidMain(), CVCL::SearchEngineFast::checkValidMain(), and CVCL::SearchImplBase::processResult().

CDMap<Expr,Theorem> CVCL::SearchImplBase::d_assumptions [protected, inherited]

Maintain the list of current assumptions (user asserts and splitters) for getAssumptions(). Definition at line 99 of file search_impl_base.h. Referenced by CVCL::SearchSimple::checkValidInternal(), CVCL::SearchEngineFast::checkValidInternal(), CVCL::SearchEngineFast::checkValidMain(), CVCL::SearchImplBase::getAssumptions(), CVCL::SearchImplBase::getInternalAssumptions(), CVCL::SearchImplBase::isAssumption(), CVCL::SearchImplBase::newIntAssumption(), CVCL::SearchImplBase::newUserAssumption(), CVCL::SearchSimple::restartInternal(), CVCL::SearchEngineFast::restartInternal(), and CVCL::SearchImplBase::SearchImplBase().

CDMap<Expr, Theorem> CVCL::SearchImplBase::d_cnfCache [protected, inherited]

Backtracking cache for the CNF generator. Definition at line 102 of file search_impl_base.h. Referenced by CVCL::SearchImplBase::addToCNFCache(), and CVCL::SearchImplBase::findInCNFCache().

CDMap<Expr, bool> CVCL::SearchImplBase::d_cnfVars [protected, inherited]

Backtracking set of new variables generated by CNF translator. Specific search engines do not have to split on these variables Definition at line 105 of file search_impl_base.h. Referenced by CVCL::SearchImplBase::addToCNFCache(), CVCL::SearchImplBase::enqueueCNFrec(), and CVCL::SearchImplBase::isCNFVar().

const bool* CVCL::SearchImplBase::d_cnfOption [protected, inherited]

Command line flag whether to convert to CNF. Definition at line 107 of file search_impl_base.h.

const bool* CVCL::SearchImplBase::d_ifLiftOption [protected, inherited]

Flag: whether to convert term ITEs into CNF. Definition at line 109 of file search_impl_base.h. Referenced by CVCL::SearchImplBase::enqueueCNFrec().

const bool* CVCL::SearchImplBase::d_ignoreCnfVarsOption [protected, inherited]

Flag: ignore auxiliary CNF variables when searching for a splitter. Definition at line 111 of file search_impl_base.h. Referenced by CVCL::SearchImplBase::isGoodSplitter().

const bool* CVCL::SearchImplBase::d_origFormulaOption [protected, inherited]

Flag: Preserve the original formula with +cnf (for splitter heuristics). Definition at line 113 of file search_impl_base.h.

---