#include <search_sat.h>
Inheritance diagram for CVC3::SearchSat:
Definition at line 39 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 805 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, and SearchSatTheoryAPI.
SearchSat::~SearchSat | ( | ) | [virtual] |
Destructor.
Definition at line 857 of file search_sat.cpp.
References d_cnfCallback, d_cnfManager, d_coreSatAPI, d_decider, d_dpllt, and d_theoryAPI.
void SearchSat::restorePre | ( | ) | [private] |
Get rid of bottom scope entries in prioritySet.
Definition at line 114 of file search_sat.cpp.
References d_bottomScope, CVC3::SearchEngine::d_core, d_prioritySet, d_prioritySetBottomEntries, d_prioritySetBottomEntriesSize, d_prioritySetBottomEntriesSizeStack, DebugAssert, CVC3::TheoryCore::getCM(), and CVC3::ContextManager::scopeLevel().
Referenced by CVC3::SearchSat::Restorer::notifyPre().
void SearchSat::restore | ( | ) | [private] |
Get rid of entries in prioritySet and pendingLemmas added since last push.
Definition at line 128 of file search_sat.cpp.
References d_pendingLemmas, d_pendingLemmasSize, d_prioritySet, d_prioritySetEntries, d_prioritySetEntriesSize, d_vars, d_varsUndoList, d_varsUndoListSize, and SAT::Var::UNKNOWN.
Referenced by CVC3::SearchSat::Restorer::notify().
bool SearchSat::recordNewRootLit | ( | SAT::Lit | lit, | |
int | priority = 0 , |
|||
bool | atBottomScope = false | |||
) | [private] |
Helper for addLemma and check.
Definition at line 144 of file search_sat.cpp.
References d_bottomScope, CVC3::SearchEngine::d_core, d_prioritySet, d_prioritySetBottomEntries, d_prioritySetBottomEntriesSize, d_prioritySetEntries, d_prioritySetEntriesSize, d_prioritySetStart, DebugAssert, CVC3::TheoryCore::getCM(), and CVC3::ContextManager::scopeLevel().
Referenced by getNewClauses(), and newUserAssumptionInt().
void SearchSat::addLemma | ( | const Theorem & | thm, | |
int | priority = 0 | |||
) | [private] |
Core theory callback which adds a new lemma from the core theory.
Definition at line 168 of file search_sat.cpp.
References d_pendingLemmas, d_pendingLemmasNext, d_pendingLemmasSize, DebugAssert, CVC3::Theorem::getExpr(), IF_DEBUG, CVC3::Expr::isAbsLiteral(), CVC3::PRESENTATION_LANG, CVC3::SearchEngine::theoryCore(), CVC3::Expr::toString(), and CVC3::TRACE.
Referenced by CVC3::SearchSatCoreSatAPI::addLemma(), and addSplitter().
int CVC3::SearchSat::getBottomScope | ( | ) | [inline, private] |
Core theory callback which asks for the bottom scope for current query.
Definition at line 180 of file search_sat.h.
References d_bottomScope.
void SearchSat::addSplitter | ( | const Expr & | e, | |
int | priority | |||
) | [private] |
Core theory callback which suggests a splitter.
Definition at line 182 of file search_sat.cpp.
References addLemma(), CVC3::SearchEngine::d_commonRules, and CVC3::CommonProofRules::excludedMiddle().
Referenced by CVC3::SearchSatCoreSatAPI::addSplitter().
void SearchSat::assertLit | ( | SAT::Lit | l | ) | [private] |
DPLLT callback to inform theory that a literal has been assigned.
Definition at line 188 of file search_sat.cpp.
References SAT::CNF_Manager::addAssumption(), CVC3::TheoryCore::addFact(), CVC3::CommonProofRules::assumpRule(), SAT::CNF_Manager::concreteLit(), d_cnfManager, CVC3::SearchEngine::d_commonRules, CVC3::SearchEngine::d_core, d_intAssumptions, DebugAssert, CVC3::TheoryCore::getCM(), getValue(), SAT::Lit::getVar(), IF_DEBUG, CVC3::Expr::isAbsLiteral(), CVC3::Expr::isIntAssumption(), CVC3::Expr::isNot(), CVC3::Expr::isNull(), SAT::Lit::isPositive(), CVC3::ContextManager::scopeLevel(), CVC3::Expr::setIntAssumption(), CVC3::Theorem::setQuantLevel(), setValue(), CVC3::SearchEngine::theoryCore(), CVC3::Expr::toString(), CVC3::TRACE, SAT::Var::TRUE_VAL, and SAT::Var::UNKNOWN.
Referenced by CVC3::SearchSatTheoryAPI::assertLit().
SAT::DPLLT::ConsistentResult SearchSat::checkConsistent | ( | SAT::Clause & | c, | |
bool | fullEffort | |||
) | [private] |
DPLLT callback to ask if theory has detected inconsistency.
Definition at line 250 of file search_sat.cpp.
References CVC3::TheoryCore::checkSATCore(), SAT::CNF_Manager::convertLemma(), d_cnfManager, CVC3::SearchEngine::d_core, d_inCheckSat, d_lemmas, d_lemmasNext, d_pendingLemmas, d_pendingLemmasNext, DebugAssert, CVC3::TheoryCore::inconsistent(), CVC3::TheoryCore::inconsistentThm(), and SAT::CD_CNF_Formula::numClauses().
Referenced by CVC3::SearchSatTheoryAPI::checkConsistent().
Lit SearchSat::getImplication | ( | ) | [private] |
DPLLT callback to get theory propagations.
Definition at line 270 of file search_sat.cpp.
References d_cnfManager, CVC3::SearchEngine::d_core, d_theorems, DebugAssert, SAT::CNF_Manager::getCNFLit(), CVC3::Theorem::getExpr(), CVC3::TheoryCore::getImpliedLiteral(), getValue(), SAT::Lit::isNull(), CVC3::Theorem::isNull(), CVC3::Expr::isUserRegisteredAtom(), SAT::Lit::reset(), and CVC3::Expr::unnegate().
Referenced by CVC3::SearchSatTheoryAPI::getImplication().
void SearchSat::getExplanation | ( | SAT::Lit | l, | |
SAT::Clause & | c | |||
) | [private] |
DPLLT callback to explain a theory propagation.
Definition at line 290 of file search_sat.cpp.
References SAT::CNF_Manager::concreteLit(), SAT::CNF_Manager::convertLemma(), d_cnfManager, d_theorems, DebugAssert, and SAT::Clause::size().
Referenced by CVC3::SearchSatTheoryAPI::getExplanation().
bool SearchSat::getNewClauses | ( | SAT::CNF_Formula & | cnf | ) | [private] |
DPLLT callback to get more general theory clauses.
Definition at line 301 of file search_sat.cpp.
References SAT::CNF_Manager::addLemma(), d_cnfManager, d_lemmas, d_lemmasNext, d_pendingLemmas, d_pendingLemmasNext, d_vars, SAT::CD_CNF_Formula::deleteLast(), getValue(), SAT::Lit::getVar(), SAT::Lit::isVar(), SAT::CD_CNF_Formula::numClauses(), SAT::CNF_Manager::numVars(), recordNewRootLit(), and SAT::Var::UNKNOWN.
Referenced by check(), and CVC3::SearchSatTheoryAPI::getNewClauses().
Lit SearchSat::makeDecision | ( | ) | [private] |
DPLLT callback to decide which literal to split on next.
Definition at line 341 of file search_sat.cpp.
References d_inCheckSat, d_prioritySet, d_prioritySetStart, DebugAssert, findSplitterRec(), and getValue().
Referenced by CVC3::SearchSatDecider::makeDecision().
bool SearchSat::findSplitterRec | ( | SAT::Lit | lit, | |
SAT::Var::Val | value, | |||
SAT::Lit * | litDecision | |||
) | [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 CVC3::AND, checkJustified(), SAT::CNF_Manager::concreteLit(), d_cnfManager, DebugAssert, std::endl(), FatalAssert, SAT::CNF_Manager::getFanin(), CVC3::Expr::getKind(), getValue(), SAT::Lit::getVar(), CVC3::IFF, CVC3::IMPLIES, CVC3::Expr::isAbsAtomicFormula(), SAT::Lit::isFalse(), SAT::Lit::isInverted(), SAT::Lit::isTrue(), SAT::Lit::isVar(), CVC3::ITE, SAT::CNF_Manager::numFanins(), CVC3::OR, setJustified(), UNKNOWN, and CVC3::XOR.
Referenced by makeDecision().
SAT::Var::Val CVC3::SearchSat::getValue | ( | SAT::Lit | c | ) | [inline, private] |
Get the value of a CNF Literal.
Definition at line 210 of file search_sat.h.
References d_vars, DebugAssert, SAT::Var::FALSE_VAL, SAT::Lit::getVar(), SAT::Var::invertValue(), SAT::Lit::isFalse(), SAT::Lit::isInverted(), SAT::Lit::isTrue(), SAT::Lit::isVar(), and SAT::Var::TRUE_VAL.
Referenced by assertLit(), findSplitterRec(), getImplication(), getNewClauses(), and makeDecision().
void CVC3::SearchSat::setValue | ( | SAT::Var | v, | |
SAT::Var::Val | val | |||
) | [inline, private] |
Set the value of a variable.
Definition at line 218 of file search_sat.h.
References d_vars, d_varsUndoList, d_varsUndoListSize, DebugAssert, SAT::Var::isNull(), and SAT::Var::UNKNOWN.
Referenced by assertLit().
bool CVC3::SearchSat::checkJustified | ( | SAT::Var | v | ) | [inline, private] |
Check whether this variable's value is justified.
Definition at line 230 of file search_sat.h.
References SAT::CNF_Manager::concreteLit(), d_cnfManager, and CVC3::Expr::isJustified().
Referenced by findSplitterRec().
void CVC3::SearchSat::setJustified | ( | SAT::Var | v | ) | [inline, private] |
Mark this variable as justified.
Definition at line 234 of file search_sat.h.
References SAT::CNF_Manager::concreteLit(), d_cnfManager, and CVC3::Expr::setJustified().
Referenced by findSplitterRec().
QueryResult SearchSat::check | ( | const Expr & | e, | |
Theorem & | result, | |||
bool | isRestart = false | |||
) | [private] |
Main checking procedure shared by checkValid and restart.
Definition at line 635 of file search_sat.cpp.
References CVC3::CommonProofRules::assumpRule(), SAT::DPLLT::checkSat(), SAT::DPLLT::continueCheck(), d_bottomScope, d_cnfManager, CVC3::SearchEngine::d_commonRules, CVC3::SearchEngine::d_core, d_dpllt, d_dplltReady, d_inCheckSat, d_lastCheck, d_lastValid, d_lemmas, d_lemmasNext, d_prioritySetBottomEntriesSize, d_prioritySetBottomEntriesSizeStack, CVC3::SearchEngine::d_rules, DebugAssert, CVC3::debugger, std::endl(), CVC3::Theory::findExpr(), CVC3::TheoryCore::getCM(), getNewClauses(), CVC3::TheoryCore::getPredicates(), CVC3::TheoryCore::getTerms(), CVC3::Expr::getType(), CVC3::TheoryCore::incomplete(), CVC3::TheoryCore::inconsistent(), CVC3::TheoryCore::inconsistentThm(), CVC3::INVALID, CVC3::Type::isBool(), CVC3::Expr::isFalse(), CVC3::Expr::isNot(), CVC3::Expr::isTrue(), newUserAssumptionInt(), SAT::CD_CNF_Formula::numClauses(), pop(), CVC3::SearchEngineRules::proofByContradiction(), push(), CVC3::SATISFIABLE, CVC3::ContextManager::scopeLevel(), SAT::CNF_Manager::setBottomScope(), CVC3::Theory::simplifyExpr(), CVC3::CDList< T >::size(), CVC3::Type::toString(), CVC3::Expr::toString(), CVC3::TRACE, CVC3::CommonProofRules::trueTheorem(), CVC3::UNKNOWN, CVC3::UNSATISFIABLE, and CVC3::VALID.
Referenced by CVC3::SearchSatCoreSatAPI::check(), checkValid(), and restart().
Theorem SearchSat::newUserAssumptionInt | ( | const Expr & | e, | |
SAT::CNF_Formula_Impl & | cnf, | |||
bool | atBottomScope | |||
) | [private] |
Helper for newUserAssumption.
Definition at line 908 of file search_sat.cpp.
References SAT::CNF_Manager::addAssumption(), 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, SAT::CNF_Formula_Impl::deleteLast(), CVC3::TheoryCore::getCM(), CVC3::Theorem::getExpr(), CVC3::TheoryCore::getExprTrans(), isAssumption(), CVC3::Expr::isFalse(), CVC3::Expr::isTrue(), SAT::CNF_Manager::numVars(), CVC3::ExprTransform::preprocess(), recordNewRootLit(), CVC3::ContextManager::scopeLevel(), setRecursiveInUserAssumption(), CVC3::Expr::setUserAssumption(), and SAT::Var::UNKNOWN.
Referenced by check(), and newUserAssumption().
virtual const std::string& CVC3::SearchSat::getName | ( | ) | [inline, virtual] |
Name of this search engine.
Implements CVC3::SearchEngine.
Definition at line 254 of file search_sat.h.
References d_name.
void SearchSat::registerAtom | ( | const Expr & | e | ) | [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 868 of file search_sat.cpp.
References CVC3::SearchEngine::d_core, CVC3::Expr::isRegisteredAtom(), CVC3::TheoryCore::registerAtom(), and CVC3::Expr::setUserRegisteredAtom().
Theorem SearchSat::getImpliedLiteral | ( | ) | [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 876 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().
virtual void CVC3::SearchSat::push | ( | ) | [inline, virtual] |
Push a checkpoint.
Implements CVC3::SearchEngine.
Definition at line 257 of file search_sat.h.
References d_dpllt, and SAT::DPLLT::push().
Referenced by check(), and CVC3::SearchSatCoreSatAPI::check().
virtual void CVC3::SearchSat::pop | ( | ) | [inline, virtual] |
Restore last checkpoint.
Implements CVC3::SearchEngine.
Definition at line 258 of file search_sat.h.
References d_dpllt, and SAT::DPLLT::pop().
Referenced by check(), CVC3::SearchSatCoreSatAPI::check(), and returnFromCheck().
virtual QueryResult CVC3::SearchSat::checkValid | ( | const Expr & | e, | |
Theorem & | result | |||
) | [inline, virtual] |
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 259 of file search_sat.h.
References check().
virtual QueryResult CVC3::SearchSat::restart | ( | const Expr & | e, | |
Theorem & | result | |||
) | [inline, virtual] |
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 261 of file search_sat.h.
References check().
void SearchSat::returnFromCheck | ( | ) | [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 888 of file search_sat.cpp.
References d_bottomScope, and pop().
virtual Theorem CVC3::SearchSat::lastThm | ( | ) | [inline, virtual] |
Returns the result of the most recent valid theorem.
Returns Null Theorem if last call was not valid
Implements CVC3::SearchEngine.
Definition at line 264 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 948 of file search_sat.cpp.
References SAT::DPLLT::addAssertion(), d_dpllt, and newUserAssumptionInt().
Referenced by CVC3::SearchSatCoreSatAPI::addAssumption().
void SearchSat::getUserAssumptions | ( | std::vector< Expr > & | assumptions | ) | [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 957 of file search_sat.cpp.
References d_userAssumptions.
void SearchSat::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.
assumptions | should be empty on entry. |
Implements CVC3::SearchEngine.
Definition at line 965 of file search_sat.cpp.
References d_intAssumptions.
Referenced by getCounterExample().
void SearchSat::getAssumptions | ( | std::vector< Expr > & | assumptions | ) | [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 973 of file search_sat.cpp.
References d_intAssumptions, d_userAssumptions, CVC3::Theorem::getExpr(), CVC3::Expr::isUserAssumption(), and CVC3::CDList< T >::push_back().
bool SearchSat::isAssumption | ( | const Expr & | e | ) | [virtual] |
Check if the formula has already been assumed previously.
Implements CVC3::SearchEngine.
Definition at line 1008 of file search_sat.cpp.
References CVC3::Expr::isIntAssumption(), and CVC3::Expr::isUserAssumption().
Referenced by newUserAssumptionInt().
void SearchSat::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 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 1014 of file search_sat.cpp.
References d_lastValid, and getInternalAssumptions().
Proof SearchSat::getProof | ( | ) | [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 1023 of file search_sat.cpp.
References CVC3::SearchEngine::d_core, d_lastValid, CVC3::TheoryCore::getTM(), and CVC3::TheoremManager::withProof().
friend class Restorer [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 154 of file search_sat.h.
friend class SearchSatCoreSatAPI [friend] |
friend class SearchSatCNFCallback [friend] |
friend class SearchSatTheoryAPI [friend] |
friend class SearchSatDecider [friend] |
std::string CVC3::SearchSat::d_name [private] |
CDO<int> CVC3::SearchSat::d_bottomScope [private] |
Bottom scope for current query.
Definition at line 45 of file search_sat.h.
Referenced by check(), getBottomScope(), newUserAssumptionInt(), recordNewRootLit(), restorePre(), and returnFromCheck().
CDO<Expr> CVC3::SearchSat::d_lastCheck [private] |
CDO<Theorem> CVC3::SearchSat::d_lastValid [private] |
Theorem from the last successful checkValid call. It is used by getProof and getAssumptions.
Definition at line 52 of file search_sat.h.
Referenced by check(), getCounterExample(), getProof(), and lastThm().
CDList<Theorem> CVC3::SearchSat::d_userAssumptions [private] |
List of all user assumptions.
Definition at line 55 of file search_sat.h.
Referenced by getAssumptions(), getUserAssumptions(), and newUserAssumptionInt().
CDList<Theorem> CVC3::SearchSat::d_intAssumptions [private] |
List of all internal assumptions.
Definition at line 58 of file search_sat.h.
Referenced by assertLit(), getAssumptions(), and getInternalAssumptions().
CDO<unsigned> CVC3::SearchSat::d_idxUserAssump [private] |
SAT::DPLLT* CVC3::SearchSat::d_dpllt [private] |
Pointer to DPLLT implementation.
Definition at line 66 of file search_sat.h.
Referenced by check(), newUserAssumption(), pop(), push(), SearchSat(), and ~SearchSat().
Implementation of TheoryAPI for DPLLT.
Definition at line 69 of file search_sat.h.
Referenced by SearchSat(), and ~SearchSat().
SAT::DPLLT::Decider* CVC3::SearchSat::d_decider [private] |
Implementation of Decider for DPLLT.
Definition at line 72 of file search_sat.h.
Referenced by SearchSat(), and ~SearchSat().
CDMap<Expr, Theorem> CVC3::SearchSat::d_theorems [private] |
Store of theorems for expressions sent to DPLLT.
Definition at line 75 of file search_sat.h.
Referenced by getExplanation(), and getImplication().
SAT::CNF_Manager* CVC3::SearchSat::d_cnfManager [private] |
Manages CNF formula and its relationship to original Exprs and Theorems.
Definition at line 78 of file search_sat.h.
Referenced by assertLit(), check(), checkConsistent(), checkJustified(), findSplitterRec(), getExplanation(), getImplication(), getNewClauses(), newUserAssumptionInt(), SearchSat(), setJustified(), and ~SearchSat().
Callback for CNF_Manager.
Definition at line 81 of file search_sat.h.
Referenced by SearchSat(), and ~SearchSat().
std::vector<SAT::Var::Val> CVC3::SearchSat::d_vars [private] |
Cached values of variables.
Definition at line 84 of file search_sat.h.
Referenced by getNewClauses(), getValue(), newUserAssumptionInt(), restore(), and setValue().
bool CVC3::SearchSat::d_inCheckSat [private] |
Whether we are currently in a call to dpllt->checkSat.
Definition at line 87 of file search_sat.h.
Referenced by check(), checkConsistent(), makeDecision(), and newUserAssumptionInt().
SAT::CD_CNF_Formula CVC3::SearchSat::d_lemmas [private] |
CNF Formula used for theory lemmas.
Definition at line 90 of file search_sat.h.
Referenced by check(), checkConsistent(), and getNewClauses().
std::vector<std::pair<Theorem, int> > CVC3::SearchSat::d_pendingLemmas [private] |
Lemmas waiting to be translated since last call to getNewClauses().
Definition at line 93 of file search_sat.h.
Referenced by addLemma(), checkConsistent(), getNewClauses(), and restore().
CDO<unsigned> CVC3::SearchSat::d_pendingLemmasSize [private] |
Backtracking size of d_pendingLemmas.
Definition at line 96 of file search_sat.h.
Referenced by addLemma(), and restore().
CDO<unsigned> CVC3::SearchSat::d_pendingLemmasNext [private] |
Backtracking next item in d_pendingLemmas.
Definition at line 99 of file search_sat.h.
Referenced by addLemma(), checkConsistent(), and getNewClauses().
CDO<unsigned> CVC3::SearchSat::d_lemmasNext [private] |
Current position in d_lemmas.
Definition at line 102 of file search_sat.h.
Referenced by check(), checkConsistent(), and getNewClauses().
std::vector<unsigned> CVC3::SearchSat::d_varsUndoList [private] |
List for backtracking var values.
Definition at line 105 of file search_sat.h.
Referenced by restore(), and setValue().
CDO<unsigned> CVC3::SearchSat::d_varsUndoListSize [private] |
Backtracking size of d_varsUndoList.
Definition at line 108 of file search_sat.h.
Referenced by restore(), and setValue().
std::set<LitPriorityPair> CVC3::SearchSat::d_prioritySet [private] |
Used to determine order to find splitters.
Definition at line 127 of file search_sat.h.
Referenced by makeDecision(), recordNewRootLit(), restore(), restorePre(), and SearchSat().
CDO<std::set<LitPriorityPair>::const_iterator> CVC3::SearchSat::d_prioritySetStart [private] |
Current position in prioritySet.
Definition at line 129 of file search_sat.h.
Referenced by makeDecision(), recordNewRootLit(), and SearchSat().
CDO<unsigned> CVC3::SearchSat::d_prioritySetEntriesSize [private] |
Backtracking size of priority set entries.
Definition at line 131 of file search_sat.h.
Referenced by recordNewRootLit(), and restore().
std::vector<std::set<LitPriorityPair>::iterator> CVC3::SearchSat::d_prioritySetEntries [private] |
Entries in priority set in insertion order (so set can be backtracked).
Definition at line 133 of file search_sat.h.
Referenced by recordNewRootLit(), and restore().
std::vector<unsigned> CVC3::SearchSat::d_prioritySetBottomEntriesSizeStack [private] |
Backtracking size of priority set entries at bottom scope.
Definition at line 135 of file search_sat.h.
Referenced by check(), and restorePre().
unsigned CVC3::SearchSat::d_prioritySetBottomEntriesSize [private] |
Current size of bottom entries.
Definition at line 137 of file search_sat.h.
Referenced by check(), recordNewRootLit(), and restorePre().
std::vector<std::set<LitPriorityPair>::iterator> CVC3::SearchSat::d_prioritySetBottomEntries [private] |
Entries in priority set in insertion order (so set can be backtracked).
Definition at line 139 of file search_sat.h.
Referenced by recordNewRootLit(), and restorePre().
CDO<unsigned> CVC3::SearchSat::d_lastRegisteredVar [private] |
CDO<bool> CVC3::SearchSat::d_dplltReady [private] |
Whether it's OK to call DPLLT solver from the current scope.
Definition at line 145 of file search_sat.h.
Referenced by check().
CDO<unsigned> CVC3::SearchSat::d_nextImpliedLiteral [private] |
Restorer CVC3::SearchSat::d_restorer [private] |