SatSolver Class Reference

#include <sat_api.h>

Inheritance diagram for SatSolver:

[legend]List of all members.

Public Types

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

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 14 of file xchaff.cpp.
Referenced by SAT::DPLLTBasic::createManager().

virtual int SatSolver::NumVariables ( ) [pure virtual]

Implemented in Xchaff.
Referenced by SAT::DPLLTBasic::addNewClause(), SAT::DPLLTBasic::generate_CDB(), and SAT::DPLLTBasic::handle_result().

virtual Var SatSolver::AddVariables ( int nvars ) [pure virtual]

Implemented in Xchaff.
Referenced by 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::cvcl2SAT(), SAT::DPLLTBasic::getValue(), and SAT::DPLLTBasic::handle_result().

virtual int SatSolver::GetVarIndex ( Var v ) [pure virtual]

Referenced by SAT::DPLLTBasic::SAT2cvcl(), 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::cvcl2SAT().

virtual Var SatSolver::GetVarFromLit ( Lit lit ) [pure virtual]

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

virtual int SatSolver::GetPhaseFromLit ( Lit lit ) [pure virtual]

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

virtual int SatSolver::NumClauses ( ) [pure virtual]

Implemented in Xchaff.

virtual Clause SatSolver::AddClause ( std::vector< Lit > & lits ) [pure virtual]

Referenced by SAT::DPLLTBasic::addNewClause(), 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(), SAT::DPLLTBasic::handle_result(), 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.

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

Reimplemented in Xchaff.
Definition at line 246 of file sat_api.h.

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

Reimplemented in Xchaff.
Definition at line 249 of file sat_api.h.

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

Reimplemented in Xchaff.
Definition at line 252 of file sat_api.h.

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

Reimplemented in Xchaff.
Definition at line 256 of file sat_api.h.

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

Reimplemented in Xchaff.
Definition at line 259 of file sat_api.h.

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

Reimplemented in Xchaff.
Definition at line 263 of file sat_api.h.

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

Reimplemented in Xchaff.
Definition at line 266 of file sat_api.h.

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

Reimplemented in Xchaff.
Definition at line 269 of file sat_api.h.

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

Reimplemented in Xchaff.
Definition at line 272 of file sat_api.h.

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

Reimplemented in Xchaff.
Definition at line 275 of file sat_api.h.

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

Reimplemented in Xchaff.
Definition at line 278 of file sat_api.h.

void SatSolver::PrintStatistics ( std::ostream & os = std::cout )

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

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

Generated on Thu Apr 13 16:57:37 2006 for CVC Lite by

1.4.4