CVC3::VariableValue Class Reference

#include <variable.h>

Collaboration diagram for CVC3::VariableValue:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Private Member Functions

Private Attributes

Friends


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  doxygen 1.5.2