#include <theorem_value.h>
Inheritance diagram for CVC3::TheoremValue:
Definition at line 59 of file theorem_value.h.
CVC3::TheoremValue::TheoremValue | ( | TheoremManager * | tm, | |
const Expr & | thm, | |||
const Proof & | pf, | |||
bool | isAssump | |||
) | [inline, private] |
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 104 of file theorem_value.h.
CVC3::TheoremValue::TheoremValue | ( | const TheoremValue & | t | ) | [inline, private] |
virtual CVC3::TheoremValue::~TheoremValue | ( | ) | [inline, virtual] |
TheoremValue& CVC3::TheoremValue::operator= | ( | const TheoremValue & | t | ) | [inline, private] |
bool CVC3::TheoremValue::isFlagged | ( | ) | const [inline, private] |
Definition at line 118 of file theorem_value.h.
References d_flag, d_tm, and CVC3::TheoremManager::getFlag().
Referenced by CVC3::Theorem::isFlagged().
void CVC3::TheoremValue::clearAllFlags | ( | ) | [inline, private] |
Definition at line 122 of file theorem_value.h.
References CVC3::TheoremManager::clearAllFlags(), and d_tm.
Referenced by CVC3::Theorem::clearAllFlags().
void CVC3::TheoremValue::setFlag | ( | ) | [inline, private] |
Definition at line 126 of file theorem_value.h.
References d_flag, d_tm, and CVC3::TheoremManager::getFlag().
Referenced by CVC3::Theorem::setFlag().
void CVC3::TheoremValue::setCachedValue | ( | int | value | ) | [inline, private] |
Definition at line 130 of file theorem_value.h.
References d_cachedValue.
Referenced by CVC3::Theorem::setCachedValue().
int CVC3::TheoremValue::getCachedValue | ( | ) | const [inline, private] |
Definition at line 134 of file theorem_value.h.
References d_cachedValue.
Referenced by CVC3::Theorem::getCachedValue().
void CVC3::TheoremValue::setExpandFlag | ( | bool | val | ) | [inline, private] |
Definition at line 138 of file theorem_value.h.
References d_expand.
Referenced by CVC3::Theorem::setExpandFlag().
bool CVC3::TheoremValue::getExpandFlag | ( | ) | [inline, private] |
Definition at line 142 of file theorem_value.h.
References d_expand.
Referenced by CVC3::Theorem::getExpandFlag().
void CVC3::TheoremValue::setLitFlag | ( | bool | val | ) | [inline, private] |
Definition at line 146 of file theorem_value.h.
References d_clauselit.
Referenced by CVC3::Theorem::setLitFlag().
bool CVC3::TheoremValue::getLitFlag | ( | ) | [inline, private] |
Definition at line 150 of file theorem_value.h.
References d_clauselit.
Referenced by CVC3::Theorem::getLitFlag().
int CVC3::TheoremValue::getScope | ( | ) | [inline, private] |
Definition at line 154 of file theorem_value.h.
References d_scopeLevel.
Referenced by CVC3::Theorem::getScope().
unsigned CVC3::TheoremValue::getQuantLevel | ( | ) | [inline, private] |
Definition at line 158 of file theorem_value.h.
References d_quantLevel.
Referenced by CVC3::Theorem::getQuantLevel().
void CVC3::TheoremValue::setQuantLevel | ( | unsigned | level | ) | [inline, private] |
Definition at line 159 of file theorem_value.h.
References d_quantLevel.
Referenced by CVC3::Theorem::setQuantLevel().
virtual bool CVC3::TheoremValue::isRewrite | ( | ) | const [inline, private, virtual] |
Reimplemented in CVC3::RWTheoremValue.
Definition at line 162 of file theorem_value.h.
Referenced by getLHS(), getRHS(), and CVC3::Theorem::isRewrite().
virtual const Expr& CVC3::TheoremValue::getExpr | ( | ) | const [inline, private, virtual] |
Reimplemented in CVC3::RWTheoremValue.
Definition at line 164 of file theorem_value.h.
References d_thm.
Referenced by CVC3::Theorem::getExpr(), and toString().
virtual const Expr& CVC3::TheoremValue::getLHS | ( | ) | const [inline, private, virtual] |
Reimplemented in CVC3::RWTheoremValue.
Definition at line 165 of file theorem_value.h.
References d_thm, DebugAssert, isRewrite(), and toString().
Referenced by CVC3::Theorem::getLHS().
virtual const Expr& CVC3::TheoremValue::getRHS | ( | ) | const [inline, private, virtual] |
Reimplemented in CVC3::RWTheoremValue.
Definition at line 172 of file theorem_value.h.
References d_thm, DebugAssert, isRewrite(), and toString().
Referenced by CVC3::Theorem::getRHS().
virtual const Assumptions& CVC3::TheoremValue::getAssumptionsRef | ( | ) | const [private, pure virtual] |
Implemented in CVC3::RegTheoremValue, and CVC3::RWTheoremValue.
Referenced by CVC3::Theorem::getAssumptionsRef(), and toString().
bool CVC3::TheoremValue::isAssump | ( | ) | const [inline, private] |
Definition at line 182 of file theorem_value.h.
References d_isAssump.
Referenced by CVC3::Theorem::isAssump().
const Proof& CVC3::TheoremValue::getProof | ( | ) | [inline, private] |
Definition at line 183 of file theorem_value.h.
References d_proof.
Referenced by CVC3::Theorem::getProof().
std::string CVC3::TheoremValue::toString | ( | ) | const [inline] |
Definition at line 192 of file theorem_value.h.
References getAssumptionsRef(), getExpr(), CVC3::Expr::toString(), and CVC3::Assumptions::toString().
virtual MemoryManager* CVC3::TheoremValue::getMM | ( | ) | [pure virtual] |
Implemented in CVC3::RegTheoremValue, and CVC3::RWTheoremValue.
Referenced by CVC3::Theorem::operator=(), and CVC3::Theorem::~Theorem().
friend class Theorem [friend] |
Reimplemented in CVC3::RegTheoremValue, and CVC3::RWTheoremValue.
Definition at line 62 of file theorem_value.h.
friend class RegTheoremValue [friend] |
Definition at line 63 of file theorem_value.h.
friend class RWTheoremValue [friend] |
Definition at line 64 of file theorem_value.h.
TheoremManager* CVC3::TheoremValue::d_tm [protected] |
Theorem Manager.
Definition at line 68 of file theorem_value.h.
Referenced by clearAllFlags(), CVC3::RWTheoremValue::getMM(), CVC3::RegTheoremValue::getMM(), CVC3::RWTheoremValue::init(), isFlagged(), CVC3::RegTheoremValue::RegTheoremValue(), setFlag(), CVC3::Theorem::withAssumptions(), and CVC3::Theorem::withProof().
Expr CVC3::TheoremValue::d_thm [protected] |
The expression representing a theorem.
Definition at line 71 of file theorem_value.h.
Referenced by CVC3::RWTheoremValue::getExpr(), getExpr(), getLHS(), getRHS(), and CVC3::RWTheoremValue::init().
Proof CVC3::TheoremValue::d_proof [protected] |
unsigned CVC3::TheoremValue::d_refcount [protected] |
How many pointers to this theorem value.
Definition at line 77 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().
int CVC3::TheoremValue::d_scopeLevel [protected] |
Largest scope level of the assumptions.
Definition at line 80 of file theorem_value.h.
Referenced by getScope(), CVC3::RWTheoremValue::init(), and CVC3::RegTheoremValue::RegTheoremValue().
unsigned CVC3::TheoremValue::d_quantLevel [protected] |
Quantification level of this theorem.
Definition at line 83 of file theorem_value.h.
Referenced by getQuantLevel(), CVC3::RWTheoremValue::init(), CVC3::RegTheoremValue::RegTheoremValue(), and setQuantLevel().
unsigned CVC3::TheoremValue::d_flag [protected] |
Temporary flag used during traversals.
Definition at line 86 of file theorem_value.h.
Referenced by isFlagged(), and setFlag().
int CVC3::TheoremValue::d_cachedValue [protected] |
Temporary cache used during traversals.
Definition at line 89 of file theorem_value.h.
Referenced by getCachedValue(), and setCachedValue().
bool CVC3::TheoremValue::d_isAssump [protected] |
Definition at line 91 of file theorem_value.h.
Referenced by CVC3::RWTheoremValue::init(), isAssump(), CVC3::RegTheoremValue::~RegTheoremValue(), and CVC3::RWTheoremValue::~RWTheoremValue().
bool CVC3::TheoremValue::d_expand [protected] |
whether it should this be expanded in graph traversal
Definition at line 92 of file theorem_value.h.
Referenced by getExpandFlag(), and setExpandFlag().
bool CVC3::TheoremValue::d_clauselit [protected] |
whether it belongs to the conflict clause
Definition at line 93 of file theorem_value.h.
Referenced by getLitFlag(), and setLitFlag().