CVC3
2.4.1
|
#include <sat_api.h>
typedef enum SatSolver::SATStatus SatSolver::SATStatus |
enum SatSolver::SATStatus |
SatSolver::SatSolver | ( | ) | [inline] |
virtual SatSolver::~SatSolver | ( | ) | [inline, virtual] |
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(), and SAT::DPLLTBasic::checkSat().
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] |
Implemented in Xchaff.
Referenced by SAT::DPLLTBasic::checkSat(), SAT::DPLLTBasic::cvc2SAT(), and SAT::DPLLTBasic::getValue().
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] |
Referenced by SAT::DPLLTBasic::SAT2cvc().
virtual int SatSolver::GetPhaseFromLit | ( | Lit | lit | ) | [pure virtual] |
Referenced by SAT::DPLLTBasic::SAT2cvc().
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::addNewClauses().
virtual bool SatSolver::DeleteClause | ( | Clause | clause | ) | [inline, virtual] |
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 | ) | [inline, virtual] |
virtual bool SatSolver::SetMemLimit | ( | int | mem_limit | ) | [inline, virtual] |
virtual bool SatSolver::SetRandomness | ( | int | n | ) | [inline, virtual] |
virtual bool SatSolver::SetRandSeed | ( | int | seed | ) | [inline, virtual] |
virtual bool SatSolver::EnableClauseDeletion | ( | ) | [inline, virtual] |
virtual bool SatSolver::DisableClauseDeletion | ( | ) | [inline, virtual] |
virtual int SatSolver::GetBudgetUsed | ( | ) | [inline, virtual] |
virtual int SatSolver::GetMemUsed | ( | ) | [inline, virtual] |
virtual int SatSolver::GetNumDecisions | ( | ) | [inline, virtual] |
virtual int SatSolver::GetNumConflicts | ( | ) | [inline, virtual] |
virtual int SatSolver::GetNumExtConflicts | ( | ) | [inline, virtual] |
virtual float SatSolver::GetTotalTime | ( | ) | [inline, virtual] |
virtual float SatSolver::GetSATTime | ( | ) | [inline, virtual] |
virtual int SatSolver::GetNumLiterals | ( | ) | [inline, virtual] |
virtual int SatSolver::GetNumDeletedClauses | ( | ) | [inline, virtual] |
virtual int SatSolver::GetNumDeletedLiterals | ( | ) | [inline, virtual] |
virtual int SatSolver::GetNumImplications | ( | ) | [inline, virtual] |
virtual int SatSolver::GetMaxDLevel | ( | ) | [inline, virtual] |
void SatSolver::PrintStatistics | ( | std::ostream & | os = std::cout | ) |
Definition at line 21 of file sat_api.cpp.
References std::endl().