CVC3
2.4.1
|
#include <theorem_value.h>
Public Member Functions | |
~RWTheoremValue () | |
bool | isRewrite () const |
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 | |
Expr | d_lhs |
Expr | d_rhs |
Assumptions * | d_assump |
![]() | |
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 | |
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 |
Friends | |
class | Theorem |
Definition at line 432 of file theorem_value.h.
|
inlineprivate |
Definition at line 487 of file theorem_value.h.
|
inlineprivate |
Definition at line 494 of file theorem_value.h.
|
inline |
Definition at line 516 of file theorem_value.h.
References CVC3::TheoremValue::d_isAssump, CVC3::Theorem::d_thm, FatalAssert, CVC3::Assumptions::getFirst(), IF_DEBUG, CVC3::Assumptions::size(), and CVC3::Theorem::thm().
|
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_scopeLevel, DebugAssert, CVC3::Assumptions::empty(), CVC3::Assumptions::end(), CVC3::TheoremManager::getCM(), CVC3::Theorem::getScope(), CVC3::TheoremManager::isActive(), CVC3::ContextManager::scopeLevel(), and TRACE.
|
inlineprivatevirtual |
Reimplemented from CVC3::TheoremValue.
Definition at line 500 of file theorem_value.h.
References CVC3::TheoremValue::d_thm, CVC3::Expr::eqExpr(), CVC3::Expr::getType(), CVC3::Expr::iffExpr(), CVC3::Type::isBool(), and CVC3::Expr::isNull().
|
inlineprivatevirtual |
Reimplemented from CVC3::TheoremValue.
Definition at line 511 of file theorem_value.h.
|
inlineprivatevirtual |
Reimplemented from CVC3::TheoremValue.
Definition at line 512 of file theorem_value.h.
|
inlinevirtual |
Reimplemented from CVC3::TheoremValue.
Definition at line 525 of file theorem_value.h.
|
inlinevirtual |
Implements CVC3::TheoremValue.
Definition at line 526 of file theorem_value.h.
References CVC3::Assumptions::emptyAssump().
|
inlinevirtual |
Implements CVC3::TheoremValue.
Definition at line 532 of file theorem_value.h.
References CVC3::TheoremManager::getRWMM().
|
inline |
Definition at line 534 of file theorem_value.h.
References CVC3::MemoryManager::newData().
|
inline |
Definition at line 537 of file theorem_value.h.
|
inline |
Definition at line 541 of file theorem_value.h.
|
friend |
Definition at line 434 of file theorem_value.h.
|
protected |
Definition at line 439 of file theorem_value.h.
|
protected |
Definition at line 440 of file theorem_value.h.
|
protected |
Definition at line 441 of file theorem_value.h.