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

#include <minisat_derivation.h>

Collaboration diagram for MiniSat::Derivation:
Collaboration graph

Public Types

typedef Hash::hash_map< int,
Clause * > 
TClauses
 
typedef Hash::hash_set< int > TInputClauses
 
typedef Hash::hash_map< int,
Inference * > 
TInferences
 

Public Member Functions

 Derivation ()
 
 ~Derivation ()
 
void registerClause (Clause *clause)
 
void registerInputClause (int clauseID)
 
void removedClause (Clause *clause)
 
void registerInference (int clauseID, Inference *inference)
 
int computeRootReason (Lit implied, Solver *solver)
 
void finish (Clause *clause, Solver *solver)
 
void printDerivation (Clause *clause)
 
void printDerivation ()
 
void checkDerivation (Clause *clause)
 
SAT::SatProofcreateProof ()
 
SAT::SatProofcreateProof (Clause *clause)
 
void push (int clauseID)
 
void pop (int clauseID)
 

Private Attributes

TClauses d_clauses
 
TInputClauses d_inputClauses
 
TClauses d_unitClauses
 
TInferences d_inferences
 
std::deque< Clause * > d_removedClauses
 
Claused_emptyClause
 

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

TClauses MiniSat::Derivation::d_clauses
private

Definition at line 95 of file minisat_derivation.h.

Referenced by registerClause().

TInputClauses MiniSat::Derivation::d_inputClauses
private

Definition at line 102 of file minisat_derivation.h.

Referenced by registerInputClause().

TClauses MiniSat::Derivation::d_unitClauses
private

Definition at line 106 of file minisat_derivation.h.

TInferences MiniSat::Derivation::d_inferences
private

Definition at line 109 of file minisat_derivation.h.

Referenced by registerInference().

std::deque<Clause*> MiniSat::Derivation::d_removedClauses
private

Definition at line 112 of file minisat_derivation.h.

Referenced by removedClause().

Clause* MiniSat::Derivation::d_emptyClause
private

Definition at line 115 of file minisat_derivation.h.


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