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

Data structure of expressions in CVC3. More...

#include <expr.h>

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)
Exproperator= (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 ExprValuegetExprValue () 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 ExprgetExistential () 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 ExprgetBody () 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 RationalgetRational () const
 Get the Rational value out of RATIONAL_EXPR.
const TheoremgetTheorem () const
 Get theorem from THEOREM_EXPR.
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.
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 Exproperator[] (int i) const
const Exprunnegate () 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 TheoremgetFind () const
int getFindLevel () const
const TheoremgetEqNext () const
NotifyListgetNotify () 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 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.
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.
ExprStreamprint (ExprStream &os) const
 Print a leaf node.
ExprStreamprintAST (ExprStream &os) const
 Print the top node and then recurse through the children */.
Exprindent (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 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.
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

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: