CVC3  2.4.1
Public Member Functions | Private Member Functions | Private Attributes | List of all members
SAT::DPLLTBasic Class Reference

#include <dpllt_basic.h>

Inheritance diagram for SAT::DPLLTBasic:
SAT::DPLLT

Public Member Functions

 DPLLTBasic (TheoryAPI *theoryAPI, Decider *decider, CVC3::ContextManager *cm, bool printStats=false)
 
virtual ~DPLLTBasic ()
 
void addNewClause (const Clause &c)
 
void addNewClauses (CNF_Formula_Impl &cnf)
 
SatSolver::Lit cvc2SAT (Lit l)
 
Lit SAT2cvc (SatSolver::Lit l)
 
SatSolversatSolver ()
 
void push ()
 Set a checkpoint for backtracking. More...
 
void pop ()
 Restore checkpoint. More...
 
void addAssertion (const CNF_Formula &cnf)
 Add new clauses to the SAT solver. More...
 
virtual std::vector< SAT::LitgetCurAssignments ()
 
virtual std::vector< std::vector< SAT::Lit > > getCurClauses ()
 
CVC3::QueryResult checkSat (const CNF_Formula &cnf)
 Check the satisfiability of a set of clauses in the current context. More...
 
CVC3::QueryResult continueCheck (const CNF_Formula &cnf)
 Continue checking the last check with additional constraints. More...
 
Var::Val getValue (Var v)
 Get value of variable: unassigned, false, or true. More...
 
CVC3::Proof getSatProof (CNF_Manager *, CVC3::TheoryCore *)
 Get the proof from SAT engine. More...
 
- Public Member Functions inherited from SAT::DPLLT
 DPLLT (TheoryAPI *theoryAPI, Decider *decider)
 Constructor. More...
 
virtual ~DPLLT ()
 
TheoryAPItheoryAPI ()
 
Deciderdecider ()
 
void setDecider (Decider *decider)
 

Private Member Functions

void createManager ()
 
void generate_CDB (CNF_Formula_Impl &cnf)
 
void handle_result (SatSolver::SATStatus outcome)
 
void verify_solution ()
 

Private Attributes

CVC3::ContextManagerd_cm
 
bool d_ready
 
SatSolverd_mng
 
CNF_Formula_Impld_cnf
 
CD_CNF_Formulad_assertions
 
std::vector< SatSolver * > d_mngStack
 
std::vector< CNF_Formula_Impl * > d_cnfStack
 
std::vector< CD_CNF_Formula * > d_assertionsStack
 
bool d_printStats
 
CVC3::CDO< unsigned > d_pushLevel
 
CVC3::CDO< bool > d_readyPrev
 
CVC3::CDO< unsigned > d_prevStackSize
 
CVC3::CDO< unsigned > d_prevAStackSize
 

Additional Inherited Members

- Public Types inherited from SAT::DPLLT
enum  ConsistentResult { INCONSISTENT, MAYBE_CONSISTENT, CONSISTENT }
 
- Protected Attributes inherited from SAT::DPLLT
TheoryAPId_theoryAPI
 
Deciderd_decider
 

Detailed Description

Definition at line 32 of file dpllt_basic.h.

Constructor & Destructor Documentation

DPLLTBasic::DPLLTBasic ( TheoryAPI theoryAPI,
Decider decider,
CVC3::ContextManager cm,
bool  printStats = false 
)
DPLLTBasic::~DPLLTBasic ( )
virtual

Definition at line 254 of file dpllt_basic.cpp.

References d_assertions, d_assertionsStack, d_cnf, d_cnfStack, d_mng, and d_mngStack.

Member Function Documentation

void DPLLTBasic::createManager ( )
private
void DPLLTBasic::generate_CDB ( CNF_Formula_Impl cnf)
private
void DPLLTBasic::handle_result ( SatSolver::SATStatus  outcome)
private
void DPLLTBasic::verify_solution ( )
private

Definition at line 215 of file dpllt_basic.cpp.

References DebugAssert, and SatSolver::Clause::IsNull().

Referenced by checkSat(), and continueCheck().

