CVC3
Public Types | Public Member Functions | Private Attributes | List of all members
MiniSat::Inference Class Reference

#include <minisat_derivation.h>

Collaboration diagram for MiniSat::Inference:
Collaboration graph

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: