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

#include <sat_proof.h>

List of all members.

Public Member Functions

Private Attributes


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


Member Function Documentation

bool SAT::SatProofNode::isLeaf ( ) [inline]
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]

Definition at line 65 of file sat_proof.h.

References d_proof.

Referenced by generateSatProof().


Member Data Documentation

Definition at line 39 of file sat_proof.h.

Referenced by isLeaf(), and getLeaf().

Definition at line 40 of file sat_proof.h.

Referenced by SatProofNode(), and getLeftParent().

Definition at line 41 of file sat_proof.h.

Referenced by SatProofNode(), and getRightParent().

Definition at line 42 of file sat_proof.h.

Referenced by getLit().

Definition at line 43 of file sat_proof.h.

Referenced by hasNodeProof(), getNodeProof(), and setNodeProof().


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