CVC3
2.4.1
|
#include <sat_proof.h>
Public Member Functions | |
SatProof () | |
~SatProof () | |
SatProofNode * | registerLeaf (CVC3::Theorem theorem) |
SatProofNode * | registerNode (SatProofNode *left, SatProofNode *right, SAT::Lit l) |
void | setRoot (SatProofNode *root) |
SatProofNode * | getRoot () |
Private Attributes | |
SatProofNode * | d_root |
std::list< SatProofNode * > | d_nodes |
Definition at line 70 of file sat_proof.h.
|
inline |
Definition at line 75 of file sat_proof.h.
|
inline |
Definition at line 77 of file sat_proof.h.
|
inline |
Definition at line 87 of file sat_proof.h.
Referenced by MiniSat::Derivation::createProof().
|
inline |
Definition at line 94 of file sat_proof.h.
Referenced by MiniSat::Derivation::createProof().
|
inline |
Definition at line 100 of file sat_proof.h.
Referenced by MiniSat::Derivation::createProof().
|
inline |
Definition at line 108 of file sat_proof.h.
References d_root, and DebugAssert.
Referenced by SAT::DPLLTMiniSat::getSatProof().
|
private |
Definition at line 72 of file sat_proof.h.
Referenced by getRoot().
|
private |
Definition at line 73 of file sat_proof.h.