Open
Graph Drawing
Framework

 v. 2023.09 (Elderberry)
 

Minisat::Internal::Solver Member List

This is the complete list of members for Minisat::Internal::Solver, 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::Solverinline
addClause(Lit p)Minisat::Internal::Solverinline
addClause(Lit p, Lit q)Minisat::Internal::Solverinline
addClause(Lit p, Lit q, Lit r)Minisat::Internal::Solverinline
addClause_(vec< Lit > &ps)Minisat::Internal::Solver
addEmptyClause()Minisat::Internal::Solverinline
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
asynch_interruptMinisat::Internal::Solverprotected
attachClause(CRef cr)Minisat::Internal::Solverprotected
budgetOff()Minisat::Internal::Solverinline
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
clausesMinisat::Internal::Solverprotected
clauses_literalsMinisat::Internal::Solver
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
enqueue(Lit p, CRef from=CRef_Undef)Minisat::Internal::Solverinlineprotected
garbage_fracMinisat::Internal::Solver
garbageCollect()Minisat::Internal::Solvervirtual
insertVarOrder(Var x)Minisat::Internal::Solverinlineprotected
interrupt()Minisat::Internal::Solverinline
irand(double &seed, int size)Minisat::Internal::Solverinlineprotectedstatic
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
mkVarData(CRef cr, int l)Minisat::Internal::Solverinlineprotectedstatic
modelMinisat::Internal::Solver
modelValue(Var x) constMinisat::Internal::Solverinline
modelValue(Lit p) constMinisat::Internal::Solverinline
nAssigns() constMinisat::Internal::Solverinline
nClauses() constMinisat::Internal::Solverinline
newDecisionLevel()Minisat::Internal::Solverinlineprotected
newVar(bool polarity=true, bool dvar=true)Minisat::Internal::Solver
nFreeVars() constMinisat::Internal::Solverinline
nLearnts() constMinisat::Internal::Solverinline
nVars() constMinisat::Internal::Solverinline
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::Solverprotected
remove_satisfiedMinisat::Internal::Solverprotected
removeClause(CRef cr)Minisat::Internal::Solverprotected
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
setPolarity(Var v, bool b)Minisat::Internal::Solverinline
setPropBudget(int64_t x)Minisat::Internal::Solverinline
simpDB_assignsMinisat::Internal::Solverprotected
simpDB_propsMinisat::Internal::Solverprotected
simplify()Minisat::Internal::Solver
solve(const vec< Lit > &assumps)Minisat::Internal::Solverinline
solve()Minisat::Internal::Solverinline
solve(double t, SolverStatus &st)Minisat::Internal::Solverinline
solve(Lit p)Minisat::Internal::Solverinline
solve(Lit p, Lit q)Minisat::Internal::Solverinline
solve(Lit p, Lit q, Lit r)Minisat::Internal::Solverinline
solve_()Minisat::Internal::Solverprotected
solve_(double &t)Minisat::Internal::Solverprotected
solveLimited(const vec< Lit > &assumps)Minisat::Internal::Solverinline
Solver()Minisat::Internal::Solver
solvesMinisat::Internal::Solver
startsMinisat::Internal::Solver
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
trailMinisat::Internal::Solverprotected
trail_limMinisat::Internal::Solverprotected
uncheckedEnqueue(Lit p, CRef from=CRef_Undef)Minisat::Internal::Solverprotected
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
~Solver()Minisat::Internal::Solvervirtual