Xchaff Member List

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

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


Generated on Tue Jul 3 14:35:24 2007 for CVC3 by  doxygen 1.5.1