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

CVC3::ExprValue Class Reference

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

#include <expr_value.h>

Inherited by CVC3::BVConstExpr, CVC3::ExprBoundVar, CVC3::ExprClosure, CVC3::ExprNode, CVC3::ExprNodeTmp, CVC3::ExprRational, CVC3::ExprSkolem, CVC3::ExprString, CVC3::ExprSymbol, and CVC3::ExprVar.

Collaboration diagram for CVC3::ExprValue:
Collaboration graph
[legend]

List of all members.

Public Member Functions

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Static Protected Attributes

Private Member Functions

Private Attributes

Friends


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) [inline, private]

Set the ExprIndex.

Definition at line 139 of file expr_value.h.

void CVC3::ExprValue::incRefcount ( ) [inline, private]

Increment reference counter.

Definition at line 142 of file expr_value.h.

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

void CVC3::ExprValue::decRefcount ( ) [inline, private]

Decrement reference counter.

Definition at line 145 of file expr_value.h.

References FatalAssert, and IF_DEBUG.

Referenced by CVC3::Expr::operator=().

size_t CVC3::ExprValue::hash ( ) const [inline, private]

Caching hash function.

Do NOT implement it in subclasses! Implement computeHash() instead.

Definition at line 155 of file expr_value.h.

Referenced by CVC3::BVConstExpr::computeHash(), CVC3::ExprRational::computeHash(), CVC3::ExprString::computeHash(), CVC3::ExprNodeTmp::computeHash(), and CVC3::ExprNode::computeHash().

Unsigned CVC3::ExprValue::getSize ( ) const [inline, private]

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) [inline, static, protected]

Definition at line 185 of file expr_value.h.

size_t CVC3::ExprValue::hash ( const int  kind,
const std::vector< Expr > &  kids 
) [static, protected]

Definition at line 310 of file expr_value.cpp.

References PRIME.

static size_t CVC3::ExprValue::hash ( const int  n) [inline, static, protected]

Definition at line 189 of file expr_value.h.

Unsigned CVC3::ExprValue::sizeWithChildren ( const std::vector< Expr > &  kids) [static, protected]

Definition at line 322 of file expr_value.cpp.

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

MemoryManager* CVC3::ExprValue::getMM ( size_t  MMIndex) [inline, protected]

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 [inline, protected]

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 [inline, protected]

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 [inline, protected, virtual]

Non-caching hash function which actually computes the hash.

This is the method that all subclasses should implement

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

Definition at line 212 of file expr_value.h.

virtual Unsigned CVC3::ExprValue::computeSize ( ) const [inline, protected, virtual]

Non-caching size function which actually computes the size.

This is the method that all subclasses should implement

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

Definition at line 216 of file expr_value.h.

ExprValue * CVC3::ExprValue::copy ( ExprManager em,
ExprIndex  idx 
) const [protected, virtual]
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 [inline, virtual]
bool CVC3::ExprValue::operator== ( const ExprValue ev2) const [virtual]
virtual const ExprValue* CVC3::ExprValue::getExprValue ( ) const [inline, virtual]

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 [inline, virtual]

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 [inline, virtual]

Rational number expression tester.

Reimplemented in CVC3::ExprRational.

Definition at line 280 of file expr_value.h.

virtual bool CVC3::ExprValue::isVar ( ) const [inline, virtual]

Uninterpreted constants.

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

Definition at line 282 of file expr_value.h.

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

virtual bool CVC3::ExprValue::isApply ( ) const [inline, virtual]

Application of another expression.

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

Definition at line 284 of file expr_value.h.

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

virtual bool CVC3::ExprValue::isSymbol ( ) const [inline, virtual]

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 [inline, virtual]

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 [inline, virtual]

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 [inline, virtual]
virtual unsigned CVC3::ExprValue::arity ( ) const [inline, virtual]

Default arity = 0.

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

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 [inline, virtual]

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 [inline, virtual]

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) [inline, virtual]

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) [inline, virtual]

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 [inline, virtual]

Reimplemented in CVC3::ExprBoundVar.

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 [inline, virtual]

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 [inline, virtual]

Reimplemented in CVC3::ExprRational.

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 [inline, virtual]

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

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

Definition at line 339 of file expr_value.h.

References DebugAssert.

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

virtual const Expr& CVC3::ExprValue::getVar ( ) const [inline, virtual]

Returns the original Boolean variable (for BoolVarExprValue)

Definition at line 346 of file expr_value.h.

References DebugAssert.

virtual Op CVC3::ExprValue::getOp ( ) const [inline, virtual]

Get the Op from an Apply Expr.

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

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 [inline, virtual]

Reimplemented in CVC3::ExprClosure.

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 [inline, virtual]

Reimplemented in CVC3::ExprClosure.

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) [inline, virtual]

Reimplemented in CVC3::ExprClosure.

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 [inline, virtual]

Reimplemented in CVC3::ExprClosure.

Definition at line 374 of file expr_value.h.

References DebugAssert.

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

virtual const Expr& CVC3::ExprValue::getExistential ( ) const [inline, virtual]

Reimplemented in CVC3::ExprSkolem.

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 [inline, virtual]

Reimplemented in CVC3::ExprSkolem.

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 [inline, virtual]

Definition at line 391 of file expr_value.h.

References DebugAssert.

virtual const std::string& CVC3::ExprValue::getField ( ) const [inline, virtual]

Definition at line 396 of file expr_value.h.

References DebugAssert.

virtual int CVC3::ExprValue::getTupleIndex ( ) const [inline, virtual]

Definition at line 401 of file expr_value.h.

References DebugAssert.

virtual const Theorem& CVC3::ExprValue::getTheorem ( ) const [inline, virtual]

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]
friend class Expr::iterator [friend]

Definition at line 71 of file expr_value.h.

friend class ExprManager [friend]
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

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.

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

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

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

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

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

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::ExprSymbol::computeHash(), CVC3::ExprNodeTmp::computeHash(), CVC3::ExprApplyTmp::ExprApplyTmp(), CVC3::Expr::getKind(), CVC3::Expr::isNull(), and operator==().

Our expr. manager.

Definition at line 132 of file expr_value.h.

Referenced by CVC3::Expr::getEM(), CVC3::Expr::hasLastIndex(), and CVC3::Expr::~Expr().

std::hash< char * > CVC3::ExprValue::s_charHash [static, protected]

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::ExprBoundVar::computeHash(), CVC3::ExprSymbol::computeHash(), CVC3::ExprVar::computeHash(), CVC3::ExprRational::hash(), and CVC3::ExprString::hash().

std::hash< long int > CVC3::ExprValue::s_intHash [static, protected]

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: