CVC3
Public Member Functions | Private Member Functions | Private Attributes | Friends

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.

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]
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 
)
void CVC3::VariableValue::setValue ( const Theorem thm,
int  scope 
)
void CVC3::VariableValue::setAssumpThm ( const Theorem a,
int  scope 
)
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

Definition at line 213 of file variable.h.

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

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().

Definition at line 221 of file variable.h.

Referenced by countPrev().

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().

Definition at line 225 of file variable.h.

Referenced by countPrev().

Definition at line 226 of file variable.h.

Referenced by score().

Definition at line 228 of file variable.h.

Referenced by added().

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().

Definition at line 237 of file variable.h.

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

Definition at line 238 of file variable.h.

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

Definition at line 240 of file variable.h.

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

Definition at line 241 of file variable.h.

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

Definition at line 242 of file variable.h.

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

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: