CVC3
Xchaff Member List

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

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