CVC3::VariableValue Class Reference

#include <variable.h>

Collaboration diagram for CVC3::VariableValue:

[legend]List of all members.

Public Member Functions

~VariableValue ()
const Expr & getExpr () const
const Expr & getNegExpr () const
int getValue () const
int getScope () const
const Theorem & getTheorem () const
const Clause & getAntecedent () const
int getAntecedentIdx () const
const Theorem & getAssumpThm () const
void setValue (int val, const Clause &c, int idx)
void setValue (const Theorem &thm, int scope)
void setAssumpThm (const Theorem &a, int scope)
unsigned & count (bool neg)
unsigned & countPrev (bool neg)
int & score (bool neg)
bool & added (bool neg)
void * operator new (size_t size, MemoryManager *mm)
void operator delete (void *pMem, MemoryManager *mm)
void operator delete (void *)

Private Member Functions

VariableValue (VariableManager *vm, const Expr &e)

Private Attributes

VariableManager * d_vm
int d_refcount
Expr d_expr
Expr d_neg
unsigned d_count
unsigned d_countPrev
int d_score
unsigned d_negCount
unsigned d_negCountPrev
int d_negScore
bool d_added
bool d_negAdded
std::vector< std::pair< Clause,
int > > d_wp
std::vector< std::pair< Clause,
int > > d_negwp
CDO< int > * d_val
CDO< int > * d_scope
CDO< Theorem > * d_thm
CDO< Clause > * d_ante
CDO< int > * d_anteIdx
CDO< Theorem > * d_assump

Friends

class Variable
class VariableManager
std::ostream & operator<< (std::ostream &os, const VariableValue &v)
bool operator== (const VariableValue &v1, const VariableValue &v2)

Detailed Description

Definition at line 206 of file variable.h.

Constructor & Destructor Documentation

CVC3::VariableValue::VariableValue	(	VariableManager *	vm,
		const Expr &	e
	)			`[inline, private]`

Definition at line 245 of file variable.h.

CVC3::VariableValue::~VariableValue ( )

Definition at line 230 of file variable.cpp.

References d_ante, d_anteIdx, d_assump, d_scope, d_thm, and d_val.

Member Function Documentation

const Expr& CVC3::VariableValue::getExpr ( ) const [inline]

Definition at line 255 of file variable.h.

References d_expr.

Referenced by CVC3::Variable::getExpr(), CVC3::VariableManager::EqLV::operator()(), CVC3::VariableManager::HashLV::operator()(), CVC3::operator<<(), and setValue().

const Expr& CVC3::VariableValue::getNegExpr ( ) const [inline]

Definition at line 257 of file variable.h.

References d_expr, d_neg, CVC3::Expr::isNull(), and CVC3::Expr::negate().

Referenced by CVC3::Variable::getNegExpr().

int CVC3::VariableValue::getValue ( ) const [inline]

Definition at line 265 of file variable.h.

References d_val, and CVC3::CDO< T >::get().

Referenced by CVC3::Variable::getValue(), CVC3::operator<<(), and setValue().

int CVC3::VariableValue::getScope ( ) const [inline]

Definition at line 270 of file variable.h.

References d_scope, and CVC3::CDO< T >::get().

Referenced by CVC3::Variable::getScope(), CVC3::operator<<(), and setValue().

const Theorem& CVC3::VariableValue::getTheorem ( ) const [inline]

Definition at line 275 of file variable.h.

References d_thm, and CVC3::CDO< T >::get().

Referenced by CVC3::Variable::getTheorem(), CVC3::operator<<(), and setValue().

const Clause& CVC3::VariableValue::getAntecedent ( ) const [inline]

Definition at line 281 of file variable.h.

References d_ante, and CVC3::CDO< T >::get().

Referenced by CVC3::Variable::getAntecedent(), CVC3::operator<<(), and setValue().

int CVC3::VariableValue::getAntecedentIdx ( ) const [inline]

Definition at line 287 of file variable.h.

References d_anteIdx, and CVC3::CDO< T >::get().

Referenced by CVC3::Variable::getAntecedentIdx(), and CVC3::operator<<().

const Theorem& CVC3::VariableValue::getAssumpThm ( ) const [inline]

Definition at line 292 of file variable.h.

References d_assump, and CVC3::CDO< T >::get().

Referenced by CVC3::Variable::getAssumpThm().

void CVC3::VariableValue::setValue	(	int	val,
		const Clause &	c,
		int	idx
	)

Definition at line 242 of file variable.cpp.

References d_ante, d_anteIdx, d_scope, d_thm, d_val, d_vm, DebugAssert, CVC3::VariableManager::getCM(), CVC3::ContextManager::getCurrentContext(), getExpr(), getScope(), CVC3::Clause::getScope(), getTheorem(), getValue(), IF_DEBUG, CVC3::CDO< T >::set(), CVC3::Clause::size(), CVC3::Expr::toString(), and CVC3::Clause::toString().

Referenced by CVC3::Variable::deriveThmRec(), and CVC3::Variable::setValue().

void CVC3::VariableValue::setValue	(	const Theorem &	thm,
		int	scope
	)

Definition at line 295 of file variable.cpp.

References d_ante, d_expr, d_scope, d_thm, d_val, d_vm, DebugAssert, getAntecedent(), CVC3::VariableManager::getCM(), CVC3::ContextManager::getCurrentContext(), CVC3::Theorem::getExpr(), IF_DEBUG, CVC3::CDO< T >::set(), CVC3::Expr::toString(), and CVC3::Theorem::toString().

void CVC3::VariableValue::setAssumpThm	(	const Theorem &	a,
		int	scope
	)

Definition at line 328 of file variable.cpp.

References d_assump, d_val, d_vm, CVC3::VariableManager::getCM(), CVC3::ContextManager::getCurrentContext(), IF_DEBUG, and CVC3::CDO< T >::set().

Referenced by CVC3::Variable::setAssumpThm().

unsigned& CVC3::VariableValue::count ( bool neg ) [inline]

Definition at line 308 of file variable.h.

References d_count, and d_negCount.

Referenced by CVC3::Variable::count().

unsigned& CVC3::VariableValue::countPrev ( bool neg ) [inline]

Definition at line 312 of file variable.h.

References d_countPrev, and d_negCountPrev.

Referenced by CVC3::Variable::countPrev().

int& CVC3::VariableValue::score ( bool neg ) [inline]

Definition at line 316 of file variable.h.

References d_negScore, and d_score.

Referenced by CVC3::Variable::score().

bool& CVC3::VariableValue::added ( bool neg ) [inline]

Definition at line 320 of file variable.h.

References d_added, and d_negAdded.

Referenced by CVC3::Variable::added().

void* CVC3::VariableValue::operator new	(	size_t	size,
		MemoryManager *	mm
	)			`[inline]`

Definition at line 326 of file variable.h.

References CVC3::MemoryManager::newData().

void CVC3::VariableValue::operator delete	(	void *	pMem,
		MemoryManager *	mm
	)			`[inline]`

Definition at line 329 of file variable.h.

References CVC3::MemoryManager::deleteData().

void CVC3::VariableValue::operator delete ( void * ) [inline]

Definition at line 332 of file variable.h.

Friends And Related Function Documentation

friend class Variable [friend]

Definition at line 207 of file variable.h.

friend class VariableManager [friend]

Definition at line 208 of file variable.h.

std::ostream& operator<<	(	std::ostream &	os,
		const VariableValue &	v
	)			`[friend]`

Definition at line 337 of file variable.cpp.

bool operator==	(	const VariableValue &	v1,
		const VariableValue &	v2
	)			`[friend]`

Definition at line 336 of file variable.h.

Member Data Documentation

VariableManager* CVC3::VariableValue::d_vm [private]

Definition at line 210 of file variable.h.

Referenced by CVC3::Variable::deriveThmRec(), CVC3::Variable::operator=(), setAssumpThm(), setValue(), and CVC3::Variable::~Variable().

int CVC3::VariableValue::d_refcount [private]

Definition at line 211 of file variable.h.

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

Expr CVC3::VariableValue::d_expr [private]

Definition at line 213 of file variable.h.

Referenced by getExpr(), getNegExpr(), and setValue().

Expr CVC3::VariableValue::d_neg [private]

Definition at line 215 of file variable.h.

Referenced by getNegExpr().

unsigned CVC3::VariableValue::d_count [private]

Definition at line 220 of file variable.h.

Referenced by count().

unsigned CVC3::VariableValue::d_countPrev [private]

Definition at line 221 of file variable.h.

Referenced by countPrev().

int CVC3::VariableValue::d_score [private]

Definition at line 222 of file variable.h.

Referenced by score().

unsigned CVC3::VariableValue::d_negCount [private]

Definition at line 224 of file variable.h.

Referenced by count().

unsigned CVC3::VariableValue::d_negCountPrev [private]

Definition at line 225 of file variable.h.

Referenced by countPrev().

int CVC3::VariableValue::d_negScore [private]

Definition at line 226 of file variable.h.

Referenced by score().

bool CVC3::VariableValue::d_added [private]

Definition at line 228 of file variable.h.

Referenced by added().

bool CVC3::VariableValue::d_negAdded [private]

Definition at line 229 of file variable.h.

Referenced by added().

std::vector<std::pair<Clause, int> > CVC3::VariableValue::d_wp [private]

Definition at line 231 of file variable.h.

Referenced by CVC3::Variable::wp().

std::vector<std::pair<Clause, int> > CVC3::VariableValue::d_negwp [private]

Definition at line 232 of file variable.h.

Referenced by CVC3::Variable::wp().

CDO<int>* CVC3::VariableValue::d_val [private]

Definition at line 237 of file variable.h.

Referenced by getValue(), setAssumpThm(), setValue(), and ~VariableValue().

CDO<int>* CVC3::VariableValue::d_scope [private]

Definition at line 238 of file variable.h.

Referenced by getScope(), setValue(), and ~VariableValue().

CDO<Theorem>* CVC3::VariableValue::d_thm [private]

Definition at line 240 of file variable.h.

Referenced by getTheorem(), setValue(), and ~VariableValue().

CDO<Clause>* CVC3::VariableValue::d_ante [private]

Definition at line 241 of file variable.h.

Referenced by getAntecedent(), setValue(), and ~VariableValue().

CDO<int>* CVC3::VariableValue::d_anteIdx [private]

Definition at line 242 of file variable.h.

Referenced by getAntecedentIdx(), setValue(), and ~VariableValue().

CDO<Theorem>* CVC3::VariableValue::d_assump [private]

Definition at line 243 of file variable.h.

Referenced by getAssumpThm(), setAssumpThm(), and ~VariableValue().

The documentation for this class was generated from the following files:

Generated on Wed Nov 18 16:17:27 2009 for CVC3 by

1.5.2