SAT::DPLLT Class Reference

#include <dpllt.h>

Inheritance diagram for SAT::DPLLT:

[legend]

Collaboration diagram for SAT::DPLLT:

[legend]

List of all members.

Classes

• class Decider
• class TheoryAPI

Public Types

• enum ConsistentResult { INCONSISTENT, MAYBE_CONSISTENT, CONSISTENT }

  Public Member Functions

  • DPLLT (TheoryAPI *theoryAPI, Decider *decider)

    Constructor.
    

  • virtual ~DPLLT ()
  • TheoryAPI * theoryAPI ()
  • Decider * decider ()
  • void setDecider (Decider *decider)
  • virtual void push ()=0

    Set a checkpoint for backtracking.
    

  • virtual void pop ()=0

    Restore checkpoint.
    

  • virtual void addAssertion (const CNF_Formula &cnf)=0

    Add new clauses to the SAT solver.
    

  • virtual std::vector< SAT::Lit > getCurAssignments ()=0
  • virtual std::vector
    < std::vector< SAT::Lit > > getCurClauses ()=0
  • virtual CVC3::QueryResult checkSat (const CNF_Formula &cnf)=0

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

  • virtual CVC3::QueryResult 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 CVC3::Proof getSatProof (CNF_Manager *, CVC3::TheoryCore *)=0

    Get the proof from SAT engine.
    

  Protected Attributes

  • TheoryAPI * d_theoryAPI
  • Decider * d_decider

  ---

  Detailed Description

  Definition at line 23 of file dpllt.h.

  ---

  Member Enumeration Documentation

  enum SAT::DPLLT::ConsistentResult

  Enumerator:

  INCONSISTENT
  MAYBE_CONSISTENT
  CONSISTENT

  Definition at line 26 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 113 of file dpllt.h.

  virtual SAT::DPLLT::~DPLLT

  (

  )

  [inline, virtual]

  Definition at line 115 of file dpllt.h.

  ---

  Member Function Documentation

  TheoryAPI* SAT::DPLLT::theoryAPI

  (

  )

  [inline]

  Definition at line 117 of file dpllt.h.

  References d_theoryAPI.

  Referenced by SAT::DPLLTBasic::checkSat(), SAT::DPLLTBasic::continueCheck(), SATAssignmentHook(), SATDecisionHook(), SATDeductionHook(), and SATDLevelHook().

  Decider* SAT::DPLLT::decider

  (

  )

  [inline]

  Definition at line 118 of file dpllt.h.

  References d_decider.

  Referenced by SATDecisionHook().

  void SAT::DPLLT::setDecider

  (

  Decider *

  decider

  )

  [inline]

  Definition at line 120 of file dpllt.h.

  References d_decider.

  virtual void SAT::DPLLT::push

  (

  )

  [pure 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.

  Implemented in SAT::DPLLTBasic, and SAT::DPLLTMiniSat.

  Referenced by CVC3::SearchSat::push().

  virtual void SAT::DPLLT::pop

  (

  )

  [pure 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.

  Implemented in SAT::DPLLTBasic, and SAT::DPLLTMiniSat.

  Referenced by CVC3::SearchSat::pop().

  virtual void SAT::DPLLT::addAssertion

  (

  const CNF_Formula &

  cnf

  )

  [pure virtual]

  Add new clauses to the SAT solver.

  This is used to add clauses that form a "context" for the next call to checkSat

  Implemented in SAT::DPLLTBasic, and SAT::DPLLTMiniSat.

  Referenced by CVC3::SearchSat::newUserAssumption().

  virtual std::vector<SAT::Lit> SAT::DPLLT::getCurAssignments

  (

  )

  [pure virtual]

  Implemented in SAT::DPLLTBasic, and SAT::DPLLTMiniSat.

  Referenced by CVC3::SearchSat::check().

  virtual std::vector<std::vector<SAT::Lit> > SAT::DPLLT::getCurClauses

  (

  )

  [pure virtual]

  Implemented in SAT::DPLLTBasic, and SAT::DPLLTMiniSat.

  Referenced by CVC3::SearchSat::check().

  virtual CVC3::QueryResult 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, 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).

  Implemented in SAT::DPLLTBasic, and SAT::DPLLTMiniSat.

  Referenced by CVC3::SearchSat::check().

  virtual CVC3::QueryResult 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 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.

  Implemented in SAT::DPLLTBasic, and SAT::DPLLTMiniSat.

  Referenced by CVC3::SearchSat::check().

  virtual Var::Val SAT::DPLLT::getValue

  (

  Var

  v

  )

  [pure virtual]

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

  Implemented in SAT::DPLLTBasic, and SAT::DPLLTMiniSat.

  virtual CVC3::Proof SAT::DPLLT::getSatProof	(	CNF_Manager *	,
  		CVC3::TheoryCore *
  	)			[pure virtual]

  Get the proof from SAT engine.

  Implemented in SAT::DPLLTBasic, and SAT::DPLLTMiniSat.

  Referenced by CVC3::SearchSat::check().

  ---

  Member Data Documentation

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

  Definition at line 104 of file dpllt.h.

  Referenced by SAT::DPLLTMiniSat::addAssertion(), SAT::DPLLTBasic::addAssertion(), SAT::DPLLTMiniSat::checkSat(), SAT::DPLLTBasic::checkSat(), SAT::DPLLTBasic::continueCheck(), SAT::DPLLTMiniSat::pop(), SAT::DPLLTBasic::pop(), SAT::DPLLTMiniSat::push(), SAT::DPLLTBasic::push(), SAT::DPLLTMiniSat::pushSolver(), SAT::DPLLTMiniSat::search(), and theoryAPI().

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

  Definition at line 105 of file dpllt.h.

  Referenced by decider(), SAT::DPLLTMiniSat::pushSolver(), and setDecider().

  ---

  The documentation for this class was generated from the following file:
  • dpllt.h