CVC3  2.4.1
Public Member Functions | Static Public Member Functions | Protected Member Functions | Protected Attributes | Static Protected Attributes | List of all members
MiniSat::Solver Class Reference

#include <minisat_solver.h>

Public Member Functions

 Solver (SAT::DPLLT::TheoryAPI *theoryAPI, SAT::DPLLT::Decider *decider, bool logDerivation)
 Initialization. More...
 
 ~Solver ()
 
ClausecvcToMiniSat (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...
 
DerivationgetProof ()
 
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
 
ClausegetReason (Var var) const
 
ClausegetReason (Lit literal, bool resolveTheoryImplication=true)
 
const std::vector< Clause * > & getClauses () const
 
const std::vector< Clause * > & getLemmas () const
 
const std::vector< Lit > & getTrail () const
 
DerivationgetDerivation ()
 
const SolverStatsgetStats () 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::LitcurAssigns ()
 
std::vector< std::vector
< SAT::Lit > > 
curClauses ()
 

Static Public Member Functions

static SolvercreateFrom (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 &params)
 
Clauseanalyze (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
 
Claused_conflict
 
std::vector< std::vector
< Clause * > > 
d_watches
 variable assignments, and pending propagations More...
 
std::vector< signed char > d_assigns
 
std::vector< Litd_trail
 
std::vector< int > d_trail_lim
 
std::vector< size_typed_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< PushEntryd_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::TheoryAPId_theoryAPI
 CVC interface. More...
 
SAT::DPLLT::Deciderd_decider
 
Derivationd_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< Litd_analyze_stack
 
std::vector< Litd_analyze_redundant
 
SolverStats d_stats
 

Static Protected Attributes

static const int d_rootLevel = 0
 variables More...
 

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.

Solver::~Solver ( )

Member Function Documentation

int MiniSat::Solver::decisionLevel ( ) const
inlineprotected
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)
inlineprotected

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
inlineprotected

Definition at line 481 of file minisat_solver.h.

References d_watches, and MiniSat::Lit::index().

void MiniSat::Solver::addWatch ( Lit  literal,
Clause clause 
)
inlineprotected

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
inlineprotected

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
inlineprotected

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)
inlineprotected
void MiniSat::Solver::varDecayActivity ( )
inlineprotected

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

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

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

Definition at line 731 of file minisat_solver.h.

References d_derivation.

Referenced by addClause(), analyze(), analyze_minimize(), 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
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
staticprotected
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<signed 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().

size_type MiniSat::Solver::d_qhead
protected
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
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
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().

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

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