|
CVC3
|
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 |
1.8.2