CVCL::Theorem3 Class Reference

Theorem3. More...

#include <theorem.h>

Collaboration diagram for CVCL::Theorem3:

[legend]List of all members.

Public Member Functions

• void printDebug () const
• Theorem3 ()
• virtual ~Theorem3 ()
• bool isNull () const
• bool isRewrite () const
• bool isAssump () const
• const Expr & getExpr () const
• const Expr & getLHS () const
• const Expr & getRHS () const
• const Assumptions getAssumptions () const
• const Assumptions & getAssumptionsRef () const
• Assumptions getAssumptionsCopy () const
• const Proof & getProof () const
• int getScope () const
• bool withProof () const
• bool withAssumptions () const
• std::string toString () const
• void printx () const
• void print () const
• bool isAbsLiteral () const

  Check if the theorem is a literal.
  

Private Member Functions

• Theorem3 (TheoremManager *tm, const Expr &thm, const Assumptions &assump, const Proof &pf, bool isAssump=false, int scope=-1)
• Theorem3 (TheoremManager *tm, const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)

Private Attributes

• Theorem d_thm

Friends

• class TheoremProducer
• bool operator== (const Theorem3 &t1, const Theorem3 &t2)
• bool operator!= (const Theorem3 &t1, const Theorem3 &t2)
• std::ostream & operator<< (std::ostream &os, const Theorem3 &t)

---

Detailed Description

Theorem3.

Author: Sergey Berezin

Created: Tue Nov 4 17:57:07 2003

Implements the 3-valued theorem used for the user assertions and the result of query. It is simply a wrapper around class Theorem, but has a different semantic meaning: the formula may have partial functions and has the Kleene's 3-valued interpretation. The fact that a Theorem3 value is derived means that the TCCs for the formula and all of its assumptions are valid in the current context, and the proofs of TCCs contribute to the set of assumptions.

Definition at line 269 of file theorem.h.

---

Constructor & Destructor Documentation

CVCL::Theorem3::Theorem3 (  TheoremManager *  tm, const Expr &  thm, const Assumptions &  assump, const Proof &  pf, bool  isAssump = false, int  scope = -1 )  [inline, private]

Definition at line 286 of file theorem.h.

CVCL::Theorem3::Theorem3 (  TheoremManager *  tm, const Expr &  lhs, const Expr &  rhs, const Assumptions &  assump, const Proof &  pf )  [inline, private]

Definition at line 293 of file theorem.h.

CVCL::Theorem3::Theorem3 (   )  [inline]

Definition at line 307 of file theorem.h.

virtual CVCL::Theorem3::~Theorem3 (   )  [inline, virtual]

Definition at line 310 of file theorem.h.

---

Member Function Documentation

void CVCL::Theorem3::printDebug (   )  const [inline]

Definition at line 302 of file theorem.h. References d_thm, and CVCL::Theorem::printDebug().

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

Definition at line 312 of file theorem.h. References d_thm, and CVCL::Theorem::isNull(). Referenced by CVCL::VCL::getClosure(), CVCL::VCL::getProof(), CVCL::VCL::getProofClosure(), and CVCL::VCL::incomplete().

bool CVCL::Theorem3::isRewrite (   )  const [inline]

Definition at line 315 of file theorem.h. References d_thm, and CVCL::Theorem::isRewrite().

bool CVCL::Theorem3::isAssump (   )  const [inline]

Definition at line 316 of file theorem.h. References d_thm, and CVCL::Theorem::isAssump().

const Expr& CVCL::Theorem3::getExpr (   )  const [inline]

Definition at line 319 of file theorem.h. References d_thm, and CVCL::Theorem::getExpr(). Referenced by CVCL::VCL::getClosure().

const Expr& CVCL::Theorem3::getLHS (   )  const [inline]

Definition at line 320 of file theorem.h. References d_thm, and CVCL::Theorem::getLHS().

const Expr& CVCL::Theorem3::getRHS (   )  const [inline]

Definition at line 321 of file theorem.h. References d_thm, and CVCL::Theorem::getRHS(). Referenced by CVCL::VCL::simplify().

const Assumptions CVCL::Theorem3::getAssumptions (   )  const [inline]

Definition at line 325 of file theorem.h. References d_thm, and CVCL::Theorem::getAssumptions(). Referenced by CVCL::VCL::deriveClosure().

const Assumptions& CVCL::Theorem3::getAssumptionsRef (   )  const [inline]

Definition at line 326 of file theorem.h. References d_thm, and CVCL::Theorem::getAssumptionsRef().

Assumptions CVCL::Theorem3::getAssumptionsCopy (   )  const [inline]

Definition at line 332 of file theorem.h. References d_thm, and CVCL::Theorem::getAssumptionsCopy().

const Proof& CVCL::Theorem3::getProof (   )  const [inline]

Definition at line 337 of file theorem.h. References d_thm, and CVCL::Theorem::getProof(). Referenced by CVCL::VCL::getProofClosure().

int CVCL::Theorem3::getScope (   )  const [inline]

Definition at line 341 of file theorem.h. References d_thm, and CVCL::Theorem::getScope().

bool CVCL::Theorem3::withProof (   )  const [inline]

Definition at line 344 of file theorem.h. References d_thm, and CVCL::Theorem::withProof().

bool CVCL::Theorem3::withAssumptions (   )  const [inline]

Definition at line 345 of file theorem.h. References d_thm, and CVCL::Theorem::withAssumptions().

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

Definition at line 377 of file theorem.h.

void CVCL::Theorem3::printx (   )  const [inline]

Definition at line 351 of file theorem.h. References d_thm, and CVCL::Theorem::printx().

void CVCL::Theorem3::print (   )  const [inline]

Definition at line 352 of file theorem.h. References d_thm, and CVCL::Theorem::print().

bool CVCL::Theorem3::isAbsLiteral (   )  const [inline]

Check if the theorem is a literal. Definition at line 355 of file theorem.h. References d_thm, and CVCL::Theorem::isAbsLiteral().

---

Friends And Related Function Documentation

friend class TheoremProducer [friend]

Definition at line 273 of file theorem.h.

bool operator== (  const Theorem3 &  t1, const Theorem3 &  t2 )  [friend]

Definition at line 277 of file theorem.h.

bool operator!= (  const Theorem3 &  t1, const Theorem3 &  t2 )  [friend]

Definition at line 280 of file theorem.h.

std::ostream& operator<< (  std::ostream &  os, const Theorem3 &  t )  [friend]

Definition at line 357 of file theorem.h.

---

Member Data Documentation

Theorem CVCL::Theorem3::d_thm [private]

Definition at line 275 of file theorem.h. Referenced by getAssumptions(), getAssumptionsCopy(), getAssumptionsRef(), getExpr(), getLHS(), getProof(), getRHS(), getScope(), isAbsLiteral(), isAssump(), isNull(), isRewrite(), print(), printDebug(), printx(), withAssumptions(), and withProof().

---

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

• theorem.h

---