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 308 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 325 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 332 of file theorem.h.

CVC3::Theorem3::Theorem3

(

)

[inline]

Definition at line 346 of file theorem.h.

virtual CVC3::Theorem3::~Theorem3

(

)

[inline, virtual]

Definition at line 349 of file theorem.h.

---

Member Function Documentation

void CVC3::Theorem3::printDebug

(

)

const [inline]

Definition at line 341 of file theorem.h.

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

bool CVC3::Theorem3::isNull

(

)

const [inline]

Definition at line 351 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(), CVC3::VCL::getProofQuery(), and CVC3::VCL::incomplete().

bool CVC3::Theorem3::isRewrite

(

)

const [inline]

Definition at line 354 of file theorem.h.

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

bool CVC3::Theorem3::isAssump

(

)

const [inline]

Definition at line 355 of file theorem.h.

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

Expr CVC3::Theorem3::getExpr

(

)

const [inline]

Definition at line 358 of file theorem.h.

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

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

const Expr& CVC3::Theorem3::getLHS

(

)

const [inline]

Definition at line 359 of file theorem.h.

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

const Expr& CVC3::Theorem3::getRHS

(

)

const [inline]

Definition at line 360 of file theorem.h.

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

const Assumptions& CVC3::Theorem3::getAssumptionsRef

(

)

const [inline]

Definition at line 365 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 370 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 374 of file theorem.h.

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

bool CVC3::Theorem3::withProof

(

)

const [inline]

Definition at line 377 of file theorem.h.

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

bool CVC3::Theorem3::withAssumptions

(

)

const [inline]

Definition at line 378 of file theorem.h.

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

std::string CVC3::Theorem3::toString

(

)

const [inline]

Definition at line 410 of file theorem.h.

void CVC3::Theorem3::printx

(

)

const [inline]

Definition at line 384 of file theorem.h.

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

void CVC3::Theorem3::print

(

)

const [inline]

Definition at line 385 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 388 of file theorem.h.

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

---

Friends And Related Function Documentation

friend class TheoremProducer [friend]

Definition at line 312 of file theorem.h.

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

Definition at line 316 of file theorem.h.

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

Definition at line 319 of file theorem.h.

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

Definition at line 390 of file theorem.h.

---

Member Data Documentation

Theorem CVC3::Theorem3::d_thm [private]

Definition at line 314 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