CVC3
Public Types | Public Member Functions | Private Attributes

MiniSat::Derivation Class Reference

#include <minisat_derivation.h>

Collaboration diagram for MiniSat::Derivation:
Collaboration graph
[legend]

List of all members.

Public Types

Public Member Functions

Private Attributes


Detailed Description

Definition at line 87 of file minisat_derivation.h.


Member Typedef Documentation

Definition at line 89 of file minisat_derivation.h.

Definition at line 90 of file minisat_derivation.h.

Definition at line 91 of file minisat_derivation.h.


Constructor & Destructor Documentation

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().


Member Function Documentation

void MiniSat::Derivation::registerClause ( Clause clause) [inline]
void MiniSat::Derivation::registerInputClause ( int  clauseID) [inline]
void MiniSat::Derivation::removedClause ( Clause clause) [inline]

Definition at line 162 of file minisat_derivation.h.

References d_removedClauses, and FatalAssert.

Referenced by MiniSat::Solver::addClause(), and MiniSat::Solver::remove().

void MiniSat::Derivation::registerInference ( int  clauseID,
Inference inference 
) [inline]
int Derivation::computeRootReason ( Lit  implied,
Solver solver 
)
void Derivation::finish ( Clause clause,
Solver solver 
)
void Derivation::printDerivation ( Clause clause)
void Derivation::printDerivation ( )

Definition at line 336 of file minisat_derivation.cpp.

References FatalAssert.

void Derivation::checkDerivation ( Clause clause)
SAT::SatProof * Derivation::createProof ( )

Definition at line 253 of file minisat_derivation.cpp.

References FatalAssert.

SAT::SatProof * Derivation::createProof ( Clause clause)
void Derivation::push ( int  clauseID)

Definition at line 402 of file minisat_derivation.cpp.

Referenced by MiniSat::Solver::push().

void Derivation::pop ( int  clauseID)

Member Data Documentation

Definition at line 95 of file minisat_derivation.h.

Referenced by registerClause().

Definition at line 102 of file minisat_derivation.h.

Referenced by registerInputClause().

Definition at line 106 of file minisat_derivation.h.

Definition at line 109 of file minisat_derivation.h.

Referenced by registerInference().

Definition at line 112 of file minisat_derivation.h.

Referenced by removedClause().

Definition at line 115 of file minisat_derivation.h.


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