CVC3
2.4.1
|
#include <sat_proof.h>
SAT::SatProofNode::SatProofNode | ( | CVC3::Theorem | theorem | ) | [inline] |
Definition at line 45 of file sat_proof.h.
References DebugAssert, and CVC3::Theorem::isNull().
SAT::SatProofNode::SatProofNode | ( | SatProofNode * | left, |
SatProofNode * | right, | ||
SAT::Lit | lit | ||
) | [inline] |
Definition at line 52 of file sat_proof.h.
References DebugAssert, d_left, and d_right.
bool SAT::SatProofNode::isLeaf | ( | ) | [inline] |
Definition at line 58 of file sat_proof.h.
References d_theorem, and CVC3::Theorem::isNull().
Referenced by generateSatProof(), printSatProof(), getLeaf(), getLeftParent(), getRightParent(), and getLit().
CVC3::Theorem SAT::SatProofNode::getLeaf | ( | ) | [inline] |
Definition at line 59 of file sat_proof.h.
References DebugAssert, isLeaf(), and d_theorem.
Referenced by generateSatProof(), and printSatProof().
SatProofNode* SAT::SatProofNode::getLeftParent | ( | ) | [inline] |
Definition at line 60 of file sat_proof.h.
References DebugAssert, isLeaf(), and d_left.
Referenced by generateSatProof(), and printSatProof().
SatProofNode* SAT::SatProofNode::getRightParent | ( | ) | [inline] |
Definition at line 61 of file sat_proof.h.
References DebugAssert, isLeaf(), and d_right.
Referenced by generateSatProof(), and printSatProof().
SAT::Lit SAT::SatProofNode::getLit | ( | ) | [inline] |
Definition at line 62 of file sat_proof.h.
References DebugAssert, isLeaf(), and d_lit.
Referenced by generateSatProof().
bool SAT::SatProofNode::hasNodeProof | ( | ) | [inline] |
Definition at line 63 of file sat_proof.h.
References d_proof, and CVC3::Proof::isNull().
Referenced by generateSatProof().
CVC3::Proof SAT::SatProofNode::getNodeProof | ( | ) | [inline] |
Definition at line 64 of file sat_proof.h.
References DebugAssert, d_proof, and CVC3::Proof::isNull().
Referenced by generateSatProof().
void SAT::SatProofNode::setNodeProof | ( | CVC3::Proof | pf | ) | [inline] |
CVC3::Theorem SAT::SatProofNode::d_theorem [private] |
Definition at line 39 of file sat_proof.h.
SatProofNode* SAT::SatProofNode::d_left [private] |
Definition at line 40 of file sat_proof.h.
Referenced by SatProofNode(), and getLeftParent().
SatProofNode* SAT::SatProofNode::d_right [private] |
Definition at line 41 of file sat_proof.h.
Referenced by SatProofNode(), and getRightParent().
SAT::Lit SAT::SatProofNode::d_lit [private] |
Definition at line 42 of file sat_proof.h.
Referenced by getLit().
CVC3::Proof SAT::SatProofNode::d_proof [private] |
Definition at line 43 of file sat_proof.h.
Referenced by hasNodeProof(), getNodeProof(), and setNodeProof().