CVC3::RegTheoremValue Class Reference

#include <theorem_value.h>

Inheritance diagram for CVC3::RegTheoremValue:

[legend]Collaboration diagram for CVC3::RegTheoremValue:

[legend]List of all members.

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 210 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 220 of file theorem_value.h.

References CVC3::Assumptions::add1(), CVC3::Assumptions::begin(), d_assump, 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::Expr::getIndex(), CVC3::TheoremManager::isActive(), CVC3::ContextManager::scopeLevel(), CVC3::Expr::toString(), and CVC3::TRACE.

CVC3::RegTheoremValue::~RegTheoremValue

(

)

[inline]

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

const Assumptions& CVC3::RegTheoremValue::getAssumptionsRef

(

)

const [inline, virtual]

Implements CVC3::TheoremValue.

Definition at line 264 of file theorem_value.h.

References d_assump.

MemoryManager* CVC3::RegTheoremValue::getMM

(

)

[inline, virtual]

Implements CVC3::TheoremValue.

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

References CVC3::MemoryManager::newData().

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

Definition at line 272 of file theorem_value.h.

References CVC3::MemoryManager::deleteData().

void CVC3::RegTheoremValue::operator delete

(

void *

d

)

[inline]

Definition at line 276 of file theorem_value.h.

---

Friends And Related Function Documentation

friend class Theorem [friend]

Reimplemented from CVC3::TheoremValue.

Definition at line 212 of file theorem_value.h.

---

Member Data Documentation

Assumptions CVC3::RegTheoremValue::d_assump [protected]

The assumptions for the theorem.

Definition at line 216 of file theorem_value.h.

Referenced by getAssumptionsRef(), RegTheoremValue(), and ~RegTheoremValue().

---

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

• theorem_value.h

---