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

The base class for holding the actual data in expressions. More...

#include <expr_value.h>

Inheritance diagram for CVC3::ExprValue:
CVC3::BVConstExpr CVC3::ExprBoundVar CVC3::ExprClosure CVC3::ExprNode CVC3::ExprNodeTmp CVC3::ExprRational CVC3::ExprSkolem CVC3::ExprString CVC3::ExprSymbol CVC3::ExprVar

Public Member Functions

 ExprValue (ExprManager *em, int kind, ExprIndex idx=0)
 Constructor.
virtual ~ExprValue ()
 Destructor.
int getKind () const
 Get the kind of the expression.
void * operator new (size_t size, MemoryManager *mm)
 Overload operator new.
void operator delete (void *pMem, MemoryManager *mm)
void operator delete (void *)
 Overload operator delete.
virtual size_t getMMIndex () const
 Get unique memory manager ID.
virtual bool operator== (const ExprValue &ev2) const
 Equality between any two ExprValue objects (including subclasses)
virtual const ExprValuegetExprValue () const
 Test whether the expression is a generic subclass.
virtual bool isString () const
 String expression tester.
virtual bool isRational () const
 Rational number expression tester.
virtual bool isVar () const
 Uninterpreted constants.
virtual bool isApply () const
 Application of another expression.
virtual bool isSymbol () const
 Special named symbol.
virtual bool isClosure () const
 A LAMBDA-expression or a quantifier.
virtual bool isTheorem () const
 Special Expr holding a theorem.
virtual const std::vector< Expr > & getKids () const
 Get kids: by default, returns a ref to an empty vector.
virtual unsigned arity () const
 Default arity = 0.
virtual CDO< Theorem > * getSig () const
 Special attributes for uninterpreted functions.
virtual CDO< Theorem > * getRep () const
virtual void setSig (CDO< Theorem > *sig)
virtual void setRep (CDO< Theorem > *rep)
virtual const std::string & getUid () const
virtual const std::string & getString () const
virtual const RationalgetRational () const
virtual const std::string & getName () const
 Returns the string name of UCONST and BOUND_VAR expr's.
virtual const ExprgetVar () const
 Returns the original Boolean variable (for BoolVarExprValue)
virtual Op getOp () const
 Get the Op from an Apply Expr.
virtual const std::vector< Expr > & getVars () const
virtual const ExprgetBody () const
virtual void setTriggers (const std::vector< std::vector< Expr > > &triggers)
virtual const std::vector
< std::vector< Expr > > & 
getTriggers () const
virtual const ExprgetExistential () const
virtual int getBoundIndex () const
virtual const std::vector
< std::string > & 
getFields () const
virtual const std::string & getField () const
virtual int getTupleIndex () const
virtual const TheoremgetTheorem () const

Protected Member Functions

MemoryManagergetMM (size_t MMIndex)
 Return the memory manager (for the benefit of subclasses)
ExprValuerebuild (ExprManager *em) const
 Make a clean copy of itself using the given ExprManager.
Expr rebuild (Expr e, ExprManager *em) const
 Make a clean copy of the expr using the given ExprManager.
virtual size_t computeHash () const
 Non-caching hash function which actually computes the hash.
virtual Unsigned computeSize () const
 Non-caching size function which actually computes the size.
virtual ExprValuecopy (ExprManager *em, ExprIndex idx) const
 Make a clean copy of itself using the given ExprManager.

Static Protected Member Functions

static size_t pointerHash (void *p)
static size_t hash (const int kind, const std::vector< Expr > &kids)
static size_t hash (const int n)
static Unsigned sizeWithChildren (const std::vector< Expr > &kids)

Protected Attributes

int d_kind
 The kind of the expression. In particular, it determines which subclass of ExprValue is used to store the expression.
ExprManagerd_em
 Our expr. manager.

Static Protected Attributes

static std::hash< char * > s_charHash
 Return child with greatest height.
static std::hash< long int > s_intHash

Private Member Functions

void setIndex (ExprIndex idx)
 Set the ExprIndex.
void incRefcount ()
 Increment reference counter.
void decRefcount ()
 Decrement reference counter.
size_t hash () const
 Caching hash function.
Unsigned getSize () const
 Return DAG-size of Expr.

Private Attributes

ExprIndex d_index
 Unique expression id.
unsigned d_refcount
 Reference counter for garbage collection.
size_t d_hash
 Cached hash value (initially 0)
CDO< Theorem > * d_find
 The find attribute (may be NULL)
CDO< Theorem > * d_eqNext
 Equality between this term and next term in ring of all terms in the equivalence class.
Type d_type
 The cached type of the expression (may be Null)
NotifyListd_notifyList
 The cached TCC of the expression (may be Null)
Theorem d_simpCache
 For caching calls to Simplify.
unsigned d_simpCacheTag
 For checking whether simplify cache is valid.
CDFlags d_dynamicFlags
 context-dependent bit-vector for flags that are context-dependent
Unsigned d_size
 Size of dag rooted at this expression.
unsigned d_flag
 Which child has the largest height.

Friends

class Expr
class Expr::iterator
class ExprManager
class ::CInterface
class ExprApply
class Theorem
class ExprClosure

Detailed Description

The base class for holding the actual data in expressions.

Author: Sergey Berezin

Created: long time ago

The base class just holds the operator. All the additional data resides in subclasses.

Definition at line 69 of file expr_value.h.

Constructor & Destructor Documentation

CVC3::ExprValue::ExprValue ( ExprManager em,
int  kind,
ExprIndex  idx = 0 
)
inline

Constructor.

Definition at line 223 of file expr_value.h.

References APPLY, DebugAssert, CVC3::int2string(), and CVC3::ExprManager::isKindRegistered().

CVC3::ExprValue::~ExprValue ( )
virtual

Destructor.

Definition at line 41 of file expr_value.cpp.

Member Function Documentation

void CVC3::ExprValue::setIndex ( ExprIndex  idx)
inlineprivate

Set the ExprIndex.

Definition at line 139 of file expr_value.h.

void CVC3::ExprValue::incRefcount ( )
inlineprivate

Increment reference counter.

Definition at line 142 of file expr_value.h.

Referenced by CVC3::Expr::Expr(), CVC3::Theorem::operator=(), CVC3::Expr::operator=(), and CVC3::Theorem::Theorem().

void CVC3::ExprValue::decRefcount ( )
inlineprivate

Decrement reference counter.

Definition at line 145 of file expr_value.h.

References FatalAssert, and IF_DEBUG.

Referenced by CVC3::Expr::operator=(), and CVC3::Theorem::~Theorem().

size_t CVC3::ExprValue::hash ( ) const
inlineprivate
Unsigned CVC3::ExprValue::getSize ( ) const
inlineprivate

Return DAG-size of Expr.

Definition at line 162 of file expr_value.h.

Referenced by CVC3::ExprClosure::computeSize(), and CVC3::Expr::getSize().

static size_t CVC3::ExprValue::pointerHash ( void *  p)
inlinestaticprotected

Definition at line 185 of file expr_value.h.

size_t CVC3::ExprValue::hash ( const int  kind,
const std::vector< Expr > &  kids 
)
staticprotected

Definition at line 310 of file expr_value.cpp.

References PRIME.

static size_t CVC3::ExprValue::hash ( const int  n)
inlinestaticprotected

Definition at line 189 of file expr_value.h.

Unsigned CVC3::ExprValue::sizeWithChildren ( const std::vector< Expr > &  kids)
staticprotected

Definition at line 322 of file expr_value.cpp.

Referenced by CVC3::ExprNode::computeSize(), and CVC3::ExprNodeTmp::computeSize().

MemoryManager* CVC3::ExprValue::getMM ( size_t  MMIndex)
inlineprotected

Return the memory manager (for the benefit of subclasses)

Definition at line 195 of file expr_value.h.

References DebugAssert.

ExprValue* CVC3::ExprValue::rebuild ( ExprManager em) const
inlineprotected

Make a clean copy of itself using the given ExprManager.

Definition at line 201 of file expr_value.h.

Referenced by CVC3::ExprManager::rebuildRec().

Expr CVC3::ExprValue::rebuild ( Expr  e,
ExprManager em 
) const
inlineprotected

Make a clean copy of the expr using the given ExprManager.

Definition at line 205 of file expr_value.h.

References CVC3::ExprManager::rebuildRec().

virtual size_t CVC3::ExprValue::computeHash ( ) const
inlineprotectedvirtual

Non-caching hash function which actually computes the hash.

This is the method that all subclasses should implement

Reimplemented in CVC3::ExprClosure, CVC3::ExprBoundVar, CVC3::ExprSymbol, CVC3::ExprVar, CVC3::ExprRational, CVC3::ExprSkolem, CVC3::ExprString, CVC3::ExprApply, CVC3::ExprApplyTmp, CVC3::ExprNodeTmp, CVC3::ExprNode, and CVC3::BVConstExpr.

Definition at line 212 of file expr_value.h.

virtual Unsigned CVC3::ExprValue::computeSize ( ) const
inlineprotectedvirtual

Non-caching size function which actually computes the size.

This is the method that all subclasses should implement

Reimplemented in CVC3::ExprClosure, CVC3::ExprNodeTmp, and CVC3::ExprNode.

Definition at line 216 of file expr_value.h.

ExprValue * CVC3::ExprValue::copy ( ExprManager em,
ExprIndex  idx 
) const
protectedvirtual
int CVC3::ExprValue::getKind ( ) const
inline
void* CVC3::ExprValue::operator new ( size_t  size,
MemoryManager mm 
)
inline
void CVC3::ExprValue::operator delete ( void *  pMem,
MemoryManager mm 
)
inline
void CVC3::ExprValue::operator delete ( void *  )
inline
virtual size_t CVC3::ExprValue::getMMIndex ( ) const
inlinevirtual
bool CVC3::ExprValue::operator== ( const ExprValue ev2) const
virtual
virtual const ExprValue* CVC3::ExprValue::getExprValue ( ) const
inlinevirtual

Test whether the expression is a generic subclass.

Returns
0 for the core classes, and getMMIndex() value for generic subclasses (those defined in DPs)

Reimplemented in CVC3::BVConstExpr.

Definition at line 275 of file expr_value.h.

Referenced by CVC3::Expr::getExprValue().

virtual bool CVC3::ExprValue::isString ( ) const
inlinevirtual

String expression tester.

Reimplemented in CVC3::ExprString.

Definition at line 278 of file expr_value.h.

Referenced by CVC3::Expr::isString().

virtual bool CVC3::ExprValue::isRational ( ) const
inlinevirtual

Rational number expression tester.

Reimplemented in CVC3::ExprRational.

Definition at line 280 of file expr_value.h.

virtual bool CVC3::ExprValue::isVar ( ) const
inlinevirtual

Uninterpreted constants.

Reimplemented in CVC3::ExprBoundVar, CVC3::ExprVar, and CVC3::ExprSkolem.

Definition at line 282 of file expr_value.h.

Referenced by CVC3::Expr::isVar().

virtual bool CVC3::ExprValue::isApply ( ) const
inlinevirtual

Application of another expression.

Reimplemented in CVC3::ExprApply, and CVC3::ExprApplyTmp.

Definition at line 284 of file expr_value.h.

Referenced by CVC3::Expr::isApply().

virtual bool CVC3::ExprValue::isSymbol ( ) const
inlinevirtual

Special named symbol.

Reimplemented in CVC3::ExprSymbol.

Definition at line 286 of file expr_value.h.

Referenced by CVC3::Expr::isSymbol().

virtual bool CVC3::ExprValue::isClosure ( ) const
inlinevirtual

A LAMBDA-expression or a quantifier.

Reimplemented in CVC3::ExprClosure.

Definition at line 288 of file expr_value.h.

Referenced by CVC3::Expr::isClosure().

virtual bool CVC3::ExprValue::isTheorem ( ) const
inlinevirtual

Special Expr holding a theorem.

Definition at line 290 of file expr_value.h.

Referenced by CVC3::Expr::isTheorem().

virtual const std::vector<Expr>& CVC3::ExprValue::getKids ( ) const
inlinevirtual
virtual unsigned CVC3::ExprValue::arity ( ) const
inlinevirtual

Default arity = 0.

Reimplemented in CVC3::ExprNodeTmp, and CVC3::ExprNode.

Definition at line 299 of file expr_value.h.

Referenced by CVC3::Expr::arity(), CVC3::Expr::begin(), and CVC3::Expr::end().

virtual CDO<Theorem>* CVC3::ExprValue::getSig ( ) const
inlinevirtual

Special attributes for uninterpreted functions.

Reimplemented in CVC3::ExprNode.

Definition at line 302 of file expr_value.h.

References DebugAssert.

Referenced by CVC3::Expr::getSig(), CVC3::Expr::hasSig(), and CVC3::Expr::setSig().

virtual CDO<Theorem>* CVC3::ExprValue::getRep ( ) const
inlinevirtual

Reimplemented in CVC3::ExprNode.

Definition at line 307 of file expr_value.h.

References DebugAssert.

Referenced by CVC3::Expr::getRep(), CVC3::Expr::hasRep(), and CVC3::Expr::setRep().

virtual void CVC3::ExprValue::setSig ( CDO< Theorem > *  sig)
inlinevirtual

