CVC3::TheoremValue Class Reference

#include <theorem_value.h>

Inheritance diagram for CVC3::TheoremValue:

Inheritance graph
[legend]
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 59 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 104 of file theorem_value.h.

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

Definition at line 110 of file theorem_value.h.

References FatalAssert.

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

Definition at line 187 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 113 of file theorem_value.h.

References FatalAssert.

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().

Referenced by getLHS(), and getRHS().

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

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

Referenced by CVC3::Theorem::operator=(), and CVC3::Theorem::~Theorem().


Friends And Related Function Documentation

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.


Member Data Documentation

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]

Proof of the theorem.

Definition at line 74 of file theorem_value.h.

Referenced by getProof().

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().


The documentation for this class was generated from the following file:
Generated on Tue Jul 3 14:41:17 2007 for CVC3 by  doxygen 1.5.1