CVC3
2.4.1
|
#include <dpllt_basic.h>
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) |
SatSolver * | satSolver () |
void | push () |
Set a checkpoint for backtracking. | |
void | pop () |
Restore checkpoint. | |
void | addAssertion (const CNF_Formula &cnf) |
Add new clauses to the SAT solver. | |
virtual std::vector< SAT::Lit > | getCurAssignments () |
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. | |
CVC3::QueryResult | continueCheck (const CNF_Formula &cnf) |
Continue checking the last check with additional constraints. | |
Var::Val | getValue (Var v) |
Get value of variable: unassigned, false, or true. | |
CVC3::Proof | getSatProof (CNF_Manager *, CVC3::TheoryCore *) |
Get the proof from SAT engine. | |
![]() | |
DPLLT (TheoryAPI *theoryAPI, Decider *decider) | |
Constructor. | |
virtual | ~DPLLT () |
TheoryAPI * | theoryAPI () |
Decider * | decider () |
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::ContextManager * | d_cm |
bool | d_ready |
SatSolver * | d_mng |
CNF_Formula_Impl * | d_cnf |
CD_CNF_Formula * | d_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 | |
![]() | |
enum | ConsistentResult { INCONSISTENT, MAYBE_CONSISTENT, CONSISTENT } |
![]() | |
TheoryAPI * | d_theoryAPI |
Decider * | d_decider |
Definition at line 32 of file dpllt_basic.h.
DPLLTBasic::DPLLTBasic | ( | TheoryAPI * | theoryAPI, |
Decider * | decider, | ||
CVC3::ContextManager * | cm, | ||
bool | printStats = false |
||
) |
Definition at line 239 of file dpllt_basic.cpp.
References createManager(), d_assertions, d_cm, d_cnf, and CVC3::ContextManager::getCurrentContext().
|
virtual |
Definition at line 254 of file dpllt_basic.cpp.
References d_assertions, d_assertionsStack, d_cnf, d_cnfStack, d_mng, and d_mngStack.
|
private |
Definition at line 137 of file dpllt_basic.cpp.
References SatSolver::Create(), SATAssignmentHook(), SATDecisionHook(), SATDeductionHook(), and SATDLevelHook().
Referenced by checkSat(), continueCheck(), DPLLTBasic(), and pop().
|
private |
Definition at line 147 of file dpllt_basic.cpp.
References SAT::CNF_Formula_Impl::begin(), SAT::CNF_Formula_Impl::end(), SAT::CNF_Formula_Impl::numVars(), and SAT::CNF_Formula_Impl::simplify().
Referenced by addNewClauses(), checkSat(), and continueCheck().
|
private |
Definition at line 170 of file dpllt_basic.cpp.
References SatSolver::BUDGET_EXCEEDED, std::endl(), SatSolver::OUT_OF_MEMORY, SatSolver::SATISFIABLE, and SatSolver::UNSATISFIABLE.
Referenced by checkSat(), and continueCheck().
|
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 | ) |
Definition at line 275 of file dpllt_basic.cpp.
References SatSolver::AddClause(), SAT::Clause::begin(), cvc2SAT(), d_mng, DebugAssert, SAT::Clause::end(), SAT::Clause::getMaxVar(), SatSolver::NumVariables(), satSolver(), and SAT::Clause::size().
void DPLLTBasic::addNewClauses | ( | CNF_Formula_Impl & | cnf | ) |
Definition at line 289 of file dpllt_basic.cpp.
References SatSolver::AddClause(), SatSolver::AddVariables(), SAT::CNF_Formula_Impl::begin(), cvc2SAT(), d_mng, SAT::CNF_Formula_Impl::end(), generate_CDB(), SatSolver::NumVariables(), SAT::CNF_Formula_Impl::numVars(), and SAT::CNF_Formula_Impl::simplify().
Referenced by SATAssignmentHook(), SATDecisionHook(), and SATDeductionHook().
|
inline |
Definition at line 64 of file dpllt_basic.h.
References d_mng, SAT::Lit::getVar(), SatSolver::GetVar(), SAT::Lit::isNull(), SAT::Lit::isPositive(), and SatSolver::MakeLit().
Referenced by addNewClause(), addNewClauses(), and SATDecisionHook().
|
inline |
Definition at line 68 of file dpllt_basic.h.
References d_mng, SatSolver::GetPhaseFromLit(), SatSolver::GetVarFromLit(), SatSolver::GetVarIndex(), and SatSolver::Lit::IsNull().
|
inline |
Definition at line 73 of file dpllt_basic.h.
References d_mng.
Referenced by addNewClause(), and SATAssignmentHook().
|
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().
|
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().
|
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().
|
virtual |
Implements SAT::DPLLT.
Definition at line 368 of file dpllt_basic.cpp.
|
virtual |
Implements SAT::DPLLT.
Definition at line 373 of file dpllt_basic.cpp.
|
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().
|
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().
Get value of variable: unassigned, false, or true.
Implements SAT::DPLLT.
Definition at line 85 of file dpllt_basic.h.
References d_mng, SatSolver::GetVar(), and SatSolver::GetVarAssignment().
|
virtual |
Get the proof from SAT engine.
Implements SAT::DPLLT.
Definition at line 522 of file dpllt_basic.cpp.
|
private |
Definition at line 34 of file dpllt_basic.h.
Referenced by checkSat(), and DPLLTBasic().
|
private |
Definition at line 36 of file dpllt_basic.h.
Referenced by checkSat(), continueCheck(), pop(), and push().
|
private |
Definition at line 37 of file dpllt_basic.h.
Referenced by addNewClause(), addNewClauses(), checkSat(), continueCheck(), cvc2SAT(), getValue(), pop(), SAT2cvc(), satSolver(), and ~DPLLTBasic().
|
private |
Definition at line 38 of file dpllt_basic.h.
Referenced by checkSat(), continueCheck(), DPLLTBasic(), pop(), and ~DPLLTBasic().
|
private |
Definition at line 39 of file dpllt_basic.h.
Referenced by checkSat(), continueCheck(), DPLLTBasic(), pop(), and ~DPLLTBasic().
|
private |
Definition at line 41 of file dpllt_basic.h.
Referenced by checkSat(), continueCheck(), pop(), push(), and ~DPLLTBasic().
|
private |
Definition at line 42 of file dpllt_basic.h.
Referenced by checkSat(), continueCheck(), pop(), and ~DPLLTBasic().
|
private |
Definition at line 43 of file dpllt_basic.h.
Referenced by checkSat(), pop(), push(), and ~DPLLTBasic().
|
private |
Definition at line 44 of file dpllt_basic.h.
|
private |
Definition at line 46 of file dpllt_basic.h.
|
private |
Definition at line 47 of file dpllt_basic.h.
|
private |
Definition at line 48 of file dpllt_basic.h.
|
private |
Definition at line 49 of file dpllt_basic.h.