void DPLLTBasic::addNewClause ( const Clause c)
void DPLLTBasic::addNewClauses ( CNF_Formula_Impl cnf)
SatSolver::Lit SAT::DPLLTBasic::cvc2SAT ( Lit  l)
inline
Lit SAT::DPLLTBasic::SAT2cvc ( SatSolver::Lit  l)
inline
SatSolver* SAT::DPLLTBasic::satSolver ( )
inline

Definition at line 73 of file dpllt_basic.h.

References d_mng.

Referenced by addNewClause(), and SATAssignmentHook().

void DPLLTBasic::push ( )
virtual

Set a checkpoint for backtracking.

This should effectively save the current state of the solver. Note that it should also result in a call to TheoryAPI::push.

Implements SAT::DPLLT.

Definition at line 314 of file dpllt_basic.cpp.

References d_assertionsStack, d_mngStack, d_prevAStackSize, d_prevStackSize, d_pushLevel, d_ready, d_readyPrev, SAT::DPLLT::d_theoryAPI, and SAT::DPLLT::TheoryAPI::push().

void DPLLTBasic::pop ( )
virtual

Restore checkpoint.

This should return the state to what it was immediately before the last call to push. In particular, if one or more calls to checkSat, continueCheck, or addAssertion have been made since the last push, these should be undone. Note also that in this case, a single call to DPLLT::pop may result in multiple calls to TheoryAPI::pop.

Implements SAT::DPLLT.

Definition at line 324 of file dpllt_basic.cpp.

References createManager(), d_assertions, d_assertionsStack, d_cnf, d_cnfStack, d_mng, d_mngStack, d_prevAStackSize, d_prevStackSize, d_pushLevel, d_ready, d_readyPrev, SAT::DPLLT::d_theoryAPI, DebugAssert, and SAT::DPLLT::TheoryAPI::pop().

void DPLLTBasic::addAssertion ( const CNF_Formula cnf)
virtual

Add new clauses to the SAT solver.

This is used to add clauses that form a "context" for the next call to checkSat

Implements SAT::DPLLT.

Definition at line 379 of file dpllt_basic.cpp.

References SAT::DPLLT::TheoryAPI::assertLit(), SAT::CNF_Formula::begin(), SAT::DPLLT::d_theoryAPI, and SAT::CNF_Formula::end().

std::vector< SAT::Lit > DPLLTBasic::getCurAssignments ( )
virtual

Implements SAT::DPLLT.

Definition at line 368 of file dpllt_basic.cpp.

std::vector< std::vector< SAT::Lit > > DPLLTBasic::getCurClauses ( )
virtual

Implements SAT::DPLLT.

Definition at line 373 of file dpllt_basic.cpp.

QueryResult DPLLTBasic::checkSat ( const CNF_Formula cnf)
virtual

Check the satisfiability of a set of clauses in the current context.

If the result is SATISFIABLE, UNKNOWN, or ABORT, the DPLLT engine should remain in the state it is in until pop() is called. If the result is UNSATISFIABLE, the DPLLT engine should return to the state it was in when called. Note that it should be possible to call checkSat multiple times, even if the result is true (each additional call should use the context left by the previous call).

Implements SAT::DPLLT.

Definition at line 396 of file dpllt_basic.cpp.

References CVC3::ABORT, SAT::CNF_Formula::addLiteral(), SatSolver::BUDGET_EXCEEDED, createManager(), d_assertions, d_assertionsStack, d_cm, d_cnf, d_cnfStack, d_mng, d_mngStack, d_ready, SAT::DPLLT::d_theoryAPI, DebugAssert, generate_CDB(), CVC3::ContextManager::getCurrentContext(), SatSolver::GetVar(), SatSolver::GetVarAssignment(), handle_result(), SAT::CNF_Formula_Impl::newClause(), SAT::CD_CNF_Formula::numClauses(), SatSolver::NumVariables(), SAT::DPLLT::TheoryAPI::pop(), SAT::DPLLT::TheoryAPI::push(), SatSolver::SATISFIABLE, SATISFIABLE, SatSolver::Satisfiable(), SAT::DPLLT::theoryAPI(), SatSolver::UNSATISFIABLE, UNSATISFIABLE, and verify_solution().

QueryResult DPLLTBasic::continueCheck ( const CNF_Formula cnf)
virtual

Continue checking the last check with additional constraints.

Should only be called after a previous call to checkSat (or continueCheck) that returned SATISFIABLE. It should add the clauses in cnf to the existing clause database and search for a satisfying assignment. As with checkSat, if the result is not UNSATISFIABLE, the DPLLT engine should remain in the state containing the satisfiable assignment until pop() is called. Similarly, if the result is UNSATISFIABLE, the DPLLT engine should return to the state it was in when checkSat was last called.

Implements SAT::DPLLT.

Definition at line 472 of file dpllt_basic.cpp.

References CVC3::ABORT, SatSolver::BUDGET_EXCEEDED, SatSolver::Continue(), createManager(), d_assertions, d_cnf, d_cnfStack, d_mng, d_mngStack, d_ready, SAT::DPLLT::d_theoryAPI, DebugAssert, generate_CDB(), handle_result(), SAT::CD_CNF_Formula::numClauses(), SAT::DPLLT::TheoryAPI::pop(), SatSolver::SATISFIABLE, SATISFIABLE, SAT::DPLLT::theoryAPI(), SatSolver::UNSATISFIABLE, UNSATISFIABLE, and verify_solution().

Var::Val SAT::DPLLTBasic::getValue ( Var  v)
inlinevirtual

Get value of variable: unassigned, false, or true.

Implements SAT::DPLLT.

Definition at line 85 of file dpllt_basic.h.

References SatSolver::GetVar(), and SatSolver::GetVarAssignment().

CVC3::Proof DPLLTBasic::getSatProof ( CNF_Manager ,
CVC3::TheoryCore  
)
virtual

Get the proof from SAT engine.

Implements SAT::DPLLT.

Definition at line 522 of file dpllt_basic.cpp.

Member Data Documentation

CVC3::ContextManager* SAT::DPLLTBasic::d_cm
private

Definition at line 34 of file dpllt_basic.h.

Referenced by checkSat(), and DPLLTBasic().

bool SAT::DPLLTBasic::d_ready
private

Definition at line 36 of file dpllt_basic.h.

Referenced by checkSat(), continueCheck(), pop(), and push().

SatSolver* SAT::DPLLTBasic::d_mng
private
CNF_Formula_Impl* SAT::DPLLTBasic::d_cnf
private

Definition at line 38 of file dpllt_basic.h.

Referenced by checkSat(), continueCheck(), DPLLTBasic(), pop(), and ~DPLLTBasic().

CD_CNF_Formula* SAT::DPLLTBasic::d_assertions
private

Definition at line 39 of file dpllt_basic.h.

Referenced by checkSat(), continueCheck(), DPLLTBasic(), pop(), and ~DPLLTBasic().

std::vector<SatSolver*> SAT::DPLLTBasic::d_mngStack
private

Definition at line 41 of file dpllt_basic.h.

Referenced by checkSat(), continueCheck(), pop(), push(), and ~DPLLTBasic().

std::vector<CNF_Formula_Impl*> SAT::DPLLTBasic::d_cnfStack
private

Definition at line 42 of file dpllt_basic.h.

Referenced by checkSat(), continueCheck(), pop(), and ~DPLLTBasic().

std::vector<CD_CNF_Formula*> SAT::DPLLTBasic::d_assertionsStack
private

Definition at line 43 of file dpllt_basic.h.

Referenced by checkSat(), pop(), push(), and ~DPLLTBasic().

bool SAT::DPLLTBasic::d_printStats
private

Definition at line 44 of file dpllt_basic.h.

CVC3::CDO<unsigned> SAT::DPLLTBasic::d_pushLevel
private

Definition at line 46 of file dpllt_basic.h.

Referenced by pop(), and push().

CVC3::CDO<bool> SAT::DPLLTBasic::d_readyPrev
private

Definition at line 47 of file dpllt_basic.h.

Referenced by pop(), and push().

CVC3::CDO<unsigned> SAT::DPLLTBasic::d_prevStackSize
private

Definition at line 48 of file dpllt_basic.h.

Referenced by pop(), and push().

CVC3::CDO<unsigned> SAT::DPLLTBasic::d_prevAStackSize
private

Definition at line 49 of file dpllt_basic.h.

Referenced by pop(), and push().


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