CVC3
2.4.1
|
#include <theorem_value.h>
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) |
![]() | |
virtual | ~TheoremValue () |
std::string | toString () const |
Protected Attributes | |
Assumptions | d_assump |
The assumptions for the theorem. More... | |
![]() | |
TheoremManager * | d_tm |
Theorem Manager. More... | |
Expr | d_thm |
The expression representing a theorem. More... | |
Proof | d_proof |
Proof of the theorem. More... | |
unsigned | d_refcount |
How many pointers to this theorem value. More... | |
int | d_scopeLevel |
Largest scope level of the assumptions. More... | |
unsigned | d_quantLevel |
Quantification level of this theorem. More... | |
unsigned | d_flag |
debug quantlevel, this one is from proof, not from assumption list More... | |
int | d_cachedValue: 28 |
Temporary cache used during traversals. More... | |
bool | d_isSubst: 1 |
whether this theorem was generated by substitution More... | |
bool | d_isAssump: 1 |
bool | d_expand: 1 |
whether it should this be expanded in graph traversal More... | |
bool | d_clauselit: 1 |
whether it belongs to the conflict clause More... | |
Private Member Functions | |
RegTheoremValue (TheoremManager *tm, const Expr &thm, const Assumptions &assump, const Proof &pf, bool isAssump, int scope=-1) | |
Friends | |
class | Theorem |
Definition at line 343 of file theorem_value.h.
|
inlineprivate |
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 TRACE.
|
inline |
Definition at line 397 of file theorem_value.h.
References CVC3::TheoremValue::d_isAssump, FatalAssert, and IF_DEBUG.
|
inlinevirtual |
Implements CVC3::TheoremValue.
Definition at line 405 of file theorem_value.h.
|
inlinevirtual |
Implements CVC3::TheoremValue.
Definition at line 408 of file theorem_value.h.
References CVC3::TheoremValue::d_tm, and CVC3::TheoremManager::getMM().
|
inline |
Definition at line 410 of file theorem_value.h.
References CVC3::MemoryManager::newData().
|
inline |
Definition at line 413 of file theorem_value.h.
|
inline |
Definition at line 417 of file theorem_value.h.
|
friend |
Definition at line 345 of file theorem_value.h.
|
protected |
The assumptions for the theorem.
Definition at line 349 of file theorem_value.h.