CVC3
|
#include <minisat_derivation.h>
Public Types | |
typedef std::vector< std::pair < Lit, int > > | TSteps |
Public Member Functions | |
Inference (int clauseID) | |
void | add (Lit lit, int clauseID) |
void | add (Lit lit, Clause *clause) |
int | getStart () const |
const TSteps & | getSteps () const |
std::string | toString () const |
Private Attributes | |
int | d_start |
TSteps | d_steps |
Definition at line 40 of file minisat_derivation.h.
typedef std::vector<std::pair<Lit, int> > MiniSat::Inference::TSteps |
Definition at line 42 of file minisat_derivation.h.
|
inline |
Definition at line 54 of file minisat_derivation.h.
|
inline |
Definition at line 58 of file minisat_derivation.h.
References d_steps.
Referenced by add(), MiniSat::Solver::addClause(), MiniSat::Solver::analyze(), MiniSat::Solver::analyze_minimize(), MiniSat::Derivation::computeRootReason(), and MiniSat::Derivation::finish().
Definition at line 62 of file minisat_derivation.h.
References add(), and MiniSat::Clause::id().
|
inline |
Definition at line 66 of file minisat_derivation.h.
References d_start.
Referenced by MiniSat::Derivation::checkDerivation(), MiniSat::Derivation::createProof(), and MiniSat::Derivation::printDerivation().
|
inline |
Definition at line 70 of file minisat_derivation.h.
References d_steps.
Referenced by MiniSat::Derivation::checkDerivation(), MiniSat::Derivation::createProof(), and MiniSat::Derivation::printDerivation().
std::string Inference::toString | ( | ) | const |
Definition at line 31 of file minisat_derivation.cpp.
Referenced by MiniSat::Derivation::printDerivation().
|
private |
Definition at line 46 of file minisat_derivation.h.
Referenced by getStart().
|
private |
Definition at line 51 of file minisat_derivation.h.
Referenced by add(), and getSteps().