Public Member Functions

~RegTheoremValue ()
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

Assumptions d_assump
The assumptions for the theorem.

Private Member Functions

RegTheoremValue (TheoremManager *tm, const Expr &thm, const Assumptions &assump, const Proof &pf, bool isAssump, int scope=-1)

Friends

class Theorem

Detailed Description

Definition at line 343 of file theorem_value.h.

Constructor & Destructor Documentation

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

Definition at line 354 of file theorem_value.h.

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

CVC3::RegTheoremValue::~RegTheoremValue ( ) [inline]

Definition at line 397 of file theorem_value.h.

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

Member Function Documentation

const Assumptions& CVC3::RegTheoremValue::getAssumptionsRef ( ) const [inline, virtual]

Implements CVC3::TheoremValue.

Definition at line 405 of file theorem_value.h.

MemoryManager* CVC3::RegTheoremValue::getMM ( ) [inline, virtual]

Implements CVC3::TheoremValue.

Definition at line 408 of file theorem_value.h.

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

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

Definition at line 410 of file theorem_value.h.

References CVC3::MemoryManager::newData().

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

Definition at line 413 of file theorem_value.h.

References CVC3::MemoryManager::deleteData().

void CVC3::RegTheoremValue::operator delete ( void * d ) [inline]

Definition at line 417 of file theorem_value.h.

Friends And Related Function Documentation

friend class Theorem [friend]

Reimplemented from CVC3::TheoremValue.

Definition at line 345 of file theorem_value.h.

Member Data Documentation

Assumptions CVC3::RegTheoremValue::d_assump [protected]

The assumptions for the theorem.

Definition at line 349 of file theorem_value.h.

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

theorem_value.h

CVC3::RegTheoremValue Class Reference