21 #ifndef _cvc3__sat__proof_h_
22 #define _cvc3__sat__proof_h_
46 d_theorem(theorem), d_left(NULL), d_right(NULL){
53 d_left(left), d_right(right), d_lit(lit) {
54 DebugAssert(d_left != NULL,
"SatProofNode: constructor");
55 DebugAssert(d_right != NULL,
"SatProofNode: constructor");
78 for (std::list<SatProofNode*>::iterator i = d_nodes.begin(); i != d_nodes.end(); ++i) {
89 d_nodes.push_back(node);
96 d_nodes.push_back(node);
109 DebugAssert(d_root != NULL,
"null root found in getRoot");
std::list< SatProofNode * > d_nodes
#define DebugAssert(cond, str)
CVC3::Proof getNodeProof()
SatProofNode(SatProofNode *left, SatProofNode *right, SAT::Lit lit)
SatProofNode(CVC3::Theorem theorem)
void setRoot(SatProofNode *root)
SatProofNode * registerNode(SatProofNode *left, SatProofNode *right, SAT::Lit l)
SatProofNode * getLeftParent()
SatProofNode * getRightParent()
SatProofNode * registerLeaf(CVC3::Theorem theorem)
void setNodeProof(CVC3::Proof pf)