CVCL::VariableValue Class Reference

#include <variable.h>

Collaboration diagram for CVCL::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 *)

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 214 of file variable.h.

Constructor & Destructor Documentation

CVCL::VariableValue::VariableValue ( VariableManager * vm,

const Expr & e

) [inline, private]

Definition at line 253 of file variable.h.

CVCL::VariableValue::~VariableValue ( )

Definition at line 238 of file variable.cpp.
References d_ante, d_anteIdx, d_assump, d_scope, d_thm, and d_val.

Member Function Documentation

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

Definition at line 263 of file variable.h.
References d_expr.
Referenced by CVCL::Variable::getExpr(), CVCL::VariableManager::EqLV::operator()(), CVCL::VariableManager::HashLV::operator()(), CVCL::operator<<(), and setValue().

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

Definition at line 265 of file variable.h.
References d_expr, d_neg, CVCL::Expr::isNull(), and CVCL::Expr::negate().
Referenced by CVCL::Variable::getNegExpr().

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

Definition at line 273 of file variable.h.
References d_val, and CVCL::CDO< T >::get().
Referenced by CVCL::Variable::getValue(), CVCL::operator<<(), and setValue().

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

Definition at line 278 of file variable.h.
References d_scope, and CVCL::CDO< T >::get().
Referenced by CVCL::Variable::getScope(), CVCL::operator<<(), and setValue().

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

Definition at line 283 of file variable.h.
References d_thm, and CVCL::CDO< T >::get().
Referenced by CVCL::Variable::getTheorem(), CVCL::operator<<(), and setValue().

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

Definition at line 289 of file variable.h.
References d_ante, and CVCL::CDO< T >::get().
Referenced by CVCL::Variable::getAntecedent(), CVCL::operator<<(), and setValue().

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

Definition at line 295 of file variable.h.
References d_anteIdx, and CVCL::CDO< T >::get().
Referenced by CVCL::Variable::getAntecedentIdx(), and CVCL::operator<<().

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

Definition at line 300 of file variable.h.
References d_assump, and CVCL::CDO< T >::get().
Referenced by CVCL::Variable::getAssumpThm().

void CVCL::VariableValue::setValue ( int val,

const Clause & c,

int idx

)

Definition at line 250 of file variable.cpp.
References d_ante, d_anteIdx, d_scope, d_thm, d_val, d_vm, CVCL::VariableManager::getCM(), CVCL::ContextManager::getCurrentContext(), getExpr(), getScope(), CVCL::Clause::getScope(), getTheorem(), getValue(), IF_DEBUG(), CVCL::int2string(), CVCL::Theorem::isNull(), CVCL::CDO< T >::set(), CVCL::Clause::size(), CVCL::Expr::toString(), and CVCL::Clause::toString().
Referenced by CVCL::Variable::deriveThmRec(), and CVCL::Variable::setValue().

void CVCL::VariableValue::setValue ( const Theorem & thm,

int scope

)

Definition at line 303 of file variable.cpp.
References d_ante, d_expr, d_scope, d_thm, d_val, d_vm, getAntecedent(), CVCL::VariableManager::getCM(), CVCL::ContextManager::getCurrentContext(), CVCL::Theorem::getExpr(), IF_DEBUG(), CVCL::Expr::isNot(), CVCL::Clause::isNull(), CVCL::CDO< T >::set(), CVCL::Expr::toString(), and CVCL::Theorem::toString().

void CVCL::VariableValue::setAssumpThm ( const Theorem & a,

int scope

)

Definition at line 336 of file variable.cpp.
References d_assump, d_val, d_vm, CVCL::VariableManager::getCM(), CVCL::ContextManager::getCurrentContext(), IF_DEBUG(), and CVCL::CDO< T >::set().
Referenced by CVCL::Variable::setAssumpThm().

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

Definition at line 316 of file variable.h.
References d_count, and d_negCount.
Referenced by CVCL::Variable::count().

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

Definition at line 320 of file variable.h.
References d_countPrev, and d_negCountPrev.
Referenced by CVCL::Variable::countPrev().

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

Definition at line 324 of file variable.h.
References d_negScore, and d_score.
Referenced by CVCL::Variable::score().

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

Definition at line 328 of file variable.h.
References d_added, and d_negAdded.
Referenced by CVCL::Variable::added().

void* CVCL::VariableValue::operator new ( size_t size,

MemoryManager * mm

) [inline]

Definition at line 334 of file variable.h.
References CVCL::MemoryManager::newData().

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

Definition at line 337 of file variable.h.

Friends And Related Function Documentation

friend class Variable [friend]

Definition at line 215 of file variable.h.

friend class VariableManager [friend]

Definition at line 216 of file variable.h.

std::ostream& operator<< ( std::ostream & os,

const VariableValue & v

) [friend]

bool operator== ( const VariableValue & v1,

const VariableValue & v2

) [friend]

Definition at line 341 of file variable.h.

Member Data Documentation

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

Definition at line 218 of file variable.h.
Referenced by CVCL::Variable::deriveThmRec(), CVCL::Variable::operator=(), setAssumpThm(), setValue(), and CVCL::Variable::~Variable().

int CVCL::VariableValue::d_refcount [private]

Definition at line 219 of file variable.h.
Referenced by CVCL::Variable::operator=(), CVCL::Variable::Variable(), and CVCL::Variable::~Variable().

Expr CVCL::VariableValue::d_expr [private]

Definition at line 221 of file variable.h.
Referenced by getExpr(), getNegExpr(), and setValue().

Expr CVCL::VariableValue::d_neg [private]

Definition at line 223 of file variable.h.
Referenced by getNegExpr().

unsigned CVCL::VariableValue::d_count [private]

Definition at line 228 of file variable.h.
Referenced by count().

unsigned CVCL::VariableValue::d_countPrev [private]

Definition at line 229 of file variable.h.
Referenced by countPrev().

int CVCL::VariableValue::d_score [private]

Definition at line 230 of file variable.h.
Referenced by score().

unsigned CVCL::VariableValue::d_negCount [private]

Definition at line 232 of file variable.h.
Referenced by count().

unsigned CVCL::VariableValue::d_negCountPrev [private]

Definition at line 233 of file variable.h.
Referenced by countPrev().

int CVCL::VariableValue::d_negScore [private]

Definition at line 234 of file variable.h.
Referenced by score().

bool CVCL::VariableValue::d_added [private]

Definition at line 236 of file variable.h.
Referenced by added().

bool CVCL::VariableValue::d_negAdded [private]

Definition at line 237 of file variable.h.
Referenced by added().

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

Definition at line 239 of file variable.h.
Referenced by CVCL::Variable::wp().

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

Definition at line 240 of file variable.h.
Referenced by CVCL::Variable::wp().

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

Definition at line 245 of file variable.h.
Referenced by getValue(), setAssumpThm(), setValue(), and ~VariableValue().

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

Definition at line 246 of file variable.h.
Referenced by getScope(), setValue(), and ~VariableValue().

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

Definition at line 248 of file variable.h.
Referenced by getTheorem(), setValue(), and ~VariableValue().

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

Definition at line 249 of file variable.h.
Referenced by getAntecedent(), setValue(), and ~VariableValue().

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

Definition at line 250 of file variable.h.
Referenced by getAntecedentIdx(), setValue(), and ~VariableValue().

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

Definition at line 251 of file variable.h.
Referenced by getAssumpThm(), setAssumpThm(), and ~VariableValue().

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

Generated on Thu Apr 13 16:57:45 2006 for CVC Lite by

1.4.4