SatSolver Class Reference

#include <sat_api.h>

Inheritance diagram for SatSolver:

[legend]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]

Implemented in Xchaff.

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]

Implemented in Xchaff.

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]

Implemented in Xchaff.

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]

Implemented in Xchaff.

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]

Implemented in Xchaff.

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]

Implemented in Xchaff.

virtual Clause SatSolver::GetFirstClause ( ) [pure virtual]

Implemented in Xchaff.

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]

Implemented in Xchaff.

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]

Implemented in Xchaff.

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

virtual void SatSolver::Restart ( ) [pure virtual]

Implemented in Xchaff.

virtual void SatSolver::Reset ( ) [pure virtual]

Implemented in Xchaff.

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

Implemented in Xchaff.

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]`

Implemented in Xchaff.

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

virtual bool SatSolver::SetBudget ( int budget ) [inline, virtual]

Reimplemented in Xchaff.

Definition at line 218 of file sat_api.h.

virtual bool SatSolver::SetMemLimit ( int mem_limit ) [inline, virtual]

Reimplemented in Xchaff.

Definition at line 221 of file sat_api.h.

virtual bool SatSolver::SetRandomness ( int n ) [inline, virtual]

Reimplemented in Xchaff.

Definition at line 225 of file sat_api.h.

virtual bool SatSolver::SetRandSeed ( int seed ) [inline, virtual]

Reimplemented in Xchaff.

Definition at line 226 of file sat_api.h.

virtual bool SatSolver::EnableClauseDeletion ( ) [inline, virtual]

Reimplemented in Xchaff.

Definition at line 229 of file sat_api.h.

virtual bool SatSolver::DisableClauseDeletion ( ) [inline, virtual]

Reimplemented in Xchaff.

Definition at line 230 of file sat_api.h.

virtual int SatSolver::GetBudgetUsed ( ) [inline, virtual]

Reimplemented in Xchaff.

Definition at line 243 of file sat_api.h.

Referenced by PrintStatistics().

virtual int SatSolver::GetMemUsed ( ) [inline, virtual]

Reimplemented in Xchaff.

Definition at line 246 of file sat_api.h.

Referenced by PrintStatistics().

virtual int SatSolver::GetNumDecisions ( ) [inline, virtual]

Reimplemented in Xchaff.

Definition at line 249 of file sat_api.h.

Referenced by PrintStatistics().

virtual int SatSolver::GetNumConflicts ( ) [inline, virtual]

Reimplemented in Xchaff.

Definition at line 252 of file sat_api.h.

Referenced by PrintStatistics().

virtual int SatSolver::GetNumExtConflicts ( ) [inline, virtual]

Reimplemented in Xchaff.

Definition at line 256 of file sat_api.h.

Referenced by PrintStatistics().

virtual float SatSolver::GetTotalTime ( ) [inline, virtual]

Reimplemented in Xchaff.

Definition at line 259 of file sat_api.h.

Referenced by PrintStatistics().

virtual float SatSolver::GetSATTime ( ) [inline, virtual]

Reimplemented in Xchaff.

Definition at line 263 of file sat_api.h.

Referenced by PrintStatistics().

virtual int SatSolver::GetNumLiterals ( ) [inline, virtual]

Reimplemented in Xchaff.

Definition at line 266 of file sat_api.h.

Referenced by PrintStatistics().

virtual int SatSolver::GetNumDeletedClauses ( ) [inline, virtual]

Reimplemented in Xchaff.

Definition at line 269 of file sat_api.h.

Referenced by PrintStatistics().

virtual int SatSolver::GetNumDeletedLiterals ( ) [inline, virtual]

Reimplemented in Xchaff.

Definition at line 272 of file sat_api.h.

Referenced by PrintStatistics().

virtual int SatSolver::GetNumImplications ( ) [inline, virtual]

Reimplemented in Xchaff.

Definition at line 275 of file sat_api.h.

Referenced by PrintStatistics().

virtual int SatSolver::GetMaxDLevel ( ) [inline, virtual]

Reimplemented in Xchaff.

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:

Generated on Tue Jul 3 14:35:24 2007 for CVC3 by

1.5.1