CVC3::RWTheoremValue Class Reference

#include <theorem_value.h>

Inheritance diagram for CVC3::RWTheoremValue:

[legend]Collaboration diagram for CVC3::RWTheoremValue:

[legend]List of all members.

Public Member Functions

• ~RWTheoremValue ()
• bool isRewrite () const
• const Assumptions & getAssumptionsRef () const
• MemoryManager * getMM ()
• void * operator new (size_t size, MemoryManager *mm)
• void operator delete (void *pMem, MemoryManager *mm)
• void operator delete (void *d)

Protected Attributes

• Expr d_lhs
• Expr d_rhs
• Assumptions * d_assump

Private Member Functions

• void init (const Assumptions &assump, int scope)
• RWTheoremValue (TheoremManager *tm, const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf, bool isAssump, int scope=-1)
• RWTheoremValue (TheoremManager *tm, const Expr &thm, const Assumptions &assump, const Proof &pf, bool isAssump, int scope=-1)
• const Expr & getExpr () const
• const Expr & getLHS () const
• const Expr & getRHS () const

Friends

• class Theorem

---

Detailed Description

Definition at line 291 of file theorem_value.h.

---

Constructor & Destructor Documentation

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

Definition at line 335 of file theorem_value.h.

References init().

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

Definition at line 342 of file theorem_value.h.

References init().

CVC3::RWTheoremValue::~RWTheoremValue

(

)

[inline]

Definition at line 364 of file theorem_value.h.

References d_assump, CVC3::TheoremValue::d_isAssump, CVC3::Theorem::d_thm, FatalAssert, CVC3::Assumptions::getFirst(), IF_DEBUG, CVC3::Assumptions::size(), and CVC3::Theorem::thm().

---

Member Function Documentation

void CVC3::RWTheoremValue::init	(	const Assumptions &	assump,
		int	scope
	)			[inline, private]

Definition at line 303 of file theorem_value.h.

References d_assump, CVC3::TheoremValue::d_isAssump, CVC3::TheoremValue::d_quantLevel, CVC3::TheoremValue::d_refcount, CVC3::TheoremValue::d_scopeLevel, CVC3::TheoremValue::d_thm, CVC3::TheoremValue::d_tm, DebugAssert, CVC3::Assumptions::empty(), CVC3::Assumptions::end(), CVC3::TheoremManager::getCM(), CVC3::TheoremManager::isActive(), CVC3::ContextManager::scopeLevel(), CVC3::Expr::toString(), and CVC3::TRACE.

Referenced by RWTheoremValue().

const Expr& CVC3::RWTheoremValue::getExpr

(

)

const [inline, private, virtual]

Reimplemented from CVC3::TheoremValue.

Definition at line 348 of file theorem_value.h.

References d_lhs, d_rhs, CVC3::TheoremValue::d_thm, CVC3::Expr::eqExpr(), CVC3::Expr::getType(), CVC3::Expr::iffExpr(), CVC3::Type::isBool(), and CVC3::Expr::isNull().

const Expr& CVC3::RWTheoremValue::getLHS

(

)

const [inline, private, virtual]

Reimplemented from CVC3::TheoremValue.

Definition at line 359 of file theorem_value.h.

References d_lhs.

const Expr& CVC3::RWTheoremValue::getRHS

(

)

const [inline, private, virtual]

Reimplemented from CVC3::TheoremValue.

Definition at line 360 of file theorem_value.h.

References d_rhs.

bool CVC3::RWTheoremValue::isRewrite

(

)

const [inline, virtual]

Reimplemented from CVC3::TheoremValue.

Definition at line 373 of file theorem_value.h.

const Assumptions& CVC3::RWTheoremValue::getAssumptionsRef

(

)

const [inline, virtual]

Implements CVC3::TheoremValue.

Definition at line 374 of file theorem_value.h.

References d_assump, and CVC3::Assumptions::emptyAssump().

MemoryManager* CVC3::RWTheoremValue::getMM

(

)

[inline, virtual]

Implements CVC3::TheoremValue.

Definition at line 380 of file theorem_value.h.

References CVC3::TheoremValue::d_tm, and CVC3::TheoremManager::getRWMM().

void* CVC3::RWTheoremValue::operator new	(	size_t	size,
		MemoryManager *	mm
	)			[inline]

Definition at line 382 of file theorem_value.h.

References CVC3::MemoryManager::newData().

void CVC3::RWTheoremValue::operator delete	(	void *	pMem,
		MemoryManager *	mm
	)			[inline]

Definition at line 385 of file theorem_value.h.

References CVC3::MemoryManager::deleteData().

void CVC3::RWTheoremValue::operator delete

(

void *

d

)

[inline]

Definition at line 389 of file theorem_value.h.

---

Friends And Related Function Documentation

friend class Theorem [friend]

Reimplemented from CVC3::TheoremValue.

Definition at line 293 of file theorem_value.h.

---

Member Data Documentation

Expr CVC3::RWTheoremValue::d_lhs [protected]

Definition at line 298 of file theorem_value.h.

Referenced by getExpr(), and getLHS().

Expr CVC3::RWTheoremValue::d_rhs [protected]

Definition at line 299 of file theorem_value.h.

Referenced by getExpr(), and getRHS().

Assumptions* CVC3::RWTheoremValue::d_assump [protected]

Definition at line 300 of file theorem_value.h.

Referenced by getAssumptionsRef(), init(), and ~RWTheoremValue().

---

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

• theorem_value.h

---