MiniSat::Solver Member List

This is the complete list of members for MiniSat::Solver, including all inherited members.

addClause(std::vector< Lit > &literals, int clauseID)	MiniSat::Solver	[protected]
addClause(Lit p)	MiniSat::Solver
addClause(const Clause &clause, bool keepClauseID)	MiniSat::Solver
addClause(const SAT::Clause &clause, bool isTheoryClause)	MiniSat::Solver
addFormula(const SAT::CNF_Formula &cnf, bool isTheoryClause)	MiniSat::Solver
addWatch(Lit literal, Clause *clause)	MiniSat::Solver	[inline, protected]
analyze(int &out_btlevel)	MiniSat::Solver	[protected]
analyze_minimize(std::vector< Lit > &out_learnt, Inference *inference, int &pushID)	MiniSat::Solver	[protected]
analyze_removable(Lit p, uint min_level, int pushID)	MiniSat::Solver	[protected]
assume(Lit p)	MiniSat::Solver	[protected]
backtrack(int level, Clause *clause)	MiniSat::Solver	[protected]
checkClause(const Clause &clause) const	MiniSat::Solver	[protected]
checkClauses() const	MiniSat::Solver	[protected]
checkTrail() const	MiniSat::Solver	[protected]
checkWatched(const Clause &clause) const	MiniSat::Solver	[protected]
checkWatched() const	MiniSat::Solver	[protected]
claBumpActivity(Clause *c)	MiniSat::Solver	[inline, protected]
claDecayActivity()	MiniSat::Solver	[inline, protected]
claRescaleActivity()	MiniSat::Solver	[protected]
createFrom(const Solver *solver)	MiniSat::Solver	[static]
d_activity	MiniSat::Solver	[protected]
d_analyze_redundant	MiniSat::Solver	[protected]
d_analyze_seen	MiniSat::Solver	[protected]
d_analyze_stack	MiniSat::Solver	[protected]
d_assigns	MiniSat::Solver	[protected]
d_cla_decay	MiniSat::Solver	[protected]
d_cla_inc	MiniSat::Solver	[protected]
d_clauseIDCounter	MiniSat::Solver	[protected]
d_clauses	MiniSat::Solver	[protected]
d_conflict	MiniSat::Solver	[protected]
d_decider	MiniSat::Solver	[protected]
d_default_params	MiniSat::Solver	[protected]
d_derivation	MiniSat::Solver	[protected]
d_expensive_ccmin	MiniSat::Solver	[protected]
d_inSearch	MiniSat::Solver	[protected]
d_learnts	MiniSat::Solver	[protected]
d_level	MiniSat::Solver	[protected]
d_ok	MiniSat::Solver	[protected]
d_order	MiniSat::Solver	[protected]
d_pendingClauses	MiniSat::Solver	[protected]
d_popLemmas	MiniSat::Solver	[protected]
d_popRequests	MiniSat::Solver	[protected]
d_pushes	MiniSat::Solver	[protected]
d_pushIDs	MiniSat::Solver	[protected]
d_qhead	MiniSat::Solver	[protected]
d_reason	MiniSat::Solver	[protected]
d_registeredVars	MiniSat::Solver	[protected]
d_rootLevel	MiniSat::Solver	[protected, static]
d_simpDB_assigns	MiniSat::Solver	[protected]
d_simpDB_props	MiniSat::Solver	[protected]
d_simpRD_learnts	MiniSat::Solver	[protected]
d_stats	MiniSat::Solver	[protected]
d_thead	MiniSat::Solver	[protected]
d_theoryAPI	MiniSat::Solver	[protected]
d_theoryExplanations	MiniSat::Solver	[protected]
d_trail	MiniSat::Solver	[protected]
d_trail_lim	MiniSat::Solver	[protected]
d_trail_pos	MiniSat::Solver	[protected]
d_var_decay	MiniSat::Solver	[protected]
d_var_inc	MiniSat::Solver	[protected]
d_watches	MiniSat::Solver	[protected]
decisionLevel() const	MiniSat::Solver	[inline, protected]
doPops()	MiniSat::Solver
enqueue(Lit fact, int decisionLevel, Clause *reason)	MiniSat::Solver	[protected]
getClauses() const	MiniSat::Solver	[inline]
getConflictLevel(const Clause &clause) const	MiniSat::Solver	[protected]
getDerivation()	MiniSat::Solver	[inline]
getImplicationLevel(const Clause &clause) const	MiniSat::Solver	[protected]
getLemmas() const	MiniSat::Solver	[inline]
getLevel(Var var) const	MiniSat::Solver	[inline]
getLevel(Lit lit) const	MiniSat::Solver	[inline]
getPushID(Var var) const	MiniSat::Solver	[inline, protected]
getPushID(Lit lit) const	MiniSat::Solver	[inline, protected]
getReason(Var var) const	MiniSat::Solver	[inline]
getReason(Lit literal, bool resolveTheoryImplication=true)	MiniSat::Solver
getStats() const	MiniSat::Solver	[inline]
getTrail() const	MiniSat::Solver	[inline]
getValue(Var x) const	MiniSat::Solver	[inline]
getValue(Lit p) const	MiniSat::Solver	[inline]
getWatches(Lit literal)	MiniSat::Solver	[inline, protected]
getWatches(Lit literal) const	MiniSat::Solver	[inline, protected]
inPush() const	MiniSat::Solver	[inline]
inSearch() const	MiniSat::Solver	[inline]
insertClause(Clause *clause)	MiniSat::Solver	[protected]
insertLemma(const Clause *lemma, int clauseID, int pushID)	MiniSat::Solver	[protected]
isConflicting() const	MiniSat::Solver	[protected]
isConsistent() const	MiniSat::Solver	[inline]
isImpliedAt(Lit lit, int clausePushID) const	MiniSat::Solver	[protected]
isPermSatisfied(Clause *c) const	MiniSat::Solver	[protected]
isReason(const Clause *c) const	MiniSat::Solver	[inline]
isRegistered(Var var)	MiniSat::Solver	[protected]
nAssigns() const	MiniSat::Solver	[inline]
nClauses() const	MiniSat::Solver	[inline]
nextClauseID()	MiniSat::Solver	[inline]
nLearnts() const	MiniSat::Solver	[inline]
nVars() const	MiniSat::Solver	[inline]
orderClause(std::vector< Lit > &literals) const	MiniSat::Solver	[protected]
pop()	MiniSat::Solver	[protected]
popClauses(const PushEntry &pushEntry, std::vector< Clause * > &clauses)	MiniSat::Solver	[protected]
popTheories()	MiniSat::Solver
printDIMACS() const	MiniSat::Solver
printState() const	MiniSat::Solver
propagate()	MiniSat::Solver	[protected]
propLookahead(const SearchParams &params)	MiniSat::Solver	[protected]
protocolPropagation() const	MiniSat::Solver	[protected]
push()	MiniSat::Solver
reduceDB()	MiniSat::Solver
registerVar(Var var)	MiniSat::Solver	[protected]
remove(Clause *c, bool just_dealloc=false)	MiniSat::Solver	[protected]
removeWatch(std::vector< Clause * > &ws, Clause *elem)	MiniSat::Solver	[protected]
requestPop()	MiniSat::Solver
resolveTheoryImplication(Lit literal)	MiniSat::Solver	[protected]
search()	MiniSat::Solver
setLevel(Var var, int level)	MiniSat::Solver	[inline]
setLevel(Lit lit, int level)	MiniSat::Solver	[inline]
setPushID(Var var, Clause *from)	MiniSat::Solver	[protected]
simplifyClause(std::vector< Lit > &literals, int clausePushID) const	MiniSat::Solver	[protected]
simplifyDB()	MiniSat::Solver
Solver(SAT::DPLLT::TheoryAPI *theoryAPI, SAT::DPLLT::Decider *decider)	MiniSat::Solver
toString(Lit literal, bool showAssignment) const	MiniSat::Solver
toString(const std::vector< Lit > &clause, bool showAssignment) const	MiniSat::Solver
toString(const Clause &clause, bool showAssignment) const	MiniSat::Solver
updateConflict(Clause *clause)	MiniSat::Solver	[protected]
varBumpActivity(Lit p)	MiniSat::Solver	[inline, protected]
varDecayActivity()	MiniSat::Solver	[inline, protected]
varRescaleActivity()	MiniSat::Solver	[protected]
~Solver()	MiniSat::Solver

---