CVC3  2.4.1
Public Member Functions | Private Attributes | List of all members
SAT::SatProofNode Class Reference

#include <sat_proof.h>

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: