CVC3::TheoremValue Class Reference

#include <theorem_value.h>

Inheritance diagram for CVC3::TheoremValue:

[legend]Collaboration diagram for CVC3::TheoremValue:

[legend]List of all members.

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

  Temporary flag used during traversals.
  

• 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

---

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

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]

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:

• theorem_value.h

---