CVC3
2.4.1
|
#include <minisat_solver.h>
Solver::Solver | ( | SAT::DPLLT::TheoryAPI * | theoryAPI, |
SAT::DPLLT::Decider * | decider, | ||
bool | logDerivation | ||
) |
Initialization.
Definition at line 158 of file minisat_solver.cpp.
References d_derivation.
Referenced by createFrom().
Solver::~Solver | ( | ) |
Definition at line 292 of file minisat_solver.cpp.
References d_learnts, d_clauses, d_pendingClauses, MiniSat::xfree(), d_theoryExplanations, and d_derivation.
int MiniSat::Solver::decisionLevel | ( | ) | const [inline, protected] |
Search:
Definition at line 424 of file minisat_solver.h.
References d_trail_lim.
Referenced by getImplicationLevel(), getConflictLevel(), assume(), backtrack(), protocolPropagation(), propLookahead(), search(), push(), and popTheories().
bool Solver::assume | ( | Lit | p | ) | [protected] |
Definition at line 1473 of file minisat_solver.cpp.
References d_trail_lim, d_trail, d_stats, MiniSat::SolverStats::max_level, MiniSat::max(), enqueue(), decisionLevel(), and MiniSat::Clause::Decision().
Referenced by propLookahead(), and search().
Definition at line 1575 of file minisat_solver.cpp.
References getValue(), MiniSat::l_Undef, MiniSat::l_False, MiniSat::Lit::var(), d_assigns, MiniSat::toInt(), MiniSat::Lit::sign(), setLevel(), d_reason, setPushID(), d_trail, d_derivation, and d_trail_pos.
Referenced by insertLemma(), insertClause(), assume(), propagate(), search(), and push().
void Solver::propagate | ( | ) | [protected] |
Definition at line 1689 of file minisat_solver.cpp.
References d_trail, d_qhead, getWatches(), d_stats, MiniSat::SolverStats::propagations, d_simpDB_props, getLevel(), d_rootLevel, d_simpDB_assigns, defer_theory_propagation, d_theoryAPI, SAT::DPLLT::TheoryAPI::assertLit(), MiniSat::miniSatToCVC(), d_thead, getValue(), MiniSat::l_True, DebugAssert, MiniSat::l_False, MiniSat::Clause::size(), addWatch(), IF_DEBUG, enqueue(), getImplicationLevel(), and updateConflict().
Referenced by propLookahead(), search(), and push().
void Solver::propLookahead | ( | const SearchParams & | params | ) | [protected] |
Definition at line 1950 of file minisat_solver.cpp.
References prop_lookahead, d_order, MiniSat::VarOrder::select(), MiniSat::SearchParams::random_var_freq, isRegistered(), MiniSat::var_Undef, MiniSat::VarOrder::undo(), decisionLevel(), d_trail, assume(), d_qhead, isConflicting(), protocolPropagation(), propagate(), d_assigns, MiniSat::toInt(), MiniSat::l_Undef, d_reason, and d_trail_lim.
Referenced by search().
Clause * Solver::analyze | ( | int & | out_btlevel | ) | [protected] |
Conflict handling.
Definition at line 1091 of file minisat_solver.cpp.
References DebugAssert, d_conflict, MiniSat::Clause::size(), resolveTheoryImplication(), getConflictLevel(), IF_DEBUG, d_analyze_seen, d_trail, MiniSat::lit_Undef(), getDerivation(), MiniSat::Clause::id(), MiniSat::Clause::pushID(), d_rootLevel, MiniSat::Clause::Decision(), MiniSat::Clause::TheoryImplication(), claBumpActivity(), getValue(), MiniSat::l_False, getLevel(), MiniSat::Lit::var(), d_analyze_redundant, varBumpActivity(), MiniSat::max(), getReason(), MiniSat::Inference::add(), analyze_minimize(), nextClauseID(), MiniSat::Derivation::registerInference(), and MiniSat::Lemma_new().
Referenced by search().
void Solver::analyze_minimize | ( | std::vector< Lit > & | out_learnt, |
Inference * | inference, | ||
int & | pushID | ||
) | [protected] |
Definition at line 1278 of file minisat_solver.cpp.
References d_expensive_ccmin, getLevel(), getReason(), MiniSat::Clause::Decision(), analyze_removable(), MiniSat::Clause::size(), d_analyze_seen, d_rootLevel, d_analyze_redundant, getDerivation(), d_trail_pos, MiniSat::Lit::var(), getPushID(), d_pushes, MiniSat::max(), and MiniSat::Inference::add().
Referenced by analyze().
bool Solver::analyze_removable | ( | Lit | p, |
unsigned int | min_level, | ||
int | pushID | ||
) | [protected] |
Definition at line 1395 of file minisat_solver.cpp.
References DebugAssert, getReason(), MiniSat::Clause::Decision(), d_analyze_stack, d_analyze_redundant, MiniSat::Clause::TheoryImplication(), d_analyze_seen, MiniSat::Lit::var(), getLevel(), and d_rootLevel.
Referenced by analyze_minimize().
void Solver::backtrack | ( | int | level, |
Clause * | clause | ||
) | [protected] |
Definition at line 1481 of file minisat_solver.cpp.
References DebugAssert, decisionLevel(), d_rootLevel, d_theoryAPI, SAT::DPLLT::TheoryAPI::pop(), d_trail, d_trail_lim, getLevel(), d_assigns, MiniSat::toInt(), MiniSat::l_Undef, d_reason, d_order, MiniSat::VarOrder::undo(), d_derivation, d_trail_pos, d_qhead, d_thead, insertClause(), isConflicting(), d_pendingClauses, addClause(), MiniSat::xfree(), and d_theoryExplanations.
Referenced by search().
bool Solver::isConflicting | ( | ) | const [protected] |
Definition at line 973 of file minisat_solver.cpp.
References d_conflict.
Referenced by createFrom(), backtrack(), simplifyDB(), propLookahead(), search(), push(), and isConsistent().
void Solver::updateConflict | ( | Clause * | clause | ) | [protected] |
Definition at line 977 of file minisat_solver.cpp.
References DebugAssert, IF_DEBUG, MiniSat::Clause::size(), getValue(), MiniSat::l_False, and d_conflict.
Referenced by insertLemma(), insertClause(), and propagate().
int Solver::getImplicationLevel | ( | const Clause & | clause | ) | const [protected] |
Definition at line 910 of file minisat_solver.cpp.
References decisionLevel(), d_rootLevel, MiniSat::Clause::size(), DebugAssert, getValue(), MiniSat::l_False, and getLevel().
Referenced by insertClause(), resolveTheoryImplication(), and propagate().
int Solver::getConflictLevel | ( | const Clause & | clause | ) | const [protected] |
Definition at line 935 of file minisat_solver.cpp.
References decisionLevel(), d_rootLevel, MiniSat::Clause::size(), DebugAssert, getValue(), MiniSat::l_False, and getLevel().
Referenced by analyze().
void Solver::resolveTheoryImplication | ( | Lit | literal | ) | [protected] |
Definition at line 999 of file minisat_solver.cpp.
References eager_explanation, d_reason, MiniSat::Lit::var(), MiniSat::Clause::TheoryImplication(), DebugAssert, getValue(), MiniSat::l_True, FatalAssert, cvcToMiniSat(), nextClauseID(), IF_DEBUG, MiniSat::l_False, MiniSat::Clause::size(), getImplicationLevel(), setLevel(), setPushID(), keep_lazy_explanation, addClause(), MiniSat::xfree(), and d_theoryExplanations.
Referenced by getReason(), and analyze().
std::vector<Clause*>& MiniSat::Solver::getWatches | ( | Lit | literal | ) | [inline, protected] |
unit propagation
Definition at line 478 of file minisat_solver.h.
References d_watches, and MiniSat::Lit::index().
Referenced by remove(), propagate(), allClausesSatisfied(), checkWatched(), pop(), and addWatch().
const std::vector<Clause*>& MiniSat::Solver::getWatches | ( | Lit | literal | ) | const [inline, protected] |
Definition at line 481 of file minisat_solver.h.
References d_watches, and MiniSat::Lit::index().
Definition at line 485 of file minisat_solver.h.
References getWatches().
Referenced by insertLemma(), insertClause(), and propagate().
void Solver::removeWatch | ( | std::vector< Clause * > & | ws, |
Clause * | elem | ||
) | [protected] |
void Solver::registerVar | ( | Var | var | ) | [protected] |
Operations on clauses:
Definition at line 457 of file minisat_solver.cpp.
References isRegistered(), nVars(), d_watches, d_reason, d_assigns, MiniSat::toInt(), MiniSat::l_Undef, d_level, d_activity, d_analyze_seen, d_pushIDs, d_derivation, d_trail_pos, d_trail, d_order, MiniSat::VarOrder::newVar(), DebugAssert, and d_registeredVars.
Referenced by insertLemma(), and addClause().
bool Solver::isRegistered | ( | Var | var | ) | [protected] |
Operations on clauses:
Definition at line 448 of file minisat_solver.cpp.
References d_registeredVars.
Referenced by registerVar(), and propLookahead().
void Solver::addClause | ( | std::vector< Lit > & | literals, |
CVC3::Theorem | theorem, | ||
int | clauseID | ||
) | [protected] |
Definition at line 671 of file minisat_solver.cpp.
References registerVar(), simplifyClause(), getReason(), MiniSat::Clause::learnt(), getDerivation(), MiniSat::Clause_new(), MiniSat::Derivation::registerClause(), MiniSat::Derivation::removedClause(), MiniSat::Inference::add(), nextClauseID(), MiniSat::Derivation::registerInference(), orderClause(), insertClause(), and d_reason.
Referenced by createFrom(), addClause(), addFormula(), resolveTheoryImplication(), and backtrack().
void Solver::insertClause | ( | Clause * | clause | ) | [protected] |
Definition at line 750 of file minisat_solver.cpp.
References d_ok, getDerivation(), MiniSat::Derivation::registerClause(), MiniSat::Clause::size(), d_conflict, MiniSat::Clause::learnt(), d_clauses, d_learnts, enqueue(), d_rootLevel, updateConflict(), d_pendingClauses, DebugAssert, getValue(), MiniSat::l_Undef, IF_DEBUG, MiniSat::l_False, MiniSat::max(), getLevel(), claBumpActivity(), MiniSat::l_True, getImplicationLevel(), addWatch(), d_stats, MiniSat::SolverStats::max_literals, MiniSat::SolverStats::clauses_literals, and MiniSat::SolverStats::learnts_literals.
Referenced by addClause(), and backtrack().
void Solver::insertLemma | ( | const Clause * | lemma, |
int | clauseID, | ||
int | pushID | ||
) | [protected] |
Definition at line 190 of file minisat_solver.cpp.
References MiniSat::Clause::toLit(), registerVar(), orderClause(), MiniSat::Lemma_new(), getDerivation(), MiniSat::Derivation::registerClause(), MiniSat::Clause::setActivity(), MiniSat::Clause::activity(), MiniSat::Clause::size(), addWatch(), d_learnts, d_stats, MiniSat::SolverStats::learnts_literals, getValue(), MiniSat::l_False, updateConflict(), enqueue(), d_rootLevel, and DebugAssert.
Referenced by createFrom(), and push().
bool Solver::simplifyClause | ( | std::vector< Lit > & | literals, |
int | clausePushID | ||
) | const [protected] |
Definition at line 545 of file minisat_solver.cpp.
References getLevel(), d_rootLevel, isImpliedAt(), getValue(), MiniSat::l_True, and MiniSat::l_False.
Referenced by addClause().
void Solver::orderClause | ( | std::vector< Lit > & | literals | ) | const [protected] |
Definition at line 588 of file minisat_solver.cpp.
References getLevel(), getValue(), MiniSat::l_False, and MiniSat::l_True.
Referenced by insertLemma(), and addClause().
void Solver::remove | ( | Clause * | c, |
bool | just_dealloc = false |
||
) | [protected] |
Definition at line 869 of file minisat_solver.cpp.
References MiniSat::Clause::size(), removeWatch(), getWatches(), MiniSat::Clause::learnt(), d_stats, MiniSat::SolverStats::learnts_literals, MiniSat::SolverStats::clauses_literals, getDerivation(), MiniSat::xfree(), and MiniSat::Derivation::removedClause().
bool Solver::isImpliedAt | ( | Lit | lit, |
int | clausePushID | ||
) | const [protected] |
Definition at line 1443 of file minisat_solver.cpp.
References d_pushes, and getPushID().
Referenced by simplifyClause(), isPermSatisfied(), and simplifyDB().
bool Solver::isPermSatisfied | ( | Clause * | c | ) | const [protected] |
Definition at line 1458 of file minisat_solver.cpp.
References MiniSat::Clause::size(), getValue(), MiniSat::l_True, getLevel(), d_rootLevel, isImpliedAt(), and MiniSat::Clause::pushID().
Definition at line 2496 of file minisat_solver.cpp.
References DebugAssert, getReason(), MiniSat::max(), MiniSat::Clause::Decision(), MiniSat::Clause::TheoryImplication(), MiniSat::Clause::pushID(), MiniSat::Clause::size(), getPushID(), and d_pushIDs.
Referenced by resolveTheoryImplication(), and enqueue().
int MiniSat::Solver::getPushID | ( | Var | var | ) | const [inline, protected] |
Definition at line 540 of file minisat_solver.h.
References d_pushIDs.
Referenced by analyze_minimize(), isImpliedAt(), and setPushID().
int MiniSat::Solver::getPushID | ( | Lit | lit | ) | const [inline, protected] |
Definition at line 541 of file minisat_solver.h.
References getPushID(), and MiniSat::Lit::var().
Referenced by getPushID().
void Solver::pop | ( | void | ) | [protected] |
Definition at line 2668 of file minisat_solver.cpp.
References DebugAssert, d_popRequests, d_pushes, MiniSat::PushEntry::d_clauseID, d_ok, MiniSat::PushEntry::d_trailSize, d_trail, d_assigns, MiniSat::toInt(), MiniSat::l_Undef, d_reason, d_order, MiniSat::VarOrder::undo(), d_trail_lim, d_qhead, MiniSat::PushEntry::d_qhead, d_thead, MiniSat::PushEntry::d_thead, popClauses(), d_clauses, d_popLemmas, d_learnts, isReason(), d_stats, MiniSat::SolverStats::learnts_literals, MiniSat::Clause::size(), MiniSat::Clause::pushID(), removeWatch(), getWatches(), MiniSat::SolverStats::debug, d_pendingClauses, d_theoryExplanations, d_registeredVars, MiniSat::PushEntry::d_ok, d_derivation, MiniSat::Derivation::pop(), d_conflict, and d_inSearch.
Referenced by doPops().
void Solver::popClauses | ( | const PushEntry & | pushEntry, |
std::vector< Clause * > & | clauses | ||
) | [protected] |
Definition at line 2647 of file minisat_solver.cpp.
References MiniSat::PushEntry::d_clauseID.
Referenced by pop().
void MiniSat::Solver::varBumpActivity | ( | Lit | p | ) | [inline, protected] |
Activity:
Definition at line 550 of file minisat_solver.h.
References d_var_decay, d_activity, MiniSat::Lit::var(), d_var_inc, varRescaleActivity(), d_order, and MiniSat::VarOrder::update().
Referenced by analyze().
void MiniSat::Solver::varDecayActivity | ( | ) | [inline, protected] |
Definition at line 554 of file minisat_solver.h.
References d_var_decay, and d_var_inc.
Referenced by search().
void Solver::varRescaleActivity | ( | ) | [protected] |
Activity.
Definition at line 2290 of file minisat_solver.cpp.
References nVars(), d_activity, and d_var_inc.
Referenced by varBumpActivity().
void MiniSat::Solver::claDecayActivity | ( | ) | [inline, protected] |
Definition at line 556 of file minisat_solver.h.
References d_cla_inc, and d_cla_decay.
Referenced by search().
void Solver::claRescaleActivity | ( | ) | [protected] |
Definition at line 2299 of file minisat_solver.cpp.
References d_learnts, and d_cla_inc.
Referenced by claBumpActivity().
void MiniSat::Solver::claBumpActivity | ( | Clause * | c | ) | [inline, protected] |
Definition at line 558 of file minisat_solver.h.
References MiniSat::Clause::activity(), d_cla_inc, MiniSat::Clause::setActivity(), and claRescaleActivity().
Referenced by insertClause(), and analyze().
bool Solver::allClausesSatisfied | ( | ) | [protected] |
debugging
expensive debug checks
Definition at line 2313 of file minisat_solver.cpp.
References debug_full, d_clauses, MiniSat::Clause::size(), getValue(), MiniSat::l_True, std::endl(), toString(), getWatches(), getLevel(), and d_rootLevel.
Referenced by search().
void Solver::checkWatched | ( | const Clause & | clause | ) | const [protected] |
Definition at line 2359 of file minisat_solver.cpp.
References MiniSat::Clause::size(), getWatches(), getLevel(), d_rootLevel, printState(), toString(), std::endl(), and FatalAssert.
void Solver::checkWatched | ( | ) | const [protected] |
Definition at line 2384 of file minisat_solver.cpp.
References debug_full, d_clauses, and d_learnts.
void Solver::checkClause | ( | const Clause & | clause | ) | const [protected] |
Definition at line 2398 of file minisat_solver.cpp.
References MiniSat::Clause::size(), getValue(), MiniSat::l_Undef, MiniSat::l_True, MiniSat::l_False, printState(), std::endl(), toString(), and FatalAssert.
Referenced by checkClauses().
void Solver::checkClauses | ( | ) | const [protected] |
Definition at line 2432 of file minisat_solver.cpp.
References debug_full, d_clauses, checkClause(), and d_learnts.
void Solver::checkTrail | ( | ) | const [protected] |
Definition at line 2446 of file minisat_solver.cpp.
References debug_full, d_trail, MiniSat::Lit::var(), d_reason, MiniSat::Clause::Decision(), MiniSat::Clause::TheoryImplication(), FatalAssert, MiniSat::Clause::size(), d_assigns, MiniSat::toInt(), MiniSat::Lit::sign(), and getLevel().
void Solver::protocolPropagation | ( | ) | const [protected] |
Definition at line 1937 of file minisat_solver.cpp.
References protocol, d_trail, d_qhead, decisionLevel(), MiniSat::Lit::index(), std::endl(), toString(), getLevel(), getReason(), MiniSat::Lit::var(), and MiniSat::Clause::Decision().
Referenced by propLookahead(), search(), and push().
Definition at line 248 of file minisat_solver.cpp.
References Solver(), d_theoryAPI, d_decider, d_derivation, d_cla_inc, d_var_inc, d_activity, getTrail(), addClause(), getClauses(), getLemmas(), isConflicting(), nextClauseID(), and insertLemma().
Referenced by SAT::DPLLTMiniSat::pushSolver().
Clause * Solver::cvcToMiniSat | ( | const SAT::Clause & | clause, |
int | id | ||
) |
problem specification
Definition at line 139 of file minisat_solver.cpp.
References MiniSat::cvcToMiniSat(), MiniSat::Clause_new(), and SAT::Clause::getClauseTheorem().
Referenced by resolveTheoryImplication(), search(), and push().
void Solver::addClause | ( | Lit | p, |
CVC3::Theorem | theorem | ||
) |
Definition at line 482 of file minisat_solver.cpp.
References addClause(), and nextClauseID().
void Solver::addClause | ( | const Clause & | clause, |
bool | keepClauseID | ||
) |
Definition at line 507 of file minisat_solver.cpp.
References MiniSat::Clause::size(), addClause(), MiniSat::Clause::getTheorem(), MiniSat::Clause::id(), and nextClauseID().
void Solver::addClause | ( | const SAT::Clause & | clause, |
bool | isTheoryClause | ||
) |
Definition at line 488 of file minisat_solver.cpp.
References MiniSat::cvcToMiniSat(), nextClauseID(), getDerivation(), MiniSat::Derivation::registerInputClause(), SAT::Clause::getClauseTheorem(), and addClause().
void Solver::addFormula | ( | const SAT::CNF_Formula & | cnf, |
bool | isTheoryClause | ||
) |
Definition at line 529 of file minisat_solver.cpp.
References SAT::CNF_Formula::begin(), SAT::CNF_Formula::end(), and addClause().
Referenced by SAT::DPLLTMiniSat::checkSat(), SAT::DPLLTMiniSat::continueCheck(), SAT::DPLLTMiniSat::addAssertion(), search(), and push().
int MiniSat::Solver::nextClauseID | ( | ) | [inline] |
Definition at line 636 of file minisat_solver.h.
References FatalAssert, and d_clauseIDCounter.
Referenced by MiniSat::Derivation::computeRootReason(), MiniSat::Derivation::finish(), createFrom(), addClause(), resolveTheoryImplication(), and analyze().
void Solver::simplifyDB | ( | ) |
Definition at line 1816 of file minisat_solver.cpp.
References isConflicting(), DebugAssert, d_qhead, d_trail, d_stats, MiniSat::SolverStats::db_simpl, d_learnts, d_clauses, isReason(), MiniSat::Clause::size(), getLevel(), d_rootLevel, getValue(), MiniSat::l_False, MiniSat::l_True, isImpliedAt(), MiniSat::Clause::pushID(), MiniSat::SolverStats::del_clauses, d_simpDB_assigns, d_simpDB_props, MiniSat::SolverStats::clauses_literals, and MiniSat::SolverStats::learnts_literals.
void Solver::reduceDB | ( | ) |
Definition at line 1781 of file minisat_solver.cpp.
References d_stats, MiniSat::SolverStats::lm_simpl, d_cla_inc, d_learnts, isReason(), MiniSat::SolverStats::del_lemmas, and d_simpRD_learnts.
CVC3::QueryResult Solver::search | ( | ) |
search
Definition at line 2005 of file minisat_solver.cpp.
References DebugAssert, d_popRequests, d_pushes, d_inSearch, d_default_params, d_stats, MiniSat::SolverStats::starts, d_var_decay, MiniSat::SearchParams::var_decay, d_cla_decay, MiniSat::SearchParams::clause_decay, protocol, printState(), d_ok, getDerivation(), MiniSat::Derivation::finish(), d_conflict, UNSATISFIABLE, d_thead, d_qhead, d_trail_lim, decisionLevel(), MiniSat::SolverStats::conflicts, d_theoryAPI, SAT::DPLLT::TheoryAPI::outOfResources(), CVC3::ABORT, d_rootLevel, analyze(), backtrack(), toString(), SAT::CNF_Formula::print(), varDecayActivity(), claDecayActivity(), std::endl(), SAT::DPLLT::TheoryAPI::checkConsistent(), MiniSat::SolverStats::theory_conflicts, addFormula(), SAT::CNF_Formula_Impl::reset(), isConflicting(), d_trail, protocolPropagation(), propagate(), defer_theory_propagation, SAT::DPLLT::TheoryAPI::assertLit(), MiniSat::miniSatToCVC(), SAT::DPLLT::TheoryAPI::getNewClauses(), SAT::DPLLT::TheoryAPI::getImplication(), SAT::Lit::isNull(), cvcToMiniSat(), MiniSat::Lit::index(), eager_explanation, enqueue(), MiniSat::Clause::TheoryImplication(), SAT::DPLLT::TheoryAPI::getExplanation(), MiniSat::lit_Undef(), d_decider, SAT::DPLLT::Decider::makeDecision(), d_order, MiniSat::VarOrder::select(), MiniSat::SearchParams::random_var_freq, MiniSat::var_Undef, nAssigns(), simplifyDB(), MiniSat::SolverStats::decisions, SAT::DPLLT::TheoryAPI::push(), getValue(), MiniSat::l_Undef, propLookahead(), MiniSat::SolverStats::debug, assume(), SAT::DPLLT::INCONSISTENT, SAT::DPLLT::MAYBE_CONSISTENT, SAT::DPLLT::CONSISTENT, allClausesSatisfied(), SATISFIABLE, and FatalAssert.
Referenced by SAT::DPLLTMiniSat::search().
Derivation* MiniSat::Solver::getProof | ( | ) |
bool MiniSat::Solver::inSearch | ( | ) | const [inline] |
Definition at line 668 of file minisat_solver.h.
References d_inSearch, and d_popRequests.
Referenced by push().
bool MiniSat::Solver::isConsistent | ( | ) | const [inline] |
Definition at line 671 of file minisat_solver.h.
References isConflicting().
Referenced by SAT::DPLLTMiniSat::addAssertion(), and requestPop().
void Solver::push | ( | void | ) |
Push / Pop.
Definition at line 2510 of file minisat_solver.cpp.
References DebugAssert, inSearch(), d_ok, d_pushes, d_registeredVars, d_popLemmas, insertLemma(), MiniSat::Clause::id(), MiniSat::Clause::pushID(), d_stats, MiniSat::SolverStats::learnts_literals, MiniSat::Clause::size(), push_theory_propagation, isConflicting(), d_qhead, d_trail, d_thead, protocolPropagation(), propagate(), defer_theory_propagation, d_theoryAPI, SAT::DPLLT::TheoryAPI::assertLit(), MiniSat::miniSatToCVC(), push_theory_implication, SAT::DPLLT::TheoryAPI::getImplication(), SAT::Lit::isNull(), cvcToMiniSat(), protocol, MiniSat::Lit::index(), std::endl(), eager_explanation, enqueue(), decisionLevel(), MiniSat::Clause::TheoryImplication(), SAT::DPLLT::TheoryAPI::getExplanation(), SAT::CNF_Formula::print(), addFormula(), SAT::CNF_Formula_Impl::reset(), push_theory_clause, SAT::DPLLT::TheoryAPI::getNewClauses(), printState(), simplifyDB(), d_derivation, MiniSat::Derivation::push(), and d_clauseIDCounter.
Referenced by SAT::DPLLTMiniSat::push().
void Solver::popTheories | ( | ) |
Definition at line 2641 of file minisat_solver.cpp.
References d_rootLevel, decisionLevel(), d_theoryAPI, and SAT::DPLLT::TheoryAPI::pop().
Referenced by requestPop().
void Solver::requestPop | ( | ) |
Definition at line 2621 of file minisat_solver.cpp.
References DebugAssert, inPush(), d_popRequests, isConsistent(), and popTheories().
Referenced by SAT::DPLLTMiniSat::pop().
void Solver::doPops | ( | ) |
Definition at line 2630 of file minisat_solver.cpp.
References d_popRequests, d_pushes, and pop().
Referenced by SAT::DPLLTMiniSat::checkSat(), SAT::DPLLTMiniSat::continueCheck(), SAT::DPLLTMiniSat::push(), and SAT::DPLLTMiniSat::addAssertion().
bool MiniSat::Solver::inPush | ( | ) | const [inline] |
Definition at line 692 of file minisat_solver.h.
References d_pushes, and d_popRequests.
Referenced by SAT::DPLLTMiniSat::continueCheck(), SAT::DPLLTMiniSat::pop(), and requestPop().
clauses / assignment
Definition at line 699 of file minisat_solver.h.
References MiniSat::toLbool(), and d_assigns.
Referenced by SAT::DPLLTMiniSat::getValue(), MiniSat::Derivation::computeRootReason(), insertLemma(), toString(), simplifyClause(), orderClause(), insertClause(), getImplicationLevel(), getConflictLevel(), getReason(), updateConflict(), resolveTheoryImplication(), analyze(), isPermSatisfied(), enqueue(), propagate(), simplifyDB(), search(), allClausesSatisfied(), and checkClause().
Definition at line 700 of file minisat_solver.h.
References MiniSat::Lit::sign(), getValue(), and MiniSat::Lit::var().
Referenced by getValue().
int MiniSat::Solver::getLevel | ( | Var | var | ) | const [inline] |
Definition at line 703 of file minisat_solver.h.
References d_level.
Referenced by simplifyClause(), orderClause(), insertClause(), getImplicationLevel(), getConflictLevel(), analyze(), analyze_minimize(), analyze_removable(), isPermSatisfied(), backtrack(), propagate(), simplifyDB(), protocolPropagation(), allClausesSatisfied(), checkWatched(), and checkTrail().
int MiniSat::Solver::getLevel | ( | Lit | lit | ) | const [inline] |
Definition at line 704 of file minisat_solver.h.
References getLevel(), and MiniSat::Lit::var().
Referenced by getLevel().
void MiniSat::Solver::setLevel | ( | Var | var, |
int | level | ||
) | [inline] |
Definition at line 707 of file minisat_solver.h.
References d_level.
Referenced by resolveTheoryImplication(), and enqueue().
void MiniSat::Solver::setLevel | ( | Lit | lit, |
int | level | ||
) | [inline] |
Definition at line 708 of file minisat_solver.h.
References setLevel(), and MiniSat::Lit::var().
Referenced by setLevel().
bool MiniSat::Solver::isReason | ( | const Clause * | c | ) | const [inline] |
Definition at line 712 of file minisat_solver.h.
References MiniSat::Clause::size(), and d_reason.
Referenced by reduceDB(), simplifyDB(), and pop().
Definition at line 715 of file minisat_solver.h.
References d_reason.
Referenced by MiniSat::Derivation::computeRootReason(), printState(), printDIMACS(), addClause(), analyze(), analyze_minimize(), analyze_removable(), protocolPropagation(), and setPushID().
Definition at line 950 of file minisat_solver.cpp.
References MiniSat::Lit::var(), d_reason, DebugAssert, MiniSat::Clause::TheoryImplication(), getValue(), MiniSat::l_True, and resolveTheoryImplication().
const std::vector<Clause*>& MiniSat::Solver::getClauses | ( | ) | const [inline] |
Definition at line 722 of file minisat_solver.h.
References d_clauses.
Referenced by SAT::DPLLTMiniSat::search(), and createFrom().
const std::vector<Clause*>& MiniSat::Solver::getLemmas | ( | ) | const [inline] |
Definition at line 725 of file minisat_solver.h.
References d_learnts.
Referenced by SAT::DPLLTMiniSat::search(), and createFrom().
const std::vector<Lit>& MiniSat::Solver::getTrail | ( | ) | const [inline] |
Derivation* MiniSat::Solver::getDerivation | ( | ) | [inline] |
Definition at line 731 of file minisat_solver.h.
References d_derivation.
Referenced by insertLemma(), addClause(), insertClause(), remove(), analyze(), analyze_minimize(), and search().
const SolverStats& MiniSat::Solver::getStats | ( | ) | const [inline] |
Statistics.
Definition at line 736 of file minisat_solver.h.
References d_stats.
Referenced by SAT::DPLLTMiniSat::search().
int MiniSat::Solver::nAssigns | ( | ) | const [inline] |
int MiniSat::Solver::nClauses | ( | ) | const [inline] |
Definition at line 742 of file minisat_solver.h.
References d_clauses.
int MiniSat::Solver::nLearnts | ( | ) | const [inline] |
Definition at line 745 of file minisat_solver.h.
References d_learnts.
int MiniSat::Solver::nVars | ( | ) | const [inline] |
Definition at line 749 of file minisat_solver.h.
References d_assigns.
Referenced by SAT::DPLLTMiniSat::search(), printDIMACS(), registerVar(), and varRescaleActivity().
std::string Solver::toString | ( | Lit | literal, |
bool | showAssignment | ||
) | const |
String representation:
String representation
Definition at line 319 of file minisat_solver.cpp.
References MiniSat::Lit::toString(), getValue(), MiniSat::l_True, and MiniSat::l_False.
Referenced by toString(), printState(), printDIMACS(), protocolPropagation(), search(), allClausesSatisfied(), checkWatched(), and checkClause().
std::string Solver::toString | ( | const std::vector< Lit > & | clause, |
bool | showAssignment | ||
) | const |
Definition at line 334 of file minisat_solver.cpp.
References toString(), and std::endl().
std::string Solver::toString | ( | const Clause & | clause, |
bool | showAssignment | ||
) | const |
Definition at line 344 of file minisat_solver.cpp.
References MiniSat::Clause::toLit(), and toString().
void Solver::printState | ( | ) | const |
Definition at line 375 of file minisat_solver.cpp.
References std::endl(), d_learnts, toString(), d_clauses, d_trail, getReason(), and MiniSat::Clause::Decision().
Referenced by search(), checkWatched(), checkClause(), and push().
void Solver::printDIMACS | ( | ) | const |
Definition at line 405 of file minisat_solver.cpp.
References nVars(), d_clauses, d_trail, std::endl(), MiniSat::Clause::size(), toString(), getReason(), MiniSat::Lit::var(), and MiniSat::Clause::Decision().
std::vector< SAT::Lit > Solver::curAssigns | ( | ) |
Definition at line 351 of file minisat_solver.cpp.
References std::endl(), d_trail, and MiniSat::miniSatToCVC().
Referenced by SAT::DPLLTMiniSat::getCurAssignments().
std::vector< std::vector< SAT::Lit > > Solver::curClauses | ( | ) |
Definition at line 360 of file minisat_solver.cpp.
References std::endl(), d_clauses, and MiniSat::miniSatToCVC().
Referenced by SAT::DPLLTMiniSat::getCurClauses().
const int MiniSat::Solver::d_rootLevel = 0 [static, protected] |
variables
Definition at line 205 of file minisat_solver.h.
Referenced by insertLemma(), simplifyClause(), insertClause(), getImplicationLevel(), getConflictLevel(), analyze(), analyze_minimize(), analyze_removable(), isPermSatisfied(), backtrack(), propagate(), simplifyDB(), search(), allClausesSatisfied(), checkWatched(), and popTheories().
bool MiniSat::Solver::d_inSearch [protected] |
status
Definition at line 210 of file minisat_solver.h.
Referenced by search(), pop(), and inSearch().
bool MiniSat::Solver::d_ok [protected] |
Definition at line 213 of file minisat_solver.h.
Referenced by insertClause(), search(), push(), and pop().
Clause* MiniSat::Solver::d_conflict [protected] |
Definition at line 241 of file minisat_solver.h.
Referenced by insertClause(), isConflicting(), updateConflict(), analyze(), search(), and pop().
std::vector<std::vector<Clause*> > MiniSat::Solver::d_watches [protected] |
variable assignments, and pending propagations
Definition at line 248 of file minisat_solver.h.
Referenced by registerVar(), and getWatches().
std::vector<signed char> MiniSat::Solver::d_assigns [protected] |
Definition at line 251 of file minisat_solver.h.
Referenced by registerVar(), backtrack(), enqueue(), propLookahead(), checkTrail(), pop(), getValue(), and nVars().
std::vector<Lit> MiniSat::Solver::d_trail [protected] |
Definition at line 256 of file minisat_solver.h.
Referenced by curAssigns(), printState(), printDIMACS(), registerVar(), analyze(), assume(), backtrack(), enqueue(), propagate(), simplifyDB(), protocolPropagation(), propLookahead(), search(), checkTrail(), push(), pop(), getTrail(), and nAssigns().
std::vector<int> MiniSat::Solver::d_trail_lim [protected] |
Definition at line 260 of file minisat_solver.h.
Referenced by assume(), backtrack(), propLookahead(), search(), pop(), and decisionLevel().
std::vector<size_type> MiniSat::Solver::d_trail_pos [protected] |
Definition at line 264 of file minisat_solver.h.
Referenced by registerVar(), analyze_minimize(), backtrack(), and enqueue().
size_type MiniSat::Solver::d_qhead [protected] |
Definition at line 269 of file minisat_solver.h.
Referenced by backtrack(), propagate(), simplifyDB(), protocolPropagation(), propLookahead(), search(), push(), and pop().
size_type MiniSat::Solver::d_thead [protected] |
Definition at line 273 of file minisat_solver.h.
Referenced by backtrack(), propagate(), search(), push(), and pop().
std::vector<Clause*> MiniSat::Solver::d_reason [protected] |
Definition at line 278 of file minisat_solver.h.
Referenced by registerVar(), addClause(), getReason(), resolveTheoryImplication(), backtrack(), enqueue(), propLookahead(), checkTrail(), pop(), and isReason().
std::vector<int> MiniSat::Solver::d_level [protected] |
Definition at line 284 of file minisat_solver.h.
Referenced by registerVar(), getLevel(), and setLevel().
std::vector<Hash::hash_set<Var> > MiniSat::Solver::d_registeredVars [protected] |
Definition at line 294 of file minisat_solver.h.
Referenced by isRegistered(), registerVar(), push(), and pop().
int MiniSat::Solver::d_clauseIDCounter [protected] |
std::vector<Clause*> MiniSat::Solver::d_clauses [protected] |
Definition at line 303 of file minisat_solver.h.
Referenced by ~Solver(), curClauses(), printState(), printDIMACS(), insertClause(), simplifyDB(), allClausesSatisfied(), checkWatched(), checkClauses(), pop(), getClauses(), and nClauses().
std::vector<Clause*> MiniSat::Solver::d_learnts [protected] |
Definition at line 306 of file minisat_solver.h.
Referenced by insertLemma(), ~Solver(), printState(), insertClause(), reduceDB(), simplifyDB(), claRescaleActivity(), checkWatched(), checkClauses(), pop(), getLemmas(), and nLearnts().
std::queue<Clause*> MiniSat::Solver::d_pendingClauses [protected] |
Temporary clauses.
Definition at line 314 of file minisat_solver.h.
Referenced by ~Solver(), insertClause(), backtrack(), and pop().
std::stack<std::pair<int, Clause*> > MiniSat::Solver::d_theoryExplanations [protected] |
Definition at line 319 of file minisat_solver.h.
Referenced by ~Solver(), resolveTheoryImplication(), backtrack(), and pop().
std::vector<PushEntry> MiniSat::Solver::d_pushes [protected] |
Push / Pop.
Definition at line 325 of file minisat_solver.h.
Referenced by analyze_minimize(), isImpliedAt(), search(), push(), doPops(), pop(), and inPush().
std::vector<Clause*> MiniSat::Solver::d_popLemmas [protected] |
Definition at line 328 of file minisat_solver.h.
std::vector<int> MiniSat::Solver::d_pushIDs [protected] |
Definition at line 343 of file minisat_solver.h.
Referenced by registerVar(), setPushID(), and getPushID().
unsigned int MiniSat::Solver::d_popRequests [protected] |
Definition at line 350 of file minisat_solver.h.
Referenced by search(), requestPop(), doPops(), pop(), inSearch(), and inPush().
double MiniSat::Solver::d_cla_inc [protected] |
heuristics
Definition at line 359 of file minisat_solver.h.
Referenced by createFrom(), reduceDB(), claRescaleActivity(), claDecayActivity(), and claBumpActivity().
double MiniSat::Solver::d_cla_decay [protected] |
Definition at line 361 of file minisat_solver.h.
Referenced by search(), and claDecayActivity().
std::vector<double> MiniSat::Solver::d_activity [protected] |
Definition at line 366 of file minisat_solver.h.
Referenced by createFrom(), registerVar(), varRescaleActivity(), and varBumpActivity().
double MiniSat::Solver::d_var_inc [protected] |
Definition at line 368 of file minisat_solver.h.
Referenced by createFrom(), varRescaleActivity(), varBumpActivity(), and varDecayActivity().
double MiniSat::Solver::d_var_decay [protected] |
Definition at line 371 of file minisat_solver.h.
Referenced by search(), varBumpActivity(), and varDecayActivity().
VarOrder MiniSat::Solver::d_order [protected] |
Definition at line 373 of file minisat_solver.h.
Referenced by registerVar(), backtrack(), propLookahead(), search(), pop(), and varBumpActivity().
int MiniSat::Solver::d_simpDB_assigns [protected] |
Definition at line 378 of file minisat_solver.h.
Referenced by propagate(), and simplifyDB().
int64_t MiniSat::Solver::d_simpDB_props [protected] |
Definition at line 380 of file minisat_solver.h.
Referenced by propagate(), and simplifyDB().
int MiniSat::Solver::d_simpRD_learnts [protected] |
Definition at line 382 of file minisat_solver.h.
Referenced by reduceDB().
SAT::DPLLT::TheoryAPI* MiniSat::Solver::d_theoryAPI [protected] |
CVC interface.
Definition at line 388 of file minisat_solver.h.
Referenced by createFrom(), backtrack(), propagate(), search(), push(), and popTheories().
SAT::DPLLT::Decider* MiniSat::Solver::d_decider [protected] |
Definition at line 391 of file minisat_solver.h.
Referenced by createFrom(), and search().
Derivation* MiniSat::Solver::d_derivation [protected] |
proof logging
Definition at line 397 of file minisat_solver.h.
Referenced by Solver(), createFrom(), ~Solver(), registerVar(), backtrack(), enqueue(), push(), pop(), and getDerivation().
SearchParams MiniSat::Solver::d_default_params [protected] |
bool MiniSat::Solver::d_expensive_ccmin [protected] |
Definition at line 406 of file minisat_solver.h.
Referenced by analyze_minimize().
std::vector<char> MiniSat::Solver::d_analyze_seen [protected] |
Temporaries (to reduce allocation overhead).
Definition at line 412 of file minisat_solver.h.
Referenced by registerVar(), analyze(), analyze_minimize(), and analyze_removable().
std::vector<Lit> MiniSat::Solver::d_analyze_stack [protected] |
Definition at line 413 of file minisat_solver.h.
Referenced by analyze_removable().
std::vector<Lit> MiniSat::Solver::d_analyze_redundant [protected] |
Definition at line 414 of file minisat_solver.h.
Referenced by analyze(), analyze_minimize(), and analyze_removable().
SolverStats MiniSat::Solver::d_stats [protected] |
Definition at line 417 of file minisat_solver.h.
Referenced by insertLemma(), insertClause(), remove(), assume(), propagate(), reduceDB(), simplifyDB(), search(), push(), pop(), and getStats().