#include <minisat_derivation.h>
Collaboration diagram for MiniSat::Derivation:
Definition at line 81 of file minisat_derivation.h.
typedef Hash::hash_map<int, Clause*> MiniSat::Derivation::TClauses |
Definition at line 83 of file minisat_derivation.h.
typedef Hash::hash_set<int> MiniSat::Derivation::TInputClauses |
Definition at line 84 of file minisat_derivation.h.
typedef Hash::hash_map<int, Inference*> MiniSat::Derivation::TInferences |
Definition at line 85 of file minisat_derivation.h.
MiniSat::Derivation::Derivation | ( | ) | [inline] |
Definition at line 112 of file minisat_derivation.h.
Derivation::~Derivation | ( | ) |
Definition at line 43 of file minisat_derivation.cpp.
References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::begin(), d_inferences, d_removedClauses, d_unitClauses, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), and MiniSat::xfree().
void MiniSat::Derivation::registerClause | ( | Clause * | clause | ) | [inline] |
Definition at line 120 of file minisat_derivation.h.
References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::contains(), d_clauses, DebugAssert, MiniSat::Clause::id(), IF_DEBUG, and MiniSat::Clause::size().
Referenced by MiniSat::Solver::addClause(), computeRootReason(), finish(), and MiniSat::Solver::insertClause().
void MiniSat::Derivation::registerInputClause | ( | int | clauseID | ) | [inline] |
Definition at line 152 of file minisat_derivation.h.
References d_inputClauses, and Hash::hash_set< _Key, _HashFcn, _EqualKey >::insert().
Referenced by MiniSat::Solver::addClause().
void MiniSat::Derivation::removedClause | ( | Clause * | clause | ) | [inline] |
Definition at line 158 of file minisat_derivation.h.
References d_removedClauses, and DebugAssert.
Referenced by MiniSat::Solver::addClause(), finish(), and MiniSat::Solver::remove().
void MiniSat::Derivation::registerInference | ( | int | clauseID, | |
Inference * | inference | |||
) | [inline] |
Definition at line 164 of file minisat_derivation.h.
References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::contains(), d_inferences, and DebugAssert.
Referenced by MiniSat::Solver::addClause(), MiniSat::Solver::analyze(), computeRootReason(), and finish().
Definition at line 61 of file minisat_derivation.cpp.
References MiniSat::Inference::add(), MiniSat::Clause_new(), d_unitClauses, DebugAssert, MiniSat::Clause::Decision(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find(), MiniSat::Solver::getReason(), MiniSat::Solver::getValue(), MiniSat::Clause::id(), IF_DEBUG, MiniSat::Lit::index(), MiniSat::l_False, MiniSat::l_True, MiniSat::Solver::nextClauseID(), registerClause(), registerInference(), and MiniSat::Clause::size().
Referenced by finish().
Definition at line 108 of file minisat_derivation.cpp.
References MiniSat::Inference::add(), MiniSat::Clause_new(), computeRootReason(), d_emptyClause, DebugAssert, MiniSat::Clause::id(), MiniSat::Solver::nextClauseID(), registerClause(), registerInference(), removedClause(), and MiniSat::Clause::size().
Referenced by MiniSat::Solver::search().
void Derivation::printProof | ( | Clause * | clause | ) |
Definition at line 141 of file minisat_derivation.cpp.
References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::contains(), Hash::hash_set< _Key, _HashFcn, _EqualKey >::contains(), d_clauses, d_inferences, d_inputClauses, DebugAssert, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), std::endl(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find(), MiniSat::Inference::getStart(), MiniSat::Inference::getSteps(), MiniSat::Clause::id(), and MiniSat::Inference::toString().
void Derivation::printProof | ( | ) |
void Derivation::push | ( | int | clauseID | ) |
void Derivation::pop | ( | int | clauseID | ) |
Definition at line 208 of file minisat_derivation.cpp.
References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::begin(), d_clauses, d_emptyClause, d_inferences, d_removedClauses, d_unitClauses, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::erase(), MiniSat::Clause::pushID(), and MiniSat::xfree().
Referenced by MiniSat::Solver::pop().
TClauses MiniSat::Derivation::d_clauses [private] |
Definition at line 89 of file minisat_derivation.h.
Referenced by pop(), printProof(), and registerClause().
Definition at line 96 of file minisat_derivation.h.
Referenced by printProof(), and registerInputClause().
TClauses MiniSat::Derivation::d_unitClauses [private] |
Definition at line 100 of file minisat_derivation.h.
Referenced by computeRootReason(), pop(), and ~Derivation().
TInferences MiniSat::Derivation::d_inferences [private] |
Definition at line 103 of file minisat_derivation.h.
Referenced by pop(), printProof(), registerInference(), and ~Derivation().
std::deque<Clause*> MiniSat::Derivation::d_removedClauses [private] |
Definition at line 106 of file minisat_derivation.h.
Referenced by pop(), removedClause(), and ~Derivation().
Clause* MiniSat::Derivation::d_emptyClause [private] |
Definition at line 109 of file minisat_derivation.h.
Referenced by finish(), pop(), and printProof().