SAT::DPLLTBasic Class Reference

#include <dpllt_basic.h>

Inheritance diagram for SAT::DPLLTBasic:

[legend]Collaboration diagram for SAT::DPLLTBasic:

[legend]List of all members.

Public Member Functions

• DPLLTBasic::DPLLTBasic (TheoryAPI *theoryAPI, Decider *decider, bool printStats=false)
• virtual ~DPLLTBasic ()
• bool popScopes (void)
• void addNewClause (const Clause &c)
• void addNewClauses (CNF_Formula_Impl &cnf)
• SatSolver::Lit cvcl2SAT (Lit l)
• Lit SAT2cvcl (SatSolver::Lit l)
• SatSolver * satSolver ()
• Result checkSat (const CNF_Formula &cnf)

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

• Result 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.
  

• void returnFromSat ()

  Return to the state just before the last satisfiable call to checkSat.
  

• void reset (bool popScopes=false)

Private Member Functions

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

Private Attributes

• SatSolver * d_mng
• bool d_ready
• bool d_popScopes
• std::vector< SatSolver * > d_mngStack
• std::vector< CNF_Formula_Impl * > d_cnfStack
• bool d_printStats
• CNF_Formula_Impl * d_cnf

---

Detailed Description

Definition at line 20 of file dpllt_basic.h.

---

Constructor & Destructor Documentation

DPLLTBasic::~DPLLTBasic (   )  [virtual]

Definition at line 217 of file dpllt_basic.cpp. References d_cnf, and d_mng.

---

Member Function Documentation

void DPLLTBasic::createManager (   )  [private]

Definition at line 107 of file dpllt_basic.cpp. References SatSolver::Create(), d_mng, SatSolver::RegisterAssignmentHook(), SatSolver::RegisterDecisionHook(), SatSolver::RegisterDeductionHook(), SatSolver::RegisterDLevelHook(), SATAssignmentHook(), SATDecisionHook(), SATDeductionHook(), and SATDLevelHook(). Referenced by checkSat(), continueCheck(), and returnFromSat().

void DPLLTBasic::generate_CDB (  CNF_Formula_Impl &  cnf  )  [private]

Definition at line 117 of file dpllt_basic.cpp. References SatSolver::AddClause(), SatSolver::AddVariables(), SAT::CNF_Formula_Impl::begin(), SAT::Clause::clear(), cvcl2SAT(), d_mng, SAT::CNF_Formula_Impl::end(), SatSolver::NumVariables(), SAT::CNF_Formula_Impl::numVars(), and SAT::CNF_Formula_Impl::simplify(). Referenced by addNewClauses(), checkSat(), and continueCheck().

void DPLLTBasic::handle_result (  SatSolver::SATStatus  outcome  )  [private]

Definition at line 139 of file dpllt_basic.cpp. References SatSolver::BUDGET_EXCEEDED, d_mng, d_printStats, std::endl(), SatSolver::GetVar(), SatSolver::GetVarAssignment(), SatSolver::NumVariables(), SatSolver::OUT_OF_MEMORY, SatSolver::PrintStatistics(), SatSolver::SATISFIABLE, and SatSolver::UNSATISFIABLE. Referenced by checkSat(), and continueCheck().

void DPLLTBasic::verify_solution (   )  [private]

Definition at line 184 of file dpllt_basic.cpp. References d_mng, SatSolver::GetClauseLits(), SatSolver::GetFirstClause(), SatSolver::GetNextClause(), SatSolver::GetPhaseFromLit(), SatSolver::GetVarAssignment(), and SatSolver::GetVarFromLit(). Referenced by checkSat(), and continueCheck().

SAT::DPLLTBasic::DPLLTBasic::DPLLTBasic (  TheoryAPI *  theoryAPI, Decider *  decider, bool  printStats = false )

bool SAT::DPLLTBasic::popScopes (  void   )  [inline]

Definition at line 40 of file dpllt_basic.h. References d_popScopes. Referenced by SATDLevelHook().

void DPLLTBasic::addNewClause (  const Clause &  c  )

Definition at line 224 of file dpllt_basic.cpp. References SatSolver::AddClause(), SAT::Clause::begin(), cvcl2SAT(), d_mng, SAT::Clause::end(), SAT::Clause::getMaxVar(), SatSolver::NumVariables(), satSolver(), and SAT::Clause::size(). Referenced by SATAssignmentHook(), SATDecisionHook(), and SATDeductionHook().

void DPLLTBasic::addNewClauses (  CNF_Formula_Impl &  cnf  )

Definition at line 238 of file dpllt_basic.cpp. References generate_CDB(). Referenced by SATDecisionHook(), and SATDeductionHook().

SatSolver::Lit SAT::DPLLTBasic::cvcl2SAT (  Lit  l  )  [inline]

Definition at line 45 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(), generate_CDB(), and SATDecisionHook().

Lit SAT::DPLLTBasic::SAT2cvcl (  SatSolver::Lit  l  )  [inline]

Definition at line 49 of file dpllt_basic.h. References d_mng, SatSolver::GetPhaseFromLit(), SatSolver::GetVarFromLit(), SatSolver::GetVarIndex(), and SatSolver::Lit::IsNull().

SatSolver* SAT::DPLLTBasic::satSolver (   )  [inline]

Definition at line 54 of file dpllt_basic.h. References d_mng. Referenced by addNewClause(), and SATAssignmentHook().

DPLLTBasic::Result DPLLTBasic::checkSat (  const CNF_Formula &  cnf  )  [virtual]

Check the satisfiability of a set of clauses in the current context. If the result is SATISFIABLE, the DPLLT engine should remain in the state containing the satisfiable assignment until returnFromSat() is called. If the result is UNSAT or ABORT, 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 245 of file dpllt_basic.cpp. References SAT::DPLLT::ABORT, createManager(), d_cnf, d_cnfStack, d_mng, d_mngStack, d_ready, SAT::DPLLT::d_theoryAPI, generate_CDB(), SatSolver::GetVar(), SatSolver::GetVarAssignment(), handle_result(), SAT::DPLLT::SATISFIABLE, SatSolver::SATISFIABLE, SatSolver::Satisfiable(), SAT::DPLLT::UNSAT, SatSolver::UNSATISFIABLE, and verify_solution().

DPLLTBasic::Result 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 SATISFIABLE, the DPLLT engine should remain in the state containing the satisfiable assignment until returnFromSat() is called. Note that returnFromSat should return to the state just before the last call to checkSat, NOT the last call to continueCheck. Similarly, if the result is UNSAT or ABORT, the DPLLT engine should return to the state it was in when checkSat was last called. Implements SAT::DPLLT. Definition at line 310 of file dpllt_basic.cpp. References SAT::DPLLT::ABORT, SatSolver::Continue(), createManager(), d_cnf, d_cnfStack, d_mng, d_mngStack, d_ready, SAT::DPLLT::d_theoryAPI, generate_CDB(), handle_result(), SAT::DPLLT::SATISFIABLE, SatSolver::SATISFIABLE, SAT::DPLLT::UNSAT, SatSolver::UNSATISFIABLE, and verify_solution().

Var::Val SAT::DPLLTBasic::getValue (  Var  v  )  [inline, virtual]

Get value of variable: unassigned, false, or true. Implements SAT::DPLLT. Definition at line 59 of file dpllt_basic.h. References d_mng, SatSolver::GetVar(), and SatSolver::GetVarAssignment().

void DPLLTBasic::returnFromSat (   )  [virtual]

Return to the state just before the last satisfiable call to checkSat. Each time a call to checkSat returns SATISFIABLE, the resulting assignment is retained. Multiple calls to checkSat can be used to refine assignments, adding additional constraints each time. returnFromSat() returns to the state just before the last call to checkSat which returned SATISFIABLE. Implements SAT::DPLLT. Definition at line 354 of file dpllt_basic.cpp. References createManager(), d_cnf, d_cnfStack, d_mng, d_mngStack, d_popScopes, and d_ready.

void SAT::DPLLTBasic::reset (  bool  popScopes = false  )

---

Member Data Documentation

SatSolver* SAT::DPLLTBasic::d_mng [private]

Definition at line 22 of file dpllt_basic.h. Referenced by addNewClause(), checkSat(), continueCheck(), createManager(), cvcl2SAT(), generate_CDB(), getValue(), handle_result(), returnFromSat(), SAT2cvcl(), satSolver(), verify_solution(), and ~DPLLTBasic().

bool SAT::DPLLTBasic::d_ready [private]

Definition at line 23 of file dpllt_basic.h. Referenced by checkSat(), continueCheck(), and returnFromSat().

bool SAT::DPLLTBasic::d_popScopes [private]

Definition at line 24 of file dpllt_basic.h. Referenced by popScopes(), and returnFromSat().

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

Definition at line 25 of file dpllt_basic.h. Referenced by checkSat(), continueCheck(), and returnFromSat().

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

Definition at line 26 of file dpllt_basic.h. Referenced by checkSat(), continueCheck(), and returnFromSat().

bool SAT::DPLLTBasic::d_printStats [private]

Definition at line 27 of file dpllt_basic.h. Referenced by handle_result().

CNF_Formula_Impl* SAT::DPLLTBasic::d_cnf [private]

Definition at line 28 of file dpllt_basic.h. Referenced by checkSat(), continueCheck(), returnFromSat(), and ~DPLLTBasic().

---

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

• dpllt_basic.h
• dpllt_basic.cpp

---