#include <minisat_derivation.h>

Collaboration diagram for MiniSat::Derivation:

[legend]

List of all members.

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::SatProof * createProof ()
SAT::SatProof * createProof (Clause *clause)
void push (int clauseID)
void pop (int clauseID)

Private Attributes

Detailed Description

Definition at line 87 of file minisat_derivation.h.

Member Typedef Documentation

typedef Hash::hash_map<int, Clause*> MiniSat::Derivation::TClauses

Definition at line 89 of file minisat_derivation.h.

typedef Hash::hash_set<int> MiniSat::Derivation::TInputClauses

Definition at line 90 of file minisat_derivation.h.

typedef Hash::hash_map<int, Inference*> MiniSat::Derivation::TInferences

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]

Definition at line 126 of file minisat_derivation.h.

References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::contains(), d_clauses, FatalAssert, MiniSat::Clause::id(), and MiniSat::Clause::size().

Referenced by MiniSat::Solver::addClause(), MiniSat::Solver::insertClause(), and MiniSat::Solver::insertLemma().

void MiniSat::Derivation::registerInputClause ( int clauseID ) [inline]

Definition at line 155 of file minisat_derivation.h.

References d_inputClauses, and Hash::hash_set< _Key, _HashFcn, _EqualKey >::insert().

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

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]`

Definition at line 168 of file minisat_derivation.h.

References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::contains(), d_inferences, and FatalAssert.

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

int Derivation::computeRootReason	(	Lit	implied,
		Solver *	solver
	)

Definition at line 62 of file minisat_derivation.cpp.

References MiniSat::Inference::add(), MiniSat::Clause_new(), MiniSat::Clause::Decision(), FatalAssert, MiniSat::Solver::getReason(), MiniSat::Solver::getValue(), MiniSat::Clause::id(), IF_DEBUG, MiniSat::Lit::index(), MiniSat::l_False, MiniSat::l_True, MiniSat::Solver::nextClauseID(), and MiniSat::Clause::size().

void Derivation::finish	(	Clause *	clause,
		Solver *	solver
	)

Definition at line 115 of file minisat_derivation.cpp.

References MiniSat::Inference::add(), MiniSat::Clause_new(), FatalAssert, MiniSat::Clause::id(), IF_DEBUG, MiniSat::Solver::nextClauseID(), and MiniSat::Clause::size().

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

void Derivation::printDerivation ( Clause * clause )

Definition at line 343 of file minisat_derivation.cpp.

References std::endl(), MiniSat::Inference::getStart(), MiniSat::Inference::getSteps(), MiniSat::Clause::id(), IF_DEBUG, MiniSat::Inference::toString(), and MiniSat::Clause::toString().

void Derivation::printDerivation ( )

Definition at line 336 of file minisat_derivation.cpp.

References FatalAssert.

void Derivation::checkDerivation ( Clause * clause )

Definition at line 148 of file minisat_derivation.cpp.

References FatalAssert, MiniSat::Inference::getStart(), MiniSat::Inference::getSteps(), and MiniSat::Clause::id().

SAT::SatProof * Derivation::createProof ( )

Definition at line 253 of file minisat_derivation.cpp.

References FatalAssert.

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

Definition at line 260 of file minisat_derivation.cpp.

References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::contains(), FatalAssert, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find(), MiniSat::Inference::getStart(), MiniSat::Inference::getSteps(), MiniSat::Clause::getTheorem(), MiniSat::Clause::id(), CVC3::Theorem::isNull(), MiniSat::left(), MiniSat::miniSatToCVC(), SAT::SatProof::registerLeaf(), SAT::SatProof::registerNode(), MiniSat::right(), and SAT::SatProof::setRoot().

void Derivation::push ( int clauseID )

Definition at line 402 of file minisat_derivation.cpp.

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

void Derivation::pop ( int clauseID )

Definition at line 406 of file minisat_derivation.cpp.

References FatalAssert, MiniSat::Clause::id(), MiniSat::Clause::pushID(), MiniSat::Clause::size(), and MiniSat::xfree().

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

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:

MiniSat::Derivation Class Reference