SatSolver Class Reference

#include <sat_api.h>

List of all members.

Public Types

Public Member Functions

Static Public Member Functions

Classes


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:
Generated on Wed Nov 18 16:14:15 2009 for CVC3 by  doxygen 1.5.2