Reimplemented in CVC3::ExprNode.

Definition at line 312 of file expr_value.h.

References DebugAssert.

Referenced by CVC3::Expr::setSig().

virtual void CVC3::ExprValue::setRep ( CDO< Theorem > *  rep)
inlinevirtual

Reimplemented in CVC3::ExprNode.

Definition at line 316 of file expr_value.h.

References DebugAssert.

Referenced by CVC3::Expr::setRep().

virtual const std::string& CVC3::ExprValue::getUid ( ) const
inlinevirtual

Definition at line 320 of file expr_value.h.

References DebugAssert.

Referenced by CVC3::Expr::getUid(), and CVC3::ExprBoundVar::operator==().

virtual const std::string& CVC3::ExprValue::getString ( ) const
inlinevirtual

Reimplemented in CVC3::ExprString.

Definition at line 326 of file expr_value.h.

References DebugAssert.

Referenced by CVC3::Expr::getString(), and CVC3::ExprString::operator==().

virtual const Rational& CVC3::ExprValue::getRational ( ) const
inlinevirtual

Definition at line 332 of file expr_value.h.

References DebugAssert.

Referenced by CVC3::Expr::getRational(), and CVC3::ExprRational::operator==().

virtual const std::string& CVC3::ExprValue::getName ( ) const
inlinevirtual

Returns the string name of UCONST and BOUND_VAR expr's.

Definition at line 339 of file expr_value.h.

References DebugAssert.

Referenced by CVC3::Expr::getName(), CVC3::ExprVar::operator==(), CVC3::ExprSymbol::operator==(), and CVC3::ExprBoundVar::operator==().

virtual const Expr& CVC3::ExprValue::getVar ( ) const
inlinevirtual

Returns the original Boolean variable (for BoolVarExprValue)

Definition at line 346 of file expr_value.h.

References DebugAssert.

virtual Op CVC3::ExprValue::getOp ( ) const
inlinevirtual

Get the Op from an Apply Expr.

Reimplemented in CVC3::ExprApply, and CVC3::ExprApplyTmp.

Definition at line 353 of file expr_value.h.

References DebugAssert, and NULL_KIND.

Referenced by CVC3::Expr::getOp(), CVC3::ExprApplyTmp::operator==(), and CVC3::ExprApply::operator==().

virtual const std::vector<Expr>& CVC3::ExprValue::getVars ( ) const
inlinevirtual

Definition at line 358 of file expr_value.h.

References DebugAssert.

Referenced by CVC3::Expr::getVars(), and CVC3::ExprClosure::operator==().

virtual const Expr& CVC3::ExprValue::getBody ( ) const
inlinevirtual

Definition at line 364 of file expr_value.h.

References DebugAssert.

Referenced by CVC3::Expr::getBody(), and CVC3::ExprClosure::operator==().

virtual void CVC3::ExprValue::setTriggers ( const std::vector< std::vector< Expr > > &  triggers)
inlinevirtual

Definition at line 370 of file expr_value.h.

References DebugAssert.

Referenced by CVC3::Expr::setTriggers().

virtual const std::vector<std::vector<Expr> >& CVC3::ExprValue::getTriggers ( ) const
inlinevirtual

Definition at line 374 of file expr_value.h.

References DebugAssert.

Referenced by CVC3::Expr::getTriggers().

virtual const Expr& CVC3::ExprValue::getExistential ( ) const
inlinevirtual

Definition at line 381 of file expr_value.h.

References DebugAssert.

Referenced by CVC3::Expr::getExistential(), and CVC3::ExprSkolem::operator==().

virtual int CVC3::ExprValue::getBoundIndex ( ) const
inlinevirtual

Definition at line 386 of file expr_value.h.

References DebugAssert.

Referenced by CVC3::Expr::getBoundIndex(), and CVC3::ExprSkolem::operator==().

virtual const std::vector<std::string>& CVC3::ExprValue::getFields ( ) const
inlinevirtual

Definition at line 391 of file expr_value.h.

References DebugAssert.

virtual const std::string& CVC3::ExprValue::getField ( ) const
inlinevirtual

Definition at line 396 of file expr_value.h.

References DebugAssert.

virtual int CVC3::ExprValue::getTupleIndex ( ) const
inlinevirtual

Definition at line 401 of file expr_value.h.

References DebugAssert.

virtual const Theorem& CVC3::ExprValue::getTheorem ( ) const
inlinevirtual

Definition at line 405 of file expr_value.h.

References DebugAssert.

Referenced by CVC3::Expr::getTheorem().

Friends And Related Function Documentation

friend class Expr
friend

Definition at line 70 of file expr_value.h.

friend class Expr::iterator
friend

Definition at line 71 of file expr_value.h.

friend class ExprManager
friend

Definition at line 72 of file expr_value.h.

friend class ::CInterface
friend

Definition at line 73 of file expr_value.h.

friend class ExprApply
friend

Definition at line 74 of file expr_value.h.

friend class Theorem
friend

Definition at line 75 of file expr_value.h.

friend class ExprClosure
friend

Definition at line 76 of file expr_value.h.

Member Data Documentation

ExprIndex CVC3::ExprValue::d_index
private

Unique expression id.

Definition at line 79 of file expr_value.h.

Referenced by CVC3::Expr::getIndex().

unsigned CVC3::ExprValue::d_refcount
private

Reference counter for garbage collection.

Definition at line 82 of file expr_value.h.

Referenced by CVC3::Expr::~Expr().

size_t CVC3::ExprValue::d_hash
private

Cached hash value (initially 0)

Definition at line 85 of file expr_value.h.

CDO<Theorem>* CVC3::ExprValue::d_find
private

The find attribute (may be NULL)

Definition at line 88 of file expr_value.h.

Referenced by CVC3::Expr::getFind(), CVC3::Expr::getFindLevel(), CVC3::Expr::hasFind(), and CVC3::Expr::setFind().

CDO<Theorem>* CVC3::ExprValue::d_eqNext
private

Equality between this term and next term in ring of all terms in the equivalence class.

Definition at line 91 of file expr_value.h.

Referenced by CVC3::Expr::getEqNext(), and CVC3::Expr::setEqNext().

Type CVC3::ExprValue::d_type
private

The cached type of the expression (may be Null)

Definition at line 94 of file expr_value.h.

Referenced by CVC3::Expr::getType(), CVC3::Expr::lookupType(), CVC3::ExprManager::rebuildRec(), and CVC3::Expr::setType().

NotifyList* CVC3::ExprValue::d_notifyList
private

The cached TCC of the expression (may be Null)

Subtyping predicate for the expression and all subexpressions Notify list may be NULL (== no such attribute)

Definition at line 103 of file expr_value.h.

Referenced by CVC3::Expr::getNotify().

Theorem CVC3::ExprValue::d_simpCache
private

For caching calls to Simplify.

Definition at line 106 of file expr_value.h.

Referenced by CVC3::Expr::getSimpCache(), and CVC3::Expr::setSimpCache().

unsigned CVC3::ExprValue::d_simpCacheTag
private

For checking whether simplify cache is valid.

Definition at line 109 of file expr_value.h.

Referenced by CVC3::Expr::setSimpCache(), and CVC3::Expr::validSimpCache().

CDFlags CVC3::ExprValue::d_dynamicFlags
private
Unsigned CVC3::ExprValue::d_size
private

Size of dag rooted at this expression.

Definition at line 115 of file expr_value.h.

Referenced by CVC3::Expr::getSize().

unsigned CVC3::ExprValue::d_flag
private

Which child has the largest height.

Most distant expression we were simplified from Generic flag for marking expressions (e.g. in DAG traversal)

Definition at line 124 of file expr_value.h.

Referenced by CVC3::Expr::getFlag(), and CVC3::Expr::setFlag().

int CVC3::ExprValue::d_kind
protected

The kind of the expression. In particular, it determines which subclass of ExprValue is used to store the expression.

Definition at line 129 of file expr_value.h.

Referenced by CVC3::ExprNodeTmp::computeHash(), CVC3::ExprSymbol::computeHash(), CVC3::ExprApplyTmp::ExprApplyTmp(), CVC3::Expr::getKind(), CVC3::Expr::isNull(), and operator==().

ExprManager* CVC3::ExprValue::d_em
protected
std::hash< char * > CVC3::ExprValue::s_charHash
staticprotected

Return child with greatest height.

Get Expr simplified to obtain this expr Set Expr simplified to obtain this expr

Definition at line 182 of file expr_value.h.

Referenced by CVC3::ExprVar::computeHash(), CVC3::ExprSymbol::computeHash(), CVC3::ExprBoundVar::computeHash(), CVC3::ExprString::hash(), and CVC3::ExprRational::hash().

std::hash< long int > CVC3::ExprValue::s_intHash
staticprotected

Definition at line 183 of file expr_value.h.

Referenced by CVC3::ExprSymbol::computeHash().


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