CVCL::Proof Class Reference

#include <proof.h>

Collaboration diagram for CVCL::Proof:

[legend]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 46 of file proof.h.

---

Constructor & Destructor Documentation

CVCL::Proof::Proof (  const Expr &  e  )  [inline]

Definition at line 50 of file proof.h.

CVCL::Proof::Proof (  const Proof &  p  )  [inline]

Definition at line 51 of file proof.h.

CVCL::Proof::Proof (   )  [inline]

Definition at line 52 of file proof.h.

---

Member Function Documentation

Expr CVCL::Proof::getExpr (   )  const [inline]

Definition at line 53 of file proof.h. References d_proof. Referenced by CVCL::TheoremProducer::newPf(), CVCL::operator<<(), and CVCL::operator==().

bool CVCL::Proof::isNull (   )  const [inline]

Definition at line 54 of file proof.h. References d_proof, and CVCL::Expr::isNull(). Referenced by CVCL::VCCmd::evaluateCommand(), CVCL::SearchEngineTheoremProducer::negIntro(), CVCL::SearchEngineTheoremProducer::proofByContradiction(), and CVCL::Theorem::Theorem().

std::string CVCL::Proof::toString (   )  const [inline]

Definition at line 57 of file proof.h.

---

Friends And Related Function Documentation

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

Definition at line 64 of file proof.h.

---

Member Data Documentation

Expr CVCL::Proof::d_proof [private]

Definition at line 48 of file proof.h. Referenced by getExpr(), and isNull().

---

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

• proof.h

---