MiniSat::Derivation Class Reference
#include <minisat_derivation.h>
Public Types
- typedef Hash::hash_map< int,
Clause * > TClauses - typedef Hash::hash_set< int > TInputClauses
- typedef Hash::hash_map< int,
Inference * > TInferences
Public Member Functions
- Derivation ()
- ~Derivation ()
- void registerClause (Clause *clause)
- void registerInputClause (int clauseID)
- void removedClause (Clause *clause)
- void registerInference (int clauseID, Inference *inference)
- int computeRootReason (Lit implied, Solver *solver)
- void finish (Clause *clause, Solver *solver)
- void printDerivation (Clause *clause)
- void printDerivation ()
- void checkDerivation (Clause *clause)
- SAT::SatProof * createProof ()
- SAT::SatProof * createProof (Clause *clause)
- void push (int clauseID)
- void pop (int clauseID)
Private Attributes
- TClauses d_clauses
- TInputClauses d_inputClauses
- TClauses d_unitClauses
- TInferences d_inferences
- std::deque< Clause * > d_removedClauses
- Clause * d_emptyClause
Detailed Description
Definition at line 87 of file minisat_derivation.h.
Member Typedef Documentation
| typedef Hash::hash_map<int, Clause*> MiniSat::Derivation::TClauses |
Definition at line 89 of file minisat_derivation.h.
| typedef Hash::hash_set<int> MiniSat::Derivation::TInputClauses |
Definition at line 90 of file minisat_derivation.h.
| typedef Hash::hash_map<int, Inference*> MiniSat::Derivation::TInferences |
Definition at line 91 of file minisat_derivation.h.
Constructor & Destructor Documentation
| MiniSat::Derivation::Derivation | ( | ) | [inline] |
Definition at line 118 of file minisat_derivation.h.
| Derivation::~Derivation | ( | ) |
Definition at line 44 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().
Member Function Documentation
| void MiniSat::Derivation::registerClause | ( | Clause * | clause | ) | [inline] |
Definition at line 126 of file minisat_derivation.h.
References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::contains(), d_clauses, FatalAssert, MiniSat::Clause::id(), and MiniSat::Clause::size().
Referenced by MiniSat::Solver::addClause(), computeRootReason(), finish(), MiniSat::Solver::insertClause(), and MiniSat::Solver::insertLemma().
| void MiniSat::Derivation::registerInputClause | ( | int | clauseID | ) | [inline] |
Definition at line 155 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 162 of file minisat_derivation.h.
References d_removedClauses, and FatalAssert.
Referenced by MiniSat::Solver::addClause(), finish(), and MiniSat::Solver::remove().
| void MiniSat::Derivation::registerInference | ( | int | clauseID, | |
| Inference * | inference | |||
| ) | [inline] |
Definition at line 168 of file minisat_derivation.h.
References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::contains(), d_inferences, and FatalAssert.
Referenced by MiniSat::Solver::addClause(), MiniSat::Solver::analyze(), computeRootReason(), and finish().
Definition at line 62 of file minisat_derivation.cpp.
References MiniSat::Inference::add(), MiniSat::Clause_new(), d_clauses, d_unitClauses, MiniSat::Clause::Decision(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), FatalAssert, 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 115 of file minisat_derivation.cpp.
References MiniSat::Inference::add(), checkDerivation(), MiniSat::Clause_new(), computeRootReason(), d_emptyClause, FatalAssert, MiniSat::Clause::id(), IF_DEBUG, MiniSat::Solver::nextClauseID(), registerClause(), registerInference(), removedClause(), and MiniSat::Clause::size().
Referenced by MiniSat::Solver::search().
| void Derivation::printDerivation | ( | Clause * | clause | ) |
Definition at line 343 of file minisat_derivation.cpp.
References checkDerivation(), Hash::hash_set< _Key, _HashFcn, _EqualKey >::contains(), d_clauses, d_inferences, d_inputClauses, 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(), IF_DEBUG, MiniSat::Inference::toString(), and MiniSat::Clause::toString().
| void Derivation::printDerivation | ( | ) |
Definition at line 336 of file minisat_derivation.cpp.
References d_emptyClause, FatalAssert, and MiniSat::Clause::size().
| void Derivation::checkDerivation | ( | Clause * | clause | ) |
Definition at line 148 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, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), FatalAssert, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find(), MiniSat::Inference::getStart(), MiniSat::Inference::getSteps(), and MiniSat::Clause::id().
Referenced by createProof(), finish(), and printDerivation().
| SAT::SatProof * Derivation::createProof | ( | ) |
Definition at line 253 of file minisat_derivation.cpp.
References d_emptyClause, FatalAssert, and MiniSat::Clause::size().
| SAT::SatProof * Derivation::createProof | ( | Clause * | clause | ) |
Definition at line 260 of file minisat_derivation.cpp.
References checkDerivation(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::contains(), d_clauses, d_inferences, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), FatalAssert, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find(), MiniSat::Inference::getStart(), MiniSat::Inference::getSteps(), MiniSat::Clause::getTheorem(), MiniSat::Clause::id(), CVC3::Theorem::isNull(), MiniSat::left(), MiniSat::miniSatToCVC(), SAT::SatProof::registerLeaf(), SAT::SatProof::registerNode(), MiniSat::right(), and SAT::SatProof::setRoot().
| void Derivation::push | ( | int | clauseID | ) |
| void Derivation::pop | ( | int | clauseID | ) |
Definition at line 406 of file minisat_derivation.cpp.
References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::begin(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::contains(), d_clauses, d_emptyClause, d_inferences, d_inputClauses, d_removedClauses, d_unitClauses, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::erase(), Hash::hash_set< _Key, _HashFcn, _EqualKey >::erase(), FatalAssert, MiniSat::Clause::id(), MiniSat::Clause::pushID(), MiniSat::Clause::size(), and MiniSat::xfree().
Referenced by MiniSat::Solver::pop().
Member Data Documentation
TClauses MiniSat::Derivation::d_clauses [private] |
Definition at line 95 of file minisat_derivation.h.
Referenced by checkDerivation(), computeRootReason(), createProof(), pop(), printDerivation(), and registerClause().
Definition at line 102 of file minisat_derivation.h.
Referenced by checkDerivation(), pop(), printDerivation(), and registerInputClause().
TClauses MiniSat::Derivation::d_unitClauses [private] |
Definition at line 106 of file minisat_derivation.h.
Referenced by computeRootReason(), pop(), and ~Derivation().
TInferences MiniSat::Derivation::d_inferences [private] |
Definition at line 109 of file minisat_derivation.h.
Referenced by checkDerivation(), createProof(), pop(), printDerivation(), registerInference(), and ~Derivation().
std::deque<Clause*> MiniSat::Derivation::d_removedClauses [private] |
Definition at line 112 of file minisat_derivation.h.
Referenced by pop(), removedClause(), and ~Derivation().
Clause* MiniSat::Derivation::d_emptyClause [private] |
Definition at line 115 of file minisat_derivation.h.
Referenced by createProof(), finish(), pop(), and printDerivation().
The documentation for this class was generated from the following files:
