CVC3  2.4.1
Public Member Functions | Private Attributes
SAT::SatProofNode Class Reference

#include <sat_proof.h>

List of all members.

Public Member Functions

 SatProofNode (CVC3::Theorem theorem)
 SatProofNode (SatProofNode *left, SatProofNode *right, SAT::Lit lit)
bool isLeaf ()
CVC3::Theorem getLeaf ()
SatProofNodegetLeftParent ()
SatProofNodegetRightParent ()
SAT::Lit getLit ()
bool hasNodeProof ()
CVC3::Proof getNodeProof ()
void setNodeProof (CVC3::Proof pf)

Private Attributes

CVC3::Theorem d_theorem
SatProofNoded_left
SatProofNoded_right
SAT::Lit d_lit
CVC3::Proof d_proof

Detailed Description

Definition at line 37 of file sat_proof.h.


Constructor & Destructor Documentation

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 d_left, d_right, and DebugAssert.


Member Function Documentation

bool SAT::SatProofNode::isLeaf ( )
inline
CVC3::Theorem SAT::SatProofNode::getLeaf ( )
inline

Definition at line 59 of file sat_proof.h.

References d_theorem, DebugAssert, and isLeaf().

Referenced by generateSatProof(), and printSatProof().

SatProofNode* SAT::SatProofNode::getLeftParent ( )
inline

Definition at line 60 of file sat_proof.h.

References d_left, DebugAssert, and isLeaf().

Referenced by generateSatProof(), and printSatProof().

SatProofNode* SAT::SatProofNode::getRightParent ( )
inline

Definition at line 61 of file sat_proof.h.

References d_right, DebugAssert, and isLeaf().

Referenced by generateSatProof(), and printSatProof().

SAT::Lit SAT::SatProofNode::getLit ( )
inline

Definition at line 62 of file sat_proof.h.

References d_lit, DebugAssert, and isLeaf().

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 d_proof, DebugAssert, and CVC3::Proof::isNull().

Referenced by generateSatProof().

void SAT::SatProofNode::setNodeProof ( CVC3::Proof  pf)
inline

Definition at line 65 of file sat_proof.h.

References d_proof.

Referenced by generateSatProof().


Member Data Documentation

CVC3::Theorem SAT::SatProofNode::d_theorem
private

Definition at line 39 of file sat_proof.h.

Referenced by getLeaf(), and isLeaf().

SatProofNode* SAT::SatProofNode::d_left
private

Definition at line 40 of file sat_proof.h.

Referenced by getLeftParent(), and SatProofNode().

SatProofNode* SAT::SatProofNode::d_right
private

Definition at line 41 of file sat_proof.h.

Referenced by getRightParent(), and SatProofNode().

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 getNodeProof(), hasNodeProof(), and setNodeProof().


The documentation for this class was generated from the following file: