SAT::DPLLT Class Reference

#include <dpllt.h>

Inheritance diagram for SAT::DPLLT:

[legend]Collaboration diagram for SAT::DPLLT:

[legend]List of all members.

Public Types

• enum Result { UNSAT, SATISFIABLE, ABORT }
• enum ConsistentResult { INCONSISTENT, MAYBE_CONSISTENT, CONSISTENT }

Public Member Functions

• DPLLT (TheoryAPI *theoryAPI, Decider *decider)

  Constructor.
  

• virtual ~DPLLT ()
• TheoryAPI * theoryAPI ()
• Decider * decider ()
• virtual Result checkSat (const CNF_Formula &cnf)=0

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

• virtual Result continueCheck (const CNF_Formula &cnf)=0

  Continue checking the last check with additional constraints.
  

• virtual Var::Val getValue (Var v)=0

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

• virtual void returnFromSat ()=0

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

Protected Attributes

• TheoryAPI * d_theoryAPI
• Decider * d_decider

Classes

• class Decider
• class TheoryAPI

---

Detailed Description

Definition at line 19 of file dpllt.h.

---

Member Enumeration Documentation

enum SAT::DPLLT::Result

Enumerator: UNSAT  SATISFIABLE  ABORT  Definition at line 22 of file dpllt.h.

enum SAT::DPLLT::ConsistentResult

Enumerator: INCONSISTENT  MAYBE_CONSISTENT  CONSISTENT  Definition at line 23 of file dpllt.h.

---

Constructor & Destructor Documentation

SAT::DPLLT::DPLLT (  TheoryAPI *  theoryAPI, Decider *  decider )  [inline]

Constructor. The client constructing DPLLT must provide an implementation of TheoryAPI. It may also optionally provide an implementation of Decider. If decider is NULL, then the DPLLT class must make its own decisions. Definition at line 101 of file dpllt.h.

virtual SAT::DPLLT::~DPLLT (   )  [inline, virtual]

Definition at line 103 of file dpllt.h.

---

Member Function Documentation

TheoryAPI* SAT::DPLLT::theoryAPI (   )  [inline]

Definition at line 105 of file dpllt.h. References d_theoryAPI. Referenced by SATAssignmentHook(), SATDecisionHook(), SATDeductionHook(), and SATDLevelHook().

Decider* SAT::DPLLT::decider (   )  [inline]

Definition at line 106 of file dpllt.h. References d_decider. Referenced by SATDecisionHook().

virtual Result SAT::DPLLT::checkSat (  const CNF_Formula &  cnf  )  [pure 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). Implemented in SAT::DPLLTBasic. Referenced by CVCL::SearchSat::check().

virtual Result SAT::DPLLT::continueCheck (  const CNF_Formula &  cnf  )  [pure 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. Implemented in SAT::DPLLTBasic. Referenced by CVCL::SearchSat::check().

virtual Var::Val SAT::DPLLT::getValue (  Var  v  )  [pure virtual]

Get value of variable: unassigned, false, or true. Implemented in SAT::DPLLTBasic.

virtual void SAT::DPLLT::returnFromSat (   )  [pure 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. Implemented in SAT::DPLLTBasic. Referenced by CVCL::SearchSat::restoreDPLLT().

---

Member Data Documentation

TheoryAPI* SAT::DPLLT::d_theoryAPI [protected]

Definition at line 92 of file dpllt.h. Referenced by SAT::DPLLTBasic::checkSat(), SAT::DPLLTBasic::continueCheck(), and theoryAPI().

Decider* SAT::DPLLT::d_decider [protected]

Definition at line 93 of file dpllt.h. Referenced by decider().

---

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

• dpllt.h

---