CVC3
2.4.1
|
#include <theorem_value.h>
Public Member Functions | |
virtual | ~TheoremValue () |
std::string | toString () const |
virtual MemoryManager * | getMM ()=0 |
Protected Attributes | |
TheoremManager * | d_tm |
Theorem Manager. | |
Expr | d_thm |
The expression representing a theorem. | |
Proof | d_proof |
Proof of the theorem. | |
unsigned | d_refcount |
How many pointers to this theorem value. | |
int | d_scopeLevel |
Largest scope level of the assumptions. | |
unsigned | d_quantLevel |
Quantification level of this theorem. | |
unsigned | d_flag |
debug quantlevel, this one is from proof, not from assumption list | |
int | d_cachedValue: 28 |
Temporary cache used during traversals. | |
bool | d_isSubst: 1 |
whether this theorem was generated by substitution | |
bool | d_isAssump: 1 |
bool | d_expand: 1 |
whether it should this be expanded in graph traversal | |
bool | d_clauselit: 1 |
whether it belongs to the conflict clause |
Private Member Functions | |
TheoremValue (TheoremManager *tm, const Expr &thm, const Proof &pf, bool isAssump) | |
TheoremValue (const TheoremValue &t) | |
TheoremValue & | operator= (const TheoremValue &t) |
bool | isFlagged () const |
void | clearAllFlags () |
void | setFlag () |
void | setCachedValue (int value) |
int | getCachedValue () const |
void | setSubst () |
bool | isSubst () |
void | setExpandFlag (bool val) |
bool | getExpandFlag () |
void | setLitFlag (bool val) |
bool | getLitFlag () |
int | getScope () |
unsigned | getQuantLevel () |
unsigned | getQuantLevelDebug () |
void | setQuantLevel (unsigned level) |
unsigned | recQuantLevel (Expr proof) |
unsigned | findQuantLevelDebug () |
virtual bool | isRewrite () const |
virtual const Expr & | getExpr () const |
virtual const Expr & | getLHS () const |
virtual const Expr & | getRHS () const |
virtual const Assumptions & | getAssumptionsRef () const =0 |
bool | isAssump () const |
const Proof & | getProof () |
Friends | |
class | Theorem |
class | RegTheoremValue |
class | RWTheoremValue |
Definition at line 56 of file theorem_value.h.
|
inlineprivate |
NOTE: it is private; only friend classes can call it.
If the assumptions refer to only one theorem, grab the assumptions of that theorem instead.
Definition at line 110 of file theorem_value.h.
|
inlineprivate |
Definition at line 117 of file theorem_value.h.
References FatalAssert.
|
inlinevirtual |
Definition at line 320 of file theorem_value.h.
References d_refcount, FatalAssert, and IF_DEBUG.
|
inlineprivate |
Definition at line 120 of file theorem_value.h.
References FatalAssert.
|
inlineprivate |
Definition at line 125 of file theorem_value.h.
References d_flag, d_tm, and CVC3::TheoremManager::getFlag().
Referenced by CVC3::Theorem::isFlagged().
|
inlineprivate |
Definition at line 129 of file theorem_value.h.
References CVC3::TheoremManager::clearAllFlags(), and d_tm.
Referenced by CVC3::Theorem::clearAllFlags().
|
inlineprivate |
Definition at line 133 of file theorem_value.h.
References d_flag, d_tm, and CVC3::TheoremManager::getFlag().
Referenced by CVC3::Theorem::setFlag().
|
inlineprivate |
Definition at line 137 of file theorem_value.h.
References d_cachedValue.
Referenced by CVC3::Theorem::setCachedValue().
|
inlineprivate |
Definition at line 141 of file theorem_value.h.
References d_cachedValue.
Referenced by CVC3::Theorem::getCachedValue().
|
inlineprivate |
Definition at line 145 of file theorem_value.h.
References d_isSubst.
Referenced by CVC3::Theorem::setSubst().
|
inlineprivate |
Definition at line 146 of file theorem_value.h.
References d_isSubst.
Referenced by CVC3::Theorem::isSubst().
|
inlineprivate |
Definition at line 148 of file theorem_value.h.
References d_expand.
Referenced by CVC3::Theorem::setExpandFlag().
|
inlineprivate |
Definition at line 152 of file theorem_value.h.
References d_expand.
Referenced by CVC3::Theorem::getExpandFlag().
|
inlineprivate |
Definition at line 156 of file theorem_value.h.
References d_clauselit.
Referenced by CVC3::Theorem::setLitFlag().
|
inlineprivate |
Definition at line 160 of file theorem_value.h.
References d_clauselit.
Referenced by CVC3::Theorem::getLitFlag().
|
inlineprivate |
Definition at line 164 of file theorem_value.h.
References d_scopeLevel.
Referenced by CVC3::Theorem::getScope().
|
inlineprivate |
Definition at line 168 of file theorem_value.h.
References d_quantLevel.
Referenced by CVC3::Theorem::getQuantLevel().
|
inlineprivate |
Definition at line 170 of file theorem_value.h.
Referenced by CVC3::Theorem::getQuantLevelDebug().
|
inlineprivate |
Definition at line 175 of file theorem_value.h.
References d_quantLevel.
Referenced by CVC3::Theorem::setQuantLevel().
|
inlineprivate |
Definition at line 177 of file theorem_value.h.
References d_quantLevel.
|
inlineprivate |
Definition at line 247 of file theorem_value.h.
References d_quantLevel.
|
inlineprivatevirtual |
Reimplemented in CVC3::RWTheoremValue.
Definition at line 295 of file theorem_value.h.
Referenced by getLHS(), getRHS(), and CVC3::Theorem::isRewrite().
|
inlineprivatevirtual |
Reimplemented in CVC3::RWTheoremValue.
Definition at line 297 of file theorem_value.h.
References d_thm.
Referenced by CVC3::VCL::deriveClosure(), CVC3::VCL::getAssumptions(), CVC3::Theorem::getExpr(), and toString().
|
inlineprivatevirtual |
Reimplemented in CVC3::RWTheoremValue.
Definition at line 298 of file theorem_value.h.
References d_thm, DebugAssert, isRewrite(), and toString().
Referenced by CVC3::Theorem::getLHS().
|
inlineprivatevirtual |
Reimplemented in CVC3::RWTheoremValue.
Definition at line 305 of file theorem_value.h.
References d_thm, DebugAssert, isRewrite(), and toString().
Referenced by CVC3::Theorem::getRHS().
|
privatepure virtual |
Implemented in CVC3::RWTheoremValue, and CVC3::RegTheoremValue.
Referenced by CVC3::Theorem::getAssumptionsRef(), and toString().
|
inlineprivate |
Definition at line 315 of file theorem_value.h.
References d_isAssump.
Referenced by CVC3::Theorem::isAssump().
|
inlineprivate |
Definition at line 316 of file theorem_value.h.
References d_proof.
Referenced by CVC3::Theorem::getProof().
|
inline |
Definition at line 325 of file theorem_value.h.
References getAssumptionsRef(), getExpr(), CVC3::Assumptions::toString(), and CVC3::Expr::toString().
|
pure virtual |
Implemented in CVC3::RWTheoremValue, and CVC3::RegTheoremValue.
Referenced by CVC3::Theorem::operator=(), and CVC3::Theorem::~Theorem().
|
friend |
Reimplemented in CVC3::RWTheoremValue, and CVC3::RegTheoremValue.
Definition at line 59 of file theorem_value.h.
|
friend |
Definition at line 60 of file theorem_value.h.
|
friend |
Definition at line 61 of file theorem_value.h.
|
protected |
Theorem Manager.
Definition at line 65 of file theorem_value.h.
Referenced by clearAllFlags(), CVC3::RegTheoremValue::getMM(), CVC3::RWTheoremValue::getMM(), CVC3::RWTheoremValue::init(), isFlagged(), CVC3::RegTheoremValue::RegTheoremValue(), setFlag(), CVC3::Theorem::withAssumptions(), and CVC3::Theorem::withProof().
|
protected |
The expression representing a theorem.
Definition at line 68 of file theorem_value.h.
Referenced by getExpr(), CVC3::RWTheoremValue::getExpr(), getLHS(), and getRHS().
|
protected |
|
protected |
How many pointers to this theorem value.
Definition at line 74 of file theorem_value.h.
Referenced by CVC3::RWTheoremValue::init(), CVC3::Theorem::operator=(), CVC3::Theorem::print(), CVC3::RegTheoremValue::RegTheoremValue(), CVC3::Theorem::Theorem(), CVC3::Theorem::~Theorem(), and ~TheoremValue().
|
protected |
Largest scope level of the assumptions.
Definition at line 77 of file theorem_value.h.
Referenced by getScope(), CVC3::RWTheoremValue::init(), and CVC3::RegTheoremValue::RegTheoremValue().
|
protected |
Quantification level of this theorem.
Definition at line 80 of file theorem_value.h.
Referenced by findQuantLevelDebug(), getQuantLevel(), CVC3::RWTheoremValue::init(), recQuantLevel(), CVC3::RegTheoremValue::RegTheoremValue(), and setQuantLevel().
|
protected |
debug quantlevel, this one is from proof, not from assumption list
Temporary flag used during traversals
Definition at line 87 of file theorem_value.h.
Referenced by isFlagged(), and setFlag().
|
protected |
Temporary cache used during traversals.
Definition at line 90 of file theorem_value.h.
Referenced by getCachedValue(), and setCachedValue().
|
protected |
whether this theorem was generated by substitution
Definition at line 92 of file theorem_value.h.
Referenced by isSubst(), and setSubst().
|
protected |
Definition at line 93 of file theorem_value.h.
Referenced by CVC3::RWTheoremValue::init(), isAssump(), CVC3::RegTheoremValue::~RegTheoremValue(), and CVC3::RWTheoremValue::~RWTheoremValue().
|
protected |
whether it should this be expanded in graph traversal
Definition at line 94 of file theorem_value.h.
Referenced by getExpandFlag(), and setExpandFlag().
|
protected |
whether it belongs to the conflict clause
Definition at line 95 of file theorem_value.h.
Referenced by getLitFlag(), and setLitFlag().