SatSolver Class Reference

#include <sat_api.h>

List of all members.

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 ()

Classes

• union Clause
• union Lit
• union Var

---

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

---