CVC3  2.4.1
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::Solverprotected
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::Solverinlineprotected
allClausesSatisfied()MiniSat::Solverprotected
analyze(int &out_btlevel)MiniSat::Solverprotected
analyze_minimize(std::vector< Lit > &out_learnt, Inference *inference, int &pushID)MiniSat::Solverprotected
analyze_removable(Lit p, unsigned int min_level, int pushID)MiniSat::Solverprotected
assume(Lit p)MiniSat::Solverprotected
backtrack(int level, Clause *clause)MiniSat::Solverprotected
checkClause(const Clause &clause) const MiniSat::Solverprotected
checkClauses() const MiniSat::Solverprotected
checkTrail() const MiniSat::Solverprotected
checkWatched(const Clause &clause) const MiniSat::Solverprotected
checkWatched() const MiniSat::Solverprotected
claBumpActivity(Clause *c)MiniSat::Solverinlineprotected
claDecayActivity()MiniSat::Solverinlineprotected
claRescaleActivity()MiniSat::Solverprotected
createFrom(const Solver *solver)MiniSat::Solverstatic
curAssigns()MiniSat::Solver
curClauses()MiniSat::Solver
cvcToMiniSat(const SAT::Clause &clause, int id)MiniSat::Solver
d_activityMiniSat::Solverprotected
d_analyze_redundantMiniSat::Solverprotected
d_analyze_seenMiniSat::Solverprotected
d_analyze_stackMiniSat::Solverprotected
d_assignsMiniSat::Solverprotected
d_cla_decayMiniSat::Solverprotected
d_cla_incMiniSat::Solverprotected
d_clauseIDCounterMiniSat::Solverprotected
d_clausesMiniSat::Solverprotected
d_conflictMiniSat::Solverprotected
d_deciderMiniSat::Solverprotected
d_default_paramsMiniSat::Solverprotected
d_derivationMiniSat::Solverprotected
d_expensive_ccminMiniSat::Solverprotected
d_inSearchMiniSat::Solverprotected
d_learntsMiniSat::Solverprotected
d_levelMiniSat::Solverprotected
d_okMiniSat::Solverprotected
d_orderMiniSat::Solverprotected
d_pendingClausesMiniSat::Solverprotected
d_popLemmasMiniSat::Solverprotected
d_popRequestsMiniSat::Solverprotected
d_pushesMiniSat::Solverprotected
d_pushIDsMiniSat::Solverprotected
d_qheadMiniSat::Solverprotected
d_reasonMiniSat::Solverprotected
d_registeredVarsMiniSat::Solverprotected
d_rootLevelMiniSat::Solverprotectedstatic
d_simpDB_assignsMiniSat::Solverprotected
d_simpDB_propsMiniSat::Solverprotected
d_simpRD_learntsMiniSat::Solverprotected
d_statsMiniSat::Solverprotected
d_theadMiniSat::Solverprotected
d_theoryAPIMiniSat::Solverprotected
d_theoryExplanationsMiniSat::Solverprotected
d_trailMiniSat::Solverprotected
d_trail_limMiniSat::Solverprotected
d_trail_posMiniSat::Solverprotected
d_var_decayMiniSat::Solverprotected
d_var_incMiniSat::Solverprotected
d_watchesMiniSat::Solverprotected
decisionLevel() const MiniSat::Solverinlineprotected
doPops()MiniSat::Solver
enqueue(Lit fact, int decisionLevel, Clause *reason)MiniSat::Solverprotected
getClauses() const MiniSat::Solverinline
getConflictLevel(const Clause &clause) const MiniSat::Solverprotected
getDerivation()MiniSat::Solverinline
getImplicationLevel(const Clause &clause) const MiniSat::Solverprotected
getLemmas() const MiniSat::Solverinline
getLevel(Var var) const MiniSat::Solverinline
getLevel(Lit lit) const MiniSat::Solverinline
getProof()MiniSat::Solver
getPushID(Var var) const MiniSat::Solverinlineprotected
getPushID(Lit lit) const MiniSat::Solverinlineprotected
getReason(Var var) const MiniSat::Solverinline
getReason(Lit literal, bool resolveTheoryImplication=true)MiniSat::Solver
getStats() const MiniSat::Solverinline
getTrail() const MiniSat::Solverinline
getValue(Var x) const MiniSat::Solverinline
getValue(Lit p) const MiniSat::Solverinline
getWatches(Lit literal)MiniSat::Solverinlineprotected
getWatches(Lit literal) const MiniSat::Solverinlineprotected
inPush() const MiniSat::Solverinline
inSearch() const MiniSat::Solverinline
insertClause(Clause *clause)MiniSat::Solverprotected
insertLemma(const Clause *lemma, int clauseID, int pushID)MiniSat::Solverprotected
isConflicting() const MiniSat::Solverprotected
isConsistent() const MiniSat::Solverinline
isImpliedAt(Lit lit, int clausePushID) const MiniSat::Solverprotected
isPermSatisfied(Clause *c) const MiniSat::Solverprotected
isReason(const Clause *c) const MiniSat::Solverinline
isRegistered(Var var)MiniSat::Solverprotected
nAssigns() const MiniSat::Solverinline
nClauses() const MiniSat::Solverinline
nextClauseID()MiniSat::Solverinline
nLearnts() const MiniSat::Solverinline
nVars() const MiniSat::Solverinline
orderClause(std::vector< Lit > &literals) const MiniSat::Solverprotected
pop()MiniSat::Solverprotected
popClauses(const PushEntry &pushEntry, std::vector< Clause * > &clauses)MiniSat::Solverprotected
popTheories()MiniSat::Solver
printDIMACS() const MiniSat::Solver
printState() const MiniSat::Solver
propagate()MiniSat::Solverprotected
propLookahead(const SearchParams &params)MiniSat::Solverprotected
protocolPropagation() const MiniSat::Solverprotected
push()MiniSat::Solver
reduceDB()MiniSat::Solver
registerVar(Var var)MiniSat::Solverprotected
remove(Clause *c, bool just_dealloc=false)MiniSat::Solverprotected
removeWatch(std::vector< Clause * > &ws, Clause *elem)MiniSat::Solverprotected
requestPop()MiniSat::Solver
resolveTheoryImplication(Lit literal)MiniSat::Solverprotected
search()MiniSat::Solver
setLevel(Var var, int level)MiniSat::Solverinline
setLevel(Lit lit, int level)MiniSat::Solverinline
setPushID(Var var, Clause *from)MiniSat::Solverprotected
simplifyClause(std::vector< Lit > &literals, int clausePushID) const MiniSat::Solverprotected
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::Solverprotected
varBumpActivity(Lit p)MiniSat::Solverinlineprotected
varDecayActivity()MiniSat::Solverinlineprotected
varRescaleActivity()MiniSat::Solverprotected
~Solver()MiniSat::Solver