CVC3

expr.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file expr.h
00004  * \brief Definition of the API to expression package.  See class Expr for details.
00005  *
00006  * Author: Clark Barrett
00007  *
00008  * Created: Tue Nov 26 00:27:40 2002
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  *
00017  * <hr>
00018  *
00019  */
00020 /*****************************************************************************/
00021 
00022 #ifndef _cvc3__expr_h_
00023 #define _cvc3__expr_h_
00024 
00025 #include <stdlib.h>
00026 #include <sstream>
00027 #include <set>
00028 #include <functional>
00029 #include <iterator>
00030 #include <map>
00031 
00032 #include "os.h"
00033 #include "compat_hash_map.h"
00034 #include "compat_hash_set.h"
00035 #include "rational.h"
00036 #include "kinds.h"
00037 #include "cdo.h"
00038 #include "cdflags.h"
00039 #include "lang.h"
00040 #include "memory_manager.h"
00041 
00042 class CInterface;
00043 
00044 namespace CVC3 {
00045 
00046   class NotifyList;
00047   class Theory;
00048   class Op;
00049   class Type;
00050   class Theorem;
00051 
00052   template<class Data>
00053   class ExprHashMap;
00054 
00055   class ExprManager;
00056   // Internal data-holding classes
00057   class ExprValue;
00058   class ExprNode;
00059   // Printing
00060   class ExprStream;
00061 
00062   //! Type ID of each ExprValue subclass.
00063   /*! It is defined in expr.h, so that ExprManager can use it before loading
00064     expr_value.h */
00065   typedef enum {
00066     EXPR_VALUE,
00067     EXPR_NODE,
00068     EXPR_APPLY, //!< Application of functions and predicates
00069     EXPR_STRING,
00070     EXPR_RATIONAL,
00071     EXPR_SKOLEM,
00072     EXPR_UCONST,
00073     EXPR_SYMBOL,
00074     EXPR_BOUND_VAR,
00075     EXPR_CLOSURE,
00076     EXPR_VALUE_TYPE_LAST // The end of list; don't assign it to any subclass
00077   } ExprValueType;
00078 
00079   //! Enum for cardinality of types
00080   typedef enum {
00081     CARD_FINITE,
00082     CARD_INFINITE,
00083     CARD_UNKNOWN
00084   } Cardinality;
00085 
00086   //! Expression index type
00087   typedef long unsigned ExprIndex;
00088 
00089   /**************************************************************************/
00090   /*! \defgroup ExprPkg Expression Package
00091    * \ingroup BuildingBlocks
00092    */
00093   /**************************************************************************/
00094   /*! \defgroup Expr_SmartPointer Smart Pointer Functionality in Expr
00095    * \ingroup ExprPkg
00096    */
00097   /**************************************************************************/
00098 
00099   /**************************************************************************/
00100   //! Data structure of expressions in CVC3
00101   /*! \ingroup ExprPkg
00102    * Class: Expr <br>
00103    * Author: Clark Barrett <br>
00104    * Created: Mon Nov 25 15:29:37 2002
00105    *
00106    * This class is the main data structure for expressions that all
00107    * other components should use.  It is actually a <em>smart
00108    * pointer</em> to the actual data holding class ExprValue and its
00109    * subclasses.
00110    *
00111    * Expressions are represented as DAGs with maximal sharing of
00112    * subexpressions.  Therefore, testing for equality is a constant time
00113    * operation (simply compare the pointers).
00114    *
00115    * Unused expressions are automatically garbage-collected.  The use is
00116    * determined by a reference counting mechanism.  In particular, this
00117    * means that if there is a circular dependency among expressions
00118    * (e.g. an attribute points back to the expression itself), these
00119    * expressions will not be garbage-collected, even if no one else is
00120    * using them.
00121    *
00122    * The most frequently used operations are getKind() (determining the
00123    * kind of the top level node of the expression), arity() (how many
00124    * children an Expr has), operator[]() for accessing a child, and
00125    * various testers and methods for constructing new expressions.
00126    *
00127    * In addition, a total ordering operator<() is provided.  It is
00128    * guaranteed to remain the same for the lifetime of the expressions
00129    * (it may change, however, if the expression is garbage-collected and
00130    * reborn).
00131    */
00132   /**************************************************************************/
00133 class CVC_DLL Expr {
00134   friend class ExprHasher;
00135   friend class ExprManager;
00136   friend class Op;
00137   friend class ExprValue;
00138   friend class ExprNode;
00139   friend class ExprClosure;
00140   friend class ::CInterface;
00141   friend class Theorem;
00142 
00143   /*! \addtogroup ExprPkg
00144    * @{
00145    */
00146   //! bit-masks for static flags
00147   typedef enum {
00148     //! Whether is valid TYPE expr
00149     VALID_TYPE = 0x1,
00150     //! Whether IS_ATOMIC flag is valid (initialized)
00151     VALID_IS_ATOMIC = 0x2,
00152     //! Whether the expression is an atomic term or formula
00153     IS_ATOMIC = 0x4,
00154     //! Expression is the result of a "normal" (idempotent) rewrite
00155     REWRITE_NORMAL = 0x8,
00156     //! Finite type
00157     IS_FINITE = 0x400,
00158     //! Well-founded (used in datatypes)
00159     WELL_FOUNDED = 0x800,
00160     //! Compute transitive closure (for binary uninterpreted predicates)
00161     COMPUTE_TRANS_CLOSURE = 0x1000,
00162     //! Whether expr contains a bounded variable (for quantifier instantiation)
00163     CONTAINS_BOUND_VAR = 0x00020000,
00164     //! Whether expr uses CC algorithm that relies on not simplifying an expr that has a find
00165     USES_CC = 0x00080000,
00166     //! Whether TERMINALS_CONST flag is valid (initialized)
00167     VALID_TERMINALS_CONST = 0x00100000,
00168     //! Whether expr contains only numerical constants at all possible ite terminals
00169     TERMINALS_CONST = 0x00200000
00170   } StaticFlagsEnum;
00171 
00172   //! bit-masks for dynamic flags
00173   // TODO: Registered flags instead of hard-wired
00174   typedef enum {
00175     //! Whether expr has been added as an implied literal
00176     IMPLIED_LITERAL = 0x10,
00177     IS_USER_ASSUMPTION = 0x20,
00178     IS_INT_ASSUMPTION = 0x40,
00179     IS_JUSTIFIED = 0x80,
00180     IS_TRANSLATED = 0x100,
00181     IS_USER_REGISTERED_ATOM = 0x200,
00182     IS_SELECTED = 0x2000,
00183     IS_STORED_PREDICATE = 0x4000,
00184     IS_REGISTERED_ATOM = 0x8000,
00185     IN_USER_ASSUMPTION = 0x00010000,
00186     //! Whether expr is normalized (in array theory)
00187     NOT_ARRAY_NORMALIZED = 0x00040000
00188   } DynamicFlagsEnum;
00189 
00190   //! Convenient null expr
00191   static Expr s_null;
00192 
00193   /////////////////////////////////////////////////////////////////////////////
00194   // Private Dynamic Data                                                    //
00195   /////////////////////////////////////////////////////////////////////////////
00196   //! The value.  This is the only data member in this class.
00197   ExprValue* d_expr;
00198 
00199   /////////////////////////////////////////////////////////////////////////////
00200   // Private methods                                                         //
00201   /////////////////////////////////////////////////////////////////////////////
00202 
00203   //! Private constructor, simply wraps around the pointer
00204   Expr(ExprValue* expr);
00205 
00206   Expr recursiveSubst(const ExprHashMap<Expr>& subst,
00207                       ExprHashMap<Expr>& visited) const;
00208 
00209   Expr recursiveQuantSubst(const ExprHashMap<Expr>& subst,
00210                       ExprHashMap<Expr>& visited) const;
00211 
00212   std::vector<std::vector<Expr> > substTriggers(const ExprHashMap<Expr> & subst,
00213         ExprHashMap<Expr> & visited) const;
00214 public:
00215   /////////////////////////////////////////////////////////////////////////////
00216   // Public Classes and Types                                                //
00217   /////////////////////////////////////////////////////////////////////////////
00218 
00219   /////////////////////////////////////////////////////////////////////////////
00220   /*!
00221    * Class: Expr::iterator
00222    * Author: Sergey Berezin
00223    * Created: Fri Dec  6 15:38:51 2002
00224    * Description: STL-like iterator API to the Expr's children.
00225    * IMPORTANT: the iterator will not be valid after the originating
00226    * expression is destroyed.
00227   */
00228   /////////////////////////////////////////////////////////////////////////////
00229   class CVC_DLL iterator
00230     : public std::iterator<std::input_iterator_tag,Expr,ptrdiff_t>
00231   {
00232     friend class Expr;
00233   private:
00234     std::vector<Expr>::const_iterator d_it;
00235     // Private constructors (used by Expr only)
00236     //
00237     //! Construct an iterator out of the vector's iterator
00238     iterator(std::vector<Expr>::const_iterator it): d_it(it) { }
00239     // Public methods
00240   public:
00241     //! Default constructor
00242     iterator() { }
00243     // Copy constructor and operator= are defined by C++, that's good enough
00244 
00245     //! Equality
00246     bool operator==(const iterator& i) const {
00247       return d_it == i.d_it;
00248     }
00249     //! Disequality
00250     bool operator!=(const iterator& i) const { return !(*this == i); }
00251     //! Dereference operator
00252     const Expr& operator*() const { return *d_it; }
00253     //! Dereference and member access
00254     const Expr* operator->() const { return &(operator*()); }
00255     //! Prefix increment
00256     iterator& operator++() {
00257       ++d_it;
00258       return *this;
00259     }
00260     /*! @brief Postfix increment requires a Proxy object to hold the
00261      * intermediate value for dereferencing */
00262     class Proxy {
00263       const Expr* d_e;
00264     public:
00265       Proxy(const Expr& e) : d_e(&e) { }
00266       Expr operator*() { return *d_e; }
00267     };
00268     //! Postfix increment
00269     /*! \return Proxy with the old Expr.
00270      *
00271      * Now, an expression like *i++ will return the current *i, and
00272      * then advance the iterator.  However, don't try to use Proxy for
00273      * anything else.
00274      */
00275     Proxy operator++(int) {
00276       Proxy e(*(*this));
00277       ++(*this);
00278       return e;
00279     }
00280   }; // end of class Expr::iterator
00281 
00282   /////////////////////////////////////////////////////////////////////////////
00283   // Constructors                                                            //
00284   /////////////////////////////////////////////////////////////////////////////
00285 
00286   //! Default constructor creates the Null Expr
00287   Expr(): d_expr(NULL) {}
00288 
00289   /*! @brief Copy constructor and assignment (copy the pointer and take care
00290     of the refcount) */
00291   Expr(const Expr& e);
00292   //! Assignment operator: take care of the refcounting and GC
00293   Expr& operator=(const Expr& e);
00294 
00295   // These constructors grab the ExprManager from the Op or the first
00296   // child.  The operator and all children must belong to the same
00297   // ExprManager.
00298   Expr(const Op& op, const Expr& child);
00299   Expr(const Op& op, const Expr& child0, const Expr& child1);
00300   Expr(const Op& op, const Expr& child0, const Expr& child1,
00301        const Expr& child2);
00302   Expr(const Op& op, const Expr& child0, const Expr& child1,
00303        const Expr& child2, const Expr& child3);
00304   Expr(const Op& op, const std::vector<Expr>& children,
00305        ExprManager* em = NULL);
00306 
00307   //! Destructor
00308   ~Expr();
00309 
00310   // Compound expression constructors
00311   Expr eqExpr(const Expr& right) const;
00312   Expr notExpr() const;
00313   Expr negate() const; // avoid double-negatives
00314   Expr andExpr(const Expr& right) const;
00315   Expr orExpr(const Expr& right) const;
00316   Expr iteExpr(const Expr& thenpart, const Expr& elsepart) const;
00317   Expr iffExpr(const Expr& right) const;
00318   Expr impExpr(const Expr& right) const;
00319   Expr xorExpr(const Expr& right) const;
00320   //! Create a Skolem constant for the i'th variable of an existential (*this)
00321   Expr skolemExpr(int i) const;
00322   //! Create a Boolean variable out of the expression
00323   //  Expr boolVarExpr() const;
00324   //! Rebuild Expr with a new ExprManager
00325   Expr rebuild(ExprManager* em) const;
00326 //    Expr newForall(const Expr& e);
00327 //    Expr newExists(const Expr& e);
00328   Expr substExpr(const std::vector<Expr>& oldTerms,
00329                  const std::vector<Expr>& newTerms) const;
00330   Expr substExpr(const ExprHashMap<Expr>& oldToNew) const;
00331 
00332 // by yeting, a special subst function for TheoryQuant
00333   Expr substExprQuant(const std::vector<Expr>& oldTerms,
00334           const std::vector<Expr>& newTerms) const;
00335   Expr substExprQuant(const ExprHashMap<Expr>& oldToNew) const;
00336 
00337   Expr operator!() const { return notExpr(); }
00338   Expr operator&&(const Expr& right) const { return andExpr(right); }
00339   Expr operator||(const Expr& right) const { return orExpr(right); }
00340 
00341   /////////////////////////////////////////////////////////////////////////////
00342   // Public Static Methods                                                   //
00343   /////////////////////////////////////////////////////////////////////////////
00344 
00345   static size_t hash(const Expr& e);
00346 
00347   /////////////////////////////////////////////////////////////////////////////
00348   // Read-only (const) methods                                               //
00349   /////////////////////////////////////////////////////////////////////////////
00350 
00351   size_t hash() const;
00352 
00353   // Core expression testers
00354 
00355   bool isFalse() const { return getKind() == FALSE_EXPR; }
00356   bool isTrue() const { return getKind() == TRUE_EXPR; }
00357   bool isBoolConst() const { return isFalse() || isTrue(); }
00358   bool isVar() const;
00359   bool isBoundVar() const { return getKind() == BOUND_VAR; }
00360   bool isString() const;
00361   bool isClosure() const;
00362   bool isQuantifier() const;
00363   bool isLambda() const;
00364   bool isApply() const;
00365   bool isSymbol() const;
00366   bool isTheorem() const;
00367 
00368   bool isConstant() const { return getOpKind() <= MAX_CONST; }
00369   
00370   bool isRawList() const {return getKind() == RAW_LIST;}
00371 
00372   //! Expr represents a type
00373   bool isType() const;
00374   /*
00375   bool isRecord() const;
00376   bool isRecordAccess() const;
00377   bool isTupleAccess() const;
00378   */
00379   //! Provide access to ExprValue for client subclasses of ExprValue *only*
00380   /*@ Calling getExprValue on an Expr with a built-in ExprValue class will
00381    * cause an error */
00382   const ExprValue* getExprValue() const;
00383 
00384   //! Test if e is a term (as opposed to a predicate/formula)
00385   bool isTerm() const;
00386   //! Test if e is atomic
00387   /*! An atomic expression is TRUE or FALSE or one that does not
00388    *  contain a formula (including not being a formula itself).
00389    *  \sa isAtomicFormula */
00390   bool isAtomic() const;
00391   //! Test if e is an atomic formula
00392   /*! An atomic formula is TRUE or FALSE or an application of a predicate
00393     (possibly 0-ary) which does not properly contain any formula.  For
00394     instance, the formula "x = IF f THEN y ELSE z ENDIF" is not an atomic
00395     formula, since it contains the condition "f", which is a formula. */
00396   bool isAtomicFormula() const;
00397   //! An abstract atomic formua is an atomic formula or a quantified formula
00398   bool isAbsAtomicFormula() const
00399     { return isQuantifier() || isAtomicFormula(); }
00400   //! Test if e is a literal
00401   /*! A literal is an atomic formula, or its negation.
00402     \sa isAtomicFormula */
00403   bool isLiteral() const
00404   { return (isAtomicFormula() || (isNot() && (*this)[0].isAtomicFormula())); }
00405   //! Test if e is an abstract literal
00406   bool isAbsLiteral() const
00407   { return (isAbsAtomicFormula() || (isNot() && (*this)[0].isAbsAtomicFormula())); }
00408   //! A Bool connective is one of NOT,AND,OR,IMPLIES,IFF,XOR,ITE (with type Bool)
00409   bool isBoolConnective() const;
00410   //! True iff expr is not a Bool connective
00411   bool isPropAtom() const { return !isTerm() && !isBoolConnective(); }
00412   //! PropAtom or negation of PropAtom
00413   bool isPropLiteral() const
00414     { return (isNot() && (*this)[0].isPropAtom()) || isPropAtom(); }
00415   //! Return whether Expr contains a non-bool type ITE as a sub-term
00416   bool containsTermITE() const;
00417 
00418 
00419   bool isEq() const { return getKind() == EQ; }
00420   bool isNot() const { return getKind() == NOT; }
00421   bool isAnd() const { return getKind() == AND; }
00422   bool isOr() const { return getKind() == OR; }
00423   bool isITE() const { return getKind() == ITE; }
00424   bool isIff() const { return getKind() == IFF; }
00425   bool isImpl() const { return getKind() == IMPLIES; }
00426   bool isXor() const { return getKind() == XOR;}
00427 
00428   bool isForall() const { return getKind() == FORALL; }
00429   bool isExists() const { return getKind() == EXISTS; }
00430 
00431   bool isRational() const { return getKind() == RATIONAL_EXPR; }
00432   bool isSkolem() const { return getKind() == SKOLEM_VAR;}
00433 
00434   // Leaf accessors - these functions must only be called one expressions of
00435   // the appropriate kind.
00436 
00437   // For UCONST and BOUND_VAR Expr's
00438   const std::string& getName() const;
00439   //! For BOUND_VAR, get the UID
00440   const std::string& getUid() const;
00441 
00442   // For STRING_EXPR's
00443   const std::string& getString() const;
00444   //! Get bound variables from a closure Expr
00445   const std::vector<Expr>& getVars() const;
00446   //! Get the existential axiom expression for skolem constant
00447   const Expr& getExistential() const;
00448   //! Get the index of the bound var that skolem constant comes from
00449   int getBoundIndex() const;
00450 
00451   //! Get the body of the closure Expr
00452   const Expr& getBody() const;
00453 
00454   //! Set the triggers for a closure Expr
00455   void setTriggers(const std::vector<std::vector<Expr> >& triggers) const;
00456   void setTriggers(const std::vector<Expr>& triggers) const;
00457   void setTrigger(const Expr& trigger) const;
00458   void setMultiTrigger(const std::vector<Expr>& multiTrigger) const;
00459 
00460   //! Get the manual triggers of the closure Expr
00461   const std::vector<std::vector<Expr> >& getTriggers() const; //by yeting
00462 
00463   //! Get the Rational value out of RATIONAL_EXPR
00464   const Rational& getRational() const;
00465   //! Get theorem from THEOREM_EXPR
00466   const Theorem& getTheorem() const;
00467 
00468   // Get the expression manager.  The expression must be non-null.
00469   ExprManager *getEM() const;
00470 
00471   // Return a ref to the vector of children.
00472   const std::vector<Expr>& getKids() const;
00473 
00474   // Get the kind of this expr.
00475   int getKind() const;
00476 
00477   // Get the index field
00478   ExprIndex getIndex() const;
00479 
00480   // True if this is the most recently created expression
00481   bool hasLastIndex() const;
00482 
00483   //! Make the expr into an operator
00484   Op mkOp() const;
00485 
00486   //! Get operator from expression
00487   Op getOp() const;
00488 
00489   //! Get expression of operator (for APPLY Exprs only)
00490   Expr getOpExpr() const;
00491 
00492   //! Get kind of operator (for APPLY Exprs only)
00493   int getOpKind() const;
00494 
00495   // Return the number of children.  Note, that an application of a
00496   // user-defined function has the arity of that function (the number
00497   // of arguments), and the function name itself is part of the
00498   // operator.
00499   int arity() const;
00500 
00501   // Return the ith child.  As with arity, it's also the ith argument
00502   // in function application.
00503   const Expr& operator[](int i) const;
00504 
00505   //! Remove leading NOT if any
00506   const Expr& unnegate() const { return isNot() ? (*this)[0] : *this; }
00507 
00508   //! Begin iterator
00509   iterator begin() const;
00510 
00511   //! End iterator
00512   iterator end() const;
00513 
00514   // Check if Expr is Null
00515   bool isNull() const;
00516 
00517   // Check if Expr is not Null
00518   bool isInitialized() const { return d_expr != NULL; }
00519   //! Get the memory manager index (it uniquely identifies the subclass)
00520   size_t getMMIndex() const;
00521 
00522   // Attributes
00523 
00524   // True if the find attribute has been set to something other than NULL.
00525   bool hasFind() const;
00526 
00527   // Return the attached find attribute for the expr.  Note that this
00528   // must be called repeatedly to get the root of the union-find tree.
00529   // Should only be called if hasFind is true.
00530   const Theorem& getFind() const;
00531   int getFindLevel() const;
00532   const Theorem& getEqNext() const;
00533 
00534   // Return the notify list
00535   NotifyList* getNotify() const;
00536 
00537   //! Get the type.  Recursively compute if necessary
00538   Type getType() const;
00539   //! Look up the current type. Do not recursively compute (i.e. may be NULL)
00540   Type lookupType() const;
00541   //! Return cardinality of type
00542   Cardinality typeCard() const;
00543   //! Return nth (starting with 0) element in a finite type
00544   /*! Returns NULL Expr if unable to compute nth element
00545    */
00546   Expr typeEnumerateFinite(Unsigned n) const;
00547   //! Return size of a finite type; returns 0 if size cannot be determined
00548   Unsigned typeSizeFinite() const;
00549 
00550   /*! @brief Return true if there is a valid cached value for calling
00551       simplify on this Expr. */
00552   bool validSimpCache() const;
00553 
00554   // Get the cached Simplify of this Expr.
00555   const Theorem& getSimpCache() const;
00556 
00557   // Return true if valid type flag is set for Expr
00558   bool isValidType() const;
00559 
00560   // Return true if there is a valid flag for whether Expr is atomic
00561   bool validIsAtomicFlag() const;
00562 
00563   // Return true if there is a valid flag for whether terminals are const
00564   bool validTerminalsConstFlag() const;
00565 
00566   // Get the isAtomic flag
00567   bool getIsAtomicFlag() const;
00568 
00569   // Get the TerminalsConst flag
00570   bool getTerminalsConstFlag() const;
00571 
00572   // Get the RewriteNormal flag
00573   bool isRewriteNormal() const;
00574 
00575   // Get the isFinite flag
00576   bool isFinite() const;
00577 
00578   // Get the WellFounded flag
00579   bool isWellFounded() const;
00580 
00581   // Get the ComputeTransClosure flag
00582   bool computeTransClosure() const;
00583 
00584   // Get the ContainsBoundVar flag
00585   bool containsBoundVar() const;
00586 
00587   // Get the usesCC flag
00588   bool usesCC() const;
00589 
00590   // Get the notArrayNormalized flag
00591   bool notArrayNormalized() const;
00592 
00593   // Get the ImpliedLiteral flag
00594   bool isImpliedLiteral() const;
00595 
00596   // Get the UserAssumption flag
00597   bool isUserAssumption() const;
00598 
00599   // Get the inUserAssumption flag
00600   bool inUserAssumption() const;
00601 
00602   // Get the IntAssumption flag
00603   bool isIntAssumption() const;
00604 
00605   // Get the Justified flag
00606   bool isJustified() const;
00607 
00608   // Get the Translated flag
00609   bool isTranslated() const;
00610 
00611   // Get the UserRegisteredAtom flag
00612   bool isUserRegisteredAtom() const;
00613 
00614   // Get the RegisteredAtom flag
00615   bool isRegisteredAtom() const;
00616 
00617   // Get the Selected flag
00618   bool isSelected() const;
00619 
00620   // Get the Stored Predicate flag
00621   bool isStoredPredicate() const;
00622 
00623   //! Check if the generic flag is set
00624   bool getFlag() const;
00625   //! Set the generic flag
00626   void setFlag() const;
00627   //! Clear the generic flag in all Exprs
00628   void clearFlags() const;
00629 
00630   // Printing functions
00631 
00632   //! Print the expression to a string
00633   std::string toString() const;
00634   //! Print the expression to a string using the given output language
00635   std::string toString(InputLanguage lang) const;
00636   //! Print the expression in the specified format
00637   void print(InputLanguage lang, bool dagify = true) const;
00638 
00639   //! Print the expression as AST (lisp-like format)
00640   void print() const { print(AST_LANG); }
00641   //! Print the expression as AST without dagifying
00642   void printnodag() const;
00643 
00644   //! Pretty-print the expression
00645   void pprint() const;
00646   //! Pretty-print without dagifying
00647   void pprintnodag() const;
00648 
00649   //! Print a leaf node
00650   /*@ The top node is pretty-printed if it is a basic leaf type;
00651    * otherwise, just the kind is printed.  Should only be called on expressions
00652    * with no children. */
00653   ExprStream& print(ExprStream& os) const;
00654   //! Print the top node and then recurse through the children */
00655   /*@ The top node is printed as an AST with all the information, including
00656    * "hidden" Exprs that are part of the ExprValue */
00657   ExprStream& printAST(ExprStream& os) const;
00658   //! Set initial indentation to n.
00659   /*! The indentation will be reset to default unless the second
00660     argument is true.
00661     \return reference to itself, so one can write `os << e.indent(5)'
00662   */
00663   Expr& indent(int n, bool permanent = false);
00664 
00665   /////////////////////////////////////////////////////////////////////////////
00666   // Other Public methods                                                    //
00667   /////////////////////////////////////////////////////////////////////////////
00668 
00669   // Attributes
00670 
00671   //! Set the find attribute to e
00672   void setFind(const Theorem& e) const;
00673 
00674   //! Set the eqNext attribute to e
00675   void setEqNext(const Theorem& e) const;
00676 
00677   //! Add (e,i) to the notify list of this expression
00678   void addToNotify(Theory* i, const Expr& e) const;
00679 
00680   //! Set the cached type
00681   void setType(const Type& t) const;
00682 
00683   // Cache the result of a call to Simplify on this Expr
00684   void setSimpCache(const Theorem& e) const;
00685 
00686   // Set the valid type flag for this Expr
00687   void setValidType() const;
00688 
00689   // Set the isAtomicFlag for this Expr
00690   void setIsAtomicFlag(bool value) const;
00691 
00692   // Set the TerminalsConst flag for this Expr
00693   void setTerminalsConstFlag(bool value) const;
00694 
00695   // Set or clear the RewriteNormal flag
00696   void setRewriteNormal() const;
00697   void clearRewriteNormal() const;
00698 
00699   // Set the isFinite flag
00700   void setFinite() const;
00701 
00702   // Set the WellFounded flag
00703   void setWellFounded() const;
00704 
00705   // Set the ComputeTransClosure flag
00706   void setComputeTransClosure() const;
00707 
00708   // Set the ContainsBoundVar flag
00709   void setContainsBoundVar() const;
00710 
00711   // Set the UsesCC flag
00712   void setUsesCC() const;
00713 
00714   // Set the notArrayNormalized flag
00715   void setNotArrayNormalized() const;
00716 
00717   // Set the impliedLiteral flag for this Expr
00718   void setImpliedLiteral() const;
00719 
00720   // Set the user assumption flag for this Expr
00721   void setUserAssumption(int scope = -1) const;
00722 
00723   // Set the in user assumption flag for this Expr
00724   void setInUserAssumption(int scope = -1) const;
00725 
00726   // Set the internal assumption flag for this Expr
00727   void setIntAssumption() const;
00728 
00729   // Set the justified flag for this Expr
00730   void setJustified() const;
00731 
00732   //! Set the translated flag for this Expr
00733   void setTranslated(int scope = -1) const;
00734 
00735   //! Set the UserRegisteredAtom flag for this Expr
00736   void setUserRegisteredAtom() const;
00737 
00738   //! Set the RegisteredAtom flag for this Expr
00739   void setRegisteredAtom() const;
00740 
00741   //! Set the Selected flag for this Expr
00742   void setSelected() const;
00743 
00744   //! Set the Stored Predicate flag for this Expr
00745   void setStoredPredicate() const;
00746 
00747   //! Check if the current Expr (*this) is a subexpression of e
00748   bool subExprOf(const Expr& e) const;
00749   // Returns the maximum number of Boolean expressions on a path from
00750   // this to a leaf, including this.
00751 
00752   inline Unsigned getSize() const;
00753 
00754 //   inline int getHeight() const;
00755 
00756 //   // Returns the index of the highest kid.
00757 //   inline int getHighestKid() const;
00758 
00759 //   // Gets/sets an expression that this expression was simplified from
00760 //   // (see newRWTheorem). This is the equivalent of SVC's Sigx.
00761 //   inline bool hasSimpFrom() const;
00762 //   inline const Expr& getSimpFrom() const;
00763 //   inline void setSimpFrom(const Expr& simpFrom);
00764 
00765   // Attributes for uninterpreted function symbols.
00766   bool hasSig() const;
00767   bool hasRep() const;
00768   const Theorem& getSig() const;
00769   const Theorem& getRep() const;
00770   void setSig(const Theorem& e) const;
00771   void setRep(const Theorem& e) const;
00772 
00773   /////////////////////////////////////////////////////////////////////////////
00774   // Friend methods                                                          //
00775   /////////////////////////////////////////////////////////////////////////////
00776 
00777   friend CVC_DLL std::ostream& operator<<(std::ostream& os, const Expr& e);
00778 
00779   // The master method which defines some fixed total ordering on all
00780   // Exprs.  If e1 < e2, e1==e2, and e1 > e2, it returns -1, 0, 1
00781   // respectively.  A Null expr is always "smaller" than any other
00782   // expr, but is equal to itself.
00783   friend int compare(const Expr& e1, const Expr& e2);
00784 
00785   friend bool operator==(const Expr& e1, const Expr& e2);
00786   friend bool operator!=(const Expr& e1, const Expr& e2);
00787 
00788   friend bool operator<(const Expr& e1, const Expr& e2);
00789   friend bool operator<=(const Expr& e1, const Expr& e2);
00790   friend bool operator>(const Expr& e1, const Expr& e2);
00791   friend bool operator>=(const Expr& e1, const Expr& e2);
00792 
00793   /*!@}*/ // end of group Expr
00794 
00795 }; // end of class Expr
00796 
00797 } // end of namespace CVC3
00798 
00799 // Include expr_value.h here.  We cannot include it earlier, since it
00800 // needs the definition of class Expr.  See comments in expr_value.h.
00801 #ifndef DOXYGEN
00802 #include "expr_op.h"
00803 #include "expr_manager.h"
00804 #endif
00805 namespace CVC3 {
00806 
00807 inline Expr::Expr(ExprValue* expr) : d_expr(expr) { d_expr->incRefcount(); }
00808 
00809 inline Expr::Expr(const Expr& e) : d_expr(e.d_expr) {
00810   if (d_expr != NULL) d_expr->incRefcount();
00811 }
00812 
00813 inline Expr& Expr::operator=(const Expr& e) {
00814   if(&e == this) return *this; // Self-assignment
00815   ExprValue* tmp = e.d_expr;
00816   if(tmp == d_expr) return *this;
00817   if (tmp == NULL) {
00818     d_expr->decRefcount();
00819   }
00820   else {
00821     tmp->incRefcount();
00822     if(d_expr != NULL) {
00823       d_expr->decRefcount();
00824     }
00825   }
00826   d_expr = tmp;
00827   return *this;
00828 }
00829 
00830 inline Expr::Expr(const Op& op, const Expr& child) {
00831   ExprManager* em = child.getEM();
00832   if (op.getKind() != APPLY) {
00833     ExprNode ev(em, op.getKind());
00834     std::vector<Expr>& kids = ev.getKids1();
00835     kids.push_back(child);
00836     d_expr = em->newExprValue(&ev);
00837   } else {
00838     ExprApply ev(em, op);
00839     std::vector<Expr>& kids = ev.getKids1();
00840     kids.push_back(child);
00841     d_expr = em->newExprValue(&ev);
00842   }
00843   d_expr->incRefcount();
00844 }
00845 
00846 inline Expr::Expr(const Op& op, const Expr& child0, const Expr& child1) {
00847   ExprManager* em = child0.getEM();
00848   if (op.getKind() != APPLY) {
00849     ExprNode ev(em, op.getKind());
00850     std::vector<Expr>& kids = ev.getKids1();
00851     kids.push_back(child0);
00852     kids.push_back(child1);
00853     d_expr = em->newExprValue(&ev);
00854   } else {
00855     ExprApply ev(em, op);
00856     std::vector<Expr>& kids = ev.getKids1();
00857     kids.push_back(child0);
00858     kids.push_back(child1);
00859     d_expr = em->newExprValue(&ev);
00860   }
00861   d_expr->incRefcount();
00862 }
00863 
00864 inline Expr::Expr(const Op& op, const Expr& child0, const Expr& child1,
00865                   const Expr& child2) {
00866   ExprManager* em = child0.getEM();
00867   if (op.getKind() != APPLY) {
00868     ExprNode ev(em, op.getKind());
00869     std::vector<Expr>& kids = ev.getKids1();
00870     kids.push_back(child0);
00871     kids.push_back(child1);
00872     kids.push_back(child2);
00873     d_expr = em->newExprValue(&ev);
00874   } else {
00875     ExprApply ev(em, op);
00876     std::vector<Expr>& kids = ev.getKids1();
00877     kids.push_back(child0);
00878     kids.push_back(child1);
00879     kids.push_back(child2);
00880     d_expr = em->newExprValue(&ev);
00881   }
00882   d_expr->incRefcount();
00883 }
00884 
00885 inline Expr::Expr(const Op& op, const Expr& child0, const Expr& child1,
00886                   const Expr& child2, const Expr& child3) {
00887   ExprManager* em = child0.getEM();
00888   if (op.getKind() != APPLY) {
00889     ExprNode ev(em, op.getKind());
00890     std::vector<Expr>& kids = ev.getKids1();
00891     kids.push_back(child0);
00892     kids.push_back(child1);
00893     kids.push_back(child2);
00894     kids.push_back(child3);
00895     d_expr = em->newExprValue(&ev);
00896   } else {
00897     ExprApply ev(em, op);
00898     std::vector<Expr>& kids = ev.getKids1();
00899     kids.push_back(child0);
00900     kids.push_back(child1);
00901     kids.push_back(child2);
00902     kids.push_back(child3);
00903     d_expr = em->newExprValue(&ev);
00904   }
00905   d_expr->incRefcount();
00906 }
00907 
00908 inline Expr::Expr(const Op& op, const std::vector<Expr>& children,
00909                   ExprManager* em) {
00910   if (em == NULL) {
00911     if (op.getKind() == APPLY) em = op.getExpr().getEM();
00912     else {
00913       DebugAssert(children.size() > 0,
00914                   "Expr::Expr(Op, children): op's EM is NULL and "
00915                   "no children given");
00916       em = children[0].getEM();
00917     }
00918   }
00919   if (op.getKind() != APPLY) {
00920     ExprNodeTmp ev(em, op.getKind(), children);
00921     d_expr = em->newExprValue(&ev);
00922   } else {
00923     ExprApplyTmp ev(em, op, children);
00924     d_expr = em->newExprValue(&ev);
00925   }
00926   d_expr->incRefcount();
00927 }
00928 
00929 inline Expr Expr::eqExpr(const Expr& right) const {
00930   return Expr(EQ, *this, right);
00931 }
00932 
00933 inline Expr Expr::notExpr() const {
00934   return Expr(NOT, *this);
00935 }
00936 
00937 inline Expr Expr::negate() const {
00938   return isNot() ? (*this)[0] : this->notExpr();
00939 }
00940 
00941 inline Expr Expr::andExpr(const Expr& right) const {
00942   return Expr(AND, *this, right);
00943 }
00944 
00945 inline Expr andExpr(const std::vector <Expr>& children) {
00946   DebugAssert(children.size()>0 && !children[0].isNull(),
00947               "Expr::andExpr(kids)");
00948   return Expr(AND, children);
00949 }
00950 
00951 inline Expr Expr::orExpr(const Expr& right) const {
00952   return Expr(OR, *this, right);
00953 }
00954 
00955 inline Expr orExpr(const std::vector <Expr>& children) {
00956   DebugAssert(children.size()>0 && !children[0].isNull(),
00957               "Expr::andExpr(kids)");
00958   return Expr(OR, children);
00959 }
00960 
00961 inline Expr Expr::iteExpr(const Expr& thenpart, const Expr& elsepart) const {
00962   return Expr(ITE, *this, thenpart, elsepart);
00963 }
00964 
00965 inline Expr Expr::iffExpr(const Expr& right) const {
00966   return Expr(IFF, *this, right);
00967 }
00968 
00969 inline Expr Expr::impExpr(const Expr& right) const {
00970   return Expr(IMPLIES, *this, right);
00971 }
00972 
00973 inline Expr Expr::xorExpr(const Expr& right) const {
00974   return Expr(XOR, *this, right);
00975 }
00976 
00977 inline Expr Expr::skolemExpr(int i) const {
00978   return getEM()->newSkolemExpr(*this, i);
00979 }
00980 
00981 inline Expr Expr::rebuild(ExprManager* em) const {
00982   return em->rebuild(*this);
00983 }
00984 
00985 inline Expr::~Expr() {
00986   if(d_expr != NULL) {
00987     IF_DEBUG(FatalAssert(d_expr->d_refcount > 0, "Mis-handled the ref. counting");)
00988     if (--(d_expr->d_refcount) == 0) d_expr->d_em->gc(d_expr);
00989   }
00990 }
00991 
00992 inline size_t Expr::hash(const Expr& e) { return e.getEM()->hash(e); }
00993 
00994 /////////////////////////////////////////////////////////////////////////////
00995 // Read-only (const) methods                                               //
00996 /////////////////////////////////////////////////////////////////////////////
00997 
00998 inline size_t Expr::hash() const { return getEM()->hash(*this); }
00999 
01000 inline const ExprValue* Expr::getExprValue() const
01001   { return d_expr->getExprValue(); }
01002 
01003 // Core Expression Testers
01004 
01005 inline bool Expr::isVar() const { return d_expr->isVar(); }
01006 inline bool Expr::isString() const { return d_expr->isString(); }
01007 inline bool Expr::isClosure() const { return d_expr->isClosure(); }
01008 inline bool Expr::isQuantifier() const {
01009   return (isClosure() && (getKind() == FORALL || getKind() == EXISTS));
01010 }
01011 inline bool Expr::isLambda() const {
01012   return (isClosure() && getKind() == LAMBDA);
01013 }
01014 inline bool Expr::isApply() const
01015 { DebugAssert((getKind() != APPLY || d_expr->isApply()) &&
01016               (!d_expr->isApply() || getKind() == APPLY), "APPLY mismatch");
01017   return getKind() == APPLY; }
01018 inline bool Expr::isSymbol() const { return d_expr->isSymbol(); }
01019 inline bool Expr::isTheorem() const { return d_expr->isTheorem(); }
01020 inline bool Expr::isType() const { return getEM()->isTypeKind(getOpKind()); }
01021 inline bool Expr::isTerm() const { return !getType().isBool(); }
01022 inline bool Expr::isBoolConnective() const {
01023   if (!getType().isBool()) return false;
01024   switch (getKind()) {
01025     case NOT: case AND: case OR: case IMPLIES: case IFF: case XOR: case ITE:
01026       return true; }
01027   return false;
01028 }
01029 
01030 inline Unsigned Expr::getSize() const {
01031   if (d_expr->d_size == 0) {
01032     clearFlags();
01033     const_cast<ExprValue*>(d_expr)->d_size = d_expr->getSize();
01034   }
01035   return d_expr->d_size;
01036 }
01037 
01038   //inline int Expr::getHeight() const { return d_expr->getHeight(); }
01039   //inline int Expr::getHighestKid() const { return d_expr->getHighestKid(); }
01040 
01041   //inline bool Expr::hasSimpFrom() const
01042 //   { return !d_expr->getSimpFrom().isNull(); }
01043 // inline const Expr& Expr::getSimpFrom() const
01044 //   { return hasSimpFrom() ? d_expr->getSimpFrom() : *this; }
01045 // inline void Expr::setSimpFrom(const Expr& simpFrom)
01046 //   { d_expr->setSimpFrom(simpFrom); }
01047 
01048 // Leaf accessors
01049 
01050 inline const std::string& Expr::getName() const {
01051   DebugAssert(!isNull(), "Expr::getName() on Null expr");
01052   return d_expr->getName();
01053 }
01054 
01055 inline const std::string& Expr::getString() const {
01056    DebugAssert(isString(),
01057         "CVC3::Expr::getString(): not a string Expr:\n  "
01058         + toString(AST_LANG));
01059    return d_expr->getString();
01060 }
01061 
01062 inline const std::vector<Expr>& Expr::getVars() const {
01063    DebugAssert(isClosure(),
01064         "CVC3::Expr::getVars(): not a closure Expr:\n  "
01065         + toString(AST_LANG));
01066    return d_expr->getVars();
01067 }
01068 
01069 inline const Expr& Expr::getBody() const {
01070    DebugAssert(isClosure(),
01071         "CVC3::Expr::getBody(): not a closure Expr:\n  "
01072         + toString(AST_LANG));
01073    return d_expr->getBody();
01074 }
01075 
01076  inline void Expr::setTriggers(const std::vector< std::vector<Expr> >& triggers) const {
01077   DebugAssert(isClosure(),
01078         "CVC3::Expr::setTriggers(): not a closure Expr:\n  "
01079         + toString(AST_LANG));
01080   d_expr->setTriggers(triggers);
01081 }
01082 
01083 inline void Expr::setTriggers(const std::vector<Expr>& triggers) const {
01084    DebugAssert(isClosure(),
01085                "CVC3::Expr::setTriggers(): not a closure Expr:\n  "
01086                + toString(AST_LANG));
01087    std::vector<std::vector<Expr> > patternvv;
01088    for(std::vector<Expr>::const_iterator i = triggers.begin(); i != triggers.end(); ++i ) {
01089      std::vector<Expr> patternv;
01090      patternv.push_back(*i);
01091      patternvv.push_back(patternv);
01092    }
01093    d_expr->setTriggers(patternvv);
01094  }
01095 
01096 inline void Expr::setTrigger(const Expr& trigger) const {
01097   DebugAssert(isClosure(),
01098         "CVC3::Expr::setTrigger(): not a closure Expr:\n  "
01099         + toString(AST_LANG));
01100   std::vector<std::vector<Expr> > patternvv;
01101   std::vector<Expr> patternv;
01102   patternv.push_back(trigger);
01103   patternvv.push_back(patternv);
01104   setTriggers(patternvv);
01105 }
01106 
01107 inline void Expr::setMultiTrigger(const std::vector<Expr>& multiTrigger) const {
01108   DebugAssert(isClosure(),
01109               "CVC3::Expr::setTrigger(): not a closure Expr:\n  "
01110               + toString(AST_LANG));
01111   std::vector<std::vector<Expr> > patternvv;
01112   patternvv.push_back(multiTrigger);
01113   setTriggers(patternvv);
01114 }
01115 
01116  inline const std::vector<std::vector<Expr> >& Expr::getTriggers() const { //by yeting
01117   DebugAssert(isClosure(),
01118         "CVC3::Expr::getTrigs(): not a closure Expr:\n  "
01119         + toString(AST_LANG));
01120   return d_expr->getTriggers();
01121 }
01122 
01123 inline const Expr& Expr::getExistential() const {
01124   DebugAssert(isSkolem(),
01125               "CVC3::Expr::getExistential() not a skolem variable");
01126   return d_expr->getExistential();
01127 }
01128 inline int Expr::getBoundIndex() const {
01129   DebugAssert(isSkolem(),
01130               "CVC3::Expr::getBoundIndex() not a skolem variable");
01131   return d_expr->getBoundIndex();
01132 }
01133 
01134 
01135 inline const Rational& Expr::getRational() const {
01136   DebugAssert(isRational(),
01137         "CVC3::Expr::getRational(): not a rational Expr:\n  "
01138         + toString(AST_LANG));
01139    return d_expr->getRational();
01140 }
01141 
01142 inline const Theorem& Expr::getTheorem() const {
01143   DebugAssert(isTheorem(),
01144         "CVC3::Expr::getTheorem(): not a Theorem Expr:\n  "
01145         + toString(AST_LANG));
01146    return d_expr->getTheorem();
01147 }
01148 
01149 inline const std::string& Expr::getUid() const {
01150    DebugAssert(getKind() == BOUND_VAR,
01151         "CVC3::Expr::getUid(): not a BOUND_VAR Expr:\n  "
01152         + toString(AST_LANG));
01153    return d_expr->getUid();
01154 }
01155 
01156 inline ExprManager* Expr::getEM() const {
01157   DebugAssert(d_expr != NULL,
01158               "CVC3::Expr:getEM: on Null Expr (not initialized)");
01159   return d_expr->d_em;
01160 }
01161 
01162 inline const std::vector<Expr>& Expr::getKids() const {
01163   DebugAssert(d_expr != NULL, "Expr::getKids on Null Expr");
01164   if(isNull()) return getEM()->getEmptyVector();
01165   else return d_expr->getKids();
01166 }
01167 
01168 inline int Expr::getKind() const {
01169    if(d_expr == NULL) return NULL_KIND; // FIXME: invent a better Null kind
01170    return d_expr->d_kind;
01171  }
01172 
01173 inline ExprIndex Expr::getIndex() const { return d_expr->d_index; }
01174 
01175 inline bool Expr::hasLastIndex() const
01176 { return d_expr->d_em->lastIndex() == getIndex(); }
01177 
01178 inline Op Expr::mkOp() const {
01179   DebugAssert(!isNull(), "Expr::mkOp() on Null expr");
01180   return Op(*this);
01181 }
01182 
01183 inline Op Expr::getOp() const {
01184   DebugAssert(!isNull(), "Expr::getOp() on Null expr");
01185   if (isApply()) return d_expr->getOp();
01186   DebugAssert(arity() > 0,
01187               "Expr::getOp() called on non-apply expr with no children");
01188   return Op(getKind());
01189 }
01190 
01191 inline Expr Expr::getOpExpr() const {
01192   DebugAssert(isApply(), "getOpExpr() called on non-apply");
01193   return getOp().getExpr();
01194 }
01195 
01196 inline int Expr::getOpKind() const {
01197   if (!isApply()) return getKind();
01198   return getOp().getExpr().getKind();
01199 }
01200 
01201 inline int Expr::arity() const {
01202   if(isNull()) return 0;
01203   else return d_expr->arity();
01204 }
01205 
01206 inline const Expr& Expr::operator[](int i) const {
01207   DebugAssert(i < arity(), "out of bounds access");
01208   return (d_expr->getKids())[i];
01209 }
01210 
01211 inline Expr::iterator Expr::begin() const {
01212   if (isNull() || d_expr->arity() == 0)
01213     return Expr::iterator(getEM()->getEmptyVector().begin());
01214   else return Expr::iterator(d_expr->getKids().begin());
01215 }
01216 
01217 inline Expr::iterator Expr::end() const {
01218   if (isNull() || d_expr->arity() == 0)
01219     return Expr::iterator(getEM()->getEmptyVector().end());
01220   else return Expr::iterator(d_expr->getKids().end());
01221 }
01222 
01223 inline bool Expr::isNull() const {
01224   return (d_expr == NULL) || (d_expr->d_kind == NULL_KIND);
01225 }
01226 
01227 inline size_t Expr::getMMIndex() const {
01228   DebugAssert(!isNull(), "Expr::getMMIndex()");
01229   return d_expr->getMMIndex();
01230 }
01231 
01232 inline bool Expr::hasFind() const {
01233   DebugAssert(!isNull(), "hasFind called on NULL Expr");
01234   return (d_expr->d_find && !(d_expr->d_find->get().isNull()));
01235 }
01236 
01237 inline const Theorem& Expr::getFind() const {
01238   DebugAssert(hasFind(), "Should only be called if find is valid");
01239   return d_expr->d_find->get();
01240 }
01241 
01242 inline int  Expr::getFindLevel() const {
01243   DebugAssert(hasFind(), "Should only be called if find is valid");
01244   return d_expr->d_find->level();
01245 }
01246 
01247 inline const Theorem& Expr::getEqNext() const {
01248   DebugAssert(!isNull(), "getEqNext called on NULL Expr");
01249   DebugAssert(hasFind(), "Should only be called if find is valid");
01250   DebugAssert(d_expr->d_eqNext, "getEqNext: d_eqNext is NULL");
01251   return d_expr->d_eqNext->get();
01252 }
01253 
01254 inline NotifyList* Expr::getNotify() const {
01255   if(isNull()) return NULL;
01256   else return d_expr->d_notifyList;
01257 }
01258 
01259 inline Type Expr::getType() const {
01260   if (isNull()) return s_null;
01261   if (d_expr->d_type.isNull()) getEM()->computeType(*this);
01262   return d_expr->d_type;
01263 }
01264 
01265 inline Type Expr::lookupType() const {
01266   if (isNull()) return s_null;
01267   return d_expr->d_type;
01268 }
01269 
01270 inline Cardinality Expr::typeCard() const {
01271   DebugAssert(!isNull(), "typeCard called on NULL Expr");
01272   Expr e(*this);
01273   Unsigned n;
01274   return getEM()->finiteTypeInfo(e, n, false, false);
01275 }
01276 
01277 inline Expr Expr::typeEnumerateFinite(Unsigned n) const {
01278   DebugAssert(!isNull(), "typeEnumerateFinite called on NULL Expr");
01279   Expr e(*this);
01280   Cardinality card = getEM()->finiteTypeInfo(e, n, true, false);
01281   if (card != CARD_FINITE) e = Expr();
01282   return e;
01283 }
01284 
01285 inline Unsigned Expr::typeSizeFinite() const {
01286   DebugAssert(!isNull(), "typeCard called on NULL Expr");
01287   Expr e(*this);
01288   Unsigned n;
01289   Cardinality card = getEM()->finiteTypeInfo(e, n, false, true);
01290   if (card != CARD_FINITE) n = 0;
01291   return n;
01292 }
01293 
01294 inline bool Expr::validSimpCache() const {
01295   return d_expr->d_simpCacheTag == getEM()->getSimpCacheTag();
01296 }
01297 
01298 inline const Theorem& Expr::getSimpCache() const {
01299   return d_expr->d_simpCache;
01300 }
01301 
01302 inline bool Expr::isValidType() const {
01303   return d_expr->d_dynamicFlags.get(VALID_TYPE);
01304 }
01305 
01306 inline bool Expr::validIsAtomicFlag() const {
01307   return d_expr->d_dynamicFlags.get(VALID_IS_ATOMIC);
01308 }
01309 
01310 inline bool Expr::validTerminalsConstFlag() const {
01311   return d_expr->d_dynamicFlags.get(VALID_TERMINALS_CONST);
01312 }
01313 
01314 inline bool Expr::getIsAtomicFlag() const {
01315   return d_expr->d_dynamicFlags.get(IS_ATOMIC);
01316 }
01317 
01318 inline bool Expr::getTerminalsConstFlag() const {
01319   return d_expr->d_dynamicFlags.get(TERMINALS_CONST);
01320 }
01321 
01322 inline bool Expr::isRewriteNormal() const {
01323   return d_expr->d_dynamicFlags.get(REWRITE_NORMAL);
01324 }
01325 
01326 inline bool Expr::isFinite() const {
01327   return d_expr->d_dynamicFlags.get(IS_FINITE);
01328 }
01329 
01330 inline bool Expr::isWellFounded() const {
01331   return d_expr->d_dynamicFlags.get(WELL_FOUNDED);
01332 }
01333 
01334 inline bool Expr::computeTransClosure() const {
01335   return d_expr->d_dynamicFlags.get(COMPUTE_TRANS_CLOSURE);
01336 }
01337 
01338 inline bool Expr::containsBoundVar() const {
01339   return d_expr->d_dynamicFlags.get(CONTAINS_BOUND_VAR);
01340 }
01341 
01342 inline bool Expr::usesCC() const {
01343   return d_expr->d_dynamicFlags.get(USES_CC);
01344 }
01345 
01346 inline bool Expr::notArrayNormalized() const {
01347   return d_expr->d_dynamicFlags.get(NOT_ARRAY_NORMALIZED);
01348 }
01349 
01350 inline bool Expr::isImpliedLiteral() const {
01351   return d_expr->d_dynamicFlags.get(IMPLIED_LITERAL);
01352 }
01353 
01354 inline bool Expr::isUserAssumption() const {
01355   return d_expr->d_dynamicFlags.get(IS_USER_ASSUMPTION);
01356 }
01357 
01358 inline bool Expr::inUserAssumption() const {
01359   return d_expr->d_dynamicFlags.get(IN_USER_ASSUMPTION);
01360 }
01361 
01362 inline bool Expr::isIntAssumption() const {
01363   return d_expr->d_dynamicFlags.get(IS_INT_ASSUMPTION);
01364 }
01365 
01366 inline bool Expr::isJustified() const {
01367   return d_expr->d_dynamicFlags.get(IS_JUSTIFIED);
01368 }
01369 
01370 inline bool Expr::isTranslated() const {
01371   return d_expr->d_dynamicFlags.get(IS_TRANSLATED);
01372 }
01373 
01374 inline bool Expr::isUserRegisteredAtom() const {
01375   return d_expr->d_dynamicFlags.get(IS_USER_REGISTERED_ATOM);
01376 }
01377 
01378 inline bool Expr::isRegisteredAtom() const {
01379   return d_expr->d_dynamicFlags.get(IS_REGISTERED_ATOM);
01380 }
01381 
01382 inline bool Expr::isSelected() const {
01383   return d_expr->d_dynamicFlags.get(IS_SELECTED);
01384 }
01385 
01386 inline bool Expr::isStoredPredicate() const {
01387   return d_expr->d_dynamicFlags.get(IS_STORED_PREDICATE);
01388 }
01389 
01390 inline bool Expr::getFlag() const {
01391   DebugAssert(!isNull(), "Expr::getFlag() on Null Expr");
01392   return (d_expr->d_flag == getEM()->getFlag());
01393 }
01394 
01395 inline void Expr::setFlag() const {
01396   DebugAssert(!isNull(), "Expr::setFlag() on Null Expr");
01397   d_expr->d_flag = getEM()->getFlag();
01398 }
01399 
01400 inline void Expr::clearFlags() const {
01401   DebugAssert(!isNull(), "Expr::clearFlags() on Null Expr");
01402   getEM()->clearFlags();
01403 }
01404 
01405 inline void Expr::setFind(const Theorem& e) const {
01406   DebugAssert(!isNull(), "Expr::setFind() on Null expr");
01407   DebugAssert(e.getLHS() == *this, "bad call to setFind");
01408   if (d_expr->d_find) d_expr->d_find->set(e);
01409   else {
01410     CDO<Theorem>* tmp = new(true) CDO<Theorem>(getEM()->getCurrentContext(), e);
01411     d_expr->d_find = tmp;
01412     IF_DEBUG(tmp->setName("CDO[Expr.find]");)
01413   }
01414 }
01415 
01416 inline void Expr::setEqNext(const Theorem& e) const {
01417   DebugAssert(!isNull(), "Expr::setEqNext() on Null expr");
01418   DebugAssert(e.getLHS() == *this, "bad call to setEqNext");
01419   if (d_expr->d_eqNext) d_expr->d_eqNext->set(e);
01420   else {
01421     CDO<Theorem>* tmp = new(true) CDO<Theorem>(getEM()->getCurrentContext(), e);
01422     d_expr->d_eqNext = tmp;
01423     IF_DEBUG(tmp->setName("CDO[Expr.eqNext]");)
01424   }
01425 }
01426 
01427 inline void Expr::setType(const Type& t) const {
01428   DebugAssert(!isNull(), "Expr::setType() on Null expr");
01429   d_expr->d_type = t;
01430 }
01431 
01432 inline void Expr::setSimpCache(const Theorem& e) const {
01433   DebugAssert(!isNull(), "Expr::setSimpCache() on Null expr");
01434   d_expr->d_simpCache = e;
01435   d_expr->d_simpCacheTag = getEM()->getSimpCacheTag();
01436 }
01437 
01438 inline void Expr::setValidType() const {
01439   DebugAssert(!isNull(), "Expr::setValidType() on Null expr");
01440   d_expr->d_dynamicFlags.set(VALID_TYPE, 0);
01441 }
01442 
01443 inline void Expr::setIsAtomicFlag(bool value) const {
01444   DebugAssert(!isNull(), "Expr::setIsAtomicFlag() on Null expr");
01445   d_expr->d_dynamicFlags.set(VALID_IS_ATOMIC, 0);
01446   if (value) d_expr->d_dynamicFlags.set(IS_ATOMIC, 0);
01447   else d_expr->d_dynamicFlags.clear(IS_ATOMIC, 0);
01448 }
01449 
01450 inline void Expr::setTerminalsConstFlag(bool value) const {
01451   DebugAssert(!isNull(), "Expr::setTerminalsConstFlag() on Null expr");
01452   d_expr->d_dynamicFlags.set(VALID_TERMINALS_CONST, 0);
01453   if (value) d_expr->d_dynamicFlags.set(TERMINALS_CONST, 0);
01454   else d_expr->d_dynamicFlags.clear(TERMINALS_CONST, 0);
01455 }
01456 
01457 inline void Expr::setRewriteNormal() const {
01458   DebugAssert(!isNull(), "Expr::setRewriteNormal() on Null expr");
01459   TRACE("setRewriteNormal", "setRewriteNormal(", *this, ")");
01460   d_expr->d_dynamicFlags.set(REWRITE_NORMAL, 0);
01461 }
01462 
01463 inline void Expr::setFinite() const {
01464   DebugAssert(!isNull(), "Expr::setFinite() on Null expr");
01465   d_expr->d_dynamicFlags.set(IS_FINITE, 0);
01466 }
01467 
01468 inline void Expr::setWellFounded() const {
01469   DebugAssert(!isNull(), "Expr::setWellFounded() on Null expr");
01470   d_expr->d_dynamicFlags.set(WELL_FOUNDED, 0);
01471 }
01472 
01473 inline void Expr::setComputeTransClosure() const {
01474   DebugAssert(!isNull(), "Expr::setComputeTransClosure() on Null expr");
01475   d_expr->d_dynamicFlags.set(COMPUTE_TRANS_CLOSURE, 0);
01476 }
01477 
01478 inline void Expr::setContainsBoundVar() const {
01479   DebugAssert(!isNull(), "Expr::setContainsBoundVar() on Null expr");
01480   d_expr->d_dynamicFlags.set(CONTAINS_BOUND_VAR, 0);
01481 }
01482 
01483 inline void Expr::setUsesCC() const {
01484   DebugAssert(!isNull(), "Expr::setUsesCC() on Null expr");
01485   d_expr->d_dynamicFlags.set(USES_CC, 0);
01486 }
01487 
01488 inline void Expr::setNotArrayNormalized() const {
01489   DebugAssert(!isNull(), "Expr::setContainsBoundVar() on Null expr");
01490   d_expr->d_dynamicFlags.set(NOT_ARRAY_NORMALIZED);
01491 }
01492 
01493 inline void Expr::setImpliedLiteral() const {
01494   DebugAssert(!isNull(), "Expr::setImpliedLiteral() on Null expr");
01495   d_expr->d_dynamicFlags.set(IMPLIED_LITERAL);
01496 }
01497 
01498 inline void Expr::setUserAssumption(int scope) const {
01499   DebugAssert(!isNull(), "Expr::setUserAssumption() on Null expr");
01500   d_expr->d_dynamicFlags.set(IS_USER_ASSUMPTION, scope);
01501 }
01502 
01503 inline void Expr::setInUserAssumption(int scope) const {
01504   DebugAssert(!isNull(), "Expr::setInUserAssumption() on Null expr");
01505   d_expr->d_dynamicFlags.set(IN_USER_ASSUMPTION, scope);
01506 }
01507 
01508 inline void Expr::setIntAssumption() const {
01509   DebugAssert(!isNull(), "Expr::setIntAssumption() on Null expr");
01510   d_expr->d_dynamicFlags.set(IS_INT_ASSUMPTION);
01511 }
01512 
01513 inline void Expr::setJustified() const {
01514   DebugAssert(!isNull(), "Expr::setJustified() on Null expr");
01515   d_expr->d_dynamicFlags.set(IS_JUSTIFIED);
01516 }
01517 
01518 inline void Expr::setTranslated(int scope) const {
01519   DebugAssert(!isNull(), "Expr::setTranslated() on Null expr");
01520   d_expr->d_dynamicFlags.set(IS_TRANSLATED, scope);
01521 }
01522 
01523 inline void Expr::setUserRegisteredAtom() const {
01524   DebugAssert(!isNull(), "Expr::setUserRegisteredAtom() on Null expr");
01525   d_expr->d_dynamicFlags.set(IS_USER_REGISTERED_ATOM);
01526 }
01527 
01528 inline void Expr::setRegisteredAtom() const {
01529   DebugAssert(!isNull(), "Expr::setUserRegisteredAtom() on Null expr");
01530   d_expr->d_dynamicFlags.set(IS_REGISTERED_ATOM);
01531 }
01532 
01533 inline void Expr::setSelected() const {
01534   DebugAssert(!isNull(), "Expr::setSelected() on Null expr");
01535   d_expr->d_dynamicFlags.set(IS_SELECTED);
01536 }
01537 
01538 inline void Expr::setStoredPredicate() const {
01539   DebugAssert(!isNull(), "Expr::setStoredPredicate() on Null expr");
01540   d_expr->d_dynamicFlags.set(IS_STORED_PREDICATE);
01541 }
01542 
01543 inline void Expr::clearRewriteNormal() const {
01544   DebugAssert(!isNull(), "Expr::clearRewriteNormal() on Null expr");
01545   d_expr->d_dynamicFlags.clear(REWRITE_NORMAL, 0);
01546 }
01547 
01548 inline bool Expr::hasSig() const {
01549   return (!isNull()
01550           && d_expr->getSig() != NULL
01551           && !(d_expr->getSig()->get().isNull()));
01552 }
01553 
01554 inline bool Expr::hasRep() const {
01555   return (!isNull()
01556           && d_expr->getRep() != NULL
01557           && !(d_expr->getRep()->get().isNull()));
01558 }
01559 
01560 inline const Theorem& Expr::getSig() const {
01561   static Theorem nullThm;
01562   DebugAssert(!isNull(), "Expr::getSig() on Null expr");
01563   if(d_expr->getSig() != NULL)
01564     return d_expr->getSig()->get();
01565   else
01566     return nullThm;
01567 }
01568 
01569 inline const Theorem& Expr::getRep() const {
01570   static Theorem nullThm;
01571   DebugAssert(!isNull(), "Expr::getRep() on Null expr");
01572   if(d_expr->getRep() != NULL)
01573     return d_expr->getRep()->get();
01574   else
01575     return nullThm;
01576 }
01577 
01578 inline void Expr::setSig(const Theorem& e) const {
01579   DebugAssert(!isNull(), "Expr::setSig() on Null expr");
01580   CDO<Theorem>* sig = d_expr->getSig();
01581   if(sig != NULL) sig->set(e);
01582   else {
01583     CDO<Theorem>* tmp = new(true) CDO<Theorem>(getEM()->getCurrentContext(), e);
01584     d_expr->setSig(tmp);
01585     IF_DEBUG(tmp->setName("CDO[Expr.sig] in "+toString());)
01586   }
01587 }
01588 
01589 inline void Expr::setRep(const Theorem& e) const {
01590   DebugAssert(!isNull(), "Expr::setRep() on Null expr");
01591   CDO<Theorem>* rep = d_expr->getRep();
01592   if(rep != NULL) rep->set(e);
01593   else {
01594     CDO<Theorem>* tmp = new(true) CDO<Theorem>(getEM()->getCurrentContext(), e);
01595     d_expr->setRep(tmp);
01596     IF_DEBUG(tmp->setName("CDO[Expr.rep] in "+toString());)
01597   }
01598 }
01599 
01600 inline bool operator==(const Expr& e1, const Expr& e2) {
01601   // Comparing pointers (equal expressions are always shared)
01602   return e1.d_expr == e2.d_expr;
01603 }
01604 
01605 inline bool operator!=(const Expr& e1, const Expr& e2)
01606   { return !(e1 == e2); }
01607 
01608 // compare() is defined in expr.cpp
01609 
01610 inline bool operator<(const Expr& e1, const Expr& e2)
01611   { return compare(e1,e2) < 0; }
01612 inline bool operator<=(const Expr& e1, const Expr& e2)
01613   { return compare(e1,e2) <= 0; }
01614 inline bool operator>(const Expr& e1, const Expr& e2)
01615   { return compare(e1,e2) > 0; }
01616 inline bool operator>=(const Expr& e1, const Expr& e2)
01617   { return compare(e1,e2) >= 0; }
01618 
01619 } // end of namespace CVC3
01620 
01621 #endif