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

Referenced by CVC3::Theorem::isFlagged().

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

Definition at line 129 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 133 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 137 of file theorem_value.h.

References d_cachedValue.

Referenced by CVC3::Theorem::setCachedValue().

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

Definition at line 141 of file theorem_value.h.

References d_cachedValue.

Referenced by CVC3::Theorem::getCachedValue().

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

Definition at line 145 of file theorem_value.h.

References d_isSubst.

Referenced by CVC3::Theorem::setSubst().

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

Definition at line 146 of file theorem_value.h.

References d_isSubst.

Referenced by CVC3::Theorem::isSubst().

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

Definition at line 148 of file theorem_value.h.

References d_expand.

Referenced by CVC3::Theorem::setExpandFlag().

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

Definition at line 152 of file theorem_value.h.

References d_expand.

Referenced by CVC3::Theorem::getExpandFlag().

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

Definition at line 156 of file theorem_value.h.

References d_clauselit.

Referenced by CVC3::Theorem::setLitFlag().

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

Definition at line 160 of file theorem_value.h.

References d_clauselit.

Referenced by CVC3::Theorem::getLitFlag().

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

Definition at line 164 of file theorem_value.h.

References d_scopeLevel.

Referenced by CVC3::Theorem::getScope().

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

Definition at line 168 of file theorem_value.h.

References d_quantLevel.

Referenced by CVC3::Theorem::getQuantLevel().

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

Definition at line 170 of file theorem_value.h.

Referenced by CVC3::Theorem::getQuantLevelDebug().

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

Definition at line 175 of file theorem_value.h.

References d_quantLevel.

Referenced by CVC3::Theorem::setQuantLevel().

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(), getRHS(), and CVC3::Theorem::isRewrite().

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 CVC3::Theorem::getExpr(), and 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().

Referenced by CVC3::Theorem::getLHS().

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

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

References d_isAssump.

Referenced by CVC3::Theorem::isAssump().

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

Definition at line 316 of file theorem_value.h.

References d_proof.

Referenced by CVC3::Theorem::getProof().

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]

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 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

TheoremManager* CVC3::TheoremValue::d_tm [protected]

Theorem Manager.

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

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

Proof CVC3::TheoremValue::d_proof [protected]

Proof of the theorem.

Definition at line 71 of file theorem_value.h.

Referenced by getProof().

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

int CVC3::TheoremValue::d_scopeLevel [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]

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

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

int CVC3::TheoremValue::d_cachedValue [protected]

Temporary cache used during traversals.

Definition at line 90 of file theorem_value.h.

Referenced by getCachedValue(), and setCachedValue().

bool CVC3::TheoremValue::d_isSubst [protected]

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_isAssump [protected]

Definition at line 93 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 94 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 95 of file theorem_value.h.

Referenced by getLitFlag(), and setLitFlag().

The documentation for this class was generated from the following file:
Generated on Thu Oct 15 22:25:29 2009 for CVC3 by  doxygen 1.5.8