CVC3::RWTheoremValue Class Reference

#include <theorem_value.h>

Inherits CVC3::TheoremValue.

Collaboration diagram for CVC3::RWTheoremValue:

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 432 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 487 of file theorem_value.h.

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

Definition at line 494 of file theorem_value.h.

CVC3::RWTheoremValue::~RWTheoremValue

(

)

[inline]

Definition at line 516 of file theorem_value.h.

References CVC3::TheoremValue::d_isAssump, FatalAssert, and IF_DEBUG.

---

Member Function Documentation

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

Definition at line 444 of file theorem_value.h.

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

const Expr& CVC3::RWTheoremValue::getExpr

(

)

const [inline, private, virtual]

Reimplemented from CVC3::TheoremValue.

Definition at line 500 of file theorem_value.h.

References 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 511 of file theorem_value.h.

const Expr& CVC3::RWTheoremValue::getRHS

(

)

const [inline, private, virtual]

Reimplemented from CVC3::TheoremValue.

Definition at line 512 of file theorem_value.h.

bool CVC3::RWTheoremValue::isRewrite

(

)

const [inline, virtual]

Reimplemented from CVC3::TheoremValue.

Definition at line 525 of file theorem_value.h.

const Assumptions& CVC3::RWTheoremValue::getAssumptionsRef

(

)

const [inline, virtual]

Implements CVC3::TheoremValue.

Definition at line 526 of file theorem_value.h.

References CVC3::Assumptions::emptyAssump().

MemoryManager* CVC3::RWTheoremValue::getMM

(

)

[inline, virtual]

Implements CVC3::TheoremValue.

Definition at line 532 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 534 of file theorem_value.h.

References CVC3::MemoryManager::newData().

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

Definition at line 537 of file theorem_value.h.

References CVC3::MemoryManager::deleteData().

void CVC3::RWTheoremValue::operator delete

(

void *

d

)

[inline]

Definition at line 541 of file theorem_value.h.

---

Friends And Related Function Documentation

friend class Theorem [friend]

Reimplemented from CVC3::TheoremValue.

Definition at line 434 of file theorem_value.h.

---

Member Data Documentation

Expr CVC3::RWTheoremValue::d_lhs [protected]

Definition at line 439 of file theorem_value.h.

Expr CVC3::RWTheoremValue::d_rhs [protected]

Definition at line 440 of file theorem_value.h.

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

Definition at line 441 of file theorem_value.h.

---

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

• theorem_value.h