MiniSat::Solver Member List

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

addClause(std::vector< Lit > &literals, CVC3::Theorem theorem, int clauseID)MiniSat::Solver [protected]
addClause(Lit p, CVC3::Theorem theorem)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]
allClausesSatisfied()MiniSat::Solver [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, unsigned int 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]
curAssigns()MiniSat::Solver
curClauses()MiniSat::Solver
cvcToMiniSat(const SAT::Clause &clause, int id)MiniSat::Solver
d_activityMiniSat::Solver [protected]
d_analyze_redundantMiniSat::Solver [protected]
d_analyze_seenMiniSat::Solver [protected]
d_analyze_stackMiniSat::Solver [protected]
d_assignsMiniSat::Solver [protected]
d_cla_decayMiniSat::Solver [protected]
d_cla_incMiniSat::Solver [protected]
d_clauseIDCounterMiniSat::Solver [protected]
d_clausesMiniSat::Solver [protected]
d_conflictMiniSat::Solver [protected]
d_deciderMiniSat::Solver [protected]
d_default_paramsMiniSat::Solver [protected]
d_derivationMiniSat::Solver [protected]
d_expensive_ccminMiniSat::Solver [protected]
d_inSearchMiniSat::Solver [protected]
d_learntsMiniSat::Solver [protected]
d_levelMiniSat::Solver [protected]
d_okMiniSat::Solver [protected]
d_orderMiniSat::Solver [protected]
d_pendingClausesMiniSat::Solver [protected]
d_popLemmasMiniSat::Solver [protected]
d_popRequestsMiniSat::Solver [protected]
d_pushesMiniSat::Solver [protected]
d_pushIDsMiniSat::Solver [protected]
d_qheadMiniSat::Solver [protected]
d_reasonMiniSat::Solver [protected]
d_registeredVarsMiniSat::Solver [protected]
d_rootLevelMiniSat::Solver [protected, static]
d_simpDB_assignsMiniSat::Solver [protected]
d_simpDB_propsMiniSat::Solver [protected]
d_simpRD_learntsMiniSat::Solver [protected]
d_statsMiniSat::Solver [protected]
d_theadMiniSat::Solver [protected]
d_theoryAPIMiniSat::Solver [protected]
d_theoryExplanationsMiniSat::Solver [protected]
d_trailMiniSat::Solver [protected]
d_trail_limMiniSat::Solver [protected]
d_trail_posMiniSat::Solver [protected]
d_var_decayMiniSat::Solver [protected]
d_var_incMiniSat::Solver [protected]
d_watchesMiniSat::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]
getProof()MiniSat::Solver
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, bool logDerivation)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

Generated on Thu Oct 15 22:27:20 2009 for CVC3 by  doxygen 1.5.8