CVC3::RegTheoremValue Class Reference

#include <theorem_value.h>

Inheritance diagram for CVC3::RegTheoremValue:

Inheritance graph
[legend]
Collaboration diagram for CVC3::RegTheoremValue:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Protected Attributes

Private Member Functions

Friends


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 CVC3::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:
Generated on Wed Nov 18 16:18:07 2009 for CVC3 by  doxygen 1.5.2