CVCL::SearchSat Class Reference
[Search Engine]

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

#include <search_sat.h>

Inheritance diagram for CVCL::SearchSat:

[legend]Collaboration diagram for CVCL::SearchSat:

[legend]List of all members.

Public Member Functions

SearchSat (TheoryCore *core)
Constructor.
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 Theorem checkValid (const Expr &e)
Checks the validity of a formula in the current context.
virtual Theorem restart (const Expr &e)
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, int scope=-1)
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.

Private Member Functions

void restoreDPLLT ()
Tell DPLLT object to go back to state before last satisfiable check.
void addLemma (const Theorem &thm)
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::Clause &c, 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::Clause &c)
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.
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.
Theorem check (const Expr &e, bool isRestart=false)
Main checking procedure shared by checkValid and restart.

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.
std::vector< SmartCDO< 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.
CDO< unsigned > d_lemmasNext
Current position in d_lemmas.
CDList< SAT::Lit > d_rootLits
Vector of CNF literals which represent Exprs with no fanouts.
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 SearchSatTheoryAPI
class SearchSatDecider

Classes

class Restorer

Detailed Description

Search engine that connects to a generic SAT reasoning module.

Definition at line 46 of file search_sat.h.

Constructor & Destructor Documentation

SearchSat::SearchSat ( TheoryCore * core )

Constructor.

Definition at line 594 of file search_sat.cpp.
References d_cnfManager, d_coreSatAPI, d_decider, d_dpllt, d_theoryAPI, CVCL::TheoryCore::getTM(), CVCL::TheoryCore::registerCoreSatAPI(), SearchSatCoreSatAPI, SearchSatDecider, and SearchSatTheoryAPI.

SearchSat::~SearchSat ( ) [virtual]

Destructor.

Definition at line 623 of file search_sat.cpp.
References d_cnfManager, d_coreSatAPI, d_decider, d_dpllt, and d_theoryAPI.

Member Function Documentation

void CVCL::SearchSat::restoreDPLLT ( ) [inline, private]

Tell DPLLT object to go back to state before last satisfiable check.

Definition at line 131 of file search_sat.h.
References d_dpllt, and SAT::DPLLT::returnFromSat().
Referenced by CVCL::SearchSat::Restorer::notifyPre().

void SearchSat::addLemma ( const Theorem & thm ) [private]

Core theory callback which adds a new lemma from the core theory.

Definition at line 75 of file search_sat.cpp.
References SAT::CNF_Manager::addLemma(), SAT::CNF_Manager::concreteLit(), d_cnfManager, CVCL::SearchEngine::d_core, d_lastRegisteredVar, d_lemmas, d_rootLits, d_vars, CVCL::TheoryCore::getCM(), CVCL::ContextManager::getCurrentContext(), CVCL::Theorem::getExpr(), CVCL::Expr::isAbsAtomicFormula(), CVCL::Expr::isAbsLiteral(), CVCL::Expr::isNull(), SAT::CNF_Manager::numVars(), SAT::CD_CNF_Formula::numVars(), CVCL::CDList< T >::push_back(), CVCL::TheoryCore::registerAtom(), and SAT::Var::UNKNOWN.
Referenced by CVCL::SearchSatCoreSatAPI::addLemma().

int CVCL::SearchSat::getBottomScope ( ) [inline, private]

Core theory callback which asks for the bottom scope for current query.

Definition at line 137 of file search_sat.h.
References d_bottomScope.
Referenced by CVCL::SearchSatCoreSatAPI::getBottomScope(), and CVCL::SearchSat::Restorer::notifyPre().

void SearchSat::addSplitter ( const Expr & e,

int priority

) [private]

Core theory callback which suggests a splitter.

Definition at line 102 of file search_sat.cpp.
Referenced by CVCL::SearchSatCoreSatAPI::addSplitter().

void SearchSat::assertLit ( SAT::Lit l ) [private]

DPLLT callback to inform theory that a literal has been assigned.

Definition at line 110 of file search_sat.cpp.
References CVCL::TheoryCore::addFact(), CVCL::CommonProofRules::assumpRule(), SAT::CNF_Manager::concreteLit(), d_cnfManager, CVCL::SearchEngine::d_commonRules, CVCL::SearchEngine::d_core, d_inCheckSat, d_intAssumptions, CVCL::FALSE, SAT::Lit::getVar(), CVCL::Expr::isAbsLiteral(), CVCL::Expr::isIntAssumption(), CVCL::Expr::isNull(), SAT::Lit::isPositive(), CVCL::Expr::isUserAssumption(), CVCL::CDList< T >::push_back(), CVCL::Expr::setIntAssumption(), setValue(), and CVCL::TRUE.
Referenced by CVCL::SearchSatTheoryAPI::assertLit().

SAT::DPLLT::ConsistentResult CVCL::SearchSat::checkConsistent ( SAT::Clause & c,

bool fullEffort

) [private]

DPLLT callback to ask if theory has detected inconsistency.

Referenced by CVCL::SearchSatTheoryAPI::checkConsistent().

Lit SearchSat::getImplication ( ) [private]

DPLLT callback to get theory propagations.

Definition at line 145 of file search_sat.cpp.
References d_cnfManager, CVCL::SearchEngine::d_core, d_inCheckSat, d_theorems, SAT::CNF_Manager::getCNFLit(), CVCL::Theorem::getExpr(), CVCL::TheoryCore::getImpliedLiteral(), getValue(), CVCL::CDMap< Key, Data, HashFcn >::insert(), SAT::Lit::isNull(), CVCL::Theorem::isNull(), CVCL::Expr::isUserRegisteredAtom(), SAT::Lit::reset(), CVCL::TRUE, and CVCL::Expr::unnegate().
Referenced by CVCL::SearchSatTheoryAPI::getImplication().

void CVCL::SearchSat::getExplanation ( SAT::Lit l,

SAT::Clause & c

) [private]

DPLLT callback to explain a theory propagation.

Referenced by CVCL::SearchSatTheoryAPI::getExplanation().

bool SearchSat::getNewClauses ( SAT::CNF_Formula & cnf ) [private]

DPLLT callback to get more general theory clauses.

Definition at line 176 of file search_sat.cpp.
References d_inCheckSat, d_lemmas, d_lemmasNext, and SAT::CD_CNF_Formula::numClauses().
Referenced by CVCL::SearchSatTheoryAPI::getNewClauses().

Lit SearchSat::makeDecision ( ) [private]

DPLLT callback to decide which literal to split on next.

Definition at line 188 of file search_sat.cpp.
References CVCL::CDList< T >::begin(), d_inCheckSat, d_rootLits, CVCL::CDList< T >::end(), findSplitterRec(), and getValue().
Referenced by CVCL::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 202 of file search_sat.cpp.
References CVCL::AND, checkJustified(), SAT::CNF_Manager::concreteLit(), d_cnfManager, std::endl(), CVCL::FALSE, SAT::CNF_Manager::getFanin(), CVCL::Expr::getKind(), getValue(), SAT::Lit::getVar(), CVCL::IFF, CVCL::IMPLIES, CVCL::Expr::isAbsAtomicFormula(), SAT::Lit::isFalse(), SAT::Lit::isInverted(), SAT::Lit::isTrue(), SAT::Lit::isVar(), CVCL::ITE, SAT::CNF_Manager::numFanins(), CVCL::OR, setJustified(), CVCL::TRUE, UNKNOWN, and CVCL::XOR.
Referenced by makeDecision().

SAT::Var::Val CVCL::SearchSat::getValue ( SAT::Lit c ) [inline, private]

Get the value of a CNF Literal.

Definition at line 167 of file search_sat.h.
References d_vars, SAT::Var::FALSE, SAT::Lit::getVar(), SAT::Var::invertValue(), SAT::Lit::isFalse(), SAT::Lit::isInverted(), SAT::Lit::isTrue(), SAT::Lit::isVar(), and SAT::Var::TRUE.
Referenced by findSplitterRec(), getImplication(), and makeDecision().

