CVC3  2.4.1
Public Member Functions | Private Member Functions | Private Attributes | Friends | List of all members
CVC3::VariableValue Class Reference

#include <variable.h>

Public Member Functions

 ~VariableValue ()
 
const ExprgetExpr () const
 
const ExprgetNegExpr () const
 
int getValue () const
 
int getScope () const
 
const TheoremgetTheorem () const
 
const ClausegetAntecedent () const
 
int getAntecedentIdx () const
 
const TheoremgetAssumpThm () 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

VariableManagerd_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 
)
inlineprivate

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_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 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 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 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 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 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 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.

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

Definition at line 329 of file variable.h.

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
int CVC3::VariableValue::d_refcount
private
Expr CVC3::VariableValue::d_expr
private

Definition at line 213 of file variable.h.

Referenced by getExpr(), 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 setAssumpThm(), setValue(), and ~VariableValue().

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

Definition at line 238 of file variable.h.

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

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

Definition at line 240 of file variable.h.

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

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

Definition at line 241 of file variable.h.

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

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

Definition at line 242 of file variable.h.

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

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

Definition at line 243 of file variable.h.

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


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