#include <expr_value.h>
Inheritance diagram for CVC3::ExprTheorem:
Definition at line 907 of file expr_value.h.
CVC3::ExprTheorem::ExprTheorem | ( | ExprManager * | em, | |
const Theorem & | thm, | |||
ExprIndex | idx = 0 | |||
) | [inline] |
virtual CVC3::ExprTheorem::~ExprTheorem | ( | ) | [inline, virtual] |
Definition at line 931 of file expr_value.h.
virtual const Theorem& CVC3::ExprTheorem::getTheorem | ( | ) | const [inline, private, virtual] |
Reimplemented from CVC3::ExprValue.
Definition at line 913 of file expr_value.h.
References d_thm.
Referenced by operator==().
virtual size_t CVC3::ExprTheorem::getMMIndex | ( | ) | const [inline, private, virtual] |
Get unique memory manager ID.
Reimplemented from CVC3::ExprValue.
Definition at line 916 of file expr_value.h.
References CVC3::EXPR_THEOREM.
Referenced by copy(), and operator==().
virtual size_t CVC3::ExprTheorem::computeHash | ( | ) | const [inline, protected, virtual] |
Non-caching hash function which actually computes the hash.
This is the method that all subclasses should implement
Reimplemented from CVC3::ExprValue.
Definition at line 919 of file expr_value.h.
References d_thm, and CVC3::Theorem::hash().
ExprValue * CVC3::ExprTheorem::copy | ( | ExprManager * | em, | |
ExprIndex | idx = 0 | |||
) | const [protected, virtual] |
Make a clean copy of itself using the given memory manager.
Reimplemented from CVC3::ExprValue.
Definition at line 294 of file expr_value.cpp.
References d_thm, ExprTheorem(), CVC3::ExprManager::getMM(), and getMMIndex().
bool CVC3::ExprTheorem::isTheorem | ( | ) | const [inline, protected, virtual] |
Special Expr holding a theorem.
Reimplemented from CVC3::ExprValue.
Definition at line 924 of file expr_value.h.
bool CVC3::ExprTheorem::operator== | ( | const ExprValue & | ev2 | ) | const [virtual] |
Equality between any two ExprValue objects (including subclasses).
Reimplemented from CVC3::ExprValue.
Definition at line 286 of file expr_value.cpp.
References CVC3::ExprValue::getMMIndex(), getMMIndex(), CVC3::ExprValue::getTheorem(), and getTheorem().
void* CVC3::ExprTheorem::operator new | ( | size_t | size, | |
MemoryManager * | mm | |||
) | [inline] |
Overload operator new.
Reimplemented from CVC3::ExprValue.
Definition at line 935 of file expr_value.h.
References CVC3::MemoryManager::newData().
void CVC3::ExprTheorem::operator delete | ( | void * | pMem, | |
MemoryManager * | mm | |||
) | [inline] |
Reimplemented from CVC3::ExprValue.
Definition at line 938 of file expr_value.h.
References CVC3::MemoryManager::deleteData().
void CVC3::ExprTheorem::operator delete | ( | void * | ) | [inline] |
Overload operator delete.
Reimplemented from CVC3::ExprValue.
Definition at line 941 of file expr_value.h.
friend class Expr [friend] |
friend class ExprManager [friend] |
Theorem CVC3::ExprTheorem::d_thm [private] |