CVC3::Proof Class Reference

#include <proof.h>

Collaboration diagram for CVC3::Proof:

List of all members.

Public Member Functions

• Proof (const Expr &e)
• Proof (const Proof &p)
• Proof ()
• Expr getExpr () const
• bool isNull () const
• std::string toString () const

Private Attributes

• Expr d_proof

Friends

• std::ostream & operator<< (std::ostream &os, const Proof &pf)

---

Detailed Description

Definition at line 38 of file proof.h.

---

Constructor & Destructor Documentation

CVC3::Proof::Proof

(

const Expr &

e

)

[inline]

Definition at line 43 of file proof.h.

CVC3::Proof::Proof

(

const Proof &

p

)

[inline]

Definition at line 44 of file proof.h.

CVC3::Proof::Proof

(

)

[inline]

Definition at line 45 of file proof.h.

---

Member Function Documentation

Expr CVC3::Proof::getExpr

(

)

const [inline]

Definition at line 46 of file proof.h.

References d_proof.

Referenced by CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::TheoremProducer::newPf(), CVC3::operator<<(), CVC3::operator==(), and CVC3::SearchEngineTheoremProducer::satProof().

bool CVC3::Proof::isNull

(

)

const [inline]

Definition at line 47 of file proof.h.

References d_proof, and CVC3::Expr::isNull().

Referenced by CVC3::VCCmd::evaluateCommand(), SAT::SatProofNode::getNodeProof(), SAT::SatProofNode::hasNodeProof(), and CVC3::Theorem::Theorem().

std::string CVC3::Proof::toString

(

)

const [inline]

Definition at line 50 of file proof.h.

---

Friends And Related Function Documentation

std::ostream& operator<<	(	std::ostream &	os,
		const Proof &	pf
	)		[friend]

Definition at line 57 of file proof.h.

---

Member Data Documentation

Expr CVC3::Proof::d_proof [private]

Definition at line 40 of file proof.h.

Referenced by getExpr(), and isNull().

---

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

• proof.h