CVCL::SearchImplBase Class Reference
[Search Engine]

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

#include <search_impl_base.h>

Inheritance diagram for CVCL::SearchImplBase:

[legend]Collaboration diagram for CVCL::SearchImplBase:

[legend]List of all members.

Public Member Functions

• int getBottomScope ()
• bool isClause (const Expr &e)

  Check if e is a clause (a literal, or a disjunction of literals).
  

• bool isPropClause (const Expr &e)

  Check if e is a propositional clause.
  

• bool isCNFVar (const Expr &e)

  Check whether e is a fresh variable introduced by the CNF converter.
  

• bool isGoodSplitter (const Expr &e)

  Check if a splitter is required for completeness.
  

• SearchImplBase (TheoryCore *core)

  Constructor.
  

• virtual ~SearchImplBase ()

  Destructor.
  

• virtual void registerAtom (const Expr &e)

  Register an atomic formula of interest.
  

• virtual Theorem getImpliedLiteral ()

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

• virtual bool checkValidInternal (const Expr &e)=0

  Checks the validity of a formula in the current context.
  

• virtual Theorem checkValid (const Expr &e)

  Similar to checkValid(), only returns Theorem(e) or Null.
  

• virtual bool restartInternal (const Expr &e)=0

  Reruns last check with e as an additional assumption.
  

• virtual Theorem restart (const Expr &e)

  Reruns last check with e as an additional assumption.
  

• void returnFromCheck ()

  Returns to context immediately before last call to checkValid.
  

• virtual Theorem lastThm ()

  Returns the result of the most recent valid theorem.
  

• Theorem newUserAssumption (const Expr &e, int scope=-1)

  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().
  

• virtual Theorem newIntAssumption (const Expr &e)

  Add a new internal asserion.
  

• void newIntAssumption (const Theorem &thm)

  Helper for above function.
  

• void getUserAssumptions (std::vector< Expr > &assumptions)

  Get all assertions made in this and all previous contexts.
  

• void getInternalAssumptions (std::vector< Expr > &assumptions)

  Get assumptions made internally in this and all previous contexts.
  

• virtual void getAssumptions (std::vector< Expr > &assumptions)

  Get all assumptions made in this and all previous contexts.
  

• virtual bool isAssumption (const Expr &e)

  Check if the formula has been assumed.
  

• void addFact (const Theorem &thm)

  Add a new fact to the search engine from the core.
  

• virtual void addSplitter (const Expr &e, int priority)

  Suggest a splitter to the SearchEngine.
  

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

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

• virtual Proof getProof ()

  Returns the proof term for the last proven query.
  

• virtual const Assumptions getAssumptionsUsed ()

  Returns the set of assumptions used in the proof. It should be a subset of getAssumptions().
  

• bool processResult (const Theorem &res, const Expr &e)

  Process result of checkValid.
  

Protected Member Functions

• Literal newLiteral (const Expr &e)

  Construct a Literal out of an Expr or return an existing one.
  

• Theorem simplify (const Theorem &e)

  Our version of simplifier: take Theorem(e), apply simplifier to get Theorem(e==e'), return Theorem(e').
  

• virtual void addLiteralFact (const Theorem &thm)=0

  Notify the search engine about a new literal fact.
  

• virtual void addNonLiteralFact (const Theorem &thm)=0

  Notify the search engine about a new non-literal fact.
  

• void addCNFFact (const Theorem &thm, bool fromCore=false)

  Add a new fact to the search engine bypassing CNF converter.
  

• int scopeLevel ()

  Return the current scope level (for convenience).
  

Protected Attributes

• VariableManager * d_vm

  Variable manager for classes Variable and Literal.
  

• CDO< int > d_bottomScope

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

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

  Backtracking ordered set of DP-suggested splitters.
  

• Theorem d_lastValid

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

• ExprHashMap< bool > d_lastCounterExample

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

• CDMap< Expr, Theorem > d_assumptions

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

• CDMap< Expr, Theorem > d_cnfCache

  Backtracking cache for the CNF generator.
  

• CDMap< Expr, bool > d_cnfVars

  Backtracking set of new variables generated by CNF translator.
  

• const bool * d_cnfOption

  Command line flag whether to convert to CNF.
  

• const bool * d_ifLiftOption

  Flag: whether to convert term ITEs into CNF.
  

• const bool * d_ignoreCnfVarsOption

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

• const bool * d_origFormulaOption

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

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.

• CDMap< Expr, bool > d_enqueueCNFCache

  Cache for enqueueCNF().
  

• CDMap< Expr, bool > d_applyCNFRulesCache

  Cache for applyCNFRules().
  

• CDMap< Expr, Theorem > d_replaceITECache

  Cache for replaceITE().
  

Private Member Functions

• void enqueueCNF (const Theorem &theta)

  Translate theta to CNF and enqueue the new clauses.
  

• void enqueueCNFrec (const Theorem &theta)

  Recursive version of enqueueCNF().
  

• void applyCNFRules (const Theorem &e)

  FIXME: write a comment.
  

• void addToCNFCache (const Theorem &thm)

  Cache a theorem phi <=> v by phi, where v is a literal.
  

• Theorem findInCNFCache (const Expr &e)

  Find a theorem phi <=> v by phi, where v is a literal.
  

• Theorem replaceITE (const Expr &e)

  Replaces ITE subexpressions in e with variables.
  

Friends

• class DecisionEngine

Classes

• class Splitter

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

---

Detailed Description

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

Definition at line 52 of file search_impl_base.h.

---

Constructor & Destructor Documentation

SearchImplBase::SearchImplBase (  TheoryCore *  core  )

Constructor. Definition at line 102 of file search_impl_base.cpp. References d_assumptions, d_coreSatAPI_implBase, CVCL::SearchEngine::d_rules, d_vm, CVCL::TheoryCore::getCM(), CVCL::TheoryCore::getFlags(), IF_DEBUG(), and CVCL::TheoryCore::registerCoreSatAPI().

SearchImplBase::~SearchImplBase (   )  [virtual]

Destructor. Definition at line 127 of file search_impl_base.cpp. References d_coreSatAPI_implBase, and d_vm.

---

Member Function Documentation

Literal CVCL::SearchImplBase::newLiteral (  const Expr &  e  )  [inline, protected]

Construct a Literal out of an Expr or return an existing one. Definition at line 135 of file search_impl_base.h. References d_vm. Referenced by CVCL::SearchEngineFast::addLiteralFact(), CVCL::SearchEngineFast::addNonLiteralFact(), addSplitter(), CVCL::SearchEngineFast::addSplitter(), CVCL::SearchEngineFast::newIntAssumption(), CVCL::Circuit::propagate(), CVCL::SearchEngineFast::recordFact(), CVCL::SearchEngineFast::split(), CVCL::SearchEngineFast::traceConflict(), and CVCL::SearchEngineFast::unitPropagation().

Theorem CVCL::SearchImplBase::simplify (  const Theorem &  e  )  [inline, protected]

Our version of simplifier: take Theorem(e), apply simplifier to get Theorem(e==e'), return Theorem(e'). Definition at line 139 of file search_impl_base.h. References CVCL::SearchEngine::d_core, CVCL::Theorem::getExpr(), CVCL::Theory::iffMP(), and CVCL::TheoryCore::simplify(). Referenced by CVCL::SearchEngineFast::bcp(), CVCL::SearchEngineFast::checkValidMain(), and CVCL::SearchSimple::checkValidRec().

virtual void CVCL::SearchImplBase::addLiteralFact (  const Theorem &  thm  )  [protected, pure virtual]

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. Implemented in CVCL::SearchEngineFast, and CVCL::SearchSimple. Referenced by addCNFFact(), and CVCL::DecisionEngine::pushDecision().

virtual void CVCL::SearchImplBase::addNonLiteralFact (  const Theorem &  thm  )  [protected, pure virtual]

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. Implemented in CVCL::SearchEngineFast, and CVCL::SearchSimple. Referenced by addCNFFact().

