MiniSat::Solver Class Reference

#include <minisat_solver.h>

Collaboration diagram for MiniSat::Solver:

Collaboration graph
[legend]

List of all members.

Public Member Functions

Static Public Member Functions

Protected Member Functions

Protected Attributes

Static Protected Attributes

Detailed Description

Definition at line 200 of file minisat_solver.h.

Constructor & Destructor Documentation

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_clauses, d_derivation, d_learnts, d_pendingClauses, d_theoryExplanations, and MiniSat::xfree().

Member Function Documentation

int MiniSat::Solver::decisionLevel (  )  const [inline, protected]

Search:.

Definition at line 424 of file minisat_solver.h.

References d_trail_lim.

Referenced by assume(), backtrack(), getConflictLevel(), getImplicationLevel(), popTheories(), propLookahead(), protocolPropagation(), push(), and search().

bool Solver::assume ( Lit  p  )  [protected]

Definition at line 1473 of file minisat_solver.cpp.

References d_stats, d_trail, d_trail_lim, MiniSat::Clause::Decision(), decisionLevel(), enqueue(), MiniSat::max(), and MiniSat::SolverStats::max_level.

Referenced by propLookahead(), and search().

bool Solver::enqueue ( Lit  fact,
int  decisionLevel,
Clause *  reason 
) [protected]

Definition at line 1575 of file minisat_solver.cpp.

References d_assigns, d_derivation, d_reason, d_trail, d_trail_pos, getValue(), MiniSat::l_False, MiniSat::l_Undef, setLevel(), setPushID(), MiniSat::Lit::sign(), MiniSat::toInt(), and MiniSat::Lit::var().

Referenced by assume(), insertClause(), insertLemma(), propagate(), push(), and search().

void Solver::propagate (  )  [protected]

Definition at line 1689 of file minisat_solver.cpp.

References addWatch(), SAT::DPLLT::DPLLT::TheoryAPI::assertLit(), d_qhead, d_rootLevel, d_simpDB_assigns, d_simpDB_props, d_stats, d_thead, d_theoryAPI, d_trail, DebugAssert, defer_theory_propagation, enqueue(), getImplicationLevel(), getLevel(), getValue(), getWatches(), IF_DEBUG, MiniSat::l_False, MiniSat::l_True, MiniSat::miniSatToCVC(), MiniSat::SolverStats::propagations, MiniSat::Clause::size(), and updateConflict().

Referenced by propLookahead(), push(), and search().

void Solver::propLookahead ( const SearchParams &  params  )  [protected]

Definition at line 1950 of file minisat_solver.cpp.

References assume(), d_assigns, d_order, d_qhead, d_reason, d_trail, d_trail_lim, decisionLevel(), isConflicting(), isRegistered(), MiniSat::l_Undef, prop_lookahead, propagate(), protocolPropagation(), MiniSat::SearchParams::random_var_freq, MiniSat::VarOrder::select(), MiniSat::toInt(), MiniSat::VarOrder::undo(), and MiniSat::var_Undef.

Referenced by search().

Clause * Solver::analyze ( int &  out_btlevel  )  [protected]

Conflict handling.

Definition at line 1091 of file minisat_solver.cpp.

References MiniSat::Inference::add(), analyze_minimize(), claBumpActivity(), d_analyze_redundant, d_analyze_seen, d_conflict, d_rootLevel, d_trail, DebugAssert, MiniSat::Clause::Decision(), getConflictLevel(), getDerivation(), getLevel(), getReason(), getValue(), MiniSat::Clause::id(), IF_DEBUG, MiniSat::l_False, MiniSat::Lemma_new(), MiniSat::lit_Undef(), MiniSat::max(), nextClauseID(), MiniSat::Clause::pushID(), MiniSat::Derivation::registerInference(), resolveTheoryImplication(), MiniSat::Clause::size(), MiniSat::Clause::TheoryImplication(), MiniSat::Lit::var(), and varBumpActivity().

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 MiniSat::Inference::add(), analyze_removable(), d_analyze_redundant, d_analyze_seen, d_expensive_ccmin, d_pushes, d_rootLevel, d_trail_pos, MiniSat::Clause::Decision(), getDerivation(), getLevel(), getPushID(), getReason(), MiniSat::max(), MiniSat::Clause::size(), and MiniSat::Lit::var().

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 d_analyze_redundant, d_analyze_seen, d_analyze_stack, d_rootLevel, DebugAssert, MiniSat::Clause::Decision(), getLevel(), getReason(), MiniSat::Clause::TheoryImplication(), and MiniSat::Lit::var().

Referenced by analyze_minimize().

void Solver::backtrack ( int  level,
Clause *  clause 
) [protected]

Definition at line 1481 of file minisat_solver.cpp.

References addClause(), d_assigns, d_derivation, d_order, d_pendingClauses, d_qhead, d_reason, d_rootLevel, d_thead, d_theoryAPI, d_theoryExplanations, d_trail, d_trail_lim, d_trail_pos, DebugAssert, decisionLevel(), getLevel(), insertClause(), isConflicting(), MiniSat::l_Undef, SAT::DPLLT::DPLLT::TheoryAPI::pop(), MiniSat::toInt(), MiniSat::VarOrder::undo(), and MiniSat::xfree().

Referenced by search().

bool Solver::isConflicting (  )  const [protected]

Definition at line 973 of file minisat_solver.cpp.

References d_conflict.

Referenced by backtrack(), createFrom(), isConsistent(), propLookahead(), push(), search(), and simplifyDB().

void Solver::updateConflict ( Clause *  clause  )  [protected]

Definition at line 977 of file minisat_solver.cpp.

References d_conflict, DebugAssert, getValue(), IF_DEBUG, MiniSat::l_False, and MiniSat::Clause::size().

Referenced by insertClause(), insertLemma(), and propagate().

int Solver::getImplicationLevel ( const Clause &  clause  )  const [protected]

Definition at line 910 of file minisat_solver.cpp.

References d_rootLevel, DebugAssert, decisionLevel(), getLevel(), getValue(), MiniSat::l_False, and MiniSat::Clause::size().

Referenced by insertClause(), propagate(), and resolveTheoryImplication().

int Solver::getConflictLevel ( const Clause &  clause  )  const [protected]

Definition at line 935 of file minisat_solver.cpp.

References d_rootLevel, DebugAssert, decisionLevel(), getLevel(), getValue(), MiniSat::l_False, and MiniSat::Clause::size().

Referenced by analyze().

void Solver::resolveTheoryImplication ( Lit  literal  )  [protected]

Definition at line 999 of file minisat_solver.cpp.

References addClause(), cvcToMiniSat(), d_reason, d_theoryExplanations, DebugAssert, eager_explanation, FatalAssert, getImplicationLevel(), getValue(), IF_DEBUG, keep_lazy_explanation, MiniSat::l_False, MiniSat::l_True, nextClauseID(), setLevel(), setPushID(), MiniSat::Clause::size(), MiniSat::Clause::TheoryImplication(), MiniSat::Lit::var(), and MiniSat::xfree().

Referenced by analyze(), and getReason().

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 addWatch(), allClausesSatisfied(), checkWatched(), pop(), propagate(), and remove().

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().

void MiniSat::Solver::addWatch ( Lit  literal,
Clause *  clause 
) [inline, protected]

Definition at line 485 of file minisat_solver.h.

References getWatches().

Referenced by insertClause(), insertLemma(), and propagate().

void Solver::removeWatch ( std::vector< Clause * > &  ws,
Clause *  elem 
) [protected]

Conflict handling.

Definition at line 889 of file minisat_solver.cpp.

References DebugAssert.

Referenced by pop(), and remove().

void Solver::registerVar ( Var  var  )  [protected]

Operations on clauses:.

Definition at line 457 of file minisat_solver.cpp.

References d_activity, d_analyze_seen, d_assigns, d_derivation, d_level, d_order, d_pushIDs, d_reason, d_registeredVars, d_trail, d_trail_pos, d_watches, DebugAssert, isRegistered(), MiniSat::l_Undef, MiniSat::VarOrder::newVar(), nVars(), and MiniSat::toInt().

Referenced by addClause(), and insertLemma().

bool Solver::isRegistered ( Var  var  )  [protected]

Operations on clauses:.

Definition at line 448 of file minisat_solver.cpp.

References d_registeredVars.

Referenced by propLookahead(), and registerVar().

void Solver::addClause ( std::vector< Lit > &  literals,
CVC3::Theorem  theorem,
int  clauseID 
) [protected]

Definition at line 671 of file minisat_solver.cpp.

References MiniSat::Inference::add(), MiniSat::Clause_new(), d_reason, getDerivation(), getReason(), insertClause(), MiniSat::Clause::learnt(), nextClauseID(), orderClause(), MiniSat::Derivation::registerClause(), MiniSat::Derivation::registerInference(), registerVar(), MiniSat::Derivation::removedClause(), and simplifyClause().

Referenced by addClause(), addFormula(), backtrack(), createFrom(), and resolveTheoryImplication().

void Solver::insertClause ( Clause *  clause  )  [protected]

Definition at line 750 of file minisat_solver.cpp.

References addWatch(), claBumpActivity(), MiniSat::SolverStats::clauses_literals, d_clauses, d_conflict, d_learnts, d_ok, d_pendingClauses, d_rootLevel, d_stats, DebugAssert, enqueue(), getDerivation(), getImplicationLevel(), getLevel(), getValue(), IF_DEBUG, MiniSat::l_False, MiniSat::l_True, MiniSat::l_Undef, MiniSat::Clause::learnt(), MiniSat::SolverStats::learnts_literals, MiniSat::max(), MiniSat::SolverStats::max_literals, MiniSat::Derivation::registerClause(), MiniSat::Clause::size(), and updateConflict().

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::activity(), addWatch(), d_learnts, d_rootLevel, d_stats, DebugAssert, enqueue(), getDerivation(), getValue(), MiniSat::l_False, MiniSat::SolverStats::learnts_literals, MiniSat::Lemma_new(), orderClause(), MiniSat::Derivation::registerClause(), registerVar(), MiniSat::Clause::setActivity(), MiniSat::Clause::size(), MiniSat::Clause::toLit(), and updateConflict().

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 d_rootLevel, getLevel(), getValue(), isImpliedAt(), MiniSat::l_False, and MiniSat::l_True.

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 addClause(), and insertLemma().

void Solver::remove ( Clause *  c,
bool  just_dealloc = false 
) [protected]

Definition at line 869 of file minisat_solver.cpp.

References MiniSat::SolverStats::clauses_literals, d_stats, getDerivation(), getWatches(), MiniSat::Clause::learnt(), MiniSat::SolverStats::learnts_literals, MiniSat::Derivation::removedClause(), removeWatch(), MiniSat::Clause::size(), and MiniSat::xfree().

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 isPermSatisfied(), simplifyClause(), and simplifyDB().

bool Solver::isPermSatisfied ( Clause *  c  )  const [protected]

Definition at line 1458 of file minisat_solver.cpp.

References d_rootLevel, getLevel(), getValue(), isImpliedAt(), MiniSat::l_True, MiniSat::Clause::pushID(), and MiniSat::Clause::size().

void Solver::setPushID ( Var  var,
Clause *  from 
) [protected]

Definition at line 2496 of file minisat_solver.cpp.

References d_pushIDs, DebugAssert, MiniSat::Clause::Decision(), getPushID(), getReason(), MiniSat::max(), MiniSat::Clause::pushID(), MiniSat::Clause::size(), and MiniSat::Clause::TheoryImplication().

Referenced by enqueue(), and resolveTheoryImplication().

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 d_assigns, MiniSat::PushEntry::d_clauseID, d_clauses, d_conflict, d_derivation, d_inSearch, d_learnts, MiniSat::PushEntry::d_ok, d_ok, d_order, d_pendingClauses, d_popLemmas, d_popRequests, d_pushes, MiniSat::PushEntry::d_qhead, d_qhead, d_reason, d_registeredVars, d_stats, MiniSat::PushEntry::d_thead, d_thead, d_theoryExplanations, d_trail, d_trail_lim, MiniSat::PushEntry::d_trailSize, MiniSat::SolverStats::debug, DebugAssert, getWatches(), isReason(), MiniSat::l_Undef, MiniSat::SolverStats::learnts_literals, MiniSat::Derivation::pop(), popClauses(), MiniSat::Clause::pushID(), removeWatch(), MiniSat::Clause::size(), MiniSat::toInt(), and MiniSat::VarOrder::undo().

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_activity, d_order, d_var_decay, d_var_inc, MiniSat::VarOrder::update(), MiniSat::Lit::var(), and varRescaleActivity().

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 d_activity, d_var_inc, and nVars().

Referenced by varBumpActivity().

void MiniSat::Solver::claDecayActivity (  )  [inline, protected]

Definition at line 556 of file minisat_solver.h.

References d_cla_decay, and d_cla_inc.

Referenced by search().

void Solver::claRescaleActivity (  )  [protected]

Definition at line 2299 of file minisat_solver.cpp.

References d_cla_inc, and d_learnts.

Referenced by claBumpActivity().

void MiniSat::Solver::claBumpActivity ( Clause *  c  )  [inline, protected]

Definition at line 558 of file minisat_solver.h.

References MiniSat::Clause::activity(), claRescaleActivity(), d_cla_inc, and MiniSat::Clause::setActivity().

Referenced by analyze(), and insertClause().

bool Solver::allClausesSatisfied (  )  [protected]

debugging

expensive debug checks

Definition at line 2313 of file minisat_solver.cpp.

References d_clauses, d_rootLevel, debug_full, std::endl(), getLevel(), getValue(), getWatches(), MiniSat::l_True, MiniSat::Clause::size(), and toString().

Referenced by search().

void Solver::checkWatched ( const Clause &  clause  )  const [protected]

Definition at line 2359 of file minisat_solver.cpp.

References d_rootLevel, std::endl(), FatalAssert, getLevel(), getWatches(), printState(), MiniSat::Clause::size(), and toString().

void Solver::checkWatched (  )  const [protected]

Definition at line 2384 of file minisat_solver.cpp.

References d_clauses, d_learnts, and debug_full.

void Solver::checkClause ( const Clause &  clause  )  const [protected]

Definition at line 2398 of file minisat_solver.cpp.

References std::endl(), FatalAssert, getValue(), MiniSat::l_False, MiniSat::l_True, MiniSat::l_Undef, printState(), MiniSat::Clause::size(), and toString().

Referenced by checkClauses().

void Solver::checkClauses (  )  const [protected]

Definition at line 2432 of file minisat_solver.cpp.

References checkClause(), d_clauses, d_learnts, and debug_full.

void Solver::checkTrail (  )  const [protected]

Definition at line 2446 of file minisat_solver.cpp.

References d_assigns, d_reason, d_trail, debug_full, MiniSat::Clause::Decision(), FatalAssert, getLevel(), MiniSat::Lit::sign(), MiniSat::Clause::size(), MiniSat::Clause::TheoryImplication(), MiniSat::toInt(), and MiniSat::Lit::var().

void Solver::protocolPropagation (  )  const [protected]

Definition at line 1937 of file minisat_solver.cpp.

References d_qhead, d_trail, MiniSat::Clause::Decision(), decisionLevel(), std::endl(), getLevel(), getReason(), MiniSat::Lit::index(), protocol, toString(), and MiniSat::Lit::var().

Referenced by propLookahead(), push(), and search().

Solver * Solver::createFrom ( const Solver *  solver  )  [static]

Definition at line 248 of file minisat_solver.cpp.

References addClause(), d_activity, d_cla_inc, d_decider, d_derivation, d_theoryAPI, d_var_inc, getClauses(), getLemmas(), getTrail(), insertLemma(), isConflicting(), nextClauseID(), and Solver().

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::Clause_new(), MiniSat::cvcToMiniSat(), SAT::Clause::getClauseTheorem(), and getDerivation().

Referenced by push(), resolveTheoryImplication(), and search().

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 addClause(), MiniSat::Clause::getTheorem(), MiniSat::Clause::id(), nextClauseID(), and MiniSat::Clause::size().

void Solver::addClause ( const SAT::Clause &  clause,
bool  isTheoryClause 
)

Definition at line 488 of file minisat_solver.cpp.

References addClause(), MiniSat::cvcToMiniSat(), SAT::Clause::getClauseTheorem(), getDerivation(), nextClauseID(), and MiniSat::Derivation::registerInputClause().

void Solver::addFormula ( const SAT::CNF_Formula &  cnf,
bool  isTheoryClause 
)

Definition at line 529 of file minisat_solver.cpp.

References addClause(), SAT::CNF_Formula::begin(), and SAT::CNF_Formula::end().

Referenced by SAT::DPLLTMiniSat::addAssertion(), SAT::DPLLTMiniSat::checkSat(), SAT::DPLLTMiniSat::continueCheck(), push(), and search().

int MiniSat::Solver::nextClauseID (  )  [inline]

Definition at line 636 of file minisat_solver.h.

References d_clauseIDCounter, and FatalAssert.

Referenced by addClause(), analyze(), MiniSat::Derivation::computeRootReason(), createFrom(), MiniSat::Derivation::finish(), and resolveTheoryImplication().

void Solver::simplifyDB (  ) 

Definition at line 1816 of file minisat_solver.cpp.

References MiniSat::SolverStats::clauses_literals, d_clauses, d_learnts, d_qhead, d_rootLevel, d_simpDB_assigns, d_simpDB_props, d_stats, d_trail, MiniSat::SolverStats::db_simpl, DebugAssert, MiniSat::SolverStats::del_clauses, getLevel(), getValue(), isConflicting(), isImpliedAt(), isReason(), MiniSat::l_False, MiniSat::l_True, MiniSat::SolverStats::learnts_literals, MiniSat::Clause::pushID(), and MiniSat::Clause::size().

Referenced by push(), and search().

void Solver::reduceDB (  ) 

Definition at line 1781 of file minisat_solver.cpp.

References d_cla_inc, d_learnts, d_simpRD_learnts, d_stats, MiniSat::SolverStats::del_lemmas, isReason(), and MiniSat::SolverStats::lm_simpl.

CVC3::QueryResult Solver::search (  ) 

search

Definition at line 2005 of file minisat_solver.cpp.

References CVC3::ABORT, addFormula(), allClausesSatisfied(), analyze(), SAT::DPLLT::DPLLT::TheoryAPI::assertLit(), assume(), backtrack(), SAT::DPLLT::DPLLT::TheoryAPI::checkConsistent(), claDecayActivity(), MiniSat::SearchParams::clause_decay, MiniSat::SolverStats::conflicts, SAT::DPLLT::CONSISTENT, cvcToMiniSat(), d_cla_decay, d_conflict, d_decider, d_default_params, d_inSearch, d_ok, d_order, d_popRequests, d_pushes, d_qhead, d_rootLevel, d_stats, d_thead, d_theoryAPI, d_trail, d_trail_lim, d_var_decay, MiniSat::SolverStats::debug, DebugAssert, decisionLevel(), MiniSat::SolverStats::decisions, defer_theory_propagation, eager_explanation, std::endl(), enqueue(), FatalAssert, MiniSat::Derivation::finish(), getDerivation(), SAT::DPLLT::DPLLT::TheoryAPI::getExplanation(), SAT::DPLLT::DPLLT::TheoryAPI::getImplication(), SAT::DPLLT::DPLLT::TheoryAPI::getNewClauses(), getValue(), SAT::DPLLT::INCONSISTENT, MiniSat::Lit::index(), isConflicting(), SAT::Lit::isNull(), MiniSat::l_Undef, MiniSat::lit_Undef(), SAT::DPLLT::DPLLT::Decider::makeDecision(), SAT::DPLLT::MAYBE_CONSISTENT, MiniSat::miniSatToCVC(), nAssigns(), SAT::DPLLT::DPLLT::TheoryAPI::outOfResources(), SAT::CNF_Formula::print(), printState(), propagate(), propLookahead(), protocol, protocolPropagation(), SAT::DPLLT::DPLLT::TheoryAPI::push(), MiniSat::SearchParams::random_var_freq, SAT::CNF_Formula_Impl::reset(), CVC3::SATISFIABLE, MiniSat::VarOrder::select(), simplifyDB(), MiniSat::SolverStats::starts, MiniSat::SolverStats::theory_conflicts, MiniSat::Clause::TheoryImplication(), toString(), CVC3::UNSATISFIABLE, MiniSat::SearchParams::var_decay, MiniSat::var_Undef, and varDecayActivity().

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 addFormula(), SAT::DPLLT::DPLLT::TheoryAPI::assertLit(), cvcToMiniSat(), d_clauseIDCounter, d_derivation, d_ok, d_popLemmas, d_pushes, d_qhead, d_registeredVars, d_stats, d_thead, d_theoryAPI, d_trail, DebugAssert, decisionLevel(), defer_theory_propagation, eager_explanation, std::endl(), enqueue(), SAT::DPLLT::DPLLT::TheoryAPI::getExplanation(), SAT::DPLLT::DPLLT::TheoryAPI::getImplication(), SAT::DPLLT::DPLLT::TheoryAPI::getNewClauses(), MiniSat::Clause::id(), MiniSat::Lit::index(), inSearch(), insertLemma(), isConflicting(), SAT::Lit::isNull(), MiniSat::SolverStats::learnts_literals, MiniSat::miniSatToCVC(), SAT::CNF_Formula::print(), printState(), propagate(), protocol, protocolPropagation(), MiniSat::Derivation::push(), push_theory_clause, push_theory_implication, push_theory_propagation, MiniSat::Clause::pushID(), SAT::CNF_Formula_Impl::reset(), simplifyDB(), MiniSat::Clause::size(), and MiniSat::Clause::TheoryImplication().

Referenced by SAT::DPLLTMiniSat::push().

void Solver::popTheories (  ) 

Definition at line 2641 of file minisat_solver.cpp.

References d_rootLevel, d_theoryAPI, decisionLevel(), and SAT::DPLLT::DPLLT::TheoryAPI::pop().

Referenced by requestPop().

void Solver::requestPop (  ) 

Definition at line 2621 of file minisat_solver.cpp.

References d_popRequests, DebugAssert, inPush(), 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::addAssertion(), SAT::DPLLTMiniSat::checkSat(), SAT::DPLLTMiniSat::continueCheck(), and SAT::DPLLTMiniSat::push().

bool MiniSat::Solver::inPush (  )  const [inline]

Definition at line 692 of file minisat_solver.h.

References d_popRequests, and d_pushes.

Referenced by SAT::DPLLTMiniSat::continueCheck(), SAT::DPLLTMiniSat::pop(), and requestPop().

lbool MiniSat::Solver::getValue ( Var  x  )  const [inline]

clauses / assignment

Definition at line 699 of file minisat_solver.h.

References d_assigns, and MiniSat::toLbool().

Referenced by allClausesSatisfied(), analyze(), checkClause(), MiniSat::Derivation::computeRootReason(), enqueue(), getConflictLevel(), getImplicationLevel(), getReason(), SAT::DPLLTMiniSat::getValue(), insertClause(), insertLemma(), isPermSatisfied(), orderClause(), propagate(), resolveTheoryImplication(), search(), simplifyClause(), simplifyDB(), toString(), and updateConflict().

lbool MiniSat::Solver::getValue ( Lit  p  )  const [inline]

Definition at line 700 of file minisat_solver.h.

References getValue(), MiniSat::Lit::sign(), 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 allClausesSatisfied(), analyze(), analyze_minimize(), analyze_removable(), backtrack(), checkTrail(), checkWatched(), getConflictLevel(), getImplicationLevel(), insertClause(), isPermSatisfied(), orderClause(), propagate(), protocolPropagation(), simplifyClause(), and simplifyDB().

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 enqueue(), and resolveTheoryImplication().

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 d_reason, and MiniSat::Clause::size().

Referenced by pop(), reduceDB(), and simplifyDB().

Clause* MiniSat::Solver::getReason ( Var  var  )  const [inline]

Definition at line 715 of file minisat_solver.h.

References d_reason.

Referenced by addClause(), analyze(), analyze_minimize(), analyze_removable(), MiniSat::Derivation::computeRootReason(), printDIMACS(), printState(), protocolPropagation(), and setPushID().

Clause * Solver::getReason ( Lit  literal,
bool  resolveTheoryImplication = true 
)

Definition at line 950 of file minisat_solver.cpp.

References d_reason, DebugAssert, getValue(), MiniSat::l_True, resolveTheoryImplication(), MiniSat::Clause::TheoryImplication(), and MiniSat::Lit::var().

const std::vector<Clause*>& MiniSat::Solver::getClauses (  )  const [inline]

Definition at line 722 of file minisat_solver.h.

References d_clauses.

Referenced by createFrom(), and SAT::DPLLTMiniSat::search().

const std::vector<Clause*>& MiniSat::Solver::getLemmas (  )  const [inline]

Definition at line 725 of file minisat_solver.h.

References d_learnts.

Referenced by createFrom(), and SAT::DPLLTMiniSat::search().

const std::vector<Lit>& MiniSat::Solver::getTrail (  )  const [inline]

Definition at line 728 of file minisat_solver.h.

References d_trail.

Referenced by createFrom().

Derivation* MiniSat::Solver::getDerivation (  )  [inline]

Definition at line 731 of file minisat_solver.h.

References d_derivation.

Referenced by addClause(), analyze(), analyze_minimize(), cvcToMiniSat(), insertClause(), insertLemma(), remove(), 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]

Definition at line 739 of file minisat_solver.h.

References d_trail.

Referenced by search().

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 printDIMACS(), registerVar(), SAT::DPLLTMiniSat::search(), 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 getValue(), MiniSat::l_False, MiniSat::l_True, and MiniSat::Lit::toString().

Referenced by allClausesSatisfied(), checkClause(), checkWatched(), printDIMACS(), printState(), protocolPropagation(), search(), and toString().

std::string Solver::toString ( const std::vector< Lit > &  clause,
bool  showAssignment 
) const

Definition at line 334 of file minisat_solver.cpp.

References std::endl(), and toString().

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 d_clauses, d_learnts, d_trail, MiniSat::Clause::Decision(), std::endl(), getReason(), and toString().

Referenced by checkClause(), checkWatched(), push(), and search().

void Solver::printDIMACS (  )  const

Definition at line 405 of file minisat_solver.cpp.

References d_clauses, d_trail, MiniSat::Clause::Decision(), std::endl(), getReason(), nVars(), MiniSat::Clause::size(), toString(), and MiniSat::Lit::var().

std::vector< SAT::Lit > Solver::curAssigns (  ) 

Definition at line 351 of file minisat_solver.cpp.

References d_trail, std::endl(), 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 d_clauses, std::endl(), and MiniSat::miniSatToCVC().

Referenced by SAT::DPLLTMiniSat::getCurClauses().

Member Data Documentation

const int MiniSat::Solver::d_rootLevel = 0 [static, protected]

variables

Definition at line 205 of file minisat_solver.h.

Referenced by allClausesSatisfied(), analyze(), analyze_minimize(), analyze_removable(), backtrack(), checkWatched(), getConflictLevel(), getImplicationLevel(), insertClause(), insertLemma(), isPermSatisfied(), popTheories(), propagate(), search(), simplifyClause(), and simplifyDB().

bool MiniSat::Solver::d_inSearch [protected]

status

Definition at line 210 of file minisat_solver.h.

Referenced by inSearch(), pop(), and search().

bool MiniSat::Solver::d_ok [protected]

Definition at line 213 of file minisat_solver.h.

Referenced by insertClause(), pop(), push(), and search().

Clause* MiniSat::Solver::d_conflict [protected]

Definition at line 241 of file minisat_solver.h.

Referenced by analyze(), insertClause(), isConflicting(), pop(), search(), and updateConflict().

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 getWatches(), and registerVar().

std::vector<char> MiniSat::Solver::d_assigns [protected]

Definition at line 251 of file minisat_solver.h.

Referenced by backtrack(), checkTrail(), enqueue(), getValue(), nVars(), pop(), propLookahead(), and registerVar().

std::vector<Lit> MiniSat::Solver::d_trail [protected]

Definition at line 256 of file minisat_solver.h.

Referenced by analyze(), assume(), backtrack(), checkTrail(), curAssigns(), enqueue(), getTrail(), nAssigns(), pop(), printDIMACS(), printState(), propagate(), propLookahead(), protocolPropagation(), push(), registerVar(), search(), and simplifyDB().

std::vector<int> MiniSat::Solver::d_trail_lim [protected]

Definition at line 260 of file minisat_solver.h.

Referenced by assume(), backtrack(), decisionLevel(), pop(), propLookahead(), and search().

std::vector<size_type> MiniSat::Solver::d_trail_pos [protected]

Definition at line 264 of file minisat_solver.h.

Referenced by analyze_minimize(), backtrack(), enqueue(), and registerVar().

size_type MiniSat::Solver::d_qhead [protected]

Definition at line 269 of file minisat_solver.h.

Referenced by backtrack(), pop(), propagate(), propLookahead(), protocolPropagation(), push(), search(), and simplifyDB().

size_type MiniSat::Solver::d_thead [protected]

Definition at line 273 of file minisat_solver.h.

Referenced by backtrack(), pop(), propagate(), push(), and search().

std::vector<Clause*> MiniSat::Solver::d_reason [protected]

Definition at line 278 of file minisat_solver.h.

Referenced by addClause(), backtrack(), checkTrail(), enqueue(), getReason(), isReason(), pop(), propLookahead(), registerVar(), and resolveTheoryImplication().

std::vector<int> MiniSat::Solver::d_level [protected]

Definition at line 284 of file minisat_solver.h.

Referenced by getLevel(), registerVar(), 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(), pop(), push(), and registerVar().

int MiniSat::Solver::d_clauseIDCounter [protected]

Clauses.

Definition at line 300 of file minisat_solver.h.

Referenced by nextClauseID(), and push().

std::vector<Clause*> MiniSat::Solver::d_clauses [protected]

Definition at line 303 of file minisat_solver.h.

Referenced by allClausesSatisfied(), checkClauses(), checkWatched(), curClauses(), getClauses(), insertClause(), nClauses(), pop(), printDIMACS(), printState(), simplifyDB(), and ~Solver().

std::vector<Clause*> MiniSat::Solver::d_learnts [protected]

Definition at line 306 of file minisat_solver.h.

Referenced by checkClauses(), checkWatched(), claRescaleActivity(), getLemmas(), insertClause(), insertLemma(), nLearnts(), pop(), printState(), reduceDB(), simplifyDB(), and ~Solver().

std::queue<Clause*> MiniSat::Solver::d_pendingClauses [protected]

Temporary clauses.

Definition at line 314 of file minisat_solver.h.

Referenced by backtrack(), insertClause(), pop(), and ~Solver().

std::stack<std::pair<int, Clause*> > MiniSat::Solver::d_theoryExplanations [protected]

Definition at line 319 of file minisat_solver.h.

Referenced by backtrack(), pop(), resolveTheoryImplication(), and ~Solver().

std::vector<PushEntry> MiniSat::Solver::d_pushes [protected]

Push / Pop.

Definition at line 325 of file minisat_solver.h.

Referenced by analyze_minimize(), doPops(), inPush(), isImpliedAt(), pop(), push(), and search().

std::vector<Clause*> MiniSat::Solver::d_popLemmas [protected]

Definition at line 328 of file minisat_solver.h.

Referenced by pop(), and push().

std::vector<int> MiniSat::Solver::d_pushIDs [protected]

Definition at line 343 of file minisat_solver.h.

Referenced by getPushID(), registerVar(), and setPushID().

unsigned int MiniSat::Solver::d_popRequests [protected]

Definition at line 350 of file minisat_solver.h.

Referenced by doPops(), inPush(), inSearch(), pop(), requestPop(), and search().

double MiniSat::Solver::d_cla_inc [protected]

heuristics

Definition at line 359 of file minisat_solver.h.

Referenced by claBumpActivity(), claDecayActivity(), claRescaleActivity(), createFrom(), and reduceDB().

double MiniSat::Solver::d_cla_decay [protected]

Definition at line 361 of file minisat_solver.h.

Referenced by claDecayActivity(), and search().

std::vector<double> MiniSat::Solver::d_activity [protected]

Definition at line 366 of file minisat_solver.h.

Referenced by createFrom(), registerVar(), varBumpActivity(), and varRescaleActivity().

double MiniSat::Solver::d_var_inc [protected]

Definition at line 368 of file minisat_solver.h.

Referenced by createFrom(), varBumpActivity(), varDecayActivity(), and varRescaleActivity().

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 backtrack(), pop(), propLookahead(), registerVar(), search(), 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 backtrack(), createFrom(), popTheories(), propagate(), push(), and search().

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 backtrack(), createFrom(), enqueue(), getDerivation(), pop(), push(), registerVar(), Solver(), and ~Solver().

SearchParams MiniSat::Solver::d_default_params [protected]

Mode of operation:.

Definition at line 403 of file minisat_solver.h.

Referenced by search().

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 analyze(), analyze_minimize(), analyze_removable(), and registerVar().

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 assume(), getStats(), insertClause(), insertLemma(), pop(), propagate(), push(), reduceDB(), remove(), search(), and simplifyDB().

The documentation for this class was generated from the following files:
Generated on Thu Oct 15 22:27:20 2009 for CVC3 by  doxygen 1.5.8