SAT::SatProofNode Class Reference

#include <sat_proof.h>

Collaboration diagram for SAT::SatProofNode:

[legend]List of all members.

Public Member Functions

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

Private Attributes

• CVC3::Theorem d_theorem
• SatProofNode * d_left
• SatProofNode * d_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]

Definition at line 58 of file sat_proof.h.

References d_theorem, and CVC3::Theorem::isNull().

Referenced by generateSatProof(), getLeaf(), getLeftParent(), getLit(), getRightParent(), and printSatProof().

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:

• sat_proof.h

---