SatSolver Class Reference

#include <sat_api.h>

List of all members.

Classes

• union Clause
• union Lit
• union Var

Public Types

• enum SATStatus {
    UNKNOWN, UNSATISFIABLE, SATISFIABLE, BUDGET_EXCEEDED,
    OUT_OF_MEMORY
  }
• typedef enum SatSolver::SATStatus SATStatus

  Public Member Functions

  • SatSolver ()
  • virtual ~SatSolver ()
  • virtual int NumVariables ()=0
  • virtual Var AddVariables (int nvars)=0
  • Var AddVariable ()
  • virtual Var GetVar (int varIndex)=0
  • virtual int GetVarIndex (Var v)=0
  • virtual Var GetFirstVar ()=0
  • virtual Var GetNextVar (Var var)=0
  • virtual Lit MakeLit (Var var, int phase)=0
  • virtual Var GetVarFromLit (Lit lit)=0
  • virtual int GetPhaseFromLit (Lit lit)=0
  • virtual int NumClauses ()=0
  • virtual Clause AddClause (std::vector< Lit > &lits)=0
  • virtual bool DeleteClause (Clause clause)
  • virtual Clause GetClause (int clauseIndex)=0
  • virtual Clause GetFirstClause ()=0
  • virtual Clause GetNextClause (Clause clause)=0
  • virtual void GetClauseLits (Clause clause, std::vector< Lit > *lits)=0
  • virtual SATStatus Satisfiable (bool allowNewClauses=false)=0
  • virtual int GetVarAssignment (Var var)=0
  • virtual SATStatus Continue ()=0
  • virtual void Restart ()=0
  • virtual void Reset ()=0
  • virtual void RegisterDLevelHook (void(*f)(void *, int), void *cookie)=0
  • virtual void RegisterDecisionHook (Lit(*f)(void *, bool *), void *cookie)=0
  • virtual void RegisterAssignmentHook (void(*f)(void *, Var, int), void *cookie)=0
  • virtual void RegisterDeductionHook (void(*f)(void *), void *cookie)=0
  • virtual bool SetBudget (int budget)
  • virtual bool SetMemLimit (int mem_limit)
  • virtual bool SetRandomness (int n)
  • virtual bool SetRandSeed (int seed)
  • virtual bool EnableClauseDeletion ()
  • virtual bool DisableClauseDeletion ()
  • virtual int GetBudgetUsed ()
  • virtual int GetMemUsed ()
  • virtual int GetNumDecisions ()
  • virtual int GetNumConflicts ()
  • virtual int GetNumExtConflicts ()
  • virtual float GetTotalTime ()
  • virtual float GetSATTime ()
  • virtual int GetNumLiterals ()
  • virtual int GetNumDeletedClauses ()
  • virtual int GetNumDeletedLiterals ()
  • virtual int GetNumImplications ()
  • virtual int GetMaxDLevel ()
  • void PrintStatistics (std::ostream &os=std::cout)

  Static Public Member Functions

  • static SatSolver * Create ()

  ---

  Detailed Description

  Definition at line 24 of file sat_api.h.

  ---

  Member Typedef Documentation

  typedef enum SatSolver::SATStatus SatSolver::SATStatus

  ---

  Member Enumeration Documentation

  enum SatSolver::SATStatus

  Enumerator:

  UNKNOWN
  UNSATISFIABLE
  SATISFIABLE
  BUDGET_EXCEEDED
  OUT_OF_MEMORY

  Definition at line 26 of file sat_api.h.

  ---

  Constructor & Destructor Documentation

  SatSolver::SatSolver

  (

  )

  [inline]

  Definition at line 35 of file sat_api.h.

  virtual SatSolver::~SatSolver

  (

  )

  [inline, virtual]

  Definition at line 36 of file sat_api.h.

  ---

  Member Function Documentation

  SatSolver * SatSolver::Create

  (

  )

  [static]

  Definition at line 15 of file sat_api.cpp.

  Referenced by SAT::DPLLTBasic::createManager().

  virtual int SatSolver::NumVariables

  (

  )

  [pure virtual]

  Referenced by SAT::DPLLTBasic::addNewClause(), SAT::DPLLTBasic::addNewClauses(), SAT::DPLLTBasic::checkSat(), SAT::DPLLTBasic::generate_CDB(), and PrintStatistics().

  virtual Var SatSolver::AddVariables

  (

  int

  nvars

  )

  [pure virtual]

  Referenced by SAT::DPLLTBasic::addNewClauses(), AddVariable(), and SAT::DPLLTBasic::generate_CDB().

  Var SatSolver::AddVariable

  (

  )

  [inline]

  Definition at line 82 of file sat_api.h.

  References AddVariables().

  virtual Var SatSolver::GetVar

  (

  int

  varIndex

  )

  [pure virtual]

  Referenced by SAT::DPLLTBasic::checkSat(), SAT::DPLLTBasic::cvc2SAT(), and SAT::DPLLTBasic::getValue().

  virtual int SatSolver::GetVarIndex

  (

  Var

  v

  )

  [pure virtual]

  Referenced by SAT::DPLLTBasic::SAT2cvc(), and SATAssignmentHook().

  virtual Var SatSolver::GetFirstVar

  (

  )

  [pure virtual]

  virtual Var SatSolver::GetNextVar

  (

  Var

  var

  )

  [pure virtual]

  virtual Lit SatSolver::MakeLit	(	Var	var,
  		int	phase
  	)			[pure virtual]

  Referenced by SAT::DPLLTBasic::cvc2SAT().

  virtual Var SatSolver::GetVarFromLit

  (

  Lit

  lit

  )

  [pure virtual]

  Referenced by SAT::DPLLTBasic::SAT2cvc(), and SAT::DPLLTBasic::verify_solution().

  virtual int SatSolver::GetPhaseFromLit

  (

  Lit

  lit

  )

  [pure virtual]

  Referenced by SAT::DPLLTBasic::SAT2cvc(), and SAT::DPLLTBasic::verify_solution().

  virtual int SatSolver::NumClauses

  (

  )

  [pure virtual]

  Referenced by PrintStatistics().

  virtual Clause SatSolver::AddClause

  (

  std::vector< Lit > &

  lits

  )

  [pure virtual]

  Referenced by SAT::DPLLTBasic::addNewClause(), SAT::DPLLTBasic::addNewClauses(), and SAT::DPLLTBasic::generate_CDB().

  virtual bool SatSolver::DeleteClause

  (

  Clause

  clause

  )

  [inline, virtual]

  Definition at line 123 of file sat_api.h.

  virtual Clause SatSolver::GetClause

  (

  int

  clauseIndex

  )

  [pure virtual]

  virtual Clause SatSolver::GetFirstClause

  (

  )

  [pure virtual]

  Referenced by SAT::DPLLTBasic::verify_solution().

  virtual Clause SatSolver::GetNextClause

  (

  Clause

  clause

  )

  [pure virtual]

  Referenced by SAT::DPLLTBasic::verify_solution().

  virtual void SatSolver::GetClauseLits	(	Clause	clause,
  		std::vector< Lit > *	lits
  	)			[pure virtual]

  Referenced by SAT::DPLLTBasic::verify_solution().

  virtual SATStatus SatSolver::Satisfiable

  (

  bool

  allowNewClauses = false

  )

  [pure virtual]

  Referenced by SAT::DPLLTBasic::checkSat().

  virtual int SatSolver::GetVarAssignment

  (

  Var

  var

  )

  [pure virtual]

  Referenced by SAT::DPLLTBasic::checkSat(), SAT::DPLLTBasic::getValue(), and SAT::DPLLTBasic::verify_solution().

  virtual SATStatus SatSolver::Continue

  (

  )

  [pure virtual]

  Referenced by SAT::DPLLTBasic::continueCheck().

  virtual void SatSolver::Restart

  (

  )

  [pure virtual]

  virtual void SatSolver::Reset

  (

  )

  [pure virtual]

  virtual void SatSolver::RegisterDLevelHook	(	void(*)(void *, int)	f,
  		void *	cookie
  	)			[pure virtual]

  Referenced by SAT::DPLLTBasic::createManager().

  virtual void SatSolver::RegisterDecisionHook	(	Lit(*)(void *, bool *)	f,
  		void *	cookie
  	)			[pure virtual]

  Referenced by SAT::DPLLTBasic::createManager().

  virtual void SatSolver::RegisterAssignmentHook	(	void(*)(void *, Var, int)	f,
  		void *	cookie
  	)			[pure virtual]

  Referenced by SAT::DPLLTBasic::createManager().

  virtual void SatSolver::RegisterDeductionHook	(	void(*)(void *)	f,
  		void *	cookie
  	)			[pure virtual]

  Referenced by SAT::DPLLTBasic::createManager().

  virtual bool SatSolver::SetBudget

  (

  int

  budget

  )

  [inline, virtual]

  Definition at line 218 of file sat_api.h.

  virtual bool SatSolver::SetMemLimit

  (

  int

  mem_limit

  )

  [inline, virtual]

  Definition at line 221 of file sat_api.h.

  virtual bool SatSolver::SetRandomness

  (

  int

  n

  )

  [inline, virtual]

  Definition at line 225 of file sat_api.h.

  virtual bool SatSolver::SetRandSeed

  (

  int

  seed

  )

  [inline, virtual]

  Definition at line 226 of file sat_api.h.

  virtual bool SatSolver::EnableClauseDeletion

  (

  )

  [inline, virtual]

  Definition at line 229 of file sat_api.h.

  virtual bool SatSolver::DisableClauseDeletion

  (

  )

  [inline, virtual]

  Definition at line 230 of file sat_api.h.

  virtual int SatSolver::GetBudgetUsed

  (

  )

  [inline, virtual]

  Definition at line 243 of file sat_api.h.

  Referenced by PrintStatistics().

  virtual int SatSolver::GetMemUsed

  (

  )

  [inline, virtual]

  Definition at line 246 of file sat_api.h.

  Referenced by PrintStatistics().

  virtual int SatSolver::GetNumDecisions

  (

  )

  [inline, virtual]

  Definition at line 249 of file sat_api.h.

  Referenced by PrintStatistics().

  virtual int SatSolver::GetNumConflicts

  (

  )

  [inline, virtual]

  Definition at line 252 of file sat_api.h.

  Referenced by PrintStatistics().

  virtual int SatSolver::GetNumExtConflicts

  (

  )

  [inline, virtual]

  Definition at line 256 of file sat_api.h.

  Referenced by PrintStatistics().

  virtual float SatSolver::GetTotalTime

  (

  )

  [inline, virtual]

  Definition at line 259 of file sat_api.h.

  Referenced by PrintStatistics().

  virtual float SatSolver::GetSATTime

  (

  )

  [inline, virtual]

  Definition at line 263 of file sat_api.h.

  Referenced by PrintStatistics().

  virtual int SatSolver::GetNumLiterals

  (

  )

  [inline, virtual]

  Definition at line 266 of file sat_api.h.

  Referenced by PrintStatistics().

  virtual int SatSolver::GetNumDeletedClauses

  (

  )

  [inline, virtual]

  Definition at line 269 of file sat_api.h.

  Referenced by PrintStatistics().

  virtual int SatSolver::GetNumDeletedLiterals

  (

  )

  [inline, virtual]

  Definition at line 272 of file sat_api.h.

  Referenced by PrintStatistics().

  virtual int SatSolver::GetNumImplications

  (

  )

  [inline, virtual]

  Definition at line 275 of file sat_api.h.

  Referenced by PrintStatistics().

  virtual int SatSolver::GetMaxDLevel

  (

  )

  [inline, virtual]

  Definition at line 278 of file sat_api.h.

  Referenced by PrintStatistics().

  void SatSolver::PrintStatistics

  (

  std::ostream &

  os = std::cout

  )

  Definition at line 21 of file sat_api.cpp.

  References std::endl(), GetBudgetUsed(), GetMaxDLevel(), GetMemUsed(), GetNumConflicts(), GetNumDecisions(), GetNumDeletedClauses(), GetNumDeletedLiterals(), GetNumExtConflicts(), GetNumImplications(), GetNumLiterals(), GetSATTime(), GetTotalTime(), NumClauses(), and NumVariables().

  Referenced by SAT::DPLLTBasic::handle_result().

  ---

  The documentation for this class was generated from the following files:
  • sat_api.h
  • sat_api.cpp