#include <theorem_value.h>

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

Collaboration diagram for CVC3::TheoremValue:

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

inlineprivate

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 )

inlineprivate

Definition at line 117 of file theorem_value.h.

References FatalAssert.

virtual CVC3::TheoremValue::~TheoremValue ( )

inlinevirtual

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 )

inlineprivate

Definition at line 120 of file theorem_value.h.

References FatalAssert.

bool CVC3::TheoremValue::isFlagged ( ) const

inlineprivate

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

inlineprivate

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

inlineprivate

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 )

inlineprivate

Definition at line 137 of file theorem_value.h.

References d_cachedValue.

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

int CVC3::TheoremValue::getCachedValue ( ) const

inlineprivate

Definition at line 141 of file theorem_value.h.

References d_cachedValue.

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

void CVC3::TheoremValue::setSubst ( )

inlineprivate

Definition at line 145 of file theorem_value.h.

References d_isSubst.

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

bool CVC3::TheoremValue::isSubst ( )

inlineprivate

Definition at line 146 of file theorem_value.h.

References d_isSubst.

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

void CVC3::TheoremValue::setExpandFlag ( bool val )

inlineprivate

Definition at line 148 of file theorem_value.h.

References d_expand.

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

bool CVC3::TheoremValue::getExpandFlag ( )

inlineprivate

Definition at line 152 of file theorem_value.h.

References d_expand.

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

void CVC3::TheoremValue::setLitFlag ( bool val )

inlineprivate

Definition at line 156 of file theorem_value.h.

References d_clauselit.

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

bool CVC3::TheoremValue::getLitFlag ( )

inlineprivate

Definition at line 160 of file theorem_value.h.

References d_clauselit.

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

int CVC3::TheoremValue::getScope ( )

inlineprivate

Definition at line 164 of file theorem_value.h.

References d_scopeLevel.

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

unsigned CVC3::TheoremValue::getQuantLevel ( )

inlineprivate

Definition at line 168 of file theorem_value.h.

References d_quantLevel.

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

unsigned CVC3::TheoremValue::getQuantLevelDebug ( )

inlineprivate

Definition at line 170 of file theorem_value.h.

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

void CVC3::TheoremValue::setQuantLevel ( unsigned level )

inlineprivate

Definition at line 175 of file theorem_value.h.

References d_quantLevel.

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

unsigned CVC3::TheoremValue::recQuantLevel ( Expr proof )

inlineprivate

Definition at line 177 of file theorem_value.h.

References d_quantLevel.

unsigned CVC3::TheoremValue::findQuantLevelDebug ( )

inlineprivate

Definition at line 247 of file theorem_value.h.

References d_quantLevel.

virtual bool CVC3::TheoremValue::isRewrite ( ) const

inlineprivatevirtual

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

inlineprivatevirtual

Reimplemented in CVC3::RWTheoremValue.

Definition at line 297 of file theorem_value.h.

References d_thm.

Referenced by CVC3::VCL::deriveClosure(), CVC3::VCL::getAssumptions(), CVC3::Theorem::getExpr(), and toString().

virtual const Expr& CVC3::TheoremValue::getLHS ( ) const

inlineprivatevirtual

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

inlineprivatevirtual

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

privatepure virtual

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

Referenced by CVC3::Theorem::getAssumptionsRef(), and toString().

bool CVC3::TheoremValue::isAssump ( ) const

inlineprivate

Definition at line 315 of file theorem_value.h.

References d_isAssump.

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

const Proof& CVC3::TheoremValue::getProof ( )

inlineprivate

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::Assumptions::toString(), and CVC3::Expr::toString().

Referenced by getLHS(), and getRHS().

virtual MemoryManager* CVC3::TheoremValue::getMM ( )

pure virtual

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

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

Friends And Related Function Documentation

friend class Theorem

friend

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::RegTheoremValue::getMM(), CVC3::RWTheoremValue::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 getExpr(), CVC3::RWTheoremValue::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:

theorem_value.h

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