CVC3  2.4.1
SatSolver Member List

This is the complete list of members for SatSolver, including all inherited members.

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