#include <sat_api.h>
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) |
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
virtual SatSolver::~SatSolver |
( |
| ) |
|
|
inlinevirtual |
Member Function Documentation
virtual int SatSolver::NumVariables |
( |
| ) |
|
|
pure virtual |
virtual Var SatSolver::AddVariables |
( |
int |
nvars | ) |
|
|
pure virtual |
Var SatSolver::AddVariable |
( |
| ) |
|
|
inline |
virtual Var SatSolver::GetVar |
( |
int |
varIndex | ) |
|
|
pure virtual |
virtual int SatSolver::GetVarIndex |
( |
Var |
v | ) |
|
|
pure virtual |
virtual Var SatSolver::GetFirstVar |
( |
| ) |
|
|
pure virtual |
virtual Var SatSolver::GetNextVar |
( |
Var |
var | ) |
|
|
pure virtual |
virtual Lit SatSolver::MakeLit |
( |
Var |
var, |
|
|
int |
phase |
|
) |
| |
|
pure virtual |
virtual Var SatSolver::GetVarFromLit |
( |
Lit |
lit | ) |
|
|
pure virtual |
virtual int SatSolver::GetPhaseFromLit |
( |
Lit |
lit | ) |
|
|
pure virtual |
virtual int SatSolver::NumClauses |
( |
| ) |
|
|
pure virtual |
virtual Clause SatSolver::AddClause |
( |
std::vector< Lit > & |
lits | ) |
|
|
pure virtual |
virtual bool SatSolver::DeleteClause |
( |
Clause |
clause | ) |
|
|
inlinevirtual |
virtual Clause SatSolver::GetClause |
( |
int |
clauseIndex | ) |
|
|
pure virtual |
virtual Clause SatSolver::GetFirstClause |
( |
| ) |
|
|
pure virtual |
virtual void SatSolver::GetClauseLits |
( |
Clause |
clause, |
|
|
std::vector< Lit > * |
lits |
|
) |
| |
|
pure virtual |
virtual SATStatus SatSolver::Satisfiable |
( |
bool |
allowNewClauses = false | ) |
|
|
pure virtual |
virtual int SatSolver::GetVarAssignment |
( |
Var |
var | ) |
|
|
pure virtual |
virtual void SatSolver::Restart |
( |
| ) |
|
|
pure virtual |
virtual void SatSolver::Reset |
( |
| ) |
|
|
pure virtual |
virtual void SatSolver::RegisterDLevelHook |
( |
void(*)(void *, int) |
f, |
|
|
void * |
cookie |
|
) |
| |
|
pure virtual |
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 |
virtual void SatSolver::RegisterDeductionHook |
( |
void(*)(void *) |
f, |
|
|
void * |
cookie |
|
) |
| |
|
pure virtual |
virtual bool SatSolver::SetBudget |
( |
int |
budget | ) |
|
|
inlinevirtual |
virtual bool SatSolver::SetMemLimit |
( |
int |
mem_limit | ) |
|
|
inlinevirtual |
virtual bool SatSolver::SetRandomness |
( |
int |
n | ) |
|
|
inlinevirtual |
virtual bool SatSolver::SetRandSeed |
( |
int |
seed | ) |
|
|
inlinevirtual |
virtual bool SatSolver::EnableClauseDeletion |
( |
| ) |
|
|
inlinevirtual |
virtual bool SatSolver::DisableClauseDeletion |
( |
| ) |
|
|
inlinevirtual |
virtual int SatSolver::GetBudgetUsed |
( |
| ) |
|
|
inlinevirtual |
virtual int SatSolver::GetMemUsed |
( |
| ) |
|
|
inlinevirtual |
virtual int SatSolver::GetNumDecisions |
( |
| ) |
|
|
inlinevirtual |
virtual int SatSolver::GetNumConflicts |
( |
| ) |
|
|
inlinevirtual |
virtual int SatSolver::GetNumExtConflicts |
( |
| ) |
|
|
inlinevirtual |
virtual float SatSolver::GetTotalTime |
( |
| ) |
|
|
inlinevirtual |
virtual float SatSolver::GetSATTime |
( |
| ) |
|
|
inlinevirtual |
virtual int SatSolver::GetNumLiterals |
( |
| ) |
|
|
inlinevirtual |
virtual int SatSolver::GetNumDeletedClauses |
( |
| ) |
|
|
inlinevirtual |
virtual int SatSolver::GetNumDeletedLiterals |
( |
| ) |
|
|
inlinevirtual |
virtual int SatSolver::GetNumImplications |
( |
| ) |
|
|
inlinevirtual |
virtual int SatSolver::GetMaxDLevel |
( |
| ) |
|
|
inlinevirtual |
void SatSolver::PrintStatistics |
( |
std::ostream & |
os = std::cout | ) |
|
The documentation for this class was generated from the following files: