CVC3
2.4.1
|
#include <minisat_solver.h>
Public Member Functions | |
Solver (SAT::DPLLT::TheoryAPI *theoryAPI, SAT::DPLLT::Decider *decider, bool logDerivation) | |
Initialization. More... | |
~Solver () | |
Clause * | cvcToMiniSat (const SAT::Clause &clause, int id) |
problem specification More... | |
void | addClause (Lit p, CVC3::Theorem theorem) |
void | addClause (const Clause &clause, bool keepClauseID) |
void | addClause (const SAT::Clause &clause, bool isTheoryClause) |
void | addFormula (const SAT::CNF_Formula &cnf, bool isTheoryClause) |
int | nextClauseID () |
void | simplifyDB () |
void | reduceDB () |
CVC3::QueryResult | search () |
search More... | |
Derivation * | getProof () |
bool | inSearch () const |
bool | isConsistent () const |
void | push () |
Push / Pop. More... | |
void | popTheories () |
void | requestPop () |
void | doPops () |
bool | inPush () const |
lbool | getValue (Var x) const |
clauses / assignment More... | |
lbool | getValue (Lit p) const |
int | getLevel (Var var) const |
int | getLevel (Lit lit) const |
void | setLevel (Var var, int level) |
void | setLevel (Lit lit, int level) |
bool | isReason (const Clause *c) const |
Clause * | getReason (Var var) const |
Clause * | getReason (Lit literal, bool resolveTheoryImplication=true) |
const std::vector< Clause * > & | getClauses () const |
const std::vector< Clause * > & | getLemmas () const |
const std::vector< Lit > & | getTrail () const |
Derivation * | getDerivation () |
const SolverStats & | getStats () const |
Statistics. More... | |
int | nAssigns () const |
int | nClauses () const |
int | nLearnts () const |
int | nVars () const |
std::string | toString (Lit literal, bool showAssignment) const |
String representation: More... | |
std::string | toString (const std::vector< Lit > &clause, bool showAssignment) const |
std::string | toString (const Clause &clause, bool showAssignment) const |
void | printState () const |
void | printDIMACS () const |
std::vector< SAT::Lit > | curAssigns () |
std::vector< std::vector < SAT::Lit > > | curClauses () |
Static Public Member Functions | |
static Solver * | createFrom (const Solver *solver) |
Protected Member Functions | |
int | decisionLevel () const |
Search: More... | |
bool | assume (Lit p) |
bool | enqueue (Lit fact, int decisionLevel, Clause *reason) |
void | propagate () |
void | propLookahead (const SearchParams ¶ms) |
Clause * | analyze (int &out_btlevel) |
Conflict handling. More... | |
void | analyze_minimize (std::vector< Lit > &out_learnt, Inference *inference, int &pushID) |
bool | analyze_removable (Lit p, unsigned int min_level, int pushID) |
void | backtrack (int level, Clause *clause) |
bool | isConflicting () const |
void | updateConflict (Clause *clause) |
int | getImplicationLevel (const Clause &clause) const |
int | getConflictLevel (const Clause &clause) const |
void | resolveTheoryImplication (Lit literal) |
std::vector< Clause * > & | getWatches (Lit literal) |
unit propagation More... | |
const std::vector< Clause * > & | getWatches (Lit literal) const |
void | addWatch (Lit literal, Clause *clause) |
void | removeWatch (std::vector< Clause * > &ws, Clause *elem) |
Conflict handling. More... | |
void | registerVar (Var var) |
Operations on clauses: More... | |
bool | isRegistered (Var var) |
Operations on clauses: More... | |
void | addClause (std::vector< Lit > &literals, CVC3::Theorem theorem, int clauseID) |
void | insertClause (Clause *clause) |
void | insertLemma (const Clause *lemma, int clauseID, int pushID) |
bool | simplifyClause (std::vector< Lit > &literals, int clausePushID) const |
void | orderClause (std::vector< Lit > &literals) const |
void | remove (Clause *c, bool just_dealloc=false) |
bool | isImpliedAt (Lit lit, int clausePushID) const |
bool | isPermSatisfied (Clause *c) const |
void | setPushID (Var var, Clause *from) |
int | getPushID (Var var) const |
int | getPushID (Lit lit) const |
void | pop () |
void | popClauses (const PushEntry &pushEntry, std::vector< Clause * > &clauses) |
void | varBumpActivity (Lit p) |
Activity: More... | |
void | varDecayActivity () |
void | varRescaleActivity () |
Activity. More... | |
void | claDecayActivity () |
void | claRescaleActivity () |
void | claBumpActivity (Clause *c) |
bool | allClausesSatisfied () |
debugging More... | |
void | checkWatched (const Clause &clause) const |
void | checkWatched () const |
void | checkClause (const Clause &clause) const |
void | checkClauses () const |
void | checkTrail () const |
void | protocolPropagation () const |
Protected Attributes | |
bool | d_inSearch |
status More... | |
bool | d_ok |
Clause * | d_conflict |
std::vector< std::vector < Clause * > > | d_watches |
variable assignments, and pending propagations More... | |
std::vector< signed char > | d_assigns |
std::vector< Lit > | d_trail |
std::vector< int > | d_trail_lim |
std::vector< size_type > | d_trail_pos |
size_type | d_qhead |
size_type | d_thead |
std::vector< Clause * > | d_reason |
std::vector< int > | d_level |
std::vector< Hash::hash_set < Var > > | d_registeredVars |
int | d_clauseIDCounter |
Clauses. More... | |
std::vector< Clause * > | d_clauses |
std::vector< Clause * > | d_learnts |
std::queue< Clause * > | d_pendingClauses |
Temporary clauses. More... | |
std::stack< std::pair< int, Clause * > > | d_theoryExplanations |
std::vector< PushEntry > | d_pushes |
Push / Pop. More... | |
std::vector< Clause * > | d_popLemmas |
std::vector< int > | d_pushIDs |
unsigned int | d_popRequests |
double | d_cla_inc |
heuristics More... | |
double | d_cla_decay |
std::vector< double > | d_activity |
double | d_var_inc |
double | d_var_decay |
VarOrder | d_order |
int | d_simpDB_assigns |
int64_t | d_simpDB_props |
int | d_simpRD_learnts |
SAT::DPLLT::TheoryAPI * | d_theoryAPI |
CVC interface. More... | |
SAT::DPLLT::Decider * | d_decider |
Derivation * | d_derivation |
proof logging More... | |
SearchParams | d_default_params |
Mode of operation: More... | |
bool | d_expensive_ccmin |
std::vector< char > | d_analyze_seen |
Temporaries (to reduce allocation overhead). More... | |
std::vector< Lit > | d_analyze_stack |
std::vector< Lit > | d_analyze_redundant |
SolverStats | d_stats |
Static Protected Attributes | |
static const int | d_rootLevel = 0 |
variables More... | |
Definition at line 200 of file minisat_solver.h.
Solver::Solver | ( | SAT::DPLLT::TheoryAPI * | theoryAPI, |
SAT::DPLLT::Decider * | decider, | ||
bool | logDerivation | ||
) |
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().
|
inlineprotected |
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().
|
protected |
Definition at line 1473 of file minisat_solver.cpp.
References d_stats, d_trail, d_trail_lim, MiniSat::Clause::Decision(), decisionLevel(), enqueue(), CVC3::max(), and MiniSat::SolverStats::max_level.
Referenced by propLookahead(), and search().
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().
|
protected |
Definition at line 1689 of file minisat_solver.cpp.
References addWatch(), SAT::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().
|
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().
|
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().
|
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().
|
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().
|
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::TheoryAPI::pop(), MiniSat::toInt(), MiniSat::VarOrder::undo(), and MiniSat::xfree().
Referenced by search().
|
protected |
Definition at line 973 of file minisat_solver.cpp.
References d_conflict.
Referenced by backtrack(), createFrom(), isConsistent(), propLookahead(), push(), search(), and simplifyDB().
|
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().
|
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().
|
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().
|
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().
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().
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 insertClause(), insertLemma(), and propagate().
|
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().
|
protected |
Operations on clauses:
Definition at line 448 of file minisat_solver.cpp.
References d_registeredVars.
Referenced by propLookahead(), and registerVar().
|
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().
|
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().
|
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().
|
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().
|
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().
|
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().
|
protected |
Definition at line 1443 of file minisat_solver.cpp.
References d_pushes, and getPushID().
Referenced by isPermSatisfied(), simplifyClause(), and simplifyDB().
|
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().
Definition at line 2496 of file minisat_solver.cpp.
References d_pushIDs, DebugAssert, MiniSat::Clause::Decision(), getPushID(), getReason(), CVC3::max(), MiniSat::Clause::pushID(), MiniSat::Clause::size(), and MiniSat::Clause::TheoryImplication().
Referenced by enqueue(), and resolveTheoryImplication().
|
inlineprotected |
Definition at line 540 of file minisat_solver.h.
References d_pushIDs.
Referenced by analyze_minimize(), isImpliedAt(), and setPushID().
|
inlineprotected |
Definition at line 541 of file minisat_solver.h.
References getPushID(), and MiniSat::Lit::var().
Referenced by getPushID().
|
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().
|
protected |
Definition at line 2647 of file minisat_solver.cpp.
References MiniSat::PushEntry::d_clauseID.
Referenced by pop().
|
inlineprotected |
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().
|
inlineprotected |
Definition at line 554 of file minisat_solver.h.
References d_var_decay, and d_var_inc.
Referenced by search().
|
protected |
Activity.
Definition at line 2290 of file minisat_solver.cpp.
References d_activity, d_var_inc, and nVars().
Referenced by varBumpActivity().
|
inlineprotected |
Definition at line 556 of file minisat_solver.h.
References d_cla_decay, and d_cla_inc.
Referenced by search().
|
protected |
Definition at line 2299 of file minisat_solver.cpp.
References d_cla_inc, and d_learnts.
Referenced by claBumpActivity().
|
inlineprotected |
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().
|
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().
|
protected |
Definition at line 2359 of file minisat_solver.cpp.
References d_rootLevel, std::endl(), FatalAssert, getLevel(), getWatches(), printState(), MiniSat::Clause::size(), and toString().
|
protected |
Definition at line 2384 of file minisat_solver.cpp.
References d_clauses, d_learnts, and debug_full.
|
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().
|
protected |
Definition at line 2432 of file minisat_solver.cpp.
References checkClause(), d_clauses, d_learnts, and debug_full.
|
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().
|
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().
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(), and nextClauseID().
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(), and SAT::Clause::getClauseTheorem().
Referenced by resolveTheoryImplication().
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().
|
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().
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::TheoryAPI::assertLit(), assume(), backtrack(), SAT::DPLLT::TheoryAPI::checkConsistent(), claDecayActivity(), MiniSat::SearchParams::clause_decay, MiniSat::SolverStats::conflicts, SAT::DPLLT::CONSISTENT, MiniSat::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::TheoryAPI::getExplanation(), SAT::DPLLT::TheoryAPI::getImplication(), SAT::DPLLT::TheoryAPI::getNewClauses(), getValue(), SAT::DPLLT::INCONSISTENT, MiniSat::Lit::index(), isConflicting(), SAT::Lit::isNull(), MiniSat::l_Undef, MiniSat::lit_Undef(), SAT::DPLLT::Decider::makeDecision(), SAT::DPLLT::MAYBE_CONSISTENT, MiniSat::miniSatToCVC(), nAssigns(), SAT::DPLLT::TheoryAPI::outOfResources(), SAT::CNF_Formula::print(), printState(), propagate(), propLookahead(), protocol, protocolPropagation(), SAT::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 | ( | ) |
|
inline |
Definition at line 668 of file minisat_solver.h.
References d_inSearch, and d_popRequests.
Referenced by push().
|
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::TheoryAPI::assertLit(), MiniSat::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::TheoryAPI::getExplanation(), SAT::DPLLT::TheoryAPI::getImplication(), SAT::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::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().
|
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().
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().
Definition at line 700 of file minisat_solver.h.
References getValue(), MiniSat::Lit::sign(), and MiniSat::Lit::var().
Referenced by getValue().
|
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().
|
inline |
Definition at line 704 of file minisat_solver.h.
References getLevel(), and MiniSat::Lit::var().
Referenced by getLevel().
|
inline |
Definition at line 707 of file minisat_solver.h.
References d_level.
Referenced by enqueue(), and resolveTheoryImplication().
|
inline |
Definition at line 708 of file minisat_solver.h.
References setLevel(), and MiniSat::Lit::var().
Referenced by setLevel().
|
inline |
Definition at line 712 of file minisat_solver.h.
References d_reason, and MiniSat::Clause::size().
Referenced by pop(), reduceDB(), and simplifyDB().
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().
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().
|
inline |
Definition at line 722 of file minisat_solver.h.
References d_clauses.
Referenced by createFrom(), and SAT::DPLLTMiniSat::search().
|
inline |
Definition at line 725 of file minisat_solver.h.
References d_learnts.
Referenced by createFrom(), and SAT::DPLLTMiniSat::search().
|
inline |
|
inline |
Definition at line 731 of file minisat_solver.h.
References d_derivation.
Referenced by addClause(), analyze(), analyze_minimize(), insertClause(), insertLemma(), remove(), and search().
|
inline |
Statistics.
Definition at line 736 of file minisat_solver.h.
References d_stats.
Referenced by SAT::DPLLTMiniSat::search().
|
inline |
|
inline |
Definition at line 742 of file minisat_solver.h.
References d_clauses.
|
inline |
Definition at line 745 of file minisat_solver.h.
References d_learnts.
|
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().
|
staticprotected |
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().
|
protected |
status
Definition at line 210 of file minisat_solver.h.
Referenced by inSearch(), pop(), and search().
|
protected |
Definition at line 213 of file minisat_solver.h.
Referenced by insertClause(), pop(), push(), and search().
|
protected |
Definition at line 241 of file minisat_solver.h.
Referenced by analyze(), insertClause(), isConflicting(), pop(), search(), and updateConflict().
|
protected |
variable assignments, and pending propagations
Definition at line 248 of file minisat_solver.h.
Referenced by getWatches(), and registerVar().
|
protected |
Definition at line 251 of file minisat_solver.h.
Referenced by backtrack(), checkTrail(), enqueue(), getValue(), nVars(), pop(), propLookahead(), and registerVar().
|
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().
|
protected |
Definition at line 260 of file minisat_solver.h.
Referenced by assume(), backtrack(), decisionLevel(), pop(), propLookahead(), and search().
|
protected |
Definition at line 264 of file minisat_solver.h.
Referenced by analyze_minimize(), backtrack(), enqueue(), and registerVar().
|
protected |
Definition at line 269 of file minisat_solver.h.
Referenced by backtrack(), pop(), propagate(), propLookahead(), protocolPropagation(), push(), search(), and simplifyDB().
|
protected |
Definition at line 273 of file minisat_solver.h.
Referenced by backtrack(), pop(), propagate(), push(), and search().
|
protected |
Definition at line 278 of file minisat_solver.h.
Referenced by addClause(), backtrack(), checkTrail(), enqueue(), getReason(), isReason(), pop(), propLookahead(), registerVar(), and resolveTheoryImplication().
|
protected |
Definition at line 284 of file minisat_solver.h.
Referenced by getLevel(), registerVar(), and setLevel().
|
protected |
Definition at line 294 of file minisat_solver.h.
Referenced by isRegistered(), pop(), push(), and registerVar().
|
protected |
|
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().
|
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().
|
protected |
Temporary clauses.
Definition at line 314 of file minisat_solver.h.
Referenced by backtrack(), insertClause(), pop(), and ~Solver().
|
protected |
Definition at line 319 of file minisat_solver.h.
Referenced by backtrack(), pop(), resolveTheoryImplication(), and ~Solver().
|
protected |
Push / Pop.
Definition at line 325 of file minisat_solver.h.
Referenced by analyze_minimize(), doPops(), inPush(), isImpliedAt(), pop(), push(), and search().
|
protected |
Definition at line 328 of file minisat_solver.h.
|
protected |
Definition at line 343 of file minisat_solver.h.
Referenced by getPushID(), registerVar(), and setPushID().
|
protected |
Definition at line 350 of file minisat_solver.h.
Referenced by doPops(), inPush(), inSearch(), pop(), requestPop(), and search().
|
protected |
heuristics
Definition at line 359 of file minisat_solver.h.
Referenced by claBumpActivity(), claDecayActivity(), claRescaleActivity(), createFrom(), and reduceDB().
|
protected |
Definition at line 361 of file minisat_solver.h.
Referenced by claDecayActivity(), and search().
|
protected |
Definition at line 366 of file minisat_solver.h.
Referenced by createFrom(), registerVar(), varBumpActivity(), and varRescaleActivity().
|
protected |
Definition at line 368 of file minisat_solver.h.
Referenced by createFrom(), varBumpActivity(), varDecayActivity(), and varRescaleActivity().
|
protected |
Definition at line 371 of file minisat_solver.h.
Referenced by search(), varBumpActivity(), and varDecayActivity().
|
protected |
Definition at line 373 of file minisat_solver.h.
Referenced by backtrack(), pop(), propLookahead(), registerVar(), search(), and varBumpActivity().
|
protected |
Definition at line 378 of file minisat_solver.h.
Referenced by propagate(), and simplifyDB().
|
protected |
Definition at line 380 of file minisat_solver.h.
Referenced by propagate(), and simplifyDB().
|
protected |
Definition at line 382 of file minisat_solver.h.
Referenced by reduceDB().
|
protected |
CVC interface.
Definition at line 388 of file minisat_solver.h.
Referenced by backtrack(), createFrom(), popTheories(), propagate(), push(), and search().
|
protected |
Definition at line 391 of file minisat_solver.h.
Referenced by createFrom(), and search().
|
protected |
proof logging
Definition at line 397 of file minisat_solver.h.
Referenced by backtrack(), createFrom(), enqueue(), getDerivation(), pop(), push(), registerVar(), Solver(), and ~Solver().
|
protected |
|
protected |
Definition at line 406 of file minisat_solver.h.
Referenced by analyze_minimize().
|
protected |
Temporaries (to reduce allocation overhead).
Definition at line 412 of file minisat_solver.h.
Referenced by analyze(), analyze_minimize(), analyze_removable(), and registerVar().
|
protected |
Definition at line 413 of file minisat_solver.h.
Referenced by analyze_removable().
|
protected |
Definition at line 414 of file minisat_solver.h.
Referenced by analyze(), analyze_minimize(), and analyze_removable().
|
protected |
Definition at line 417 of file minisat_solver.h.
Referenced by assume(), getStats(), insertClause(), insertLemma(), pop(), propagate(), push(), reduceDB(), remove(), search(), and simplifyDB().