Collaboration diagram for CVC3::RegTheoremValue:

Public Member Functions
	~RegTheoremValue ()

const Assumptions &	getAssumptionsRef () const

MemoryManager *	getMM ()

void *	operator new (size_t size, MemoryManager *mm)

void	operator delete (void pMem, MemoryManager mm)

void	operator delete (void *d)

Public Member Functions inherited from CVC3::TheoremValue
virtual	~TheoremValue ()

std::string	toString () const

Protected Attributes
Assumptions	d_assump
	The assumptions for the theorem.

Protected Attributes inherited from CVC3::TheoremValue
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
	RegTheoremValue (TheoremManager *tm, const Expr &thm, const Assumptions &assump, const Proof &pf, bool isAssump, int scope=-1)

Detailed Description

Definition at line 343 of file theorem_value.h.

Constructor & Destructor Documentation

CVC3::RegTheoremValue::RegTheoremValue	(	TheoremManager *	tm,
		const Expr &	thm,
		const Assumptions &	assump,
		const Proof &	pf,
		bool	isAssump,
		int	scope = `-1`
	)