CVC3::VariableValue Class Reference

#include <variable.h>

Collaboration diagram for CVC3::VariableValue:

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.

Referenced by CVC3::VariableManager::newVariableValue().

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::int2string(), 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:

• variable.h
• variable.cpp