CVC3  2.4.1
Public Member Functions | Static Public Member Functions | Protected Member Functions | Protected Attributes | Static Protected Attributes
MiniSat::Solver Class Reference

#include <minisat_solver.h>

List of all members.

Public Member Functions

Static Public Member Functions

Protected Member Functions

Protected Attributes

Static Protected Attributes


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

Member Function Documentation

int MiniSat::Solver::decisionLevel ( ) const [inline, protected]
bool Solver::assume ( Lit  p) [protected]
bool Solver::enqueue ( Lit  fact,
int  decisionLevel,
Clause reason 
) [protected]
void Solver::propagate ( ) [protected]
void Solver::propLookahead ( const SearchParams params) [protected]
Clause * Solver::analyze ( int &  out_btlevel) [protected]
void Solver::analyze_minimize ( std::vector< Lit > &  out_learnt,
Inference inference,
int &  pushID 
) [protected]
bool Solver::analyze_removable ( Lit  p,
unsigned int  min_level,
int  pushID 
) [protected]
void Solver::backtrack ( int  level,
Clause clause 
) [protected]
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]
int Solver::getImplicationLevel ( const Clause clause) const [protected]
int Solver::getConflictLevel ( const Clause clause) const [protected]
void Solver::resolveTheoryImplication ( Lit  literal) [protected]
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().

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

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]

Conflict handling.

Definition at line 889 of file minisat_solver.cpp.

References DebugAssert.

Referenced by remove(), and pop().

void Solver::registerVar ( Var  var) [protected]
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]
void Solver::insertClause ( Clause clause) [protected]
void Solver::insertLemma ( const Clause lemma,
int  clauseID,
int  pushID 
) [protected]
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]
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]
void Solver::setPushID ( Var  var,
Clause from 
) [protected]
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]
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]
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]
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]
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]
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]
void Solver::protocolPropagation ( ) const [protected]
Solver * Solver::createFrom ( const Solver solver) [static]
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 
)
void Solver::addClause ( const SAT::Clause clause,
bool  isTheoryClause 
)
void Solver::addFormula ( const SAT::CNF_Formula cnf,
bool  isTheoryClause 
)
int MiniSat::Solver::nextClauseID ( ) [inline]
void Solver::simplifyDB ( )
void Solver::reduceDB ( )
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  )
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 ( )
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().

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

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

Clause* MiniSat::Solver::getReason ( Var  var) const [inline]
Clause * Solver::getReason ( Lit  literal,
bool  resolveTheoryImplication = true 
)
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]

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 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]

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 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
void Solver::printDIMACS ( ) const
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().


Member Data Documentation

const int MiniSat::Solver::d_rootLevel = 0 [static, protected]
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().

Definition at line 241 of file minisat_solver.h.

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

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 260 of file minisat_solver.h.

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

Definition at line 264 of file minisat_solver.h.

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

Definition at line 273 of file minisat_solver.h.

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

Definition at line 284 of file minisat_solver.h.

Referenced by registerVar(), getLevel(), and setLevel().

Definition at line 294 of file minisat_solver.h.

Referenced by isRegistered(), registerVar(), push(), and pop().

Clauses.

Definition at line 300 of file minisat_solver.h.

Referenced by push(), and nextClauseID().

Temporary clauses.

Definition at line 314 of file minisat_solver.h.

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

Definition at line 319 of file minisat_solver.h.

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

Push / Pop.

Definition at line 325 of file minisat_solver.h.

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

Definition at line 328 of file minisat_solver.h.

Referenced by push(), and pop().

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

Definition at line 366 of file minisat_solver.h.

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

double MiniSat::Solver::d_var_inc [protected]
double MiniSat::Solver::d_var_decay [protected]

Definition at line 371 of file minisat_solver.h.

Referenced by search(), varBumpActivity(), and varDecayActivity().

Definition at line 373 of file minisat_solver.h.

Referenced by registerVar(), backtrack(), propLookahead(), search(), pop(), and varBumpActivity().

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

Definition at line 382 of file minisat_solver.h.

Referenced by reduceDB().

CVC interface.

Definition at line 388 of file minisat_solver.h.

Referenced by createFrom(), backtrack(), propagate(), search(), push(), and popTheories().

Definition at line 391 of file minisat_solver.h.

Referenced by createFrom(), and search().

proof logging

Definition at line 397 of file minisat_solver.h.

Referenced by Solver(), createFrom(), ~Solver(), registerVar(), backtrack(), enqueue(), push(), pop(), and getDerivation().

Mode of operation:

Definition at line 403 of file minisat_solver.h.

Referenced by search().

Definition at line 406 of file minisat_solver.h.

Referenced by analyze_minimize().

Temporaries (to reduce allocation overhead).

Definition at line 412 of file minisat_solver.h.

Referenced by registerVar(), analyze(), analyze_minimize(), and analyze_removable().

Definition at line 413 of file minisat_solver.h.

Referenced by analyze_removable().

Definition at line 414 of file minisat_solver.h.

Referenced by analyze(), analyze_minimize(), and analyze_removable().


The documentation for this class was generated from the following files: