Open
Graph Drawing
Framework

 v. 2023.09 (Elderberry)
 

Minisat::Formula Member List

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

A_FALSE enum valueMinisat::Internal::Solverprivate
A_TRUE enum valueMinisat::Internal::Solverprivate
A_UNDEF enum valueMinisat::Internal::Solverprivate
abstractLevel(Var x) constMinisat::Internal::Solverinlineprivate
activityMinisat::Internal::Solverprivate
add_tmpMinisat::Internal::Solverprivate
addClause(const Iteratable &literals)Minisat::Formulainline
Minisat::Internal::Solver::addClause(const vec< Lit > &ps)Minisat::Internal::Solverinlineprivate
Minisat::Internal::Solver::addClause(Lit p)Minisat::Internal::Solverinlineprivate
Minisat::Internal::Solver::addClause(Lit p, Lit q)Minisat::Internal::Solverinlineprivate
Minisat::Internal::Solver::addClause(Lit p, Lit q, Lit r)Minisat::Internal::Solverinlineprivate
addClause_(vec< Lit > &ps)Minisat::Internal::Solverprivate
addEmptyClause()Minisat::Internal::Solverinlineprivate
analyze(CRef confl, vec< Lit > &out_learnt, int &out_btlevel)Minisat::Internal::Solverprivate
analyze_stackMinisat::Internal::Solverprivate
analyze_toclearMinisat::Internal::Solverprivate
analyzeFinal(Lit p, vec< Lit > &out_conflict)Minisat::Internal::Solverprivate
AnswerType enum nameMinisat::Internal::Solverprivate
assignsMinisat::Internal::Solverprivate
assumptionsMinisat::Internal::Solverprivate
asynch_interruptMinisat::Internal::Solverprivate
attachClause(CRef cr)Minisat::Internal::Solverprivate
budgetOff()Minisat::Internal::Solverinlineprivate
caMinisat::Internal::Solverprivate
cancelUntil(int level)Minisat::Internal::Solverprivate
ccmin_modeMinisat::Internal::Solverprivate
checkGarbage(double gf)Minisat::Internal::Solverinlineprivate
checkGarbage()Minisat::Internal::Solverinlineprivate
cla_incMinisat::Internal::Solverprivate
claBumpActivity(Clause &c)Minisat::Internal::Solverinlineprivate
claDecayActivity()Minisat::Internal::Solverinlineprivate
clause_decayMinisat::Internal::Solverprivate
clauseAddLiteral(unsigned int clausePos, Internal::Var signedVar)Minisat::Formulainline
clausesMinisat::Internal::Solverprivate
clauses_literalsMinisat::Internal::Solverprivate
clearInterrupt()Minisat::Internal::Solverinlineprivate
conflictMinisat::Internal::Solverprivate
conflict_budgetMinisat::Internal::Solverprivate
conflictsMinisat::Internal::Solverprivate
dec_varsMinisat::Internal::Solverprivate
decisionMinisat::Internal::Solverprivate
decisionLevel() constMinisat::Internal::Solverinlineprivate
decisionsMinisat::Internal::Solverprivate
detachClause(CRef cr, bool strict=false)Minisat::Internal::Solverprivate
drand(double &seed)Minisat::Internal::Solverinlineprivatestatic
enqueue(Lit p, CRef from=CRef_Undef)Minisat::Internal::Solverinlineprivate
finalizeClause(const clause cl)Minisat::Formula
finalizeNotExtensibleClause(const clause cl)Minisat::Formula
Formula()Minisat::Formulainline
free()Minisat::Formulaprivate
garbage_fracMinisat::Internal::Solverprivate
garbageCollect()Minisat::Internal::Solverprivatevirtual
getClause(const int pos)Minisat::Formula
getClauseCount()Minisat::Formulainline
getProblemClauseCount()Minisat::Formulainline
getVarFromLit(const Internal::Lit &lit)Minisat::Formulainline
getVariableCount()Minisat::Formulainline
insertVarOrder(Var x)Minisat::Internal::Solverinlineprivate
interrupt()Minisat::Internal::Solverinlineprivate
irand(double &seed, int size)Minisat::Internal::Solverinlineprivatestatic
learntsMinisat::Internal::Solverprivate
learnts_literalsMinisat::Internal::Solverprivate
learntsize_adjust_cntMinisat::Internal::Solverprivate
learntsize_adjust_conflMinisat::Internal::Solverprivate
learntsize_adjust_incMinisat::Internal::Solverprivate
learntsize_adjust_start_conflMinisat::Internal::Solverprivate
learntsize_factorMinisat::Internal::Solverprivate
learntsize_incMinisat::Internal::Solverprivate
level(Var x) constMinisat::Internal::Solverinlineprivate
litRedundant(Lit p, uint32_t abstract_levels)Minisat::Internal::Solverprivate
locked(const Clause &c) constMinisat::Internal::Solverinlineprivate
luby_restartMinisat::Internal::Solverprivate
m_ClausesMinisat::Formulaprivate
m_messagesMinisat::Formulaprivate
max_learntsMinisat::Internal::Solverprivate
max_literalsMinisat::Internal::Solverprivate
mkVarData(CRef cr, int l)Minisat::Internal::Solverinlineprivatestatic
modelMinisat::Internal::Solverprivate
modelValue(Var x) constMinisat::Internal::Solverinlineprivate
modelValue(Lit p) constMinisat::Internal::Solverinlineprivate
nAssigns() constMinisat::Internal::Solverinlineprivate
nClauses() constMinisat::Internal::Solverinlineprivate
newClause()Minisat::Formula
newDecisionLevel()Minisat::Internal::Solverinlineprivate
newVar()Minisat::Formulainline
Minisat::Internal::Solver::newVar(bool polarity=true, bool dvar=true)Minisat::Internal::Solverprivate
newVars(unsigned int Count)Minisat::Formulainline
nFreeVars() constMinisat::Internal::Solverinlineprivate
nLearnts() constMinisat::Internal::Solverinlineprivate
nVars() constMinisat::Internal::Solverinlineprivate
okMinisat::Internal::Solverprivate
okay() constMinisat::Internal::Solverinlineprivate
order_heapMinisat::Internal::Solverprivate
phase_savingMinisat::Internal::Solverprivate
pickBranchLit()Minisat::Internal::Solverprivate
polarityMinisat::Internal::Solverprivate
progress_estimateMinisat::Internal::Solverprivate
progressEstimate() constMinisat::Internal::Solverprivate
propagate()Minisat::Internal::Solverprivate
propagation_budgetMinisat::Internal::Solverprivate
propagationsMinisat::Internal::Solverprivate
qheadMinisat::Internal::Solverprivate
random_seedMinisat::Internal::Solverprivate
random_var_freqMinisat::Internal::Solverprivate
readDimacs(const char *filename)Minisat::Formula
readDimacs(const string &filename)Minisat::Formula
readDimacs(std::istream &in)Minisat::Formula
reason(Var x) constMinisat::Internal::Solverinlineprivate
rebuildOrderHeap()Minisat::Internal::Solverprivate
reduceDB()Minisat::Internal::Solverprivate
relocAll(ClauseAllocator &to)Minisat::Internal::Solverprivate
remove_satisfiedMinisat::Internal::Solverprivate
removeClause(int i)Minisat::Formula
Minisat::Internal::Solver::removeClause(CRef cr)Minisat::Internal::Solverprivate
removeSatisfied(vec< CRef > &cs)Minisat::Internal::Solverprivate
reset()Minisat::Formula
restart_firstMinisat::Internal::Solverprivate
restart_incMinisat::Internal::Solverprivate
rnd_decisionsMinisat::Internal::Solverprivate
rnd_init_actMinisat::Internal::Solverprivate
rnd_polMinisat::Internal::Solverprivate
satisfied(const Clause &c) constMinisat::Internal::Solverprivate
search(int nof_conflicts)Minisat::Internal::Solverprivate
search(int nof_conflicts, double &time)Minisat::Internal::Solverprivate
seenMinisat::Internal::Solverprivate
setConfBudget(int64_t x)Minisat::Internal::Solverinlineprivate
setDecisionVar(Var v, bool b)Minisat::Internal::Solverinlineprivate
setPolarity(Var v, bool b)Minisat::Internal::Solverinlineprivate
setPropBudget(int64_t x)Minisat::Internal::Solverinlineprivate
simpDB_assignsMinisat::Internal::Solverprivate
simpDB_propsMinisat::Internal::Solverprivate
simplify()Minisat::Internal::Solverprivate
solve(Model &ReturnModel)Minisat::Formula
solve(Model &ReturnModel, double &timeLimit)Minisat::Formula
Minisat::Internal::Solver::solve(const vec< Lit > &assumps)Minisat::Internal::Solverinlineprivate
Minisat::Internal::Solver::solve()Minisat::Internal::Solverinlineprivate
Minisat::Internal::Solver::solve(double t, SolverStatus &st)Minisat::Internal::Solverinlineprivate
Minisat::Internal::Solver::solve(Lit p)Minisat::Internal::Solverinlineprivate
Minisat::Internal::Solver::solve(Lit p, Lit q)Minisat::Internal::Solverinlineprivate
Minisat::Internal::Solver::solve(Lit p, Lit q, Lit r)Minisat::Internal::Solverinlineprivate
solve_()Minisat::Internal::Solverprivate
solve_(double &t)Minisat::Internal::Solverprivate
solveLimited(const vec< Lit > &assumps)Minisat::Internal::Solverinlineprivate
Solver()Minisat::Internal::Solverprivate
solvesMinisat::Internal::Solverprivate
startsMinisat::Internal::Solverprivate
toDimacs(std::ostream &out, const vec< Lit > &assumps)Minisat::Internal::Solverprivate
toDimacs(const char *file, const vec< Lit > &assumps)Minisat::Internal::Solverprivate
toDimacs(std::ostream &out, Clause &c, vec< Var > &map, Var &max)Minisat::Internal::Solverprivate
toDimacs(const char *file)Minisat::Internal::Solverinlineprivate
toDimacs(const char *file, Lit p)Minisat::Internal::Solverinlineprivate
toDimacs(const char *file, Lit p, Lit q)Minisat::Internal::Solverinlineprivate
toDimacs(const char *file, Lit p, Lit q, Lit r)Minisat::Internal::Solverinlineprivate
tot_literalsMinisat::Internal::Solverprivate
trailMinisat::Internal::Solverprivate
trail_limMinisat::Internal::Solverprivate
uncheckedEnqueue(Lit p, CRef from=CRef_Undef)Minisat::Internal::Solverprivate
value(Var x) constMinisat::Internal::Solverinlineprivate
value(Lit p) constMinisat::Internal::Solverinlineprivate
var_decayMinisat::Internal::Solverprivate
var_incMinisat::Internal::Solverprivate
varBumpActivity(Var v, double inc)Minisat::Internal::Solverinlineprivate
varBumpActivity(Var v)Minisat::Internal::Solverinlineprivate
vardataMinisat::Internal::Solverprivate
varDecayActivity()Minisat::Internal::Solverinlineprivate
verbosityMinisat::Internal::Solverprivate
watchesMinisat::Internal::Solverprivate
withinBudget() constMinisat::Internal::Solverinlineprivate
writeDimacs(const char *filename)Minisat::Formula
writeDimacs(const string &filename)Minisat::Formula
writeDimacs(std::ostream &f)Minisat::Formula
~Formula()Minisat::Formulainlinevirtual
~Solver()Minisat::Internal::Solverprivatevirtual