#include <theorem_value.h>
List of all members.
Private Member Functions |
void | init (const Assumptions &assump, int scope) |
| RWTheoremValue (TheoremManager *tm, const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf, bool isAssump, int scope=-1) |
| RWTheoremValue (TheoremManager *tm, const Expr &thm, const Assumptions &assump, const Proof &pf, bool isAssump, int scope=-1) |
const Expr & | getExpr () const |
const Expr & | getLHS () const |
const Expr & | getRHS () const |
Detailed Description
Definition at line 432 of file theorem_value.h.
Constructor & Destructor Documentation
CVC3::RWTheoremValue::~RWTheoremValue |
( |
| ) |
|
|
inline |
Member Function Documentation
void CVC3::RWTheoremValue::init |
( |
const Assumptions & |
assump, |
|
|
int |
scope |
|
) |
| |
|
inlineprivate |
Definition at line 444 of file theorem_value.h.
References CVC3::Assumptions::begin(), CVC3::TheoremValue::d_isAssump, 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::TheoremManager::isActive(), CVC3::ContextManager::scopeLevel(), and TRACE.
const Expr& CVC3::RWTheoremValue::getExpr |
( |
| ) |
const |
|
inlineprivatevirtual |
const Expr& CVC3::RWTheoremValue::getLHS |
( |
| ) |
const |
|
inlineprivatevirtual |
const Expr& CVC3::RWTheoremValue::getRHS |
( |
| ) |
const |
|
inlineprivatevirtual |
bool CVC3::RWTheoremValue::isRewrite |
( |
| ) |
const |
|
inlinevirtual |
const Assumptions& CVC3::RWTheoremValue::getAssumptionsRef |
( |
| ) |
const |
|
inlinevirtual |
void* CVC3::RWTheoremValue::operator new |
( |
size_t |
size, |
|
|
MemoryManager * |
mm |
|
) |
| |
|
inline |
void CVC3::RWTheoremValue::operator delete |
( |
void * |
pMem, |
|
|
MemoryManager * |
mm |
|
) |
| |
|
inline |
void CVC3::RWTheoremValue::operator delete |
( |
void * |
d | ) |
|
|
inline |
Friends And Related Function Documentation
Member Data Documentation
Expr CVC3::RWTheoremValue::d_lhs |
|
protected |
Expr CVC3::RWTheoremValue::d_rhs |
|
protected |
The documentation for this class was generated from the following file: