CVC3
|
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 | inlinevirtual |
DisableClauseDeletion() | SatSolver | inlinevirtual |
EnableClauseDeletion() | SatSolver | inlinevirtual |
GetBudgetUsed() | SatSolver | inlinevirtual |
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 | inlinevirtual |
GetMemUsed() | SatSolver | inlinevirtual |
GetNextClause(Clause clause)=0 | SatSolver | pure virtual |
GetNextVar(Var var)=0 | SatSolver | pure virtual |
GetNumConflicts() | SatSolver | inlinevirtual |
GetNumDecisions() | SatSolver | inlinevirtual |
GetNumDeletedClauses() | SatSolver | inlinevirtual |
GetNumDeletedLiterals() | SatSolver | inlinevirtual |
GetNumExtConflicts() | SatSolver | inlinevirtual |
GetNumImplications() | SatSolver | inlinevirtual |
GetNumLiterals() | SatSolver | inlinevirtual |
GetPhaseFromLit(Lit lit)=0 | SatSolver | pure virtual |
GetSATTime() | SatSolver | inlinevirtual |
GetTotalTime() | SatSolver | inlinevirtual |
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 | inlinevirtual |
SetMemLimit(int mem_limit) | SatSolver | inlinevirtual |
SetRandomness(int n) | SatSolver | inlinevirtual |
SetRandSeed(int seed) | SatSolver | inlinevirtual |
UNKNOWN enum value | SatSolver | |
UNSATISFIABLE enum value | SatSolver | |
~SatSolver() | SatSolver | inlinevirtual |