CVC3
Public Member Functions | Protected Attributes | Private Member Functions | Friends

CVC3::RegTheoremValue Class Reference

#include <theorem_value.h>

Inherits CVC3::TheoremValue.

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]
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

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: