| _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 | [inline, virtual] |
| BUDGET_EXCEEDED enum value | SatSolver | |
| 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)=0 | SatSolver | [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)=0 | SatSolver | [pure virtual] |
| GetNextVar(Var var) | Xchaff | [inline] |
| SatSolver::GetNextVar(Var var)=0 | SatSolver | [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)=0 | SatSolver | [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)=0 | SatSolver | [pure virtual] |
| GetVarFromLit(Lit lit) | Xchaff | [inline] |
| SatSolver::GetVarFromLit(Lit lit)=0 | SatSolver | [pure virtual] |
| GetVarIndex(Var v) | Xchaff | [inline] |
| SatSolver::GetVarIndex(Var v)=0 | SatSolver | [pure virtual] |
| MakeLit(Var var, int phase) | Xchaff | [inline] |
| SatSolver::MakeLit(Var var, int phase)=0 | SatSolver | [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 value | SatSolver | |
| 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)=0 | SatSolver | [pure virtual] |
| 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 | [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 value | SatSolver | |
| SatSolver() | SatSolver | [inline] |
| SATStatus enum name | SatSolver | |
| SATStatus typedef | SatSolver | |
| 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 value | SatSolver | |
| UNSATISFIABLE enum value | SatSolver | |
| Xchaff() | Xchaff | [inline] |
| ~SatSolver() | SatSolver | [inline, virtual] |
| ~Xchaff() | Xchaff | [inline] |
