Open
Graph Drawing
Framework

 v. 2023.09 (Elderberry)
 

Minisat::Internal::SimpSolver Member List

This is the complete list of members for Minisat::Internal::SimpSolver, including all inherited members.

A_FALSE enum valueMinisat::Internal::Solver
A_TRUE enum valueMinisat::Internal::Solver
A_UNDEF enum valueMinisat::Internal::Solver
abstractLevel(Var x) constMinisat::Internal::Solverinlineprotected
activityMinisat::Internal::Solverprotected
add_tmpMinisat::Internal::Solverprotected
addClause(const vec< Lit > &ps)Minisat::Internal::SimpSolverinline
addClause(Lit p)Minisat::Internal::SimpSolverinline
addClause(Lit p, Lit q)Minisat::Internal::SimpSolverinline
addClause(Lit p, Lit q, Lit r)Minisat::Internal::SimpSolverinline
addClause_(vec< Lit > &ps)Minisat::Internal::SimpSolver
addEmptyClause()Minisat::Internal::SimpSolverinline
analyze(CRef confl, vec< Lit > &out_learnt, int &out_btlevel)Minisat::Internal::Solverprotected
analyze_stackMinisat::Internal::Solverprotected
analyze_toclearMinisat::Internal::Solverprotected
analyzeFinal(Lit p, vec< Lit > &out_conflict)Minisat::Internal::Solverprotected
AnswerType enum nameMinisat::Internal::Solver
assignsMinisat::Internal::Solverprotected
assumptionsMinisat::Internal::Solverprotected
asymm(Var v, CRef cr)Minisat::Internal::SimpSolverprotected
asymm_litsMinisat::Internal::SimpSolver
asymmVar(Var v)Minisat::Internal::SimpSolverprotected
asynch_interruptMinisat::Internal::Solverprotected
attachClause(CRef cr)Minisat::Internal::Solverprotected
backwardSubsumptionCheck(bool verbose=false)Minisat::Internal::SimpSolverprotected
budgetOff()Minisat::Internal::Solverinline
bwdsub_assignsMinisat::Internal::SimpSolverprotected
bwdsub_tmpunitMinisat::Internal::SimpSolverprotected
caMinisat::Internal::Solverprotected
cancelUntil(int level)Minisat::Internal::Solverprotected
ccmin_modeMinisat::Internal::Solver
checkGarbage(double gf)Minisat::Internal::Solverinline
checkGarbage()Minisat::Internal::Solverinline
cla_incMinisat::Internal::Solverprotected
claBumpActivity(Clause &c)Minisat::Internal::Solverinlineprotected
claDecayActivity()Minisat::Internal::Solverinlineprotected
clause_decayMinisat::Internal::Solver
clause_limMinisat::Internal::SimpSolver
clausesMinisat::Internal::Solverprotected
clauses_literalsMinisat::Internal::Solver
cleanUpClauses()Minisat::Internal::SimpSolverprotected
clearInterrupt()Minisat::Internal::Solverinline
conflictMinisat::Internal::Solver
conflict_budgetMinisat::Internal::Solverprotected
conflictsMinisat::Internal::Solver
dec_varsMinisat::Internal::Solver
decisionMinisat::Internal::Solverprotected
decisionLevel() constMinisat::Internal::Solverinlineprotected
decisionsMinisat::Internal::Solver
detachClause(CRef cr, bool strict=false)Minisat::Internal::Solverprotected
drand(double &seed)Minisat::Internal::Solverinlineprotectedstatic
elim_heapMinisat::Internal::SimpSolverprotected
elimclausesMinisat::Internal::SimpSolverprotected
eliminate(bool turn_off_elim=false)Minisat::Internal::SimpSolver
eliminatedMinisat::Internal::SimpSolverprotected
eliminated_varsMinisat::Internal::SimpSolver
eliminateVar(Var v)Minisat::Internal::SimpSolverprotected
elimorderMinisat::Internal::SimpSolverprotected
enqueue(Lit p, CRef from=CRef_Undef)Minisat::Internal::Solverinlineprotected
extendModel()Minisat::Internal::SimpSolverprotected
frozenMinisat::Internal::SimpSolverprotected
garbage_fracMinisat::Internal::Solver
garbageCollect() overrideMinisat::Internal::SimpSolvervirtual
gatherTouchedClauses()Minisat::Internal::SimpSolverprotected
growMinisat::Internal::SimpSolver
implied(const vec< Lit > &c)Minisat::Internal::SimpSolverprotected
insertVarOrder(Var x)Minisat::Internal::Solverinlineprotected
interrupt()Minisat::Internal::Solverinline
irand(double &seed, int size)Minisat::Internal::Solverinlineprotectedstatic
isEliminated(Var v) constMinisat::Internal::SimpSolverinline
learntsMinisat::Internal::Solverprotected
learnts_literalsMinisat::Internal::Solver
learntsize_adjust_cntMinisat::Internal::Solverprotected
learntsize_adjust_conflMinisat::Internal::Solverprotected
learntsize_adjust_incMinisat::Internal::Solver
learntsize_adjust_start_conflMinisat::Internal::Solver
learntsize_factorMinisat::Internal::Solver
learntsize_incMinisat::Internal::Solver
level(Var x) constMinisat::Internal::Solverinlineprotected
litRedundant(Lit p, uint32_t abstract_levels)Minisat::Internal::Solverprotected
locked(const Clause &c) constMinisat::Internal::Solverinlineprotected
luby_restartMinisat::Internal::Solver
max_learntsMinisat::Internal::Solverprotected
max_literalsMinisat::Internal::Solver
merge(const Clause &_ps, const Clause &_qs, Var v, vec< Lit > &out_clause)Minisat::Internal::SimpSolverprotected
merge(const Clause &_ps, const Clause &_qs, Var v, int &size)Minisat::Internal::SimpSolverprotected
mergesMinisat::Internal::SimpSolver
mkVarData(CRef cr, int l)Minisat::Internal::Solverinlineprotectedstatic
modelMinisat::Internal::Solver
modelValue(Var x) constMinisat::Internal::Solverinline
modelValue(Lit p) constMinisat::Internal::Solverinline
n_occMinisat::Internal::SimpSolverprotected
n_touchedMinisat::Internal::SimpSolverprotected
nAssigns() constMinisat::Internal::Solverinline
nClauses() constMinisat::Internal::Solverinline
newDecisionLevel()Minisat::Internal::Solverinlineprotected
newVar(bool polarity=true, bool dvar=true)Minisat::Internal::SimpSolver
nFreeVars() constMinisat::Internal::Solverinline
nLearnts() constMinisat::Internal::Solverinline
nVars() constMinisat::Internal::Solverinline
occursMinisat::Internal::SimpSolverprotected
okMinisat::Internal::Solverprotected
okay() constMinisat::Internal::Solverinline
order_heapMinisat::Internal::Solverprotected
phase_savingMinisat::Internal::Solver
pickBranchLit()Minisat::Internal::Solverprotected
polarityMinisat::Internal::Solverprotected
progress_estimateMinisat::Internal::Solverprotected
progressEstimate() constMinisat::Internal::Solverprotected
propagate()Minisat::Internal::Solverprotected
propagation_budgetMinisat::Internal::Solverprotected
propagationsMinisat::Internal::Solver
qheadMinisat::Internal::Solverprotected
random_seedMinisat::Internal::Solver
random_var_freqMinisat::Internal::Solver
reason(Var x) constMinisat::Internal::Solverinlineprotected
rebuildOrderHeap()Minisat::Internal::Solverprotected
reduceDB()Minisat::Internal::Solverprotected
relocAll(ClauseAllocator &to)Minisat::Internal::SimpSolverprotected
remove_satisfiedMinisat::Internal::Solverprotected
removeClause(CRef cr)Minisat::Internal::SimpSolverprotected
removeSatisfied(vec< CRef > &cs)Minisat::Internal::Solverprotected
restart_firstMinisat::Internal::Solver
restart_incMinisat::Internal::Solver
rnd_decisionsMinisat::Internal::Solver
rnd_init_actMinisat::Internal::Solver
rnd_polMinisat::Internal::Solver
satisfied(const Clause &c) constMinisat::Internal::Solverprotected
search(int nof_conflicts)Minisat::Internal::Solverprotected
search(int nof_conflicts, double &time)Minisat::Internal::Solverprotected
seenMinisat::Internal::Solverprotected
setConfBudget(int64_t x)Minisat::Internal::Solverinline
setDecisionVar(Var v, bool b)Minisat::Internal::Solverinline
setFrozen(Var v, bool b)Minisat::Internal::SimpSolverinline
setPolarity(Var v, bool b)Minisat::Internal::Solverinline
setPropBudget(int64_t x)Minisat::Internal::Solverinline
simp_garbage_fracMinisat::Internal::SimpSolver
simpDB_assignsMinisat::Internal::Solverprotected
simpDB_propsMinisat::Internal::Solverprotected
simplify()Minisat::Internal::Solver
SimpSolver()Minisat::Internal::SimpSolver
solve(const vec< Lit > &assumps, bool do_simp=true, bool turn_off_simp=false)Minisat::Internal::SimpSolverinline
solve(bool do_simp=true, bool turn_off_simp=false)Minisat::Internal::SimpSolverinline
solve(Lit p, bool do_simp=true, bool turn_off_simp=false)Minisat::Internal::SimpSolverinline
solve(Lit p, Lit q, bool do_simp=true, bool turn_off_simp=false)Minisat::Internal::SimpSolverinline
solve(Lit p, Lit q, Lit r, bool do_simp=true, bool turn_off_simp=false)Minisat::Internal::SimpSolverinline
Minisat::Internal::Solver::solve(const vec< Lit > &assumps)Minisat::Internal::Solverinline
Minisat::Internal::Solver::solve()Minisat::Internal::Solverinline
Minisat::Internal::Solver::solve(double t, SolverStatus &st)Minisat::Internal::Solverinline
Minisat::Internal::Solver::solve(Lit p)Minisat::Internal::Solverinline
Minisat::Internal::Solver::solve(Lit p, Lit q)Minisat::Internal::Solverinline
Minisat::Internal::Solver::solve(Lit p, Lit q, Lit r)Minisat::Internal::Solverinline
solve_(bool do_simp=true, bool turn_off_simp=false)Minisat::Internal::SimpSolverprotected
Minisat::Internal::Solver::solve_()Minisat::Internal::Solverprotected
Minisat::Internal::Solver::solve_(double &t)Minisat::Internal::Solverprotected
solveLimited(const vec< Lit > &assumps, bool do_simp=true, bool turn_off_simp=false)Minisat::Internal::SimpSolverinline
Minisat::Internal::Solver::solveLimited(const vec< Lit > &assumps)Minisat::Internal::Solverinline
Solver()Minisat::Internal::Solver
solvesMinisat::Internal::Solver
startsMinisat::Internal::Solver
strengthenClause(CRef cr, Lit l)Minisat::Internal::SimpSolverprotected
substitute(Var v, Lit x)Minisat::Internal::SimpSolver
subsumption_limMinisat::Internal::SimpSolver
subsumption_queueMinisat::Internal::SimpSolverprotected
toDimacs(std::ostream &out, const vec< Lit > &assumps)Minisat::Internal::Solver
toDimacs(const char *file, const vec< Lit > &assumps)Minisat::Internal::Solver
toDimacs(std::ostream &out, Clause &c, vec< Var > &map, Var &max)Minisat::Internal::Solver
toDimacs(const char *file)Minisat::Internal::Solverinline
toDimacs(const char *file, Lit p)Minisat::Internal::Solverinline
toDimacs(const char *file, Lit p, Lit q)Minisat::Internal::Solverinline
toDimacs(const char *file, Lit p, Lit q, Lit r)Minisat::Internal::Solverinline
tot_literalsMinisat::Internal::Solver
touchedMinisat::Internal::SimpSolverprotected
trailMinisat::Internal::Solverprotected
trail_limMinisat::Internal::Solverprotected
uncheckedEnqueue(Lit p, CRef from=CRef_Undef)Minisat::Internal::Solverprotected
updateElimHeap(Var v)Minisat::Internal::SimpSolverinlineprotected
use_asymmMinisat::Internal::SimpSolver
use_elimMinisat::Internal::SimpSolver
use_rcheckMinisat::Internal::SimpSolver
use_simplificationMinisat::Internal::SimpSolverprotected
value(Var x) constMinisat::Internal::Solverinline
value(Lit p) constMinisat::Internal::Solverinline
var_decayMinisat::Internal::Solver
var_incMinisat::Internal::Solverprotected
varBumpActivity(Var v, double inc)Minisat::Internal::Solverinlineprotected
varBumpActivity(Var v)Minisat::Internal::Solverinlineprotected
vardataMinisat::Internal::Solverprotected
varDecayActivity()Minisat::Internal::Solverinlineprotected
verbosityMinisat::Internal::Solver
watchesMinisat::Internal::Solverprotected
withinBudget() constMinisat::Internal::Solverinlineprotected
~SimpSolver()Minisat::Internal::SimpSolver
~Solver()Minisat::Internal::Solvervirtual