CVC3
Public Member Functions | Protected Attributes | Private Member Functions | Friends

CVC3::TheoremValue Class Reference

#include <theorem_value.h>

Inherited by CVC3::RegTheoremValue, and CVC3::RWTheoremValue.

Collaboration diagram for CVC3::TheoremValue:
Collaboration graph
[legend]

List of all members.

Public Member Functions

Protected Attributes

Private Member Functions

Friends


Detailed Description

Definition at line 56 of file theorem_value.h.


Constructor & Destructor Documentation

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 110 of file theorem_value.h.

CVC3::TheoremValue::TheoremValue ( const TheoremValue t) [inline, private]

Definition at line 117 of file theorem_value.h.

References FatalAssert.

virtual CVC3::TheoremValue::~TheoremValue ( ) [inline, virtual]

Definition at line 320 of file theorem_value.h.

References d_refcount, FatalAssert, and IF_DEBUG.


Member Function Documentation

TheoremValue& CVC3::TheoremValue::operator= ( const TheoremValue t) [inline, private]

Definition at line 120 of file theorem_value.h.

References FatalAssert.

bool CVC3::TheoremValue::isFlagged ( ) const [inline, private]

Definition at line 125 of file theorem_value.h.

References d_flag, d_tm, and CVC3::TheoremManager::getFlag().

void CVC3::TheoremValue::clearAllFlags ( ) [inline, private]

Definition at line 129 of file theorem_value.h.

References CVC3::TheoremManager::clearAllFlags(), and d_tm.

void CVC3::TheoremValue::setFlag ( ) [inline, private]

Definition at line 133 of file theorem_value.h.

References d_flag, d_tm, and CVC3::TheoremManager::getFlag().

void CVC3::TheoremValue::setCachedValue ( int  value) [inline, private]

Definition at line 137 of file theorem_value.h.

References d_cachedValue.

int CVC3::TheoremValue::getCachedValue ( ) const [inline, private]

Definition at line 141 of file theorem_value.h.

References d_cachedValue.

void CVC3::TheoremValue::setSubst ( ) [inline, private]

Definition at line 145 of file theorem_value.h.

References d_isSubst.

bool CVC3::TheoremValue::isSubst ( ) [inline, private]

Definition at line 146 of file theorem_value.h.

References d_isSubst.

void CVC3::TheoremValue::setExpandFlag ( bool  val) [inline, private]

Definition at line 148 of file theorem_value.h.

References d_expand.

bool CVC3::TheoremValue::getExpandFlag ( ) [inline, private]

Definition at line 152 of file theorem_value.h.

References d_expand.

void CVC3::TheoremValue::setLitFlag ( bool  val) [inline, private]

Definition at line 156 of file theorem_value.h.

References d_clauselit.

bool CVC3::TheoremValue::getLitFlag ( ) [inline, private]

Definition at line 160 of file theorem_value.h.

References d_clauselit.

int CVC3::TheoremValue::getScope ( ) [inline, private]

Definition at line 164 of file theorem_value.h.

References d_scopeLevel.

unsigned CVC3::TheoremValue::getQuantLevel ( ) [inline, private]

Definition at line 168 of file theorem_value.h.

References d_quantLevel.

unsigned CVC3::TheoremValue::getQuantLevelDebug ( ) [inline, private]

Definition at line 170 of file theorem_value.h.

void CVC3::TheoremValue::setQuantLevel ( unsigned  level) [inline, private]

Definition at line 175 of file theorem_value.h.

References d_quantLevel.

unsigned CVC3::TheoremValue::recQuantLevel ( Expr  proof) [inline, private]

Definition at line 177 of file theorem_value.h.

References d_quantLevel.

unsigned CVC3::TheoremValue::findQuantLevelDebug ( ) [inline, private]

Definition at line 247 of file theorem_value.h.

References d_quantLevel.

virtual bool CVC3::TheoremValue::isRewrite ( ) const [inline, private, virtual]

Reimplemented in CVC3::RWTheoremValue.

Definition at line 295 of file theorem_value.h.

Referenced by getLHS(), and getRHS().

virtual const Expr& CVC3::TheoremValue::getExpr ( ) const [inline, private, virtual]

Reimplemented in CVC3::RWTheoremValue.

Definition at line 297 of file theorem_value.h.

References d_thm.

Referenced by toString().

virtual const Expr& CVC3::TheoremValue::getLHS ( ) const [inline, private, virtual]

Reimplemented in CVC3::RWTheoremValue.

Definition at line 298 of file theorem_value.h.

References d_thm, DebugAssert, isRewrite(), and toString().

virtual const Expr& CVC3::TheoremValue::getRHS ( ) const [inline, private, virtual]

Reimplemented in CVC3::RWTheoremValue.

Definition at line 305 of file theorem_value.h.

References d_thm, DebugAssert, isRewrite(), and toString().

virtual const Assumptions& CVC3::TheoremValue::getAssumptionsRef ( ) const [private, pure virtual]
bool CVC3::TheoremValue::isAssump ( ) const [inline, private]

Definition at line 315 of file theorem_value.h.

References d_isAssump.

const Proof& CVC3::TheoremValue::getProof ( ) [inline, private]

Definition at line 316 of file theorem_value.h.

References d_proof.

std::string CVC3::TheoremValue::toString ( ) const [inline]

Definition at line 325 of file theorem_value.h.

References getAssumptionsRef(), getExpr(), CVC3::Expr::toString(), and CVC3::Assumptions::toString().

Referenced by getLHS(), and getRHS().

virtual MemoryManager* CVC3::TheoremValue::getMM ( ) [pure virtual]

Friends And Related Function Documentation

friend class Theorem [friend]

Reimplemented in CVC3::RegTheoremValue, and CVC3::RWTheoremValue.

Definition at line 59 of file theorem_value.h.

friend class RegTheoremValue [friend]

Definition at line 60 of file theorem_value.h.

friend class RWTheoremValue [friend]

Definition at line 61 of file theorem_value.h.


Member Data Documentation

The expression representing a theorem.

Definition at line 68 of file theorem_value.h.

Referenced by CVC3::RWTheoremValue::getExpr(), getExpr(), getLHS(), and getRHS().

Proof of the theorem.

Definition at line 71 of file theorem_value.h.

Referenced by getProof().

unsigned CVC3::TheoremValue::d_refcount [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().

unsigned CVC3::TheoremValue::d_quantLevel [protected]
unsigned CVC3::TheoremValue::d_flag [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().

Temporary cache used during traversals.

Definition at line 90 of file theorem_value.h.

Referenced by getCachedValue(), and setCachedValue().

whether this theorem was generated by substitution

Definition at line 92 of file theorem_value.h.

Referenced by isSubst(), and setSubst().

bool CVC3::TheoremValue::d_expand [protected]

whether it should this be expanded in graph traversal

Definition at line 94 of file theorem_value.h.

Referenced by getExpandFlag(), and setExpandFlag().

whether it belongs to the conflict clause

Definition at line 95 of file theorem_value.h.

Referenced by getLitFlag(), and setLitFlag().


The documentation for this class was generated from the following file: