CVC3  2.4.1
Classes | Public Types | Public Member Functions | Static Public Member Functions
SatSolver Class Reference

#include <sat_api.h>

Inheritance diagram for SatSolver:
Xchaff

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

Detailed Description

Definition at line 24 of file sat_api.h.


Member Typedef Documentation


Member Enumeration Documentation

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

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
virtual Var SatSolver::AddVariables ( int  nvars)
pure virtual

Implemented in Xchaff.

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

Var SatSolver::AddVariable ( )
inline

Definition at line 82 of file sat_api.h.

References AddVariables().

virtual Var SatSolver::GetVar ( int  varIndex)
pure virtual
virtual int SatSolver::GetVarIndex ( Var  v)
pure virtual

Implemented in Xchaff.

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

virtual Var SatSolver::GetFirstVar ( )
pure virtual

Implemented in Xchaff.

virtual Var SatSolver::GetNextVar ( Var  var)
pure virtual

Implemented in Xchaff.

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

Implemented in Xchaff.

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

virtual Var SatSolver::GetVarFromLit ( Lit  lit)
pure virtual
virtual int SatSolver::GetPhaseFromLit ( Lit  lit)
pure virtual
virtual int SatSolver::NumClauses ( )
pure virtual

Implemented in Xchaff.

virtual Clause SatSolver::AddClause ( std::vector< Lit > &  lits)
pure virtual
virtual bool SatSolver::DeleteClause ( Clause  clause)
inlinevirtual

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.

virtual Clause SatSolver::GetNextClause ( Clause  clause)
pure virtual

Implemented in Xchaff.

virtual void SatSolver::GetClauseLits ( Clause  clause,
std::vector< Lit > *  lits 
)
pure virtual
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

Implemented in Xchaff.

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

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.

virtual void SatSolver::RegisterDecisionHook ( Lit(*)(void *, bool *)  f,
void *  cookie 
)
pure virtual
virtual void SatSolver::RegisterAssignmentHook ( void(*)(void *, Var, int)  f,
void *  cookie 
)
pure virtual

Implemented in Xchaff.

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

Implemented in Xchaff.

virtual bool SatSolver::SetBudget ( int  budget)
inlinevirtual

Reimplemented in Xchaff.

Definition at line 218 of file sat_api.h.

virtual bool SatSolver::SetMemLimit ( int  mem_limit)
inlinevirtual

Reimplemented in Xchaff.

Definition at line 221 of file sat_api.h.

virtual bool SatSolver::SetRandomness ( int  n)
inlinevirtual

Reimplemented in Xchaff.

Definition at line 225 of file sat_api.h.

virtual bool SatSolver::SetRandSeed ( int  seed)
inlinevirtual

Reimplemented in Xchaff.

Definition at line 226 of file sat_api.h.

virtual bool SatSolver::EnableClauseDeletion ( )
inlinevirtual

Reimplemented in Xchaff.

Definition at line 229 of file sat_api.h.

virtual bool SatSolver::DisableClauseDeletion ( )
inlinevirtual

Reimplemented in Xchaff.

Definition at line 230 of file sat_api.h.

virtual int SatSolver::GetBudgetUsed ( )
inlinevirtual

Reimplemented in Xchaff.

Definition at line 243 of file sat_api.h.

virtual int SatSolver::GetMemUsed ( )
inlinevirtual

Reimplemented in Xchaff.

Definition at line 246 of file sat_api.h.

virtual int SatSolver::GetNumDecisions ( )
inlinevirtual

Reimplemented in Xchaff.

Definition at line 249 of file sat_api.h.

virtual int SatSolver::GetNumConflicts ( )
inlinevirtual

Reimplemented in Xchaff.

Definition at line 252 of file sat_api.h.

virtual int SatSolver::GetNumExtConflicts ( )
inlinevirtual

Reimplemented in Xchaff.

Definition at line 256 of file sat_api.h.

virtual float SatSolver::GetTotalTime ( )
inlinevirtual

Reimplemented in Xchaff.

Definition at line 259 of file sat_api.h.

virtual float SatSolver::GetSATTime ( )
inlinevirtual

Reimplemented in Xchaff.

Definition at line 263 of file sat_api.h.

virtual int SatSolver::GetNumLiterals ( )
inlinevirtual

Reimplemented in Xchaff.

Definition at line 266 of file sat_api.h.

virtual int SatSolver::GetNumDeletedClauses ( )
inlinevirtual

Reimplemented in Xchaff.

Definition at line 269 of file sat_api.h.

virtual int SatSolver::GetNumDeletedLiterals ( )
inlinevirtual

Reimplemented in Xchaff.

Definition at line 272 of file sat_api.h.

virtual int SatSolver::GetNumImplications ( )
inlinevirtual

Reimplemented in Xchaff.

Definition at line 275 of file sat_api.h.

virtual int SatSolver::GetMaxDLevel ( )
inlinevirtual

Reimplemented in Xchaff.

Definition at line 278 of file sat_api.h.

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

Definition at line 21 of file sat_api.cpp.

References std::endl().


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