SatSolver Member List
This is the complete list of members for
SatSolver, including all inherited members.
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] |