#include <dpllt_minisat.h>
Inheritance diagram for SAT::DPLLTMiniSat:
Definition at line 36 of file dpllt_minisat.h.
| DPLLTMiniSat::DPLLTMiniSat | ( | TheoryAPI * | theoryAPI, | |
| Decider * | decider, | |||
| bool | printStats = false | |||
| ) |
| DPLLTMiniSat::~DPLLTMiniSat | ( | ) | [virtual] |
| MiniSat::Solver * DPLLTMiniSat::getActiveSolver | ( | ) | [protected] |
Definition at line 44 of file dpllt_minisat.cpp.
References d_solvers, and DebugAssert.
Referenced by addAssertion(), checkSat(), continueCheck(), getValue(), pop(), push(), pushSolver(), and search().
| void DPLLTMiniSat::pushSolver | ( | ) | [protected] |
Definition at line 50 of file dpllt_minisat.cpp.
References MiniSat::Solver::createFrom(), SAT::DPLLT::d_decider, d_solvers, SAT::DPLLT::d_theoryAPI, and getActiveSolver().
Referenced by addAssertion(), checkSat(), DPLLTMiniSat(), and push().
| QueryResult DPLLTMiniSat::search | ( | ) | [protected] |
Definition at line 59 of file dpllt_minisat.cpp.
References CVC3::ABORT, d_printStats, d_solvers, SAT::DPLLT::d_theoryAPI, DebugAssert, std::endl(), FatalAssert, getActiveSolver(), MiniSat::Solver::getClauses(), MiniSat::Solver::getLemmas(), MiniSat::Solver::getStats(), MiniSat::Solver::nVars(), SATISFIABLE, MiniSat::Solver::search(), UNKNOWN, and UNSATISFIABLE.
Referenced by checkSat(), and continueCheck().
| 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 117 of file dpllt_minisat.cpp.
References MiniSat::Solver::addFormula(), d_solvers, SAT::DPLLT::d_theoryAPI, DebugAssert, MiniSat::Solver::doPops(), getActiveSolver(), 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 140 of file dpllt_minisat.cpp.
References MiniSat::Solver::addFormula(), d_solvers, DebugAssert, MiniSat::Solver::doPops(), getActiveSolver(), 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 165 of file dpllt_minisat.cpp.
References SAT::DPLLT::d_theoryAPI, MiniSat::Solver::doPops(), getActiveSolver(), 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 178 of file dpllt_minisat.cpp.
References d_solvers, SAT::DPLLT::d_theoryAPI, DebugAssert, getActiveSolver(), 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 202 of file dpllt_minisat.cpp.
References MiniSat::Solver::addFormula(), SAT::CNF_Formula::begin(), SAT::DPLLT::d_theoryAPI, MiniSat::Solver::doPops(), SAT::CNF_Formula::end(), getActiveSolver(), and pushSolver().
Get value of variable: unassigned, false, or true.
Implements SAT::DPLLT.
Definition at line 221 of file dpllt_minisat.cpp.
References MiniSat::cvcToMiniSat(), d_solvers, DebugAssert, SAT::Var::FALSE_VAL, getActiveSolver(), MiniSat::Solver::getValue(), MiniSat::l_False, MiniSat::l_True, SAT::Var::TRUE_VAL, and SAT::Var::UNKNOWN.
bool SAT::DPLLTMiniSat::d_printStats [protected] |
std::stack<MiniSat::Solver*> SAT::DPLLTMiniSat::d_solvers [protected] |
Definition at line 49 of file dpllt_minisat.h.
Referenced by checkSat(), continueCheck(), getActiveSolver(), getValue(), pop(), pushSolver(), search(), and ~DPLLTMiniSat().
1.5.1