CVC3  2.4.1
Public Member Functions | Protected Member Functions | Protected Attributes
SAT::DPLLTMiniSat Class Reference

#include <dpllt_minisat.h>

Inheritance diagram for SAT::DPLLTMiniSat:
SAT::DPLLT

List of all members.

Public Member Functions

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

Protected Member Functions

MiniSat::SolvergetActiveSolver ()
void pushSolver ()
CVC3::QueryResult search ()

Protected Attributes

bool d_printStats
bool d_createProof
SatProofd_proof
std::stack< MiniSat::Solver * > d_solvers
- Protected Attributes inherited from SAT::DPLLT
TheoryAPId_theoryAPI
Deciderd_decider

Additional Inherited Members

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

Detailed Description

Definition at line 40 of file dpllt_minisat.h.


Constructor & Destructor Documentation

DPLLTMiniSat::DPLLTMiniSat ( TheoryAPI theoryAPI,
Decider decider,
bool  printStats = false,
bool  createProof = false 
)

Definition at line 34 of file dpllt_minisat.cpp.

References pushSolver().

DPLLTMiniSat::~DPLLTMiniSat ( )
virtual

Definition at line 41 of file dpllt_minisat.cpp.

References d_proof, and d_solvers.


Member Function Documentation

MiniSat::Solver * DPLLTMiniSat::getActiveSolver ( )
protected
void DPLLTMiniSat::pushSolver ( )
protected
QueryResult DPLLTMiniSat::search ( )
protected
QueryResult DPLLTMiniSat::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 131 of file dpllt_minisat.cpp.

References MiniSat::Solver::addFormula(), d_solvers, SAT::DPLLT::d_theoryAPI, DebugAssert, MiniSat::Solver::doPops(), getActiveSolver(), SAT::DPLLT::TheoryAPI::push(), pushSolver(), and search().

QueryResult DPLLTMiniSat::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 154 of file dpllt_minisat.cpp.

References MiniSat::Solver::addFormula(), d_solvers, DebugAssert, MiniSat::Solver::doPops(), getActiveSolver(), MiniSat::Solver::inPush(), and search().

void DPLLTMiniSat::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 179 of file dpllt_minisat.cpp.

References SAT::DPLLT::d_theoryAPI, MiniSat::Solver::doPops(), getActiveSolver(), SAT::DPLLT::TheoryAPI::push(), MiniSat::Solver::push(), and pushSolver().

void DPLLTMiniSat::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 192 of file dpllt_minisat.cpp.

References d_solvers, SAT::DPLLT::d_theoryAPI, DebugAssert, getActiveSolver(), MiniSat::Solver::inPush(), SAT::DPLLT::TheoryAPI::pop(), and MiniSat::Solver::requestPop().

void DPLLTMiniSat::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 223 of file dpllt_minisat.cpp.

References MiniSat::Solver::addFormula(), SAT::DPLLT::TheoryAPI::assertLit(), SAT::CNF_Formula::begin(), SAT::DPLLT::d_theoryAPI, MiniSat::Solver::doPops(), SAT::CNF_Formula::end(), getActiveSolver(), MiniSat::Solver::isConsistent(), and pushSolver().

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

Implements SAT::DPLLT.

Definition at line 215 of file dpllt_minisat.cpp.

References MiniSat::Solver::curAssigns(), and getActiveSolver().

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

Implements SAT::DPLLT.

Definition at line 219 of file dpllt_minisat.cpp.

References MiniSat::Solver::curClauses(), and getActiveSolver().

Var::Val DPLLTMiniSat::getValue ( Var  v)
virtual

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

Implements SAT::DPLLT.

Definition at line 244 of file dpllt_minisat.cpp.

References MiniSat::cvcToMiniSat(), d_solvers, DebugAssert, CVC3::FALSE_VAL, getActiveSolver(), MiniSat::Solver::getValue(), MiniSat::l_False, MiniSat::l_True, CVC3::TRUE_VAL, and UNKNOWN.

SatProof* SAT::DPLLTMiniSat::getProof ( )
inline

Definition at line 99 of file dpllt_minisat.h.

References d_proof, and DebugAssert.

Referenced by getSatProof().

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

Get the proof from SAT engine.

Implements SAT::DPLLT.

Definition at line 378 of file dpllt_minisat.cpp.

References generateSatProof(), getProof(), SAT::SatProof::getRoot(), and CVC3::TheoryCore::getTM().


Member Data Documentation

bool SAT::DPLLTMiniSat::d_printStats
protected

Definition at line 47 of file dpllt_minisat.h.

Referenced by search().

bool SAT::DPLLTMiniSat::d_createProof
protected

Definition at line 52 of file dpllt_minisat.h.

Referenced by pushSolver(), and search().

SatProof* SAT::DPLLTMiniSat::d_proof
protected

Definition at line 55 of file dpllt_minisat.h.

Referenced by getProof(), search(), and ~DPLLTMiniSat().

std::stack<MiniSat::Solver*> SAT::DPLLTMiniSat::d_solvers
protected

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