CVC3  2.4.1
Classes | Public Member Functions | Private Member Functions | Private Attributes | Friends | List of all members
CVC3::SearchSat Class Reference

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

#include <search_sat.h>

Inheritance diagram for CVC3::SearchSat:
CVC3::SearchEngine

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. More...
 
virtual const std::string & getName ()
 Name of this search engine. More...
 
virtual void registerAtom (const Expr &e)
 Register an atomic formula of interest. More...
 
virtual Theorem getImpliedLiteral ()
 Return next literal implied by last assertion. Null Expr if none. More...
 
virtual void push ()
 Push a checkpoint. More...
 
virtual void pop ()
 Restore last checkpoint. More...
 
virtual QueryResult checkValid (const Expr &e, Theorem &result)
 Checks the validity of a formula in the current context. More...
 
virtual QueryResult restart (const Expr &e, Theorem &result)
 Reruns last check with e as an additional assumption. More...
 
virtual void returnFromCheck ()
 Returns to context immediately before last call to checkValid. More...
 
virtual Theorem lastThm ()
 Returns the result of the most recent valid theorem. More...
 
virtual Theorem newUserAssumption (const Expr &e)
 Generate and add an assumption to the set of assumptions in the current context. More...
 
virtual void getUserAssumptions (std::vector< Expr > &assumptions)
 Get all user assumptions made in this and all previous contexts. More...
 
virtual void getInternalAssumptions (std::vector< Expr > &assumptions)
 Get assumptions made internally in this and all previous contexts. More...
 
virtual void getAssumptions (std::vector< Expr > &assumptions)
 Get all assumptions made in this and all previous contexts. More...
 
virtual bool isAssumption (const Expr &e)
 Check if the formula has already been assumed previously. More...
 
virtual void getCounterExample (std::vector< Expr > &assertions, bool inOrder=true)
 Will return the set of assertions which make the queried formula false. More...
 
virtual Proof getProof ()
 Returns the proof term for the last proven query. More...
 
virtual FormulaValue getValue (const CVC3::Expr &e)
 
- Public Member Functions inherited from CVC3::SearchEngine
 SearchEngine (TheoryCore *core)
 Constructor. More...
 
virtual ~SearchEngine ()
 Destructor. More...
 
CommonProofRulesgetCommonRules ()
 Accessor for common rules. More...
 
TheoryCoretheoryCore ()
 Accessor for TheoryCore. More...
 
void getConcreteModel (ExprMap< Expr > &m)
 Build a concrete Model (assign values to variables), should only be called after a query which returns INVALID. More...
 
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. More...
 

Private Member Functions

void restorePre ()
 Get rid of bottom scope entries in prioritySet. More...
 
void restore ()
 Get rid of entries in prioritySet and pendingLemmas added since last push. More...
 
bool recordNewRootLit (SAT::Lit lit, int priority=0, bool atBottomScope=false)
 Helper for addLemma and check. More...
 
void addLemma (const Theorem &thm, int priority=0, bool atBotomScope=false)
 Core theory callback which adds a new lemma from the core theory. More...
 
int getBottomScope ()
 Core theory callback which asks for the bottom scope for current query. More...
 
void addSplitter (const Expr &e, int priority)
 Core theory callback which suggests a splitter. More...
 
void assertLit (SAT::Lit l)
 DPLLT callback to inform theory that a literal has been assigned. More...
 
SAT::DPLLT::ConsistentResult checkConsistent (SAT::CNF_Formula &cnf, bool fullEffort)
 DPLLT callback to ask if theory has detected inconsistency. More...
 
SAT::Lit getImplication ()
 DPLLT callback to get theory propagations. More...
 
void getExplanation (SAT::Lit l, SAT::CNF_Formula &cnf)
 DPLLT callback to explain a theory propagation. More...
 
bool getNewClauses (SAT::CNF_Formula &cnf)
 DPLLT callback to get more general theory clauses. More...
 
SAT::Lit makeDecision ()
 DPLLT callback to decide which literal to split on next. More...
 
bool findSplitterRec (SAT::Lit lit, SAT::Var::Val value, SAT::Lit *litDecision)
 Recursively traverse DAG looking for a splitter. More...
 
SAT::Var::Val getValue (SAT::Lit c)
 Get the value of a CNF Literal. More...
 
SAT::Var::Val getValue (SAT::Var v)
 
void setValue (SAT::Var v, SAT::Var::Val val)
 Set the value of a variable. More...
 
bool checkJustified (SAT::Var v)
 Check whether this variable's value is justified. More...
 
void setJustified (SAT::Var v)
 Mark this variable as justified. More...
 
QueryResult check (const Expr &e, Theorem &result, bool isRestart=false)
 Main checking procedure shared by checkValid and restart. More...
 
void newUserAssumptionIntHelper (const Theorem &thm, SAT::CNF_Formula_Impl &cnf, bool atBottomScope)
 Helper for newUserAssumptionInt. More...
 
Theorem newUserAssumptionInt (const Expr &e, SAT::CNF_Formula_Impl &cnf, bool atBottomScope)
 Helper for newUserAssumption. More...
 

Private Attributes

std::string d_name
 Name of search engine. More...
 
CDO< int > d_bottomScope
 Bottom scope for current query. More...
 
CDO< Exprd_lastCheck
 Last expr checked for validity. More...
 
CDO< Theoremd_lastValid
 Theorem from the last successful checkValid call. It is used by getProof and getAssumptions. More...
 
CDList< Theoremd_userAssumptions
 List of all user assumptions. More...
 
CDList< Theoremd_intAssumptions
 List of all internal assumptions. More...
 
CDO< unsigned > d_idxUserAssump
 Index to where unprocessed assumptions start. More...
 
TheoryCore::CoreSatAPId_coreSatAPI
 
SAT::DPLLTd_dpllt
 Pointer to DPLLT implementation. More...
 
SAT::DPLLT::TheoryAPId_theoryAPI
 Implementation of TheoryAPI for DPLLT. More...
 
SAT::DPLLT::Deciderd_decider
 Implementation of Decider for DPLLT. More...
 
CDMap< Expr, Theoremd_theorems
 Store of theorems for expressions sent to DPLLT. More...
 
SAT::CNF_Managerd_cnfManager
 Manages CNF formula and its relationship to original Exprs and Theorems. More...
 
SAT::CNF_Manager::CNFCallbackd_cnfCallback
 Callback for CNF_Manager. More...
 
std::vector< SAT::Var::Vald_vars
 Cached values of variables. More...
 
bool d_inCheckSat
 Whether we are currently in a call to dpllt->checkSat. More...
 
SAT::CD_CNF_Formula d_lemmas
 CNF Formula used for theory lemmas. More...
 
std::vector< std::pair
< Theorem, int > > 
d_pendingLemmas
 Lemmas waiting to be translated since last call to getNewClauses() More...
 
std::vector< bool > d_pendingScopes
 Scope parameter for lemmas waiting to be translated since last call to getNewClauses() More...
 
CDO< unsigned > d_pendingLemmasSize
 Backtracking size of d_pendingLemmas. More...
 
CDO< unsigned > d_pendingLemmasNext
 Backtracking next item in d_pendingLemmas. More...
 
CDO< unsigned > d_lemmasNext
 Current position in d_lemmas. More...
 
std::vector< unsigned > d_varsUndoList
 List for backtracking var values. More...
 
CDO< unsigned > d_varsUndoListSize
 Backtracking size of d_varsUndoList. More...
 
std::set< LitPriorityPaird_prioritySet
 Used to determine order to find splitters. More...
 
CDO< std::set< LitPriorityPair >
::const_iterator > 
d_prioritySetStart
 Current position in prioritySet. More...
 
CDO< unsigned > d_prioritySetEntriesSize
 Backtracking size of priority set entries. More...
 
std::vector< std::set
< LitPriorityPair >::iterator > 
d_prioritySetEntries
 Entries in priority set in insertion order (so set can be backtracked) More...
 
std::vector< unsigned > d_prioritySetBottomEntriesSizeStack
 Backtracking size of priority set entries at bottom scope. More...
 
unsigned d_prioritySetBottomEntriesSize
 Current size of bottom entries. More...
 
std::vector< std::set
< LitPriorityPair >::iterator > 
d_prioritySetBottomEntries
 Entries in priority set in insertion order (so set can be backtracked) More...
 
CDO< unsigned > d_lastRegisteredVar
 Last Var registered with core theory. More...
 
CDO< bool > d_dplltReady
 Whether it's OK to call DPLLT solver from the current scope. More...
 
CDO< unsigned > d_nextImpliedLiteral
 
Restorer d_restorer
 Instance of Restorer class. More...
 

Friends

class Restorer
 Helper class for resetting DPLLT engine. More...
 
class SearchSatCoreSatAPI
 
class SearchSatCNFCallback
 
class SearchSatTheoryAPI
 
class SearchSatDecider
 

Additional Inherited Members

- Protected Member Functions inherited from CVC3::SearchEngine
SearchEngineRulescreateRules ()
 Create the trusted component. More...
 
SearchEngineRulescreateRules (SearchEngine *s_eng)
 
- Protected Attributes inherited from CVC3::SearchEngine
TheoryCored_core
 Access to theory reasoning. More...
 
CommonProofRulesd_commonRules
 Common proof rules. More...
 
SearchEngineRulesd_rules
 Proof rules for the search engine. More...
 

Detailed Description

Search engine that connects to a generic SAT reasoning module.

Definition at line 40 of file search_sat.h.

Constructor & Destructor Documentation

SearchSat::SearchSat ( TheoryCore core,
const std::string &  name 
)
SearchSat::~SearchSat ( )
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.

Member Function Documentation

void SearchSat::restorePre ( )
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().

void SearchSat::restore ( void  )
private

Get rid of entries in prioritySet and pendingLemmas added since last push.

Definition at line 129 of file search_sat.cpp.

References 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 146 of file search_sat.cpp.

References DebugAssert.

Referenced by newUserAssumptionIntHelper().

void SearchSat::addLemma ( const Theorem thm,
int  priority = 0,
bool  atBotomScope = false 
)
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.

int CVC3::SearchSat::getBottomScope ( )
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.

void SearchSat::addSplitter ( const Expr e,
int  priority 
)
private

Core theory callback which suggests a splitter.

Definition at line 186 of file search_sat.cpp.

References DebugAssert, and CVC3::Expr::isEq().

void SearchSat::assertLit ( SAT::Lit  l)
private
SAT::DPLLT::ConsistentResult SearchSat::checkConsistent ( SAT::CNF_Formula cnf,
bool  fullEffort 
)
private

DPLLT callback to ask if theory has detected inconsistency.

Definition at line 258 of file search_sat.cpp.

References DebugAssert, and SAT::Var::UNKNOWN.

Lit SearchSat::getImplication ( )
private
void SearchSat::getExplanation ( SAT::Lit  l,
SAT::CNF_Formula cnf 
)
private

DPLLT callback to explain a theory propagation.

Definition at line 304 of file search_sat.cpp.

References DebugAssert, SAT::CNF_Formula::empty(), and SAT::Var::UNKNOWN.

bool SearchSat::getNewClauses ( SAT::CNF_Formula cnf)
private

DPLLT callback to get more general theory clauses.

Definition at line 318 of file search_sat.cpp.

References DebugAssert, and SAT::Var::UNKNOWN.

Lit SearchSat::makeDecision ( )
private

DPLLT callback to decide which literal to split on next.

Definition at line 346 of file search_sat.cpp.

References DebugAssert.

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

SAT::Var::Val CVC3::SearchSat::getValue ( SAT::Lit  c)
inlineprivate
SAT::Var::Val CVC3::SearchSat::getValue ( SAT::Var  v)
inlineprivate

Definition at line 223 of file search_sat.h.

References d_vars, DebugAssert, and SAT::Var::isVar().

void CVC3::SearchSat::setValue ( SAT::Var  v,
SAT::Var::Val  val 
)
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.

bool CVC3::SearchSat::checkJustified ( SAT::Var  v)
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().

void CVC3::SearchSat::setJustified ( SAT::Var  v)
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().

QueryResult SearchSat::check ( const Expr e,
Theorem result,
bool  isRestart = false 
)
private
void SearchSat::newUserAssumptionIntHelper ( const Theorem thm,
SAT::CNF_Formula_Impl cnf,
bool  atBottomScope 
)
private
Theorem SearchSat::newUserAssumptionInt ( const Expr e,
SAT::CNF_Formula_Impl cnf,
bool  atBottomScope 
)
private
virtual const std::string& CVC3::SearchSat::getName ( )
inlinevirtual

Name of this search engine.

Implements CVC3::SearchEngine.

Definition at line 268 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 1002 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 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().

virtual void CVC3::SearchSat::push ( )
inlinevirtual

Push a checkpoint.

Implements CVC3::SearchEngine.

Definition at line 271 of file search_sat.h.

References d_dpllt, and SAT::DPLLT::push().

virtual void CVC3::SearchSat::pop ( )
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().

virtual QueryResult CVC3::SearchSat::checkValid ( const Expr e,
Theorem result 
)
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.

Parameters
ethe formula to check.
resultthe resulting theorem, if the formula is valid.

Implements CVC3::SearchEngine.

Definition at line 273 of file search_sat.h.

References check().

virtual QueryResult CVC3::SearchSat::restart ( const Expr e,
Theorem result 
)
inlinevirtual

Reruns last check with e as an additional assumption.

This method should only be called after a query which is invalid.

Parameters
ethe additional assumption
resultthe resulting theorem, if the query is valid.

Implements CVC3::SearchEngine.

Definition at line 275 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 1022 of file search_sat.cpp.

References d_bottomScope, and pop().

virtual Theorem CVC3::SearchSat::lastThm ( )
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.

Theorem SearchSat::newUserAssumption ( const Expr e)
virtual

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

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.

Parameters
assumptionsshould be empty on entry.

Implements CVC3::SearchEngine.

Definition at line 1111 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.

Parameters
assumptionsshould be empty on entry.

Implements CVC3::SearchEngine.

Definition at line 1119 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.

Parameters
assumptionsshould be an empty vector which will be filled \ with the assumptions

Implements CVC3::SearchEngine.

Definition at line 1128 of file search_sat.cpp.

References d_intAssumptions, d_userAssumptions, and CVC3::Expr::isUserAssumption().

bool SearchSat::isAssumption ( const Expr e)
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().

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.

Parameters
assertionsshould be empty on entry.
inOrderif 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, 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 1178 of file search_sat.cpp.

References CVC3::SearchEngine::d_core, d_lastValid, CVC3::TheoryCore::getTM(), and CVC3::TheoremManager::withProof().

virtual FormulaValue CVC3::SearchSat::getValue ( const CVC3::Expr e)
inlinevirtual

Friends And Related Function Documentation

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 158 of file search_sat.h.

friend class SearchSatCoreSatAPI
friend

Definition at line 179 of file search_sat.h.

Referenced by SearchSat().

friend class SearchSatCNFCallback
friend

Definition at line 180 of file search_sat.h.

Referenced by SearchSat().

friend class SearchSatTheoryAPI
friend

Definition at line 188 of file search_sat.h.

Referenced by SearchSat().

friend class SearchSatDecider
friend

Definition at line 200 of file search_sat.h.

Referenced by SearchSat().

Member Data Documentation

std::string CVC3::SearchSat::d_name
private

Name of search engine.

Definition at line 43 of file search_sat.h.

Referenced by getName().

CDO<int> CVC3::SearchSat::d_bottomScope
private

Bottom scope for current query.

Definition at line 46 of file search_sat.h.

Referenced by getBottomScope(), newUserAssumptionInt(), and returnFromCheck().

CDO<Expr> CVC3::SearchSat::d_lastCheck
private

Last expr checked for validity.

Definition at line 49 of file search_sat.h.

CDO<Theorem> CVC3::SearchSat::d_lastValid
private

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

CDList<Theorem> CVC3::SearchSat::d_userAssumptions
private

List of all user assumptions.

Definition at line 56 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 59 of file search_sat.h.

Referenced by getAssumptions(), and getInternalAssumptions().

CDO<unsigned> CVC3::SearchSat::d_idxUserAssump
private

Index to where unprocessed assumptions start.

Definition at line 62 of file search_sat.h.

TheoryCore::CoreSatAPI* CVC3::SearchSat::d_coreSatAPI
private

Definition at line 64 of file search_sat.h.

Referenced by SearchSat(), and ~SearchSat().

SAT::DPLLT* CVC3::SearchSat::d_dpllt
private

Pointer to DPLLT implementation.

Definition at line 67 of file search_sat.h.

Referenced by newUserAssumption(), pop(), push(), SearchSat(), and ~SearchSat().

SAT::DPLLT::TheoryAPI* CVC3::SearchSat::d_theoryAPI
private

Implementation of TheoryAPI for DPLLT.

Definition at line 70 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 73 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 76 of file search_sat.h.

SAT::CNF_Manager* CVC3::SearchSat::d_cnfManager
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().

SAT::CNF_Manager::CNFCallback* CVC3::SearchSat::d_cnfCallback
private

Callback for CNF_Manager.

Definition at line 82 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 85 of file search_sat.h.

Referenced by getValue(), newUserAssumptionInt(), and setValue().

bool CVC3::SearchSat::d_inCheckSat
private

Whether we are currently in a call to dpllt->checkSat.

Definition at line 88 of file search_sat.h.

Referenced by newUserAssumptionInt().

SAT::CD_CNF_Formula CVC3::SearchSat::d_lemmas
private

CNF Formula used for theory lemmas.

Definition at line 91 of file search_sat.h.

std::vector<std::pair<Theorem, int> > CVC3::SearchSat::d_pendingLemmas
private

Lemmas waiting to be translated since last call to getNewClauses()

Definition at line 94 of file search_sat.h.

std::vector<bool> CVC3::SearchSat::d_pendingScopes
private

Scope parameter for lemmas waiting to be translated since last call to getNewClauses()

Definition at line 97 of file search_sat.h.

CDO<unsigned> CVC3::SearchSat::d_pendingLemmasSize
private

Backtracking size of d_pendingLemmas.

Definition at line 100 of file search_sat.h.

CDO<unsigned> CVC3::SearchSat::d_pendingLemmasNext
private

Backtracking next item in d_pendingLemmas.

Definition at line 103 of file search_sat.h.

CDO<unsigned> CVC3::SearchSat::d_lemmasNext
private

Current position in d_lemmas.

Definition at line 106 of file search_sat.h.

std::vector<unsigned> CVC3::SearchSat::d_varsUndoList
private

List for backtracking var values.

Definition at line 109 of file search_sat.h.

Referenced by setValue().

CDO<unsigned> CVC3::SearchSat::d_varsUndoListSize
private

Backtracking size of d_varsUndoList.

Definition at line 112 of file search_sat.h.

Referenced by setValue().

std::set<LitPriorityPair> CVC3::SearchSat::d_prioritySet
private

Used to determine order to find splitters.

Definition at line 131 of file search_sat.h.

Referenced by SearchSat().

CDO<std::set<LitPriorityPair>::const_iterator> CVC3::SearchSat::d_prioritySetStart
private

Current position in prioritySet.

Definition at line 133 of file search_sat.h.

Referenced by SearchSat().

CDO<unsigned> CVC3::SearchSat::d_prioritySetEntriesSize
private

Backtracking size of priority set entries.

Definition at line 135 of file search_sat.h.

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 137 of file search_sat.h.

std::vector<unsigned> CVC3::SearchSat::d_prioritySetBottomEntriesSizeStack
private

Backtracking size of priority set entries at bottom scope.

Definition at line 139 of file search_sat.h.

unsigned CVC3::SearchSat::d_prioritySetBottomEntriesSize
private

Current size of bottom entries.

Definition at line 141 of file search_sat.h.

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 143 of file search_sat.h.

CDO<unsigned> CVC3::SearchSat::d_lastRegisteredVar
private

Last Var registered with core theory.

Definition at line 146 of file search_sat.h.

CDO<bool> CVC3::SearchSat::d_dplltReady
private

Whether it's OK to call DPLLT solver from the current scope.

Definition at line 149 of file search_sat.h.

CDO<unsigned> CVC3::SearchSat::d_nextImpliedLiteral
private

Definition at line 151 of file search_sat.h.

Referenced by getImpliedLiteral().

Restorer CVC3::SearchSat::d_restorer
private

Instance of Restorer class.

Definition at line 168 of file search_sat.h.


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