#include <theorem_value.h>

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

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
debug quantlevel, this one is from proof, not from assumption list
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

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]

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.

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]

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

Referenced by 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(), and setFlag().

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

theorem_value.h

CVC3::TheoremValue Class Reference

Public Member Functions

Protected Attributes

Private Member Functions

Friends

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Friends And Related Function Documentation

Member Data Documentation