CVC3::Expr Class Reference

Data structure of expressions in CVC3. More...

#include <expr.h>

Collaboration diagram for CVC3::Expr:

List of all members.

Classes

• class iterator

Public Member Functions

• Expr ()

  Default constructor creates the Null Expr.
  

• Expr (const Expr &e)

  Copy constructor and assignment (copy the pointer and take care of the refcount)
  

• Expr & operator= (const Expr &e)

  Assignment operator: take care of the refcounting and GC.
  

• Expr (const Op &op, const Expr &child)
• Expr (const Op &op, const Expr &child0, const Expr &child1)
• Expr (const Op &op, const Expr &child0, const Expr &child1, const Expr &child2)
• Expr (const Op &op, const Expr &child0, const Expr &child1, const Expr &child2, const Expr &child3)
• Expr (const Op &op, const std::vector< Expr > &children, ExprManager *em=NULL)
• ~Expr ()

  Destructor.
  

• Expr eqExpr (const Expr &right) const
• Expr notExpr () const
• Expr negate () const
• Expr andExpr (const Expr &right) const
• Expr orExpr (const Expr &right) const
• Expr iteExpr (const Expr &thenpart, const Expr &elsepart) const
• Expr iffExpr (const Expr &right) const
• Expr impExpr (const Expr &right) const
• Expr xorExpr (const Expr &right) const
• Expr skolemExpr (int i) const

  Create a Skolem constant for the i'th variable of an existential (*this)
  

• Expr rebuild (ExprManager *em) const

  Create a Boolean variable out of the expression.
  

• Expr substExpr (const std::vector< Expr > &oldTerms, const std::vector< Expr > &newTerms) const
• Expr substExpr (const ExprHashMap< Expr > &oldToNew) const
• Expr substExprQuant (const std::vector< Expr > &oldTerms, const std::vector< Expr > &newTerms) const
• Expr substExprQuant (const ExprHashMap< Expr > &oldToNew) const
• Expr operator! () const
• Expr operator&& (const Expr &right) const
• Expr operator|| (const Expr &right) const
• size_t hash () const
• bool isFalse () const
• bool isTrue () const
• bool isBoolConst () const
• bool isVar () const
• bool isBoundVar () const
• bool isString () const
• bool isClosure () const
• bool isQuantifier () const
• bool isLambda () const
• bool isApply () const
• bool isSymbol () const
• bool isTheorem () const
• bool isConstant () const
• bool isRawList () const
• bool isType () const

  Expr represents a type.
  

• const ExprValue * getExprValue () const

  Provide access to ExprValue for client subclasses of ExprValue *only*.
  

• bool isTerm () const

  Test if e is a term (as opposed to a predicate/formula)
  

• bool isAtomic () const

  Test if e is atomic.
  

• bool isAtomicFormula () const

  Test if e is an atomic formula.
  

• bool isAbsAtomicFormula () const

  An abstract atomic formua is an atomic formula or a quantified formula.
  

• bool isLiteral () const

  Test if e is a literal.
  

• bool isAbsLiteral () const

  Test if e is an abstract literal.
  

• bool isBoolConnective () const

  A Bool connective is one of NOT,AND,OR,IMPLIES,IFF,XOR,ITE (with type Bool)
  

• bool isPropAtom () const

  True iff expr is not a Bool connective.
  

• bool isPropLiteral () const

  PropAtom or negation of PropAtom.
  

• bool containsTermITE () const

  Return whether Expr contains a non-bool type ITE as a sub-term.
  

• bool isEq () const
• bool isNot () const
• bool isAnd () const
• bool isOr () const
• bool isITE () const
• bool isIff () const
• bool isImpl () const
• bool isXor () const
• bool isForall () const
• bool isExists () const
• bool isRational () const
• bool isSkolem () const
• const std::string & getName () const
• const std::string & getUid () const

  For BOUND_VAR, get the UID.
  

• const std::string & getString () const
• const std::vector< Expr > & getVars () const

  Get bound variables from a closure Expr.
  

• const Expr & getExistential () const

  Get the existential axiom expression for skolem constant.
  

• int getBoundIndex () const

  Get the index of the bound var that skolem constant comes from.
  

• const Expr & getBody () const

  Get the body of the closure Expr.
  

• void setTriggers (const std::vector< std::vector< Expr > > &triggers) const

  Set the triggers for a closure Expr.
  

• void setTriggers (const std::vector< Expr > &triggers) const
• void setTrigger (const Expr &trigger) const
• void setMultiTrigger (const std::vector< Expr > &multiTrigger) const
• const std::vector< std::vector
  < Expr > > & getTriggers () const

  Get the manual triggers of the closure Expr.
  

• const Rational & getRational () const

  Get the Rational value out of RATIONAL_EXPR.
  

• const Theorem & getTheorem () const

  Get theorem from THEOREM_EXPR.
  

• ExprManager * getEM () const
• const std::vector< Expr > & getKids () const
• int getKind () const
• ExprIndex getIndex () const
• bool hasLastIndex () const
• Op mkOp () const

  Make the expr into an operator.
  

• Op getOp () const

  Get operator from expression.
  

• Expr getOpExpr () const

  Get expression of operator (for APPLY Exprs only)
  

• int getOpKind () const

  Get kind of operator (for APPLY Exprs only)
  

• int arity () const
• const Expr & operator[] (int i) const
• const Expr & unnegate () const

  Remove leading NOT if any.
  

• iterator begin () const

  Begin iterator.
  

• iterator end () const

  End iterator.
  

• bool isNull () const
• bool isInitialized () const
• size_t getMMIndex () const

  Get the memory manager index (it uniquely identifies the subclass)
  

• bool hasFind () const
• const Theorem & getFind () const
• int getFindLevel () const
• const Theorem & getEqNext () const
• NotifyList * getNotify () const
• Type getType () const

  Get the type. Recursively compute if necessary.
  

• Type lookupType () const

  Look up the current type. Do not recursively compute (i.e. may be NULL)
  

• Cardinality typeCard () const

  Return cardinality of type.
  

• Expr typeEnumerateFinite (Unsigned n) const

  Return nth (starting with 0) element in a finite type.
  

• Unsigned typeSizeFinite () const

  Return size of a finite type; returns 0 if size cannot be determined.
  

• bool validSimpCache () const

  Return true if there is a valid cached value for calling simplify on this Expr.
  

• const Theorem & getSimpCache () const
• bool isValidType () const
• bool validIsAtomicFlag () const
• bool validTerminalsConstFlag () const
• bool getIsAtomicFlag () const
• bool getTerminalsConstFlag () const
• bool isRewriteNormal () const
• bool isFinite () const
• bool isWellFounded () const
• bool computeTransClosure () const
• bool containsBoundVar () const
• bool usesCC () const
• bool notArrayNormalized () const
• bool isImpliedLiteral () const
• bool isUserAssumption () const
• bool inUserAssumption () const
• bool isIntAssumption () const
• bool isJustified () const
• bool isTranslated () const
• bool isUserRegisteredAtom () const
• bool isRegisteredAtom () const
• bool isSelected () const
• bool isStoredPredicate () const
• bool getFlag () const

  Check if the generic flag is set.
  

• void setFlag () const

  Set the generic flag.
  

• void clearFlags () const

  Clear the generic flag in all Exprs.
  

• std::string toString () const

  Print the expression to a string.
  

• std::string toString (InputLanguage lang) const

  Print the expression to a string using the given output language.
  

• void print (InputLanguage lang, bool dagify=true) const

  Print the expression in the specified format.
  

• void print () const

  Print the expression as AST (lisp-like format)
  

• void printnodag () const

  Print the expression as AST without dagifying.
  

• void pprint () const

  Pretty-print the expression.
  

• void pprintnodag () const

  Pretty-print without dagifying.
  

• ExprStream & print (ExprStream &os) const

  Print a leaf node.
  

• ExprStream & printAST (ExprStream &os) const

  Print the top node and then recurse through the children */.
  

• Expr & indent (int n, bool permanent=false)

  Set initial indentation to n.
  

• void setFind (const Theorem &e) const

  Set the find attribute to e.
  

• void setEqNext (const Theorem &e) const

  Set the eqNext attribute to e.
  

• void addToNotify (Theory *i, const Expr &e) const

  Add (e,i) to the notify list of this expression.
  

• void setType (const Type &t) const

  Set the cached type.
  

• void setSimpCache (const Theorem &e) const
• void setValidType () const
• void setIsAtomicFlag (bool value) const
• void setTerminalsConstFlag (bool value) const
• void setRewriteNormal () const
• void clearRewriteNormal () const
• void setFinite () const
• void setWellFounded () const
• void setComputeTransClosure () const
• void setContainsBoundVar () const
• void setUsesCC () const
• void setNotArrayNormalized () const
• void setImpliedLiteral () const
• void setUserAssumption (int scope=-1) const
• void setInUserAssumption (int scope=-1) const
• void setIntAssumption () const
• void setJustified () const
• void setTranslated (int scope=-1) const

  Set the translated flag for this Expr.
  

• void setUserRegisteredAtom () const

  Set the UserRegisteredAtom flag for this Expr.
  

• void setRegisteredAtom () const

  Set the RegisteredAtom flag for this Expr.
  

• void setSelected () const

  Set the Selected flag for this Expr.
  

• void setStoredPredicate () const

  Set the Stored Predicate flag for this Expr.
  

• bool subExprOf (const Expr &e) const

  Check if the current Expr (*this) is a subexpression of e.
  

• Unsigned getSize () const
• bool hasSig () const
• bool hasRep () const
• const Theorem & getSig () const
• const Theorem & getRep () const
• void setSig (const Theorem &e) const
• void setRep (const Theorem &e) const

Static Public Member Functions

• static size_t hash (const Expr &e)

Private Types

• enum StaticFlagsEnum {
    VALID_TYPE = 0x1, VALID_IS_ATOMIC = 0x2, IS_ATOMIC = 0x4, REWRITE_NORMAL = 0x8,
    IS_FINITE = 0x400, WELL_FOUNDED = 0x800, COMPUTE_TRANS_CLOSURE = 0x1000, CONTAINS_BOUND_VAR = 0x00020000,
    USES_CC = 0x00080000, VALID_TERMINALS_CONST = 0x00100000, TERMINALS_CONST = 0x00200000
  }

  bit-masks for static flags

  More...
  

• enum DynamicFlagsEnum {
    IMPLIED_LITERAL = 0x10, IS_USER_ASSUMPTION = 0x20, IS_INT_ASSUMPTION = 0x40, IS_JUSTIFIED = 0x80,
    IS_TRANSLATED = 0x100, IS_USER_REGISTERED_ATOM = 0x200, IS_SELECTED = 0x2000, IS_STORED_PREDICATE = 0x4000,
    IS_REGISTERED_ATOM = 0x8000, IN_USER_ASSUMPTION = 0x00010000, NOT_ARRAY_NORMALIZED = 0x00040000
  }

  bit-masks for dynamic flags

  More...
  

Private Member Functions

• Expr (ExprValue *expr)

  Private constructor, simply wraps around the pointer.
  

• Expr recursiveSubst (const ExprHashMap< Expr > &subst, ExprHashMap< Expr > &visited) const
• Expr recursiveQuantSubst (const ExprHashMap< Expr > &subst, ExprHashMap< Expr > &visited) const
• std::vector< std::vector< Expr > > substTriggers (const ExprHashMap< Expr > &subst, ExprHashMap< Expr > &visited) const

Private Attributes

• ExprValue * d_expr

Static Private Attributes

• static Expr s_null

  Convenient null expr.
  

Friends

• class ExprHasher
• class ExprManager
• class Op
• class ExprValue
• class ExprNode
• class ExprClosure
• class ::CInterface
• class Theorem
• CVC_DLL std::ostream & operator<< (std::ostream &os, const Expr &e)
• int compare (const Expr &e1, const Expr &e2)
• bool operator== (const Expr &e1, const Expr &e2)
• bool operator!= (const Expr &e1, const Expr &e2)
• bool operator< (const Expr &e1, const Expr &e2)
• bool operator<= (const Expr &e1, const Expr &e2)
• bool operator> (const Expr &e1, const Expr &e2)
• bool operator>= (const Expr &e1, const Expr &e2)

---

Detailed Description

Data structure of expressions in CVC3.

Class: Expr
Author: Clark Barrett
Created: Mon Nov 25 15:29:37 2002

This class is the main data structure for expressions that all other components should use. It is actually a smart pointer to the actual data holding class ExprValue and its subclasses.

Expressions are represented as DAGs with maximal sharing of subexpressions. Therefore, testing for equality is a constant time operation (simply compare the pointers).

Unused expressions are automatically garbage-collected. The use is determined by a reference counting mechanism. In particular, this means that if there is a circular dependency among expressions (e.g. an attribute points back to the expression itself), these expressions will not be garbage-collected, even if no one else is using them.

The most frequently used operations are getKind() (determining the kind of the top level node of the expression), arity() (how many children an Expr has), operator[]() for accessing a child, and various testers and methods for constructing new expressions.

In addition, a total ordering operator<() is provided. It is guaranteed to remain the same for the lifetime of the expressions (it may change, however, if the expression is garbage-collected and reborn).

Definition at line 133 of file expr.h.

---

Friends And Related Function Documentation

friend class ExprHasher [friend]

Definition at line 134 of file expr.h.

friend class ExprManager [friend]

Definition at line 135 of file expr.h.

friend class Op [friend]

Definition at line 136 of file expr.h.

Referenced by getOp(), and mkOp().

friend class ExprValue [friend]

Definition at line 137 of file expr.h.

friend class ExprNode [friend]

Definition at line 138 of file expr.h.

friend class ExprClosure [friend]

Definition at line 139 of file expr.h.

friend class ::CInterface [friend]

Definition at line 140 of file expr.h.

friend class Theorem [friend]

Definition at line 141 of file expr.h.

---

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

• expr.h
• expr.cpp