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


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 backtrack(), createFrom(), isConsistent(), propLookahead(), push(), search(), and simplifyDB().

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

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]

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

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]

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

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]

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]

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]

void Solver::protocolPropagation (  )  const [protected]

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

Clause * Solver::cvcToMiniSat ( const SAT::Clause clause,
int  id 
)

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

void Solver::popTheories (  ) 

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

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]

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]

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]

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

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

void Solver::printDIMACS (  )  const

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]

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

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]

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

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

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]

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

Definition at line 284 of file minisat_solver.h.

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

Definition at line 294 of file minisat_solver.h.

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

Clauses.

Definition at line 300 of file minisat_solver.h.

Referenced by nextClauseID(), and push().

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

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

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]

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

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

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

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


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