CVC3
2.4.1
|
This is the complete list of members for Xchaff, including all inherited members.
_assignment_hook | Xchaff | private |
_assignment_hook_cookie | Xchaff | private |
_decision_hook | Xchaff | private |
_decision_hook_cookie | Xchaff | private |
_solver | Xchaff | private |
AddClause(std::vector< Lit > &lits) | Xchaff | inline |
SatSolver::AddClause(std::vector< Lit > &lits)=0 | SatSolver | pure virtual |
AddVariable() | SatSolver | inline |
AddVariables(int nvars) | Xchaff | inlinevirtual |
BUDGET_EXCEEDED enum value | SatSolver | |
Continue() | Xchaff | virtual |
Create() | SatSolver | static |
DeleteClause(Clause clause) | SatSolver | inlinevirtual |
DisableClauseDeletion() | Xchaff | inlinevirtual |
EnableClauseDeletion() | Xchaff | inlinevirtual |
GetBudgetUsed() | Xchaff | inlinevirtual |
GetClause(int clauseIndex) | Xchaff | virtual |
GetClauseLits(SatSolver::Clause clause, std::vector< Lit > *lits) | Xchaff | |
SatSolver::GetClauseLits(Clause clause, std::vector< Lit > *lits)=0 | SatSolver | pure virtual |
GetFirstClause() | Xchaff | inlinevirtual |
GetFirstVar() | Xchaff | inlinevirtual |
GetMaxDLevel() | Xchaff | inlinevirtual |
GetMemUsed() | Xchaff | inlinevirtual |
GetNextClause(Clause clause) | Xchaff | inlinevirtual |
GetNextVar(Var var) | Xchaff | inlinevirtual |
GetNumConflicts() | Xchaff | inlinevirtual |
GetNumDecisions() | Xchaff | inlinevirtual |
GetNumDeletedClauses() | Xchaff | inlinevirtual |
GetNumDeletedLiterals() | Xchaff | inlinevirtual |
GetNumExtConflicts() | Xchaff | inlinevirtual |
GetNumImplications() | Xchaff | inlinevirtual |
GetNumLiterals() | Xchaff | inlinevirtual |
GetPhaseFromLit(Lit lit) | Xchaff | inline |
SatSolver::GetPhaseFromLit(Lit lit)=0 | SatSolver | pure virtual |
GetSATTime() | Xchaff | inlinevirtual |
GetTotalTime() | Xchaff | inlinevirtual |
GetVar(int varIndex) | Xchaff | inlinevirtual |
GetVarAssignment(Var var) | Xchaff | inlinevirtual |
GetVarFromLit(Lit lit) | Xchaff | inline |
SatSolver::GetVarFromLit(Lit lit)=0 | SatSolver | pure virtual |
GetVarIndex(Var v) | Xchaff | inlinevirtual |
MakeLit(Var var, int phase) | Xchaff | inlinevirtual |
mkClause(int id) | Xchaff | inlineprivatestatic |
mkLit(int id) | Xchaff | inlineprivatestatic |
mkVar(int id) | Xchaff | inlineprivatestatic |
NumClauses() | Xchaff | inlinevirtual |
NumVariables() | Xchaff | inlinevirtual |
OUT_OF_MEMORY enum value | SatSolver | |
PrintStatistics(std::ostream &os=std::cout) | SatSolver | |
RegisterAssignmentHook(void(*f)(void *, Var, int), void *cookie) | Xchaff | inlinevirtual |
RegisterDecisionHook(Lit(*f)(void *, bool *), void *cookie) | Xchaff | inline |
SatSolver::RegisterDecisionHook(Lit(*f)(void *, bool *), void *cookie)=0 | SatSolver | pure virtual |
RegisterDeductionHook(void(*f)(void *), void *cookie) | Xchaff | inlinevirtual |
RegisterDLevelHook(void(*f)(void *, int), void *cookie) | Xchaff | inlinevirtual |
Reset() | Xchaff | inlinevirtual |
Restart() | Xchaff | inlinevirtual |
Satisfiable(bool allowNewClauses) | Xchaff | virtual |
SATISFIABLE enum value | SatSolver | |
SatSolver() | SatSolver | inline |
SATStatus enum name | SatSolver | |
SATStatus typedef | SatSolver | |
SetBudget(int budget) | Xchaff | inlinevirtual |
SetMemLimit(int mem_limit) | Xchaff | inlinevirtual |
SetRandomness(int n) | Xchaff | inlinevirtual |
SetRandSeed(int seed) | Xchaff | inlinevirtual |
TranslateAssignmentHook(void *cookie, int var, int value) | Xchaff | inlinestatic |
TranslateDecisionHook(void *cookie, bool *done) | Xchaff | inlinestatic |
UNKNOWN enum value | SatSolver | |
UNSATISFIABLE enum value | SatSolver | |
Xchaff() | Xchaff | inline |
~SatSolver() | SatSolver | inlinevirtual |
~Xchaff() | Xchaff | inline |