void CVCL::SearchSat::setValue ( SAT::Var v,

SAT::Var::Val val

) [inline, private]

Set the value of a variable.

Definition at line 175 of file search_sat.h.
References d_vars, and SAT::Var::isNull().
Referenced by assertLit().

bool CVCL::SearchSat::checkJustified ( SAT::Var v ) [inline, private]

Check whether this variable's value is justified.

Definition at line 181 of file search_sat.h.
References SAT::CNF_Manager::concreteLit(), d_cnfManager, and CVCL::Expr::isJustified().
Referenced by findSplitterRec().

void CVCL::SearchSat::setJustified ( SAT::Var v ) [inline, private]

Mark this variable as justified.

Definition at line 185 of file search_sat.h.
References SAT::CNF_Manager::concreteLit(), d_cnfManager, and CVCL::Expr::setJustified().
Referenced by findSplitterRec().

Theorem SearchSat::check ( const Expr & e,

bool isRestart = false

) [private]

Main checking procedure shared by checkValid and restart.

Definition at line 473 of file search_sat.cpp.
References SAT::CNF_Manager::addAssumption(), CVCL::CommonProofRules::assumpRule(), SAT::DPLLT::checkSat(), SAT::CNF_Manager::concreteLit(), SAT::DPLLT::continueCheck(), d_bottomScope, d_cnfManager, CVCL::SearchEngine::d_commonRules, CVCL::SearchEngine::d_core, d_dpllt, d_dplltReady, d_idxUserAssump, d_inCheckSat, d_lastCheck, d_lastRegisteredVar, d_lastValid, d_lemmas, d_lemmasNext, d_rootLits, d_userAssumptions, d_vars, CVCL::CDO< T >::get(), CVCL::TheoryCore::getCM(), CVCL::ContextManager::getCurrentContext(), CVCL::Theorem::getExpr(), CVCL::TheoryCore::getExprTrans(), CVCL::Expr::getType(), CVCL::Expr::isAbsAtomicFormula(), CVCL::Expr::isAbsLiteral(), CVCL::Type::isBool(), CVCL::Expr::isBoolConst(), CVCL::Expr::isFalse(), CVCL::Expr::isNot(), CVCL::Expr::isNull(), CVCL::Expr::isTrue(), CVCL::Expr::isUserAssumption(), newUserAssumption(), SAT::CD_CNF_Formula::numClauses(), SAT::CNF_Manager::numVars(), SAT::CNF_Formula_Impl::numVars(), CVCL::ContextManager::pop(), CVCL::ContextManager::popto(), CVCL::ExprTransform::preprocess(), CVCL::ContextManager::push(), CVCL::CDList< T >::push_back(), CVCL::TheoryCore::registerAtom(), CVCL::ContextManager::scopeLevel(), CVCL::CDO< T >::set(), SAT::CNF_Manager::setBottomScope(), CVCL::CDList< T >::size(), CVCL::Type::toString(), CVCL::Expr::toString(), CVCL::TRACE, CVCL::CommonProofRules::trueTheorem(), SAT::Var::UNKNOWN, and CVCL::Expr::unnegate().
Referenced by checkValid(), and restart().

virtual const std::string& CVCL::SearchSat::getName ( ) [inline, virtual]

Name of this search engine.

Implements CVCL::SearchEngine.
Definition at line 200 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 CVCL::SearchEngine.
Definition at line 633 of file search_sat.cpp.
References CVCL::SearchEngine::d_core, CVCL::TheoryCore::registerAtom(), and CVCL::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 CVCL::SearchEngine.
Definition at line 640 of file search_sat.cpp.
References CVCL::SearchEngine::d_core, d_nextImpliedLiteral, CVCL::Theorem::getExpr(), CVCL::TheoryCore::getImpliedLiteralByIndex(), CVCL::Expr::isUserRegisteredAtom(), and CVCL::Expr::unnegate().

virtual Theorem CVCL::SearchSat::checkValid ( const Expr & e ) [inline, virtual]

Checks the validity of a formula in the current context.
If the query is valid, it returns a theorem and the scope and context should be the same as when called. If the query is invalid, it returns a NULL theorem and the context will be one which falsifies the query.
Implements CVCL::SearchEngine.
Definition at line 203 of file search_sat.h.
References check().

virtual Theorem CVCL::SearchSat::restart ( const Expr & e ) [inline, virtual]

Reruns last check with e as an additional assumption.
This method should only be called after a query which is invalid.
Implements CVCL::SearchEngine.
Definition at line 204 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 is invalid.
Implements CVCL::SearchEngine.
Definition at line 652 of file search_sat.cpp.
References d_bottomScope, CVCL::SearchEngine::d_core, CVCL::TheoryCore::getCM(), CVCL::ContextManager::pop(), and CVCL::ContextManager::popto().

virtual Theorem CVCL::SearchSat::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 206 of file search_sat.h.
References d_lastValid.

Theorem SearchSat::newUserAssumption ( const Expr & e,

int scope = -1

) [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 CVCL::SearchEngine.
Definition at line 663 of file search_sat.cpp.
References CVCL::TheoryCore::addFact(), CVCL::CommonProofRules::assumpRule(), CVCL::SearchEngine::d_commonRules, CVCL::SearchEngine::d_core, d_inCheckSat, d_userAssumptions, CVCL::TheoryCore::getCM(), CVCL::Theorem::getExpr(), CVCL::Expr::isAbsLiteral(), isAssumption(), CVCL::CDList< T >::push_back(), CVCL::ContextManager::scopeLevel(), and CVCL::Expr::setUserAssumption().
Referenced by CVCL::SearchSatCoreSatAPI::addAssumption(), and check().

virtual void CVCL::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:

assumptions should be empty on entry.

Implements CVCL::SearchEngine.

virtual void CVCL::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:

assumptions should be empty on entry.

Implements CVCL::SearchEngine.

virtual void CVCL::SearchSat::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.

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

Check if the formula has already been assumed previously.

Implements CVCL::SearchEngine.
Definition at line 726 of file search_sat.cpp.
References CVCL::Expr::isIntAssumption(), and CVCL::Expr::isUserAssumption().
Referenced by newUserAssumption().

virtual void CVCL::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 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.

Proof SearchSat::getProof ( ) [virtual]

Returns the proof term for the last proven query.
It should be called only after a valid query. In any other case, it returns Null.
Implements CVCL::SearchEngine.
Definition at line 741 of file search_sat.cpp.

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

friend class SearchSatCoreSatAPI [friend]

Definition at line 133 of file search_sat.h.
Referenced by SearchSat().

friend class SearchSatTheoryAPI [friend]

Definition at line 141 of file search_sat.h.
Referenced by SearchSat().

friend class SearchSatDecider [friend]

Definition at line 153 of file search_sat.h.
Referenced by SearchSat().

Member Data Documentation

std::string CVCL::SearchSat::d_name [private]

Name of search engine.

Definition at line 49 of file search_sat.h.
Referenced by getName().

CDO<int> CVCL::SearchSat::d_bottomScope [private]

Bottom scope for current query.

Definition at line 52 of file search_sat.h.
Referenced by check(), getBottomScope(), and returnFromCheck().

CDO<Expr> CVCL::SearchSat::d_lastCheck [private]

Last expr checked for validity.

Definition at line 55 of file search_sat.h.
Referenced by check().

CDO<Theorem> CVCL::SearchSat::d_lastValid [private]

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

Definition at line 59 of file search_sat.h.
Referenced by check(), and lastThm().

CDList<Theorem> CVCL::SearchSat::d_userAssumptions [private]

List of all user assumptions.

Definition at line 62 of file search_sat.h.
Referenced by check(), and newUserAssumption().

CDList<Theorem> CVCL::SearchSat::d_intAssumptions [private]

List of all internal assumptions.

Definition at line 65 of file search_sat.h.
Referenced by assertLit().

CDO<unsigned> CVCL::SearchSat::d_idxUserAssump [private]

Index to where unprocessed assumptions start.

Definition at line 68 of file search_sat.h.
Referenced by check().

TheoryCore::CoreSatAPI* CVCL::SearchSat::d_coreSatAPI [private]

Definition at line 70 of file search_sat.h.
Referenced by SearchSat(), and ~SearchSat().

SAT::DPLLT* CVCL::SearchSat::d_dpllt [private]

Pointer to DPLLT implementation.

Definition at line 73 of file search_sat.h.
Referenced by check(), restoreDPLLT(), SearchSat(), and ~SearchSat().

SAT::DPLLT::TheoryAPI* CVCL::SearchSat::d_theoryAPI [private]

Implementation of TheoryAPI for DPLLT.

Definition at line 76 of file search_sat.h.
Referenced by SearchSat(), and ~SearchSat().

SAT::DPLLT::Decider* CVCL::SearchSat::d_decider [private]

Implementation of Decider for DPLLT.

Definition at line 79 of file search_sat.h.
Referenced by SearchSat(), and ~SearchSat().

CDMap<Expr, Theorem> CVCL::SearchSat::d_theorems [private]

Store of theorems for expressions sent to DPLLT.

Definition at line 82 of file search_sat.h.
Referenced by getImplication().

SAT::CNF_Manager* CVCL::SearchSat::d_cnfManager [private]

Manages CNF formula and its relationship to original Exprs and Theorems.

Definition at line 85 of file search_sat.h.
Referenced by addLemma(), assertLit(), check(), checkJustified(), findSplitterRec(), getImplication(), SearchSat(), setJustified(), and ~SearchSat().

std::vector<SmartCDO<SAT::Var::Val> > CVCL::SearchSat::d_vars [private]

Cached values of variables.

Definition at line 88 of file search_sat.h.
Referenced by addLemma(), check(), getValue(), and setValue().

bool CVCL::SearchSat::d_inCheckSat [private]

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

Definition at line 91 of file search_sat.h.
Referenced by assertLit(), check(), getImplication(), getNewClauses(), makeDecision(), newUserAssumption(), and CVCL::SearchSat::Restorer::notifyPre().

SAT::CD_CNF_Formula CVCL::SearchSat::d_lemmas [private]

CNF Formula used for theory lemmas.

Definition at line 94 of file search_sat.h.
Referenced by addLemma(), check(), and getNewClauses().

CDO<unsigned> CVCL::SearchSat::d_lemmasNext [private]

Current position in d_lemmas.

Definition at line 97 of file search_sat.h.
Referenced by check(), and getNewClauses().

CDList<SAT::Lit> CVCL::SearchSat::d_rootLits [private]

Vector of CNF literals which represent Exprs with no fanouts.

Definition at line 100 of file search_sat.h.
Referenced by addLemma(), check(), and makeDecision().

CDO<unsigned> CVCL::SearchSat::d_lastRegisteredVar [private]

Last Var registered with core theory.

Definition at line 103 of file search_sat.h.
Referenced by addLemma(), and check().

CDO<bool> CVCL::SearchSat::d_dplltReady [private]

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

Definition at line 106 of file search_sat.h.
Referenced by check().

CDO<unsigned> CVCL::SearchSat::d_nextImpliedLiteral [private]

Definition at line 108 of file search_sat.h.
Referenced by getImpliedLiteral().

Restorer CVCL::SearchSat::d_restorer [private]

Instance of Restorer class.

Definition at line 126 of file search_sat.h.

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

Generated on Thu Apr 13 16:57:43 2006 for CVC Lite by

1.4.4

CVCL::SearchSat Class Reference [Search Engine]