CVC3

SatSolver Member List

This is the complete list of members for SatSolver, including all inherited members.
AddClause(std::vector< Lit > &lits)=0SatSolver [pure virtual]
AddVariable()SatSolver [inline]
AddVariables(int nvars)=0SatSolver [pure virtual]
BUDGET_EXCEEDED enum valueSatSolver
Continue()=0SatSolver [pure virtual]
Create()SatSolver [static]
DeleteClause(Clause clause)SatSolver [inline, virtual]
DisableClauseDeletion()SatSolver [inline, virtual]
EnableClauseDeletion()SatSolver [inline, virtual]
GetBudgetUsed()SatSolver [inline, virtual]
GetClause(int clauseIndex)=0SatSolver [pure virtual]
GetClauseLits(Clause clause, std::vector< Lit > *lits)=0SatSolver [pure virtual]
GetFirstClause()=0SatSolver [pure virtual]
GetFirstVar()=0SatSolver [pure virtual]
GetMaxDLevel()SatSolver [inline, virtual]
GetMemUsed()SatSolver [inline, virtual]
GetNextClause(Clause clause)=0SatSolver [pure virtual]
GetNextVar(Var var)=0SatSolver [pure virtual]
GetNumConflicts()SatSolver [inline, virtual]
GetNumDecisions()SatSolver [inline, virtual]
GetNumDeletedClauses()SatSolver [inline, virtual]
GetNumDeletedLiterals()SatSolver [inline, virtual]
GetNumExtConflicts()SatSolver [inline, virtual]
GetNumImplications()SatSolver [inline, virtual]
GetNumLiterals()SatSolver [inline, virtual]
GetPhaseFromLit(Lit lit)=0SatSolver [pure virtual]
GetSATTime()SatSolver [inline, virtual]
GetTotalTime()SatSolver [inline, virtual]
GetVar(int varIndex)=0SatSolver [pure virtual]
GetVarAssignment(Var var)=0SatSolver [pure virtual]
GetVarFromLit(Lit lit)=0SatSolver [pure virtual]
GetVarIndex(Var v)=0SatSolver [pure virtual]
MakeLit(Var var, int phase)=0SatSolver [pure virtual]
NumClauses()=0SatSolver [pure virtual]
NumVariables()=0SatSolver [pure virtual]
OUT_OF_MEMORY enum valueSatSolver
PrintStatistics(std::ostream &os=std::cout)SatSolver
RegisterAssignmentHook(void(*f)(void *, Var, int), void *cookie)=0SatSolver [pure virtual]
RegisterDecisionHook(Lit(*f)(void *, bool *), void *cookie)=0SatSolver [pure virtual]
RegisterDeductionHook(void(*f)(void *), void *cookie)=0SatSolver [pure virtual]
RegisterDLevelHook(void(*f)(void *, int), void *cookie)=0SatSolver [pure virtual]
Reset()=0SatSolver [pure virtual]
Restart()=0SatSolver [pure virtual]
Satisfiable(bool allowNewClauses=false)=0SatSolver [pure virtual]
SATISFIABLE enum valueSatSolver
SatSolver()SatSolver [inline]
SATStatus enum nameSatSolver
SATStatus typedefSatSolver
SetBudget(int budget)SatSolver [inline, virtual]
SetMemLimit(int mem_limit)SatSolver [inline, virtual]
SetRandomness(int n)SatSolver [inline, virtual]
SetRandSeed(int seed)SatSolver [inline, virtual]
UNKNOWN enum valueSatSolver
UNSATISFIABLE enum valueSatSolver
~SatSolver()SatSolver [inline, virtual]