CVCL::Proof Class Reference

#include <proof.h>

Collaboration diagram for CVCL::Proof:

Collaboration graph
List of all members.

Public Member Functions

Private Attributes


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

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:
Generated on Thu Apr 13 16:57:43 2006 for CVC Lite by  doxygen 1.4.4