CVC3  2.4.1
Public Types | Public Member Functions | Private Attributes
MiniSat::Inference Class Reference

#include <minisat_derivation.h>

List of all members.

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