CVC3
2.4.1
|
Search engine that connects to a generic SAT reasoning module. More...
#include <search_sat.h>
Classes | |
class | LitPriorityPair |
Pair of Lit and priority of this Lit. More... | |
class | Restorer |
Public Member Functions | |
SearchSat (TheoryCore *core, const std::string &name) | |
virtual | ~SearchSat () |
Destructor. | |
virtual const std::string & | getName () |
Name of this search engine. | |
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 void | push () |
Push a checkpoint. | |
virtual void | pop () |
Restore last checkpoint. | |
virtual QueryResult | checkValid (const Expr &e, Theorem &result) |
Checks the validity of a formula in the current context. | |
virtual QueryResult | restart (const Expr &e, Theorem &result) |
Reruns last check with e as an additional assumption. | |
virtual void | returnFromCheck () |
Returns to context immediately before last call to checkValid. | |
virtual Theorem | lastThm () |
Returns the result of the most recent valid theorem. | |
virtual Theorem | newUserAssumption (const Expr &e) |
Generate and add an assumption to the set of assumptions in the current context. | |
virtual void | getUserAssumptions (std::vector< Expr > &assumptions) |
Get all user assumptions made in this and all previous contexts. | |
virtual 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 already been assumed previously. | |
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 FormulaValue | getValue (const CVC3::Expr &e) |
![]() | |
SearchEngine (TheoryCore *core) | |
Constructor. | |
virtual | ~SearchEngine () |
Destructor. | |
CommonProofRules * | getCommonRules () |
Accessor for common rules. | |
TheoryCore * | theoryCore () |
Accessor for TheoryCore. | |
void | getConcreteModel (ExprMap< Expr > &m) |
Build a concrete Model (assign values to variables), should only be called after a query which returns INVALID. | |
bool | tryModelGeneration (Theorem &thm) |
Try to build a concrete Model (assign values to variables), should only be called after a query which returns UNKNOWN. Returns a theorem if inconsistent. |
Private Member Functions | |
void | restorePre () |
Get rid of bottom scope entries in prioritySet. | |
void | restore () |
Get rid of entries in prioritySet and pendingLemmas added since last push. | |
bool | recordNewRootLit (SAT::Lit lit, int priority=0, bool atBottomScope=false) |
Helper for addLemma and check. | |
void | addLemma (const Theorem &thm, int priority=0, bool atBotomScope=false) |
Core theory callback which adds a new lemma from the core theory. | |
int | getBottomScope () |
Core theory callback which asks for the bottom scope for current query. | |
void | addSplitter (const Expr &e, int priority) |
Core theory callback which suggests a splitter. | |
void | assertLit (SAT::Lit l) |
DPLLT callback to inform theory that a literal has been assigned. | |
SAT::DPLLT::ConsistentResult | checkConsistent (SAT::CNF_Formula &cnf, bool fullEffort) |
DPLLT callback to ask if theory has detected inconsistency. | |
SAT::Lit | getImplication () |
DPLLT callback to get theory propagations. | |
void | getExplanation (SAT::Lit l, SAT::CNF_Formula &cnf) |
DPLLT callback to explain a theory propagation. | |
bool | getNewClauses (SAT::CNF_Formula &cnf) |
DPLLT callback to get more general theory clauses. | |
SAT::Lit | makeDecision () |
DPLLT callback to decide which literal to split on next. | |
bool | findSplitterRec (SAT::Lit lit, SAT::Var::Val value, SAT::Lit *litDecision) |
Recursively traverse DAG looking for a splitter. | |
SAT::Var::Val | getValue (SAT::Lit c) |
Get the value of a CNF Literal. | |
SAT::Var::Val | getValue (SAT::Var v) |
void | setValue (SAT::Var v, SAT::Var::Val val) |
Set the value of a variable. | |
bool | checkJustified (SAT::Var v) |
Check whether this variable's value is justified. | |
void | setJustified (SAT::Var v) |
Mark this variable as justified. | |
QueryResult | check (const Expr &e, Theorem &result, bool isRestart=false) |
Main checking procedure shared by checkValid and restart. | |
void | newUserAssumptionIntHelper (const Theorem &thm, SAT::CNF_Formula_Impl &cnf, bool atBottomScope) |
Helper for newUserAssumptionInt. | |
Theorem | newUserAssumptionInt (const Expr &e, SAT::CNF_Formula_Impl &cnf, bool atBottomScope) |
Helper for newUserAssumption. |
Private Attributes | |
std::string | d_name |
Name of search engine. | |
CDO< int > | d_bottomScope |
Bottom scope for current query. | |
CDO< Expr > | d_lastCheck |
Last expr checked for validity. | |
CDO< Theorem > | d_lastValid |
Theorem from the last successful checkValid call. It is used by getProof and getAssumptions. | |
CDList< Theorem > | d_userAssumptions |
List of all user assumptions. | |
CDList< Theorem > | d_intAssumptions |
List of all internal assumptions. | |
CDO< unsigned > | d_idxUserAssump |
Index to where unprocessed assumptions start. | |
TheoryCore::CoreSatAPI * | d_coreSatAPI |
SAT::DPLLT * | d_dpllt |
Pointer to DPLLT implementation. | |
SAT::DPLLT::TheoryAPI * | d_theoryAPI |
Implementation of TheoryAPI for DPLLT. | |
SAT::DPLLT::Decider * | d_decider |
Implementation of Decider for DPLLT. | |
CDMap< Expr, Theorem > | d_theorems |
Store of theorems for expressions sent to DPLLT. | |
SAT::CNF_Manager * | d_cnfManager |
Manages CNF formula and its relationship to original Exprs and Theorems. | |
SAT::CNF_Manager::CNFCallback * | d_cnfCallback |
Callback for CNF_Manager. | |
std::vector< SAT::Var::Val > | d_vars |
Cached values of variables. | |
bool | d_inCheckSat |
Whether we are currently in a call to dpllt->checkSat. | |
SAT::CD_CNF_Formula | d_lemmas |
CNF Formula used for theory lemmas. | |
std::vector< std::pair < Theorem, int > > | d_pendingLemmas |
Lemmas waiting to be translated since last call to getNewClauses() | |
std::vector< bool > | d_pendingScopes |
Scope parameter for lemmas waiting to be translated since last call to getNewClauses() | |
CDO< unsigned > | d_pendingLemmasSize |
Backtracking size of d_pendingLemmas. | |
CDO< unsigned > | d_pendingLemmasNext |
Backtracking next item in d_pendingLemmas. | |
CDO< unsigned > | d_lemmasNext |
Current position in d_lemmas. | |
std::vector< unsigned > | d_varsUndoList |
List for backtracking var values. | |
CDO< unsigned > | d_varsUndoListSize |
Backtracking size of d_varsUndoList. | |
std::set< LitPriorityPair > | d_prioritySet |
Used to determine order to find splitters. | |
CDO< std::set< LitPriorityPair > ::const_iterator > | d_prioritySetStart |
Current position in prioritySet. | |
CDO< unsigned > | d_prioritySetEntriesSize |
Backtracking size of priority set entries. | |
std::vector< std::set < LitPriorityPair >::iterator > | d_prioritySetEntries |
Entries in priority set in insertion order (so set can be backtracked) | |
std::vector< unsigned > | d_prioritySetBottomEntriesSizeStack |
Backtracking size of priority set entries at bottom scope. | |
unsigned | d_prioritySetBottomEntriesSize |
Current size of bottom entries. | |
std::vector< std::set < LitPriorityPair >::iterator > | d_prioritySetBottomEntries |
Entries in priority set in insertion order (so set can be backtracked) | |
CDO< unsigned > | d_lastRegisteredVar |
Last Var registered with core theory. | |
CDO< bool > | d_dplltReady |
Whether it's OK to call DPLLT solver from the current scope. | |
CDO< unsigned > | d_nextImpliedLiteral |
Restorer | d_restorer |
Instance of Restorer class. |
Friends | |
class | Restorer |
Helper class for resetting DPLLT engine. | |
class | SearchSatCoreSatAPI |
class | SearchSatCNFCallback |
class | SearchSatTheoryAPI |
class | SearchSatDecider |
Additional Inherited Members | |
![]() | |
SearchEngineRules * | createRules () |
Create the trusted component. | |
SearchEngineRules * | createRules (SearchEngine *s_eng) |
![]() | |
TheoryCore * | d_core |
Access to theory reasoning. | |
CommonProofRules * | d_commonRules |
Common proof rules. | |
SearchEngineRules * | d_rules |
Proof rules for the search engine. |
Search engine that connects to a generic SAT reasoning module.
Definition at line 40 of file search_sat.h.
SearchSat::SearchSat | ( | TheoryCore * | core, |
const std::string & | name | ||
) |
Constructor name is the name of the dpllt engine to use, as returned by getName()
Definition at line 936 of file search_sat.cpp.
References d_cnfCallback, d_cnfManager, d_coreSatAPI, d_decider, d_dpllt, d_prioritySet, d_prioritySetStart, d_theoryAPI, CVC3::TheoryCore::getCM(), CVC3::TheoryCore::getFlags(), CVC3::TheoryCore::getStatistics(), CVC3::TheoryCore::getTM(), SAT::CNF_Manager::registerCNFCallback(), CVC3::TheoryCore::registerCoreSatAPI(), SearchSatCNFCallback, SearchSatCoreSatAPI, SearchSatDecider, SearchSatTheoryAPI, and CVC3::TheoremManager::withProof().
|
virtual |
Destructor.
Definition at line 991 of file search_sat.cpp.
References d_cnfCallback, d_cnfManager, d_coreSatAPI, d_decider, d_dpllt, and d_theoryAPI.
|
private |
Get rid of bottom scope entries in prioritySet.
Definition at line 115 of file search_sat.cpp.
References DebugAssert.
Referenced by CVC3::SearchSat::Restorer::notifyPre().
|
private |
Get rid of entries in prioritySet and pendingLemmas added since last push.
Definition at line 129 of file search_sat.cpp.
References UNKNOWN.
Referenced by CVC3::SearchSat::Restorer::notify().
|
private |
Helper for addLemma and check.
Definition at line 146 of file search_sat.cpp.
References DebugAssert.
Referenced by newUserAssumptionIntHelper().
|
private |
Core theory callback which adds a new lemma from the core theory.
Definition at line 170 of file search_sat.cpp.
References DebugAssert, CVC3::Theorem::getExpr(), IF_DEBUG, CVC3::PRESENTATION_LANG, CVC3::Expr::toString(), and TRACE.
|
inlineprivate |
Core theory callback which asks for the bottom scope for current query.
Definition at line 184 of file search_sat.h.
References d_bottomScope.
|
private |
Core theory callback which suggests a splitter.
Definition at line 186 of file search_sat.cpp.
References DebugAssert, and CVC3::Expr::isEq().
|
private |
DPLLT callback to inform theory that a literal has been assigned.
Definition at line 193 of file search_sat.cpp.
References DebugAssert, CVC3::FALSE_VAL, SAT::Lit::getVar(), IF_DEBUG, CVC3::Expr::isAbsLiteral(), CVC3::Expr::isIntAssumption(), CVC3::Expr::isNot(), CVC3::Expr::isNull(), SAT::Lit::isPositive(), CVC3::Expr::setIntAssumption(), CVC3::Theorem::setQuantLevel(), CVC3::Expr::toString(), TRACE, CVC3::TRUE_VAL, and UNKNOWN.
|
private |
DPLLT callback to ask if theory has detected inconsistency.
Definition at line 258 of file search_sat.cpp.
References DebugAssert, and UNKNOWN.
|
private |
DPLLT callback to get theory propagations.
Definition at line 284 of file search_sat.cpp.
References DebugAssert, CVC3::Theorem::getExpr(), SAT::Lit::isNull(), CVC3::Theorem::isNull(), CVC3::Expr::isUserRegisteredAtom(), SAT::Lit::reset(), CVC3::TRUE_VAL, and CVC3::Expr::unnegate().
|
private |
DPLLT callback to explain a theory propagation.
Definition at line 304 of file search_sat.cpp.
References DebugAssert, SAT::CNF_Formula::empty(), CVC3::CDMap< Key, Data, HashFcn >::end(), CVC3::CDMap< Key, Data, HashFcn >::find(), and UNKNOWN.
|
private |
DPLLT callback to get more general theory clauses.
Definition at line 318 of file search_sat.cpp.
References DebugAssert, and UNKNOWN.
|
private |
DPLLT callback to decide which literal to split on next.
Definition at line 346 of file search_sat.cpp.
References DebugAssert.
|
private |
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.
Definition at line 364 of file search_sat.cpp.
References AND, DebugAssert, std::endl(), CVC3::FALSE_VAL, FatalAssert, SAT::Lit::getVar(), IFF, IMPLIES, SAT::Lit::isFalse(), SAT::Lit::isInverted(), SAT::Lit::isTrue(), SAT::Lit::isVar(), ITE, OR, CVC3::TRUE_VAL, UNKNOWN, and XOR.
|
inlineprivate |
Get the value of a CNF Literal.
Definition at line 214 of file search_sat.h.
References d_vars, DebugAssert, CVC3::FALSE_VAL, SAT::Lit::getVar(), SAT::Var::invertValue(), SAT::Lit::isInverted(), SAT::Lit::isNull(), SAT::Lit::isPositive(), SAT::Lit::isTrue(), SAT::Lit::isVar(), and SAT::Var::TRUE_VAL.
Referenced by getValue().
|
inlineprivate |
Definition at line 223 of file search_sat.h.
References d_vars, DebugAssert, and SAT::Var::isVar().
|
inlineprivate |
Set the value of a variable.
Definition at line 229 of file search_sat.h.
References d_vars, d_varsUndoList, d_varsUndoListSize, DebugAssert, SAT::Var::isNull(), and SAT::Var::UNKNOWN.
|
inlineprivate |
Check whether this variable's value is justified.
Definition at line 241 of file search_sat.h.
References SAT::CNF_Manager::concreteLit(), d_cnfManager, and CVC3::Expr::isJustified().
|
inlineprivate |
Mark this variable as justified.
Definition at line 245 of file search_sat.h.
References SAT::CNF_Manager::concreteLit(), d_cnfManager, and CVC3::Expr::setJustified().
|
private |
Main checking procedure shared by checkValid and restart.
Definition at line 638 of file search_sat.cpp.
References DebugAssert, std::endl(), FORALL, CVC3::Expr::getType(), SAT::Lit::getVar(), CVC3::INVALID, CVC3::Type::isBool(), CVC3::Expr::isEq(), CVC3::Expr::isExists(), CVC3::Expr::isFalse(), CVC3::Expr::isForall(), CVC3::Expr::isNot(), SAT::Lit::isPositive(), CVC3::Expr::isTrue(), CVC3::pop(), CVC3::push(), SATISFIABLE, CVC3::CDList< T >::size(), CVC3::Type::toString(), CVC3::Expr::toString(), TRACE, UNKNOWN, UNSATISFIABLE, and CVC3::VALID.
Referenced by checkValid(), and restart().
|
private |
Helper for newUserAssumptionInt.
Definition at line 1042 of file search_sat.cpp.
References SAT::CNF_Manager::addAssumption(), CVC3::CommonProofRules::andElim(), CVC3::Expr::arity(), d_cnfManager, CVC3::SearchEngine::d_commonRules, CVC3::SearchEngine::d_core, SAT::CNF_Formula_Impl::deleteLast(), CVC3::Theorem::getExpr(), CVC3::TheoryCore::getFlags(), CVC3::Expr::isAnd(), and recordNewRootLit().
Referenced by newUserAssumptionInt().
|
private |
Helper for newUserAssumption.
Definition at line 1064 of file search_sat.cpp.
References CVC3::TheoryCore::addFact(), CVC3::CommonProofRules::assumpRule(), d_bottomScope, d_cnfManager, CVC3::SearchEngine::d_commonRules, CVC3::SearchEngine::d_core, d_inCheckSat, d_userAssumptions, d_vars, DebugAssert, CVC3::TheoryCore::getCM(), CVC3::Theorem::getExpr(), CVC3::TheoryCore::getExprTrans(), isAssumption(), CVC3::Expr::isFalse(), CVC3::Expr::isTrue(), newUserAssumptionIntHelper(), SAT::CNF_Manager::numVars(), CVC3::ExprTransform::preprocess(), CVC3::CDList< T >::push_back(), CVC3::ContextManager::scopeLevel(), setRecursiveInUserAssumption(), CVC3::Expr::setUserAssumption(), and CVC3::UNKNOWN.
Referenced by newUserAssumption().
|
inlinevirtual |
Name of this search engine.
Implements CVC3::SearchEngine.
Definition at line 268 of file search_sat.h.
References d_name.
|
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 CVC3::SearchEngine.
Definition at line 1002 of file search_sat.cpp.
References CVC3::SearchEngine::d_core, CVC3::Expr::isRegisteredAtom(), CVC3::TheoryCore::registerAtom(), and CVC3::Expr::setUserRegisteredAtom().
|
virtual |
Return next literal implied by last assertion. Null Expr if none.
Returned literals are either registered atomic formulas or their negation
Implements CVC3::SearchEngine.
Definition at line 1010 of file search_sat.cpp.
References CVC3::SearchEngine::d_core, d_nextImpliedLiteral, CVC3::Theorem::getExpr(), CVC3::TheoryCore::getImpliedLiteralByIndex(), CVC3::Expr::isUserRegisteredAtom(), and CVC3::Expr::unnegate().
|
inlinevirtual |
Push a checkpoint.
Implements CVC3::SearchEngine.
Definition at line 271 of file search_sat.h.
References d_dpllt, and SAT::DPLLT::push().
|
inlinevirtual |
Restore last checkpoint.
Implements CVC3::SearchEngine.
Definition at line 272 of file search_sat.h.
References d_dpllt, and SAT::DPLLT::pop().
Referenced by returnFromCheck().
|
inlinevirtual |
Checks the validity of a formula in the current context.
If the query is valid, it returns VALID, the result parameter contains the corresponding theorem, and the scope and context are the same as when called. If it returns INVALID, the context will be one which falsifies the query. If it returns UNKNOWN, the context will falsify the query, but the context may be inconsistent. Finally, if it returns ABORT, the context will be one which satisfies as much as possible.
e | the formula to check. |
result | the resulting theorem, if the formula is valid. |
Implements CVC3::SearchEngine.
Definition at line 273 of file search_sat.h.
References check().
|
inlinevirtual |
Reruns last check with e as an additional assumption.
This method should only be called after a query which is invalid.
e | the additional assumption |
result | the resulting theorem, if the query is valid. |
Implements CVC3::SearchEngine.
Definition at line 275 of file search_sat.h.
References check().
|
virtual |
Returns to context immediately before last call to checkValid.
This method should only be called after a query which returns something other than VALID.
Implements CVC3::SearchEngine.
Definition at line 1022 of file search_sat.cpp.
References d_bottomScope, and pop().
|
inlinevirtual |
Returns the result of the most recent valid theorem.
Returns Null Theorem if last call was not valid
Implements CVC3::SearchEngine.
Definition at line 278 of file search_sat.h.
References d_lastValid.
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.
Implements CVC3::SearchEngine.
Definition at line 1102 of file search_sat.cpp.
References SAT::DPLLT::addAssertion(), d_dpllt, and newUserAssumptionInt().
|
virtual |
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.
assumptions | should be empty on entry. |
Implements CVC3::SearchEngine.
Definition at line 1111 of file search_sat.cpp.
References CVC3::CDList< T >::begin(), d_userAssumptions, and CVC3::CDList< T >::end().
|
virtual |
Get assumptions made internally in this and all previous contexts.
Internal assumptions are literals assumed by the sat solver.
assumptions | should be empty on entry. |
Implements CVC3::SearchEngine.
Definition at line 1119 of file search_sat.cpp.
References CVC3::CDList< T >::begin(), d_intAssumptions, and CVC3::CDList< T >::end().
Referenced by getCounterExample().
|
virtual |
Get all assumptions made in this and all previous contexts.
assumptions | should be an empty vector which will be filled \ with the assumptions |
Implements CVC3::SearchEngine.
Definition at line 1128 of file search_sat.cpp.
References CVC3::CDList< T >::begin(), d_intAssumptions, d_userAssumptions, CVC3::CDList< T >::end(), and CVC3::Expr::isUserAssumption().
|
virtual |
Check if the formula has already been assumed previously.
Implements CVC3::SearchEngine.
Definition at line 1163 of file search_sat.cpp.
References CVC3::Expr::isIntAssumption(), and CVC3::Expr::isUserAssumption().
Referenced by newUserAssumptionInt().
|
virtual |
Will return the set of assertions which make the queried formula false.
This method should only be called after an query which returns INVALID. It will try to return the simplest possible set of assertions which are sufficient to make the queried expression false.
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 CVC3::SearchEngine.
Definition at line 1169 of file search_sat.cpp.
References d_lastValid, CVC3::CDO< T >::get(), getInternalAssumptions(), and CVC3::Theorem::isNull().
|
virtual |
Returns the proof term for the last proven query.
It should be called only after a query which returns VALID. In any other case, it returns Null.
Implements CVC3::SearchEngine.
Definition at line 1178 of file search_sat.cpp.
References CVC3::SearchEngine::d_core, d_lastValid, CVC3::CDO< T >::get(), CVC3::Theorem::getProof(), CVC3::TheoryCore::getTM(), CVC3::Theorem::isNull(), and CVC3::TheoremManager::withProof().
|
inlinevirtual |
Implements CVC3::SearchEngine.
Definition at line 289 of file search_sat.h.
References d_cnfManager, DebugAssert, std::endl(), CVC3::FALSE_VAL, SAT::Var::FALSE_VAL, FatalAssert, SAT::CNF_Manager::getCNFLit(), getValue(), SAT::Lit::isNull(), CVC3::Expr::toString(), CVC3::TRUE_VAL, SAT::Var::TRUE_VAL, SAT::Var::UNKNOWN, and CVC3::UNKNOWN_VAL.
|
friend |
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.
Definition at line 158 of file search_sat.h.
|
friend |
Definition at line 179 of file search_sat.h.
Referenced by SearchSat().
|
friend |
Definition at line 180 of file search_sat.h.
Referenced by SearchSat().
|
friend |
Definition at line 188 of file search_sat.h.
Referenced by SearchSat().
|
friend |
Definition at line 200 of file search_sat.h.
Referenced by SearchSat().
|
private |
|
private |
Bottom scope for current query.
Definition at line 46 of file search_sat.h.
Referenced by getBottomScope(), newUserAssumptionInt(), and returnFromCheck().
Last expr checked for validity.
Definition at line 49 of file search_sat.h.
Theorem from the last successful checkValid call. It is used by getProof and getAssumptions.
Definition at line 53 of file search_sat.h.
Referenced by getCounterExample(), getProof(), and lastThm().
List of all user assumptions.
Definition at line 56 of file search_sat.h.
Referenced by getAssumptions(), getUserAssumptions(), and newUserAssumptionInt().
List of all internal assumptions.
Definition at line 59 of file search_sat.h.
Referenced by getAssumptions(), and getInternalAssumptions().
|
private |
Index to where unprocessed assumptions start.
Definition at line 62 of file search_sat.h.
|
private |
Definition at line 64 of file search_sat.h.
Referenced by SearchSat(), and ~SearchSat().
|
private |
Pointer to DPLLT implementation.
Definition at line 67 of file search_sat.h.
Referenced by newUserAssumption(), pop(), push(), SearchSat(), and ~SearchSat().
|
private |
Implementation of TheoryAPI for DPLLT.
Definition at line 70 of file search_sat.h.
Referenced by SearchSat(), and ~SearchSat().
|
private |
Implementation of Decider for DPLLT.
Definition at line 73 of file search_sat.h.
Referenced by SearchSat(), and ~SearchSat().
Store of theorems for expressions sent to DPLLT.
Definition at line 76 of file search_sat.h.
|
private |
Manages CNF formula and its relationship to original Exprs and Theorems.
Definition at line 79 of file search_sat.h.
Referenced by checkJustified(), getValue(), newUserAssumptionInt(), newUserAssumptionIntHelper(), SearchSat(), setJustified(), and ~SearchSat().
|
private |
Callback for CNF_Manager.
Definition at line 82 of file search_sat.h.
Referenced by SearchSat(), and ~SearchSat().
|
private |
Cached values of variables.
Definition at line 85 of file search_sat.h.
Referenced by getValue(), newUserAssumptionInt(), and setValue().
|
private |
Whether we are currently in a call to dpllt->checkSat.
Definition at line 88 of file search_sat.h.
Referenced by newUserAssumptionInt().
|
private |
CNF Formula used for theory lemmas.
Definition at line 91 of file search_sat.h.
|
private |
Lemmas waiting to be translated since last call to getNewClauses()
Definition at line 94 of file search_sat.h.
|
private |
Scope parameter for lemmas waiting to be translated since last call to getNewClauses()
Definition at line 97 of file search_sat.h.
|
private |
Backtracking size of d_pendingLemmas.
Definition at line 100 of file search_sat.h.
|
private |
Backtracking next item in d_pendingLemmas.
Definition at line 103 of file search_sat.h.
|
private |
Current position in d_lemmas.
Definition at line 106 of file search_sat.h.
|
private |
List for backtracking var values.
Definition at line 109 of file search_sat.h.
Referenced by setValue().
|
private |
Backtracking size of d_varsUndoList.
Definition at line 112 of file search_sat.h.
Referenced by setValue().
|
private |
Used to determine order to find splitters.
Definition at line 131 of file search_sat.h.
Referenced by SearchSat().
|
private |
Current position in prioritySet.
Definition at line 133 of file search_sat.h.
Referenced by SearchSat().
|
private |
Backtracking size of priority set entries.
Definition at line 135 of file search_sat.h.
|
private |
Entries in priority set in insertion order (so set can be backtracked)
Definition at line 137 of file search_sat.h.
|
private |
Backtracking size of priority set entries at bottom scope.
Definition at line 139 of file search_sat.h.
|
private |
Current size of bottom entries.
Definition at line 141 of file search_sat.h.
|
private |
Entries in priority set in insertion order (so set can be backtracked)
Definition at line 143 of file search_sat.h.
|
private |
Last Var registered with core theory.
Definition at line 146 of file search_sat.h.
|
private |
Whether it's OK to call DPLLT solver from the current scope.
Definition at line 149 of file search_sat.h.
|
private |
Definition at line 151 of file search_sat.h.
Referenced by getImpliedLiteral().
|
private |
Instance of Restorer class.
Definition at line 168 of file search_sat.h.