#include <theorem_value.h>

Collaboration diagram for CVC3::RWTheoremValue:

Public Member Functions
	~RWTheoremValue ()

bool	isRewrite () const

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

Expr	d_rhs

Assumptions *	d_assump

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
void	init (const Assumptions &assump, int scope)

	RWTheoremValue (TheoremManager *tm, const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf, bool isAssump, int scope=-1)

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

const Expr &	getExpr () const

const Expr &	getLHS () const

const Expr &	getRHS () const

Friends
class	Theorem

Detailed Description

Definition at line 432 of file theorem_value.h.

Constructor & Destructor Documentation

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

inlineprivate

Definition at line 487 of file theorem_value.h.

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

inlineprivate

Definition at line 494 of file theorem_value.h.

CVC3::RWTheoremValue::~RWTheoremValue ( )

inline

Definition at line 516 of file theorem_value.h.

References CVC3::TheoremValue::d_isAssump, FatalAssert, and IF_DEBUG.

Member Function Documentation

void CVC3::RWTheoremValue::init	(	const Assumptions &	assump,
		int	scope
	)

inlineprivate

Definition at line 444 of file theorem_value.h.

References CVC3::Assumptions::begin(), CVC3::TheoremValue::d_isAssump, CVC3::TheoremValue::d_quantLevel, CVC3::TheoremValue::d_refcount, CVC3::TheoremValue::d_scopeLevel, CVC3::TheoremValue::d_tm, DebugAssert, CVC3::Assumptions::empty(), CVC3::Assumptions::end(), CVC3::TheoremManager::getCM(), CVC3::TheoremManager::isActive(), CVC3::ContextManager::scopeLevel(), and TRACE.

const Expr& CVC3::RWTheoremValue::getExpr ( ) const

inlineprivatevirtual

Reimplemented from CVC3::TheoremValue.

Definition at line 500 of file theorem_value.h.

References CVC3::TheoremValue::d_thm, CVC3::Expr::eqExpr(), CVC3::Expr::getType(), CVC3::Expr::iffExpr(), CVC3::Type::isBool(), and CVC3::Expr::isNull().

const Expr& CVC3::RWTheoremValue::getLHS ( ) const

inlineprivatevirtual

Reimplemented from CVC3::TheoremValue.

Definition at line 511 of file theorem_value.h.

const Expr& CVC3::RWTheoremValue::getRHS ( ) const

inlineprivatevirtual

Reimplemented from CVC3::TheoremValue.

Definition at line 512 of file theorem_value.h.

bool CVC3::RWTheoremValue::isRewrite ( ) const

inlinevirtual

Reimplemented from CVC3::TheoremValue.

Definition at line 525 of file theorem_value.h.

const Assumptions& CVC3::RWTheoremValue::getAssumptionsRef ( ) const

inlinevirtual

Implements CVC3::TheoremValue.

Definition at line 526 of file theorem_value.h.

References CVC3::Assumptions::emptyAssump().

MemoryManager* CVC3::RWTheoremValue::getMM ( )

inlinevirtual

Implements CVC3::TheoremValue.

Definition at line 532 of file theorem_value.h.

References CVC3::TheoremValue::d_tm, and CVC3::TheoremManager::getRWMM().

void* CVC3::RWTheoremValue::operator new	(	size_t	size,
		MemoryManager *	mm
	)

inline

Definition at line 534 of file theorem_value.h.

References CVC3::MemoryManager::newData().

void CVC3::RWTheoremValue::operator delete	(	void *	pMem,
		MemoryManager *	mm
	)

inline

Definition at line 537 of file theorem_value.h.

void CVC3::RWTheoremValue::operator delete ( void * d )

inline

Definition at line 541 of file theorem_value.h.

Friends And Related Function Documentation

friend class Theorem

friend

Definition at line 434 of file theorem_value.h.

Member Data Documentation

Expr CVC3::RWTheoremValue::d_lhs

protected

Definition at line 439 of file theorem_value.h.

Expr CVC3::RWTheoremValue::d_rhs

protected

Definition at line 440 of file theorem_value.h.

Assumptions* CVC3::RWTheoremValue::d_assump

protected

Definition at line 441 of file theorem_value.h.

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