CVC3::Theorem3 Class Reference

Theorem3. More...

#include <theorem.h>

Collaboration diagram for CVC3::Theorem3:

[legend]List of all members.

Public Member Functions

• void printDebug () const
• Theorem3 ()
• virtual ~Theorem3 ()
• bool isNull () const
• bool isRewrite () const
• bool isAssump () const
• Expr getExpr () const
• const Expr & getLHS () const
• const Expr & getRHS () const
• const Assumptions & getAssumptionsRef () 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 291 of file theorem.h.

---

Constructor & Destructor Documentation

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

Definition at line 308 of file theorem.h.

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

Definition at line 315 of file theorem.h.

CVC3::Theorem3::Theorem3

(

)

[inline]

Definition at line 329 of file theorem.h.

virtual CVC3::Theorem3::~Theorem3

(

)

[inline, virtual]

Definition at line 332 of file theorem.h.

---

Member Function Documentation

void CVC3::Theorem3::printDebug

(

)

const [inline]

Definition at line 324 of file theorem.h.

References d_thm, and CVC3::Theorem::printDebug().

bool CVC3::Theorem3::isNull

(

)

const [inline]

Definition at line 334 of file theorem.h.

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

Referenced by CVC3::VCL::getAssumptionsTCC(), CVC3::VCL::getClosure(), CVC3::VCL::getProof(), CVC3::VCL::getProofClosure(), and CVC3::VCL::incomplete().

bool CVC3::Theorem3::isRewrite

(

)

const [inline]

Definition at line 337 of file theorem.h.

References d_thm, and CVC3::Theorem::isRewrite().

bool CVC3::Theorem3::isAssump

(

)

const [inline]

Definition at line 338 of file theorem.h.

References d_thm, and CVC3::Theorem::isAssump().

Expr CVC3::Theorem3::getExpr

(

)

const [inline]

Definition at line 341 of file theorem.h.

References d_thm, and CVC3::Theorem::getExpr().

Referenced by CVC3::VCL::getClosure(), and CVC3::CommonTheoremProducer::implIntro3().

const Expr& CVC3::Theorem3::getLHS

(

)

const [inline]

Definition at line 342 of file theorem.h.

References d_thm, and CVC3::Theorem::getLHS().

const Expr& CVC3::Theorem3::getRHS

(

)

const [inline]

Definition at line 343 of file theorem.h.

References d_thm, and CVC3::Theorem::getRHS().

const Assumptions& CVC3::Theorem3::getAssumptionsRef

(

)

const [inline]

Definition at line 348 of file theorem.h.

References d_thm, and CVC3::Theorem::getAssumptionsRef().

Referenced by CVC3::VCL::deriveClosure(), and CVC3::CommonTheoremProducer::implIntro3().

Proof CVC3::Theorem3::getProof

(

)

const [inline]

Definition at line 353 of file theorem.h.

References d_thm, and CVC3::Theorem::getProof().

Referenced by CVC3::VCL::getProofClosure(), and CVC3::CommonTheoremProducer::implIntro3().

int CVC3::Theorem3::getScope

(

)

const [inline]

Definition at line 357 of file theorem.h.

References d_thm, and CVC3::Theorem::getScope().

bool CVC3::Theorem3::withProof

(

)

const [inline]

Definition at line 360 of file theorem.h.

References d_thm, and CVC3::Theorem::withProof().

bool CVC3::Theorem3::withAssumptions

(

)

const [inline]

Definition at line 361 of file theorem.h.

References d_thm, and CVC3::Theorem::withAssumptions().

std::string CVC3::Theorem3::toString

(

)

const [inline]

Definition at line 393 of file theorem.h.

void CVC3::Theorem3::printx

(

)

const [inline]

Definition at line 367 of file theorem.h.

References d_thm, and CVC3::Theorem::printx().

void CVC3::Theorem3::print

(

)

const [inline]

Definition at line 368 of file theorem.h.

References d_thm, and CVC3::Theorem::print().

bool CVC3::Theorem3::isAbsLiteral

(

)

const [inline]

Check if the theorem is a literal.

Definition at line 371 of file theorem.h.

References d_thm, and CVC3::Theorem::isAbsLiteral().

---

Friends And Related Function Documentation

friend class TheoremProducer [friend]

Definition at line 295 of file theorem.h.

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

Definition at line 299 of file theorem.h.

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

Definition at line 302 of file theorem.h.

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

Definition at line 373 of file theorem.h.

---

Member Data Documentation

Theorem CVC3::Theorem3::d_thm [private]

Definition at line 297 of file theorem.h.

Referenced by 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

---