21 #ifndef _cvc3__sat__proof_h_
22 #define _cvc3__sat__proof_h_
78 for (std::list<SatProofNode*>::iterator i =
d_nodes.begin(); i !=
d_nodes.end(); ++i) {
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)