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

Detailed Description

Definition at line 40 of file minisat_derivation.h.

Member Typedef Documentation

typedef std::vector<std::pair<Lit, int> > MiniSat::Inference::TSteps

Definition at line 42 of file minisat_derivation.h.

Constructor & Destructor Documentation

MiniSat::Inference::Inference ( int clauseID ) [inline]

Definition at line 54 of file minisat_derivation.h.

Member Function Documentation

void MiniSat::Inference::add	(	Lit	lit,
		int	clauseID
	)		`[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().

void MiniSat::Inference::add	(	Lit	lit,
		Clause *	clause
	)		`[inline]`

Definition at line 62 of file minisat_derivation.h.

References add(), and MiniSat::Clause::id().

int MiniSat::Inference::getStart ( ) const [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().

const TSteps& MiniSat::Inference::getSteps ( ) const [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().

Member Data Documentation

int MiniSat::Inference::d_start [private]

Definition at line 46 of file minisat_derivation.h.

Referenced by getStart().

TSteps MiniSat::Inference::d_steps [private]

Definition at line 51 of file minisat_derivation.h.

Referenced by add(), and getSteps().

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

MiniSat::Inference Class Reference