void SearchImplBase::addCNFFact (  const Theorem &  thm, bool  fromCore = false )  [protected]

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. Definition at line 212 of file search_impl_base.cpp. References addLiteralFact(), addNonLiteralFact(), CVCL::SearchEngine::d_core, CVCL::TheoryCore::enqueueFact(), CVCL::Theorem::getExpr(), CVCL::Theorem::isAbsLiteral(), and CVCL::TRACE. Referenced by addFact(), applyCNFRules(), enqueueCNF(), and enqueueCNFrec().

int CVCL::SearchImplBase::getBottomScope (   )  [inline]

Definition at line 168 of file search_impl_base.h. References d_bottomScope. Referenced by CVCL::CoreSatAPI_implBase::getBottomScope().

bool SearchImplBase::isClause (  const Expr &  e  )

Check if e is a clause (a literal, or a disjunction of literals). Definition at line 677 of file search_impl_base.cpp. References CVCL::Expr::begin(), CVCL::Expr::end(), CVCL::Expr::isAbsLiteral(), and CVCL::Expr::isOr().

bool SearchImplBase::isPropClause (  const Expr &  e  )

Check if e is a propositional clause. See also: isPropAtom() Definition at line 689 of file search_impl_base.cpp. References CVCL::Expr::begin(), CVCL::Expr::end(), CVCL::Expr::isOr(), and CVCL::Expr::isPropLiteral().

bool CVCL::SearchImplBase::isCNFVar (  const Expr &  e  )  [inline]

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 Definition at line 180 of file search_impl_base.h. References CVCL::CDMap< Key, Data, HashFcn >::count(), and d_cnfVars. Referenced by isGoodSplitter().

bool SearchImplBase::isGoodSplitter (  const Expr &  e  )

Check if a splitter is required for completeness. Currently, it checks that 'e' is not an auxiliary CNF variable Definition at line 701 of file search_impl_base.cpp. References d_ignoreCnfVarsOption, isCNFVar(), CVCL::Expr::isNot(), and CVCL::TRACE. Referenced by CVCL::SearchEngineFast::findSplitter(), and CVCL::DecisionEngine::findSplitterRec().

void SearchImplBase::enqueueCNF (  const Theorem &  theta  )  [private]

Translate theta to CNF and enqueue the new clauses. Definition at line 350 of file search_impl_base.cpp. References addCNFFact(), enqueueCNFrec(), and CVCL::TRACE. Referenced by addFact().

void SearchImplBase::enqueueCNFrec (  const Theorem &  theta  )  [private]

Recursive version of enqueueCNF(). Definition at line 361 of file search_impl_base.cpp. References addCNFFact(), addToCNFCache(), CVCL::AND, CVCL::CommonProofRules::andElim(), applyCNFRules(), CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::CDMap< Key, Data, HashFcn >::count(), d_cnfVars, CVCL::SearchEngine::d_commonRules, d_enqueueCNFCache, d_ifLiftOption, CVCL::SearchEngine::d_rules, CVCL::Expr::end(), findInCNFCache(), CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Theorem::getLHS(), CVCL::Theorem::getRHS(), CVCL::Theorem::getScope(), CVCL::IFF, CVCL::CommonProofRules::iffMP(), CVCL::int2string(), CVCL::Expr::isAbsLiteral(), CVCL::Theorem::isAbsLiteral(), CVCL::Expr::isAnd(), CVCL::Expr::isNot(), CVCL::Theorem::isNull(), CVCL::Expr::isPropLiteral(), CVCL::Theorem::isRewrite(), CVCL::ITE, CVCL::SearchEngineRules::iteToClauses(), CVCL::CommonProofRules::notNotElim(), CVCL::OR, replaceITE(), TheoryCore::rewrite(), scopeLevel(), CVCL::CommonProofRules::substitutivityRule(), CVCL::CommonProofRules::symmetryRule(), CVCL::Theorem::toString(), CVCL::Expr::toString(), CVCL::TRACE, CVCL::CommonProofRules::transitivityRule(), and CVCL::CommonProofRules::varIntroSkolem(). Referenced by enqueueCNF().

void SearchImplBase::applyCNFRules (  const Theorem &  thm  )  [private]

FIXME: write a comment. Parameters: thm  is the input of the form phi <=> v Definition at line 553 of file search_impl_base.cpp. References addCNFFact(), addToCNFCache(), CVCL::AND, CVCL::SearchEngineRules::andCNFRule(), CVCL::CommonProofRules::andElim(), CVCL::Expr::arity(), CVCL::Expr::begin(), d_applyCNFRulesCache, CVCL::SearchEngine::d_commonRules, CVCL::SearchEngine::d_rules, CVCL::Expr::end(), CVCL::CDMap< Key, Data, HashFcn >::end(), CVCL::CDMap< Key, Data, HashFcn >::find(), findInCNFCache(), CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Theorem::getLHS(), CVCL::Theorem::getRHS(), CVCL::IFF, CVCL::SearchEngineRules::iffCNFRule(), CVCL::CommonProofRules::iffContrapositive(), CVCL::SearchEngineRules::iffToClauses(), CVCL::SearchEngineRules::impCNFRule(), CVCL::IMPLIES, CVCL::Expr::isAbsLiteral(), CVCL::Expr::isAnd(), CVCL::Expr::isNot(), CVCL::Theorem::isNull(), CVCL::Expr::isPropLiteral(), CVCL::Theorem::isRewrite(), CVCL::ITE, CVCL::SearchEngineRules::iteCNFRule(), CVCL::OR, CVCL::SearchEngineRules::orCNFRule(), replaceITE(), CVCL::CommonProofRules::substitutivityRule(), CVCL::CommonProofRules::symmetryRule(), CVCL::Theorem::toString(), CVCL::Expr::toString(), CVCL::TRACE, CVCL::CommonProofRules::transitivityRule(), and CVCL::CommonProofRules::varIntroSkolem(). Referenced by enqueueCNFrec(), and replaceITE().

void SearchImplBase::addToCNFCache (  const Theorem &  thm  )  [private]

Cache a theorem phi <=> v by phi, where v is a literal. Definition at line 713 of file search_impl_base.cpp. References CVCL::CDMap< Key, Data, HashFcn >::count(), CVCL::Statistics::counter(), d_bottomScope, d_cnfCache, d_cnfVars, CVCL::SearchEngine::d_commonRules, CVCL::SearchEngine::d_core, CVCL::Theorem::getExpr(), CVCL::Theorem::getLHS(), CVCL::Theorem::getRHS(), CVCL::TheoryCore::getStatistics(), CVCL::CommonProofRules::iffContrapositive(), CVCL::CDMap< Key, Data, HashFcn >::insert(), CVCL::Expr::isNot(), CVCL::Theorem::isRewrite(), CVCL::Expr::toString(), and CVCL::TRACE. Referenced by applyCNFRules(), enqueueCNFrec(), and replaceITE().

Theorem SearchImplBase::findInCNFCache (  const Expr &  e  )  [private]

Find a theorem phi <=> v by phi, where v is a literal. Returns: Null Theorem if not found. Definition at line 740 of file search_impl_base.cpp. References CVCL::Statistics::counter(), d_cnfCache, CVCL::SearchEngine::d_commonRules, CVCL::SearchEngine::d_core, CVCL::CDMap< Key, Data, HashFcn >::end(), CVCL::CDMap< Key, Data, HashFcn >::find(), CVCL::Theorem::getExpr(), CVCL::Theorem::getLHS(), CVCL::TheoryCore::getStatistics(), CVCL::CommonProofRules::iffContrapositive(), CVCL::int2string(), CVCL::Expr::isNot(), CVCL::Theorem::isRewrite(), CVCL::CommonProofRules::rewriteNotNot(), CVCL::Expr::toString(), CVCL::TRACE, and CVCL::CommonProofRules::transitivityRule(). Referenced by applyCNFRules(), enqueueCNFrec(), and replaceITE().

Theorem SearchImplBase::replaceITE (  const Expr &  e  )  [private]

Replaces ITE subexpressions in e with variables. Strategy: For a given atomic formula phi(ite(c, t1, t2)) which depends on a term ITE, generate an equisatisfiable formula: phi(x) & ite(c, t1=x, t2=x), where x is a new variable. The phi(x) part will be generated by the caller, and our job is to assert the 'ite(c, t1=x, t2=x)', and return a rewrite theorem phi(ite(c, t1, t2)) <=> phi(x). Definition at line 794 of file search_impl_base.cpp. References addToCNFCache(), applyCNFRules(), CVCL::SearchEngine::d_commonRules, CVCL::SearchEngine::d_core, d_replaceITECache, CVCL::CDMap< Key, Data, HashFcn >::end(), CVCL::CDMap< Key, Data, HashFcn >::find(), findInCNFCache(), CVCL::Theorem::getRHS(), CVCL::CommonProofRules::iffMP(), CVCL::Expr::isAbsLiteral(), CVCL::Theorem::isNull(), CVCL::Expr::isPropLiteral(), CVCL::Theorem::isRewrite(), CVCL::CommonProofRules::reflexivityRule(), CVCL::TheoryCore::rewriteLiteral(), CVCL::TRACE, CVCL::CommonProofRules::transitivityRule(), and CVCL::CommonProofRules::varIntroSkolem(). Referenced by applyCNFRules(), and enqueueCNFrec().

int CVCL::SearchImplBase::scopeLevel (   )  [inline, protected]

Return the current scope level (for convenience). Definition at line 207 of file search_impl_base.h. References CVCL::SearchEngine::d_core, CVCL::TheoryCore::getCM(), and CVCL::ContextManager::scopeLevel(). Referenced by CVCL::SearchEngineFast::addLiteralFact(), CVCL::SearchEngineFast::addNonLiteralFact(), CVCL::SearchEngineFast::bcp(), CVCL::SearchSimple::checkValidInternal(), CVCL::SearchEngineFast::checkValidInternal(), enqueueCNFrec(), CVCL::SearchEngineFast::fixConflict(), CVCL::SearchEngineFast::newIntAssumption(), CVCL::SearchEngineFast::ConflictClauseManager::notify(), CVCL::SearchEngineFast::ConflictClauseManager::setRestorePoint(), and CVCL::SearchEngineFast::traceConflict().

virtual void CVCL::SearchImplBase::registerAtom (  const Expr &  e  )  [inline, virtual]

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 Implements CVCL::SearchEngine. Definition at line 215 of file search_impl_base.h. References CVCL::SearchEngine::d_core, and CVCL::TheoryCore::registerAtom().

virtual Theorem CVCL::SearchImplBase::getImpliedLiteral (   )  [inline, virtual]

Return next literal implied by last assertion. Null Expr if none. Returned literals are either registered atomic formulas or their negation Implements CVCL::SearchEngine. Definition at line 216 of file search_impl_base.h. References CVCL::SearchEngine::d_core, and CVCL::TheoryCore::getImpliedLiteral().

virtual bool CVCL::SearchImplBase::checkValidInternal (  const Expr &  e  )  [pure virtual]

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. Implemented in CVCL::SearchEngineFast, and CVCL::SearchSimple. Referenced by checkValid().

Theorem SearchImplBase::checkValid (  const Expr &  e  )  [virtual]

Similar to checkValid(), only returns Theorem(e) or Null. Implements CVCL::SearchEngine. Definition at line 336 of file search_impl_base.cpp. References checkValidInternal(), CVCL::CommonProofRules::clearSkolemAxioms(), CVCL::SearchEngine::d_commonRules, and d_lastValid.

virtual bool CVCL::SearchImplBase::restartInternal (  const Expr &  e  )  [pure virtual]

Reruns last check with e as an additional assumption. Implemented in CVCL::SearchEngineFast, and CVCL::SearchSimple. Referenced by restart().

Theorem SearchImplBase::restart (  const Expr &  e  )  [virtual]

Reruns last check with e as an additional assumption. Implements CVCL::SearchEngine. Definition at line 343 of file search_impl_base.cpp. References d_lastValid, and restartInternal(). Referenced by returnFromCheck().

void CVCL::SearchImplBase::returnFromCheck (   )  [inline, virtual]

Returns to context immediately before last call to checkValid. This method should only be called after a query which is invalid. Implements CVCL::SearchEngine. Definition at line 234 of file search_impl_base.h. References CVCL::SearchEngine::d_core, CVCL::Theory::falseExpr(), and restart().

virtual Theorem CVCL::SearchImplBase::lastThm (   )  [inline, virtual]

Returns the result of the most recent valid theorem. Returns Null Theorem if last call was not valid Implements CVCL::SearchEngine. Definition at line 235 of file search_impl_base.h. References d_lastValid.

Theorem SearchImplBase::newUserAssumption (  const Expr &  e, int  scope = -1 )  [virtual]

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(). Implements CVCL::SearchEngine. Definition at line 136 of file search_impl_base.cpp. References CVCL::TheoryCore::addFact(), CVCL::CommonProofRules::assumpRule(), CVCL::CDMap< Key, Data, HashFcn >::begin(), d_assumptions, CVCL::SearchEngine::d_commonRules, CVCL::SearchEngine::d_core, CVCL::debugger, CVCL::CDMap< Key, Data, HashFcn >::end(), std::endl(), CVCL::CDMap< Key, Data, HashFcn >::find(), CVCL::TheoryCore::getExprTrans(), CVCL::Debug::getOS(), IF_DEBUG(), CVCL::Theorem::isNull(), CVCL::ExprTransform::preprocess(), CVCL::Expr::setUserAssumption(), CVCL::TRACE, and CVCL::Debug::trace(). Referenced by CVCL::SearchSimple::checkValidInternal(), CVCL::SearchEngineFast::checkValidInternal(), CVCL::SearchSimple::restartInternal(), and CVCL::SearchEngineFast::restartInternal().

Theorem SearchImplBase::newIntAssumption (  const Expr &  e  )  [virtual]

Add a new internal asserion. Reimplemented in CVCL::SearchEngineFast. Definition at line 166 of file search_impl_base.cpp. References CVCL::CommonProofRules::assumpRule(), and CVCL::SearchEngine::d_commonRules. Referenced by CVCL::CoreSatAPI_implBase::addAssumption(), CVCL::SearchEngineFast::newIntAssumption(), and CVCL::DecisionEngine::pushDecision().

void SearchImplBase::newIntAssumption (  const Theorem &  thm  )

Helper for above function. Definition at line 173 of file search_impl_base.cpp. References CVCL::CDMap< Key, Data, HashFcn >::count(), d_assumptions, CVCL::Theorem::getExpr(), CVCL::Expr::setIntAssumption(), CVCL::Expr::toString(), and CVCL::TRACE.

void CVCL::SearchImplBase::getUserAssumptions (  std::vector< Expr > &  assumptions  )  [virtual]

Get all assertions made in this and all previous contexts. Parameters: assertions  should be an empty vector which will be filled \ with the assertions Implements CVCL::SearchEngine.

void SearchImplBase::getInternalAssumptions (  std::vector< Expr > &  assumptions  )  [virtual]

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. Implements CVCL::SearchEngine. Definition at line 191 of file search_impl_base.cpp. References d_assumptions, CVCL::CDMap< Key, Data, HashFcn >::orderedBegin(), and CVCL::CDMap< Key, Data, HashFcn >::orderedEnd().

void SearchImplBase::getAssumptions (  std::vector< Expr > &  assumptions  )  [virtual]

Get all assumptions made in this and all previous contexts. Parameters: assumption  should be an empty vector which will be filled \ with the assumption Implements CVCL::SearchEngine. Definition at line 199 of file search_impl_base.cpp. References d_assumptions, CVCL::CDMap< Key, Data, HashFcn >::orderedBegin(), and CVCL::CDMap< Key, Data, HashFcn >::orderedEnd(). Referenced by CVCL::SearchEngineFast::getCounterExample().

bool SearchImplBase::isAssumption (  const Expr &  e  )  [virtual]

Check if the formula has been assumed. Implements CVCL::SearchEngine. Reimplemented in CVCL::SearchEngineFast. Definition at line 207 of file search_impl_base.cpp. References CVCL::CDMap< Key, Data, HashFcn >::count(), and d_assumptions. Referenced by CVCL::SearchEngineFast::isAssumption().

void SearchImplBase::addFact (  const Theorem &  thm  )

Add a new fact to the search engine from the core. It should be called by TheoryCore::assertFactCore(). Definition at line 225 of file search_impl_base.cpp. References addCNFFact(), enqueueCNF(), CVCL::Theorem::getExpr(), and CVCL::TRACE. Referenced by CVCL::CoreSatAPI_implBase::addLemma().

void SearchImplBase::addSplitter (  const Expr &  e, int  priority )  [virtual]

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. Reimplemented in CVCL::SearchEngineFast. Definition at line 235 of file search_impl_base.cpp. References d_dpSplitters, CVCL::Expr::isAbsLiteral(), newLiteral(), CVCL::CDList< T >::push_back(), and CVCL::Expr::toString(). Referenced by CVCL::CoreSatAPI_implBase::addSplitter().

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

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. Implements CVCL::SearchEngine. Referenced by CVCL::SearchEngineFast::getCounterExample().

Proof SearchImplBase::getProof (   )  [virtual]

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. Implements CVCL::SearchEngine. Definition at line 272 of file search_impl_base.cpp. References CVCL::SearchEngine::d_core, d_lastValid, CVCL::Theorem::getProof(), CVCL::TheoryCore::getTM(), CVCL::Theorem::isNull(), and CVCL::TheoremManager::withProof().

const Assumptions SearchImplBase::getAssumptionsUsed (   )  [virtual]

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. Definition at line 287 of file search_impl_base.cpp. References CVCL::SearchEngine::d_core, d_lastValid, CVCL::Theorem::getAssumptions(), CVCL::TheoryCore::getTM(), CVCL::Theorem::isNull(), and CVCL::TheoremManager::withAssumptions().

bool SearchImplBase::processResult (  const Theorem &  res, const Expr &  e )

Process result of checkValid. Given a proof of FALSE ('res') from an assumption 'e', derive the proof of the inverse of e. Parameters: res  is a proof of FALSE e  is the assumption used in the above proof Definition at line 307 of file search_impl_base.cpp. References CVCL::ExprHashMap< Data >::clear(), CVCL::SearchEngine::d_commonRules, d_lastCounterExample, d_lastValid, CVCL::SearchEngine::d_rules, CVCL::SearchEngineRules::eliminateSkolemAxioms(), CVCL::ExprHashMap< Data >::erase(), CVCL::Theorem::getExpr(), CVCL::CommonProofRules::getSkolemAxioms(), CVCL::Expr::isFalse(), CVCL::Expr::isNot(), CVCL::Theorem::isNull(), CVCL::SearchEngineRules::negIntro(), CVCL::SearchEngineRules::proofByContradiction(), and CVCL::Theorem::toString(). Referenced by CVCL::SearchSimple::checkValidMain(), and CVCL::SearchEngineFast::checkValidMain().

---

Friends And Related Function Documentation

friend class DecisionEngine [friend]

Definition at line 53 of file search_impl_base.h.

---

Member Data Documentation

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

Cache for enqueueCNF(). Definition at line 127 of file search_impl_base.h. Referenced by enqueueCNFrec().

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

Cache for applyCNFRules(). Definition at line 129 of file search_impl_base.h. Referenced by applyCNFRules().

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

Cache for replaceITE(). Definition at line 131 of file search_impl_base.h. Referenced by replaceITE().

---

The documentation for this class was generated from the following files:

• search_impl_base.h
• search_impl_base.cpp

---