CVC3
2.4.1
|
#include <minisat_derivation.h>
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.
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 MiniSat::xfree().
void MiniSat::Derivation::registerClause | ( | Clause * | clause | ) | [inline] |
Definition at line 126 of file minisat_derivation.h.
References d_clauses, Hash::hash_map::contains(), MiniSat::Clause::id(), FatalAssert, and MiniSat::Clause::size().
Referenced by MiniSat::Solver::insertLemma(), MiniSat::Solver::addClause(), and MiniSat::Solver::insertClause().
void MiniSat::Derivation::registerInputClause | ( | int | clauseID | ) | [inline] |
Definition at line 155 of file minisat_derivation.h.
References d_inputClauses, and Hash::hash_set::insert().
Referenced by MiniSat::Solver::addClause().
void MiniSat::Derivation::removedClause | ( | Clause * | clause | ) | [inline] |
Definition at line 162 of file minisat_derivation.h.
References FatalAssert, and d_removedClauses.
Referenced by MiniSat::Solver::addClause(), and MiniSat::Solver::remove().
void MiniSat::Derivation::registerInference | ( | int | clauseID, |
Inference * | inference | ||
) | [inline] |
Definition at line 168 of file minisat_derivation.h.
References FatalAssert, d_inferences, and Hash::hash_map::contains().
Referenced by MiniSat::Solver::addClause(), and MiniSat::Solver::analyze().
Definition at line 62 of file minisat_derivation.cpp.
References MiniSat::Solver::getReason(), FatalAssert, MiniSat::Clause::id(), MiniSat::Clause::Decision(), IF_DEBUG, MiniSat::Solver::getValue(), MiniSat::l_True, MiniSat::Clause::size(), MiniSat::l_False, Hash::hash_map::find(), MiniSat::Lit::index(), MiniSat::Inference::add(), MiniSat::Clause_new(), and MiniSat::Solver::nextClauseID().
Definition at line 115 of file minisat_derivation.cpp.
References FatalAssert, MiniSat::Clause::size(), MiniSat::Clause::id(), MiniSat::Inference::add(), MiniSat::Clause_new(), MiniSat::Solver::nextClauseID(), and IF_DEBUG.
Referenced by MiniSat::Solver::search().
void Derivation::printDerivation | ( | Clause * | clause | ) |
Definition at line 343 of file minisat_derivation.cpp.
References IF_DEBUG, MiniSat::Clause::id(), Hash::hash_map::find(), MiniSat::Inference::getStart(), MiniSat::Inference::getSteps(), MiniSat::Clause::toString(), MiniSat::Inference::toString(), and std::endl().
void Derivation::printDerivation | ( | ) |
Definition at line 336 of file minisat_derivation.cpp.
References FatalAssert.
void Derivation::checkDerivation | ( | Clause * | clause | ) |
Definition at line 148 of file minisat_derivation.cpp.
References MiniSat::Clause::id(), FatalAssert, Hash::hash_map::find(), MiniSat::Inference::getStart(), and MiniSat::Inference::getSteps().
SAT::SatProof * Derivation::createProof | ( | ) |
Definition at line 253 of file minisat_derivation.cpp.
References FatalAssert.
SAT::SatProof * Derivation::createProof | ( | Clause * | clause | ) |
Definition at line 260 of file minisat_derivation.cpp.
References MiniSat::Clause::id(), Hash::hash_map::find(), MiniSat::Inference::getStart(), MiniSat::Inference::getSteps(), FatalAssert, MiniSat::Clause::getTheorem(), CVC3::Theorem::isNull(), SAT::SatProof::registerLeaf(), Hash::hash_map::contains(), MiniSat::left(), MiniSat::right(), SAT::SatProof::registerNode(), MiniSat::miniSatToCVC(), and SAT::SatProof::setRoot().
void Derivation::push | ( | int | clauseID | ) |
Definition at line 402 of file minisat_derivation.cpp.
Referenced by MiniSat::Solver::push().
void Derivation::pop | ( | int | clauseID | ) |
Definition at line 406 of file minisat_derivation.cpp.
References Hash::hash_map::begin(), MiniSat::Clause::pushID(), MiniSat::Clause::id(), MiniSat::Clause::size(), FatalAssert, and MiniSat::xfree().
Referenced by MiniSat::Solver::pop().
TClauses MiniSat::Derivation::d_clauses [private] |
Definition at line 95 of file minisat_derivation.h.
Referenced by registerClause().
Definition at line 102 of file minisat_derivation.h.
Referenced by registerInputClause().
TClauses MiniSat::Derivation::d_unitClauses [private] |
Definition at line 106 of file minisat_derivation.h.
TInferences MiniSat::Derivation::d_inferences [private] |
Definition at line 109 of file minisat_derivation.h.
Referenced by registerInference().
std::deque<Clause*> MiniSat::Derivation::d_removedClauses [private] |
Definition at line 112 of file minisat_derivation.h.
Referenced by removedClause().
Clause* MiniSat::Derivation::d_emptyClause [private] |
Definition at line 115 of file minisat_derivation.h.