CVC3  2.4.1
Classes | Public Member Functions | Static Public Member Functions | Private Types | Private Member Functions | Private Attributes | Static Private Attributes | Friends | List of all members
CVC3::Expr Class Reference

Data structure of expressions in CVC3. More...

#include <expr.h>

Classes

class  iterator
 

Public Member Functions

 Expr ()
 Default constructor creates the Null Expr. More...
 
 Expr (const Expr &e)
 Copy constructor and assignment (copy the pointer and take care of the refcount) More...
 
Exproperator= (const Expr &e)
 Assignment operator: take care of the refcounting and GC. More...
 
 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. More...
 
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) More...
 
Expr rebuild (ExprManager *em) const
 Create a Boolean variable out of the expression. More...
 
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. More...
 
const ExprValuegetExprValue () const
 Provide access to ExprValue for client subclasses of ExprValue only More...
 
bool isTerm () const
 Test if e is a term (as opposed to a predicate/formula) More...
 
bool isAtomic () const
 Test if e is atomic. More...
 
bool isAtomicFormula () const
 Test if e is an atomic formula. More...
 
bool isAbsAtomicFormula () const
 An abstract atomic formua is an atomic formula or a quantified formula. More...
 
bool isLiteral () const
 Test if e is a literal. More...
 
bool isAbsLiteral () const
 Test if e is an abstract literal. More...
 
bool isBoolConnective () const
 A Bool connective is one of NOT,AND,OR,IMPLIES,IFF,XOR,ITE (with type Bool) More...
 
bool isPropAtom () const
 True iff expr is not a Bool connective. More...
 
bool isPropLiteral () const
 PropAtom or negation of PropAtom. More...
 
bool containsTermITE () const
 Return whether Expr contains a non-bool type ITE as a sub-term. More...
 
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. More...
 
const std::string & getString () const
 
const std::vector< Expr > & getVars () const
 Get bound variables from a closure Expr. More...
 
const ExprgetExistential () const
 Get the existential axiom expression for skolem constant. More...
 
int getBoundIndex () const
 Get the index of the bound var that skolem constant comes from. More...
 
const ExprgetBody () const
 Get the body of the closure Expr. More...
 
void setTriggers (const std::vector< std::vector< Expr > > &triggers) const
 Set the triggers for a closure Expr. More...
 
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. More...
 
const RationalgetRational () const
 Get the Rational value out of RATIONAL_EXPR. More...
 
const TheoremgetTheorem () const
 Get theorem from THEOREM_EXPR. More...
 
ExprManagergetEM () 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. More...
 
Op getOp () const
 Get operator from expression. More...
 
Expr getOpExpr () const
 Get expression of operator (for APPLY Exprs only) More...
 
int getOpKind () const
 Get kind of operator (for APPLY Exprs only) More...
 
int arity () const
 
const Exproperator[] (int i) const
 
const Exprunnegate () const
 Remove leading NOT if any. More...
 
iterator begin () const
 Begin iterator. More...
 
iterator end () const
 End iterator. More...
 
bool isNull () const
 
bool isInitialized () const
 
size_t getMMIndex () const
 Get the memory manager index (it uniquely identifies the subclass) More...
 
bool hasFind () const
 
const TheoremgetFind () const
 
int getFindLevel () const
 
const TheoremgetEqNext () const
 
NotifyListgetNotify () const
 
Type getType () const
 Get the type. Recursively compute if necessary. More...
 
Type lookupType () const
 Look up the current type. Do not recursively compute (i.e. may be NULL) More...
 
Cardinality typeCard () const
 Return cardinality of type. More...
 
Expr typeEnumerateFinite (Unsigned n) const
 Return nth (starting with 0) element in a finite type. More...
 
Unsigned typeSizeFinite () const
 Return size of a finite type; returns 0 if size cannot be determined. More...
 
bool validSimpCache () const
 Return true if there is a valid cached value for calling simplify on this Expr. More...
 
const TheoremgetSimpCache () 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. More...
 
void setFlag () const
 Set the generic flag. More...
 
void clearFlags () const
 Clear the generic flag in all Exprs. More...
 
std::string toString () const
 Print the expression to a string. More...
 
std::string toString (InputLanguage lang) const
 Print the expression to a string using the given output language. More...
 
void print (InputLanguage lang, bool dagify=true) const
 Print the expression in the specified format. More...
 
void print () const
 Print the expression as AST (lisp-like format) More...
 
void printnodag () const
 Print the expression as AST without dagifying. More...
 
void pprint () const
 Pretty-print the expression. More...
 
void pprintnodag () const
 Pretty-print without dagifying. More...
 
ExprStreamprint (ExprStream &os) const
 Print a leaf node. More...
 
ExprStreamprintAST (ExprStream &os) const
 Print the top node and then recurse through the children */. More...
 
Exprindent (int n, bool permanent=false)
 Set initial indentation to n. More...
 
void setFind (const Theorem &e) const
 Set the find attribute to e. More...
 
void setEqNext (const Theorem &e) const
 Set the eqNext attribute to e. More...
 
void addToNotify (Theory *i, const Expr &e) const
 Add (e,i) to the notify list of this expression. More...
 
void setType (const Type &t) const
 Set the cached type. More...
 
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. More...
 
void setUserRegisteredAtom () const
 Set the UserRegisteredAtom flag for this Expr. More...
 
void setRegisteredAtom () const
 Set the RegisteredAtom flag for this Expr. More...
 
void setSelected () const
 Set the Selected flag for this Expr. More...
 
void setStoredPredicate () const
 Set the Stored Predicate flag for this Expr. More...
 
bool subExprOf (const Expr &e) const
 Check if the current Expr (*this) is a subexpression of e. More...
 
Unsigned getSize () const
 
bool hasSig () const
 
bool hasRep () const
 
const TheoremgetSig () const
 
const TheoremgetRep () 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. More...
 
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

ExprValued_expr
 The value. This is the only data member in this class. More...
 

Static Private Attributes

static Expr s_null
 Convenient null expr. More...
 

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: