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