CVC3
|
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.
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 ExprValue * | getExprValue () 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 Rational & | getRational () const |
virtual const std::string & | getName () const |
Returns the string name of UCONST and BOUND_VAR expr's. | |
virtual const Expr & | getVar () 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 Expr & | getBody () const |
virtual void | setTriggers (const std::vector< std::vector< Expr > > &triggers) |
virtual const std::vector < std::vector< Expr > > & | getTriggers () const |
virtual const Expr & | getExistential () 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 Theorem & | getTheorem () const |
Protected Member Functions | |
MemoryManager * | getMM (size_t MMIndex) |
Return the memory manager (for the benefit of subclasses) | |
ExprValue * | rebuild (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 ExprValue * | copy (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. | |
ExprManager * | d_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) | |
NotifyList * | d_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 |
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.
|
inline |
Constructor.
Definition at line 223 of file expr_value.h.
References APPLY, DebugAssert, CVC3::int2string(), and CVC3::ExprManager::isKindRegistered().
|
virtual |
Destructor.
Definition at line 41 of file expr_value.cpp.
|
inlineprivate |
Set the ExprIndex.
Definition at line 139 of file expr_value.h.
|
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().
|
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().
|
inlineprivate |
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::ExprNode::computeHash(), CVC3::ExprNodeTmp::computeHash(), CVC3::ExprString::computeHash(), CVC3::ExprRational::computeHash(), and CVC3::ExprManager::hash().
|
inlineprivate |
Return DAG-size of Expr.
Definition at line 162 of file expr_value.h.
Referenced by CVC3::ExprClosure::computeSize(), and CVC3::Expr::getSize().
|
inlinestaticprotected |
Definition at line 185 of file expr_value.h.
|
staticprotected |
Definition at line 310 of file expr_value.cpp.
References PRIME.
|
inlinestaticprotected |
Definition at line 189 of file expr_value.h.
Definition at line 322 of file expr_value.cpp.
Referenced by CVC3::ExprNode::computeSize(), and CVC3::ExprNodeTmp::computeSize().
|
inlineprotected |
Return the memory manager (for the benefit of subclasses)
Definition at line 195 of file expr_value.h.
References DebugAssert.
|
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().
|
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().
|
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.
|
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.
|
protectedvirtual |
Make a clean copy of itself using the given ExprManager.
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 78 of file expr_value.cpp.
References DebugAssert, CVC3::EXPR_VALUE, and CVC3::ExprManager::getMM().
Referenced by CVC3::ExprManager::newExprValue().
|
inline |
Get the kind of the expression.
Definition at line 250 of file expr_value.h.
Referenced by CVC3::ExprNode::operator==(), CVC3::ExprNodeTmp::operator==(), CVC3::ExprVar::operator==(), CVC3::ExprSymbol::operator==(), CVC3::ExprBoundVar::operator==(), and CVC3::ExprClosure::operator==().
|
inline |
Overload operator new.
Definition at line 253 of file expr_value.h.
|
inline |
Definition at line 255 of file expr_value.h.
|
inline |
Overload operator delete.
Definition at line 260 of file expr_value.h.
|
inlinevirtual |
Get unique memory manager ID.
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 263 of file expr_value.h.
References CVC3::EXPR_VALUE.
Referenced by CVC3::ExprManager::clear(), CVC3::ExprManager::gc(), CVC3::Expr::getMMIndex(), CVC3::BVConstExpr::operator==(), operator==(), CVC3::ExprNode::operator==(), CVC3::ExprNodeTmp::operator==(), CVC3::ExprApplyTmp::operator==(), CVC3::ExprApply::operator==(), CVC3::ExprString::operator==(), CVC3::ExprSkolem::operator==(), CVC3::ExprRational::operator==(), CVC3::ExprVar::operator==(), CVC3::ExprSymbol::operator==(), CVC3::ExprBoundVar::operator==(), CVC3::ExprClosure::operator==(), and CVC3::ExprManager::resumeGC().
|
virtual |
Equality between any two ExprValue objects (including subclasses)
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 68 of file expr_value.cpp.
References d_kind, DebugAssert, CVC3::EXPR_VALUE, and getMMIndex().
|
inlinevirtual |
Test whether the expression is a generic subclass.
Reimplemented in CVC3::BVConstExpr.
Definition at line 275 of file expr_value.h.
Referenced by CVC3::Expr::getExprValue().
|
inlinevirtual |
String expression tester.
Reimplemented in CVC3::ExprString.
Definition at line 278 of file expr_value.h.
Referenced by CVC3::Expr::isString().
|
inlinevirtual |
Rational number expression tester.
Reimplemented in CVC3::ExprRational.
Definition at line 280 of file expr_value.h.
|
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().
|
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().
|
inlinevirtual |
Special named symbol.
Reimplemented in CVC3::ExprSymbol.
Definition at line 286 of file expr_value.h.
Referenced by CVC3::Expr::isSymbol().
|
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().
|
inlinevirtual |
Special Expr holding a theorem.
Definition at line 290 of file expr_value.h.
Referenced by CVC3::Expr::isTheorem().
|
inlinevirtual |
Get kids: by default, returns a ref to an empty vector.
Reimplemented in CVC3::ExprNodeTmp, and CVC3::ExprNode.
Definition at line 293 of file expr_value.h.
Referenced by CVC3::Expr::begin(), CVC3::Expr::end(), CVC3::Expr::getKids(), CVC3::ExprNode::operator==(), CVC3::ExprNodeTmp::operator==(), CVC3::ExprApplyTmp::operator==(), CVC3::ExprApply::operator==(), and CVC3::Expr::operator[]().
|
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().
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().
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().
Reimplemented in CVC3::ExprNode.
Definition at line 312 of file expr_value.h.
References DebugAssert.
Referenced by CVC3::Expr::setSig().
Reimplemented in CVC3::ExprNode.
Definition at line 316 of file expr_value.h.
References DebugAssert.
Referenced by CVC3::Expr::setRep().
|
inlinevirtual |
Reimplemented in CVC3::ExprBoundVar.
Definition at line 320 of file expr_value.h.
References DebugAssert.
Referenced by CVC3::Expr::getUid(), and CVC3::ExprBoundVar::operator==().
|
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==().
|
inlinevirtual |
Reimplemented in CVC3::ExprRational.
Definition at line 332 of file expr_value.h.
References DebugAssert.
Referenced by CVC3::Expr::getRational(), and CVC3::ExprRational::operator==().
|
inlinevirtual |
Returns the string name of UCONST and BOUND_VAR expr's.
Reimplemented in CVC3::ExprBoundVar, CVC3::ExprSymbol, and CVC3::ExprVar.
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==().
|
inlinevirtual |
Returns the original Boolean variable (for BoolVarExprValue)
Definition at line 346 of file expr_value.h.
References DebugAssert.
|
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==().
|
inlinevirtual |
Reimplemented in CVC3::ExprClosure.
Definition at line 358 of file expr_value.h.
References DebugAssert.
Referenced by CVC3::Expr::getVars(), and CVC3::ExprClosure::operator==().
|
inlinevirtual |
Reimplemented in CVC3::ExprClosure.
Definition at line 364 of file expr_value.h.
References DebugAssert.
Referenced by CVC3::Expr::getBody(), and CVC3::ExprClosure::operator==().
|
inlinevirtual |
Reimplemented in CVC3::ExprClosure.
Definition at line 370 of file expr_value.h.
References DebugAssert.
Referenced by CVC3::Expr::setTriggers().
|
inlinevirtual |
Reimplemented in CVC3::ExprClosure.
Definition at line 374 of file expr_value.h.
References DebugAssert.
Referenced by CVC3::Expr::getTriggers().
|
inlinevirtual |
Reimplemented in CVC3::ExprSkolem.
Definition at line 381 of file expr_value.h.
References DebugAssert.
Referenced by CVC3::Expr::getExistential(), and CVC3::ExprSkolem::operator==().
|
inlinevirtual |
Reimplemented in CVC3::ExprSkolem.
Definition at line 386 of file expr_value.h.
References DebugAssert.
Referenced by CVC3::Expr::getBoundIndex(), and CVC3::ExprSkolem::operator==().
|
inlinevirtual |
Definition at line 391 of file expr_value.h.
References DebugAssert.
|
inlinevirtual |
Definition at line 396 of file expr_value.h.
References DebugAssert.
|
inlinevirtual |
Definition at line 401 of file expr_value.h.
References DebugAssert.
|
inlinevirtual |
Definition at line 405 of file expr_value.h.
References DebugAssert.
Referenced by CVC3::Expr::getTheorem().
|
friend |
Definition at line 70 of file expr_value.h.
|
friend |
Definition at line 71 of file expr_value.h.
|
friend |
Definition at line 72 of file expr_value.h.
|
friend |
Definition at line 73 of file expr_value.h.
|
friend |
Definition at line 74 of file expr_value.h.
|
friend |
Definition at line 75 of file expr_value.h.
|
friend |
Definition at line 76 of file expr_value.h.
|
private |
Unique expression id.
Definition at line 79 of file expr_value.h.
Referenced by CVC3::Expr::getIndex().
|
private |
Reference counter for garbage collection.
Definition at line 82 of file expr_value.h.
Referenced by CVC3::Expr::~Expr().
|
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().
|
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().
|
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().
|
private |
For caching calls to Simplify.
Definition at line 106 of file expr_value.h.
Referenced by CVC3::Expr::getSimpCache(), and CVC3::Expr::setSimpCache().
|
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().
|
private |
context-dependent bit-vector for flags that are context-dependent
Definition at line 112 of file expr_value.h.
Referenced by CVC3::Expr::clearRewriteNormal(), CVC3::Expr::computeTransClosure(), CVC3::Expr::containsBoundVar(), CVC3::Expr::getIsAtomicFlag(), CVC3::Expr::getTerminalsConstFlag(), CVC3::Expr::inUserAssumption(), CVC3::Expr::isFinite(), CVC3::Expr::isImpliedLiteral(), CVC3::Expr::isIntAssumption(), CVC3::Expr::isJustified(), CVC3::Expr::isRegisteredAtom(), CVC3::Expr::isRewriteNormal(), CVC3::Expr::isSelected(), CVC3::Expr::isStoredPredicate(), CVC3::Expr::isTranslated(), CVC3::Expr::isUserAssumption(), CVC3::Expr::isUserRegisteredAtom(), CVC3::Expr::isValidType(), CVC3::Expr::isWellFounded(), CVC3::Expr::notArrayNormalized(), CVC3::Expr::setComputeTransClosure(), CVC3::Expr::setContainsBoundVar(), CVC3::Expr::setFinite(), CVC3::Expr::setImpliedLiteral(), CVC3::Expr::setIntAssumption(), CVC3::Expr::setInUserAssumption(), CVC3::Expr::setIsAtomicFlag(), CVC3::Expr::setJustified(), CVC3::Expr::setNotArrayNormalized(), CVC3::Expr::setRegisteredAtom(), CVC3::Expr::setRewriteNormal(), CVC3::Expr::setSelected(), CVC3::Expr::setStoredPredicate(), CVC3::Expr::setTerminalsConstFlag(), CVC3::Expr::setTranslated(), CVC3::Expr::setUserAssumption(), CVC3::Expr::setUserRegisteredAtom(), CVC3::Expr::setUsesCC(), CVC3::Expr::setValidType(), CVC3::Expr::setWellFounded(), CVC3::Expr::usesCC(), CVC3::Expr::validIsAtomicFlag(), and CVC3::Expr::validTerminalsConstFlag().
|
private |
Size of dag rooted at this expression.
Definition at line 115 of file expr_value.h.
Referenced by CVC3::Expr::getSize().
|
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().
|
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==().
|
protected |
Our expr. manager.
Definition at line 132 of file expr_value.h.
Referenced by CVC3::Theorem::clearAllFlags(), CVC3::Theorem::getCachedValue(), CVC3::Expr::getEM(), CVC3::Theorem::getExpandFlag(), CVC3::Theorem::getLitFlag(), CVC3::Expr::hasLastIndex(), CVC3::Theorem::isFlagged(), CVC3::Theorem::setCachedValue(), CVC3::Theorem::setExpandFlag(), CVC3::Theorem::setFlag(), CVC3::Theorem::setLitFlag(), CVC3::Theorem::withAssumptions(), CVC3::Theorem::withProof(), and CVC3::Expr::~Expr().
|
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().
|
staticprotected |
Definition at line 183 of file expr_value.h.
Referenced by CVC3::ExprSymbol::computeHash().