expr.h

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file expr.h
 * \brief Definition of the API to expression package.  See class Expr for details.
 * 
 * Author: Clark Barrett
 * 
 * Created: Tue Nov 26 00:27:40 2002
 *
 * <hr>
 * Copyright (C) 2003 by the Board of Trustees of Leland Stanford
 * Junior University and by New York University. 
 *
 * License to use, copy, modify, sell and/or distribute this software
 * and its documentation for any purpose is hereby granted without
 * royalty, subject to the terms and conditions defined in the \ref
 * LICENSE file provided with this distribution.  In particular:
 *
 * - The above copyright notice and this permission notice must appear
 * in all copies of the software and related documentation.
 *
 * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES,
 * EXPRESSED OR IMPLIED.  USE IT AT YOUR OWN RISK.
 * 
 * <hr>
 * 
 */
/*****************************************************************************/

#ifndef _CVC_lite__expr_h_
#define _CVC_lite__expr_h_

#include <iostream>
#include <functional>
#include <iterator>

#include "debug.h"
#include "rational.h"
#include "kinds.h"
#include "cdo.h"
#include "lang.h"

class CInterface;

namespace CVCL {

  class NotifyList;
  class Theory;
  class Op;
  class Type;
  class Theorem;

  template<class Data>
  class ExprHashMap;

  class ExprManager;
  // Internal data-holding classes
  class ExprValue;
  class ExprNode;
  // Printing
  class ExprStream;

  //! Type ID of each ExprValue subclass.
  /*! It is defined in expr.h, so that ExprManager can use it before loading
    expr_value.h */
  typedef enum {
    EXPR_VALUE,
    EXPR_NODE,
    EXPR_STRING,
    EXPR_RATIONAL,
    EXPR_SKOLEM,
    EXPR_UCONST,
    EXPR_BOUND_VAR,
    EXPR_CC, //!< Expression with sig and rep attributes for congruence closure
    EXPR_APPLY, //!< Application of functions and predicates
    EXPR_CLOSURE,
    EXPR_NAMED,
    EXPR_BOOL_VAR,
//     EXPR_READ,
//     EXPR_RECORD, //!< for record literals
//     EXPR_FIELD, //!< for a record field access (select, update)
//     EXPR_TUPLE_INDEX, //!< for a tuple element access (select, update)
    EXPR_VALUE_TYPE_LAST // The end of list; don't assign it to any subclass
  } ExprValueType;

  //! Expression index type
  typedef long long unsigned ExprIndex;

  /**************************************************************************/
  /*! \defgroup ExprPkg Expression Package
   * \ingroup BuildingBlocks
   */
  /**************************************************************************/
  /*! \defgroup Expr_SmartPointer Smart Pointer Functionality in Expr
   * \ingroup ExprPkg
   */
  /**************************************************************************/

  /**************************************************************************/
  //! Data structure of expressions in CVC Lite
  /*! \ingroup ExprPkg
   * Class: Expr <br>
   * Author: Clark Barrett <br>
   * 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 <em>smart
   * pointer</em> 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).
   */
  /**************************************************************************/
class Expr {
  friend class ExprHasher;
  friend class ExprManager;
  friend class Op;
  friend class ExprValue;
  friend class ExprNode;
  friend class CInterface;

  /*! \addtogroup ExprPkg
   * @{
   */
  //! bit-masks for static flags
  typedef enum {
    //! Whether IS_ATOMIC flag is valid (initialized)
    VALID_IS_ATOMIC = 0x1,
    //! Whether the expression is an atomic term or formula
    IS_ATOMIC = 0x2,
    //! Expression is the result of a "normal" (idempotent) rewrite
    REWRITE_NORMAL = 0x4
  } StaticFlagsEnum;

  /////////////////////////////////////////////////////////////////////////////
  // Private Dynamic Data                                                    //
  /////////////////////////////////////////////////////////////////////////////
  //! The value.  This is the only data member in this class.
  ExprValue* d_expr;

  /////////////////////////////////////////////////////////////////////////////
  // Private methods                                                         //
  /////////////////////////////////////////////////////////////////////////////

  //! Private constructor, simply wraps around the pointer
  /*! It includes an extra dummy argument to distinguish it from a
   * public constructor uniquifies the pointer.
   */
  Expr(ExprValue* expr, int i);
  
public:
  /////////////////////////////////////////////////////////////////////////////
  // Public Classes and Types                                                //
  /////////////////////////////////////////////////////////////////////////////

  /////////////////////////////////////////////////////////////////////////////
  /*!
   * Class: Expr::iterator
   * Author: Sergey Berezin
   * Created: Fri Dec  6 15:38:51 2002
   * Description: STL-like iterator API to the Expr's children.
   * IMPORTANT: the iterator will not be valid after the originating 
   * expression is destroyed.
  */
  /////////////////////////////////////////////////////////////////////////////
  class iterator
    : public std::iterator<std::input_iterator_tag,Expr,ptrdiff_t>
  {
    friend class Expr;
  private:
    std::vector<Expr>::const_iterator d_it;
    // Private constructors (used by Expr only)
    //
    //! Construct an iterator out of the vector's iterator
    iterator(std::vector<Expr>::const_iterator it): d_it(it) { }
    // Public methods
  public:
    //! Default constructor
    iterator() { }
    // Copy constructor and operator= are defined by C++, that's good enough

    //! Equality
    bool operator==(const iterator& i) const {
      return d_it == i.d_it;
    }
    //! Disequality
    bool operator!=(const iterator& i) const { return !(*this == i); }
    //! Dereference operator
    const Expr& operator*() const;
    //! Dereference and member access
    const Expr* operator->() const;
    //! Prefix increment
    iterator& operator++() {
      d_it++;
      return *this;
    }
    /*! @brief Postfix increment requires a Proxy object to hold the
     * intermediate value for dereferencing */
    class Proxy {
      const Expr* d_e;
    public:
      Proxy(const Expr& e) : d_e(&e) { }
      Expr operator*() { return *d_e; }
    };
    //! Postfix increment
    /*! \return Proxy with the old Expr.
     *
     * Now, an expression like *i++ will return the current *i, and
     * then advance the iterator.  However, don't try to use Proxy for
     * anything else. 
     */
    Proxy operator++(int) {
      Proxy e(*(*this));
      ++(*this);
      return e;
    }
  }; // end of class Expr::iterator

  /////////////////////////////////////////////////////////////////////////////
  // Constructors                                                            //
  /////////////////////////////////////////////////////////////////////////////

  //! Default constructor creates the Null Expr
  Expr(): d_expr(NULL) {}

  //! Constructor from generic ExprValue subclasses.
  Expr(ExprValue* expr);
  /*! @brief Copy constructor and assignment (copy the pointer and take care
    of the refcount) */
  Expr(const Expr& e);
  //! Assignment operator: take care of the refcounting and GC
  Expr& operator=(const Expr& e);

  // Create a new Expr with given ExprManager, operator and children.
  // If the children belong to another ExprManager, convert them to
  // use the given one.
  Expr(ExprManager *em, const Op& op);
  Expr(ExprManager *em, const Op& op, const Expr& child);
  Expr(ExprManager *em, const Op& op, const Expr& child0, const Expr& child1);
  Expr(ExprManager *em, const Op& op, const Expr& child0, const Expr& child1, const Expr& child2);
  Expr(ExprManager *em, const Op& op, const std::vector<Expr>& children);

  // Similar constructors, but from kinds rather than from an Op
  Expr(ExprManager *em, int kind);
  Expr(ExprManager *em, int kind, const Expr& child);
  Expr(ExprManager *em, int kind, const Expr& child0, const Expr& child1);
  Expr(ExprManager *em, int kind, const Expr& child0, const Expr& child1,
       const Expr& child2);
  Expr(ExprManager *em, int kind, const std::vector<Expr>& children);
  //! Closure Expr (quantifier, lambda, etc.)
//   Expr(ExprManager *em, int kind, const std::vector<Expr>& vars,
//        const Expr& body);
  /*
  //! Record literal
  Expr(ExprManager *em, int kind,
       const std::vector<std::string>& fields,
       const std::vector<Expr>& children);
  //! Record access (REC_SELECT, REC_UPDATE)
  Expr(ExprManager *em, int kind, const std::string& field,
       const std::vector<Expr>& children);
  //! Tuple access (TUPLE_SELECT, TUPLE_UPDATE)
  Expr(ExprManager *em, int kind, int index,
       const std::vector<Expr>& children);
  */
  // These constructors grab the ExprManager from the Op or the first
  // child.  The operator and all children must belong to the same
  // ExprManager.
  Expr(const Op& op);
  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 std::vector<Expr>& children);

  // Leaf expression constructors
//   Expr(ExprManager *em, int kind, const std::string &s);

//   Expr(ExprManager *em, const Rational &r);
  //! Constructor for BOUND_VAR
//   Expr(ExprManager *em, const std::string& name, const std::string& uid);

  // Compound expression constructors
  Expr eqExpr(const Expr& right) const;
  Expr notExpr() const;
  Expr negate() const; // avoid double-negatives
  Expr andExpr(const Expr& right) const;
  friend Expr andExpr(const std::vector <Expr>& children);
  Expr orExpr(const Expr& right) const;
  friend Expr orExpr(const std::vector <Expr>& children);
  Expr iteExpr(const Expr& thenpart, const Expr& elsepart) const;
  Expr iffExpr(const Expr& right) const;
  Expr impExpr(const Expr& right) const;
  //! Create a Skolem constant for the i'th variable of an existential (*this)
  Expr skolemExpr(int i) const;
  //! Create a Boolean variable out of the expression
  Expr boolVarExpr() const;
  //! Rebuild Expr with a new ExprManager
  Expr rebuild(ExprManager* em) const;
//    Expr newForall(const Expr& e);
//    Expr newExists(const Expr& e);

  Expr operator!() const { return notExpr(); }
  Expr operator&&(const Expr& right) const { return andExpr(right); }
  Expr operator||(const Expr& right) const { return orExpr(right); }

  //! Destructor
  ~Expr();

  /////////////////////////////////////////////////////////////////////////////
  // Public Static Methods                                                   //
  /////////////////////////////////////////////////////////////////////////////

  static size_t hash(const Expr& e);

  // Creating new Expr's.  These methods are basically the same as
  // constructors, but return value and can be nested.
  friend Expr newExpr(ExprValue* ev);
  friend Expr newExpr(ExprManager *em, const Expr& e); // Rebuild with new em
  friend Expr newExpr(ExprManager *em, const Op& op);
  friend Expr newExpr(ExprManager *em, const Op& op, const Expr& child);
  friend Expr newExpr(ExprManager *em, const Op& op, const Expr& child0,
                      const Expr& child1);
  friend Expr newExpr(ExprManager *em, const Op& op, const Expr& child0,
                      const Expr& child1, const Expr& child2);
  friend Expr newExpr(ExprManager *em, const Op& op,
                      const std::vector<Expr>& children);

  friend Expr newExpr(ExprManager *em, int kind);
  friend Expr newExpr(ExprManager *em, int kind, const Expr& child);
  friend Expr newExpr(ExprManager *em, int kind, const Expr& child0,
                      const Expr& child1);
  friend Expr newExpr(ExprManager *em, int kind, const Expr& child0,
                      const Expr& child1, const Expr& child2);
  friend Expr newExpr(ExprManager *em, int kind,
                      const std::vector<Expr>& children);
  //! Closure Expr
  friend Expr newClosureExpr(ExprManager *em, int kind,
                             const std::vector<Expr>& vars, const Expr& body);
  //! Closure Expr
  friend Expr newClosureExpr(int kind, const std::vector<Expr>& vars,
                             const Expr& body);
  //! Boolean variable expr
  friend Expr newBoolVarExpr(const Expr& e);
  //! Application of uninterpreted function
  friend Expr newApplyExpr(ExprManager* em, const Expr& func,
                           const std::vector<Expr>& args);
  friend Expr newApplyExpr(const Expr& func, const std::vector<Expr>& args)
  { return newApplyExpr(func.getEM(), func, args); }
  friend Expr newApplyExpr(const Expr& func, const Expr& arg) {
    std::vector<Expr> args;
    args.push_back(arg);
    return newApplyExpr(func.getEM(), func, args);
  }
  friend Expr newApplyExpr(const Expr& func, const Expr& a1, const Expr& a2) {
    std::vector<Expr> args;
    args.push_back(a1);
    args.push_back(a2);
    return newApplyExpr(func.getEM(), func, args);
  }
  friend Expr newApplyExpr(const Expr& func, const Expr& a1, const Expr& a2,
                           const Expr& a3) {
    std::vector<Expr> args;
    args.push_back(a1);
    args.push_back(a2);
    args.push_back(a3);
    return newApplyExpr(func.getEM(), func, args);
  }
  //! Named expressions without kids
  friend Expr newNamedExpr(ExprManager* em, int kind, const std::string& name);
  //! Named expressions with kids
  friend Expr newNamedExpr(ExprManager* em, int kind, const std::string& name,
                           const std::vector<Expr>& kids);
  friend Expr newNamedExpr(int kind, const std::string& name,
                           const std::vector<Expr>& kids);
  friend Expr newNamedExpr(int kind, const std::string& name,
                           const Expr& child) {
    std::vector<Expr> kids;
    kids.push_back(child);
    return newNamedExpr(kind, name, kids);
  }
  friend Expr newNamedExpr(int kind, const std::string& name,
                           const Expr& child1, const Expr& child2) {
    std::vector<Expr> kids;
    kids.push_back(child1);
    kids.push_back(child2);
    return newNamedExpr(kind, name, kids);
  }
  friend Expr newNamedExpr(int kind, const std::string& name,
                           const Expr& child1, const Expr& child2,
                           const Expr& child3) {
    std::vector<Expr> kids;
    kids.push_back(child1);
    kids.push_back(child2);
    kids.push_back(child3);
    return newNamedExpr(kind, name, kids);
  }
  // ExprManager is taken from the op or the children
  friend Expr newExpr(const Op& op);
  friend Expr newExpr(const Op& op, const Expr& child);
  friend Expr newExpr(const Op& op, const Expr& child0, const Expr& child1);
  friend Expr newExpr(const Op& op, const Expr& child0, const Expr& child1,
                      const Expr& child2);
  friend Expr newExpr(const Op& op, const std::vector<Expr>& children);

  // Leaf nodes
  friend Expr newStringExpr(ExprManager *em, const std::string &s);
  friend Expr newVarExpr(ExprManager *em, const std::string &s);
  friend Expr newBoundVarExpr(ExprManager *em, const std::string &name, 
                              const std::string& uid);
  friend Expr newRatExpr(ExprManager *em, const Rational &r);
  //skolem constant
  friend Expr newSkolemExpr(const Expr& e, int index);
  friend const Expr& falseExpr(ExprManager *em);
  friend const Expr& trueExpr(ExprManager *em);
  
  friend Expr substExpr(const Expr& e,
                        const std::vector<Expr>& oldTerms,
                        const std::vector<Expr>& newTerms); 
  friend Expr substExpr(const Expr& e, const ExprHashMap<Expr>& oldToNew);

  /////////////////////////////////////////////////////////////////////////////
  // Read-only (const) methods                                               //
  /////////////////////////////////////////////////////////////////////////////

  size_t hash() const;

  // Core expression testers

  bool isFalse() const { return getKind() == FALSE; }
  bool isTrue() const { return getKind() == TRUE; }
  bool isBoolConst() const { return isFalse() || isTrue(); }
  bool isVar() const;
  bool isBoolVar() const;
  bool isString() const;
  bool isClosure() const;
  bool isQuantifier() const;
  bool isLambda() const;
  //! Expr is an application of a LAMBDA-term to arguments
  bool isApply() const;
  //! Expr represents a type
  bool isType() const;
  /*
  bool isRecord() const;
  bool isRecordAccess() const;
  bool isTupleAccess() const;
  */
  size_t isGeneric() const;
  bool isGeneric(size_t idx) const;

  bool isEq() const { return getKind() == EQ; }
  bool isNot() const { return getKind() == NOT; }
  bool isAnd() const { return getKind() == AND; }
  bool isOr() const { return getKind() == OR; }
  bool isITE() const { return getKind() == ITE; }
  bool isIff() const { return getKind() == IFF; }
  bool isImpl() const { return getKind() == IMPLIES; }
  bool isXor() const { return getKind() == XOR;}

  bool isForall() const { return getKind() == FORALL; }
  bool isExists() const { return getKind() == EXISTS; }

  // Arith testers
  bool isRational() const { return getKind() == RATIONAL_EXPR; }
  bool isSkolem() const { return getKind() == SKOLEM_VAR;}
  // Leaf accessors - these functions must only be called one expressions of
  // the appropriate kind.

  // For UCONST and BOUND_VAR Expr's
  const std::string& getName() const;
  //! For BOUND_VAR, get the UID
  const std::string& getUid() const;

  // For STRING_EXPR's
  const std::string& getString() const; 
  //! Get bound variables from a closure Expr
  const std::vector<Expr>& getVars() const;
  //! Get the operator from Boolean variable
  const Expr& getVar() const;
  //! Get the operator from function application
  const Expr& getFun() const;
  //! Get the existential axiom expression for skolem constant
  const Expr& getExistential() const;
  //! Get the index of the bound var that skolem constant comes from
  int getBoundIndex() const;
 
  //! Get the body of the closure Expr
  const Expr& getBody() const;
  //! Get the body of the quantifier Expr (for backward compatibility)
  const Expr& getQuantBody() const { return getBody(); }
  //! Get the list of fields from record literal
//   const std::vector<std::string>& getRecordFields() const;
//   //! Get the field from a record access Expr
//   const std::string& getRecordField() const;
//   //! Get the index from a tuple access Expr
//   int getTupleIndex() const;
//   //! Get the index of the fieldName in the vector of strings, -1 if not found.
//   int getFieldIndex(const std::string & fieldName) const;
  //! Get the Rational value out of RATIONAL_EXPR
  const Rational& getRational() const; 

  /*! \name Generic Values
   * Methods for accessing an immutable reference to generic values in
   * DP-local subclasses and their sizes.  Unlike attributes, these
   * are considered as parts of the expression value.
   * @{
   */
  int getIntValue(int idx) const;
  const std::string& getStringValue(int idx) const;
  const Rational& getRatValue(int idx) const;
  const Expr& getExprValue(int idx) const;
  const Theorem& getTheoremValue(int idx) const;
  const CDO<int>& getCDIntValue(int idx) const;
  const CDO<Expr>& getCDExprValue(int idx) const;
  const CDO<Theorem>& getCDTheoremValue(int idx) const;
  //! Values of all other types (don't use it unless absolutely needed)
  const void* getOtherValue(int idx) const;

  size_t getIntValueSize() const;
  size_t getStringValueSize() const;
  size_t getRatValueSize() const;
  size_t getExprValueSize() const;
  size_t getTheoremValueSize() const;
  size_t getCDIntValueSize() const;
  size_t getCDExprValueSize() const;
  size_t getCDTheoremValueSize() const;
  size_t getOtherValueSize() const;
  /*!@}*/
  
  /*! \name Generic attributes 
   * Methods for accessing an assignable reference to generic
   * attributes in DP-local subclasses and their sizes
   * @{
   */
  int& getIntAttr(int idx) const;
  Expr& getExprAttr(int idx) const;
  Theorem& getTheoremAttr(int idx) const;
  CDO<int>& getCDIntAttr(int idx) const;
  CDO<Expr>& getCDExprAttr(int idx) const;
  CDO<Theorem>& getCDTheoremAttr(int idx) const;
  //! Attributes of all other types (don't use it unless absolutely needed)
  void* getOtherAttr(int idx) const;

  size_t getIntAttrSize() const;
  size_t getExprAttrSize() const;
  size_t getTheoremAttrSize() const;
  size_t getCDIntAttrSize() const;
  size_t getCDExprAttrSize() const;
  size_t getCDTheoremAttrSize() const;
  size_t getOtherAttrSize() const;
  /*!@}*/
  
  // Get the expression manager.  The expression must be non-null.
  ExprManager *getEM() const;

  // Return a ref to the vector of children.
  const std::vector<Expr>& getKids() const;

  // Get the kind of this expr.
  int getKind() const;

  // Get the index field
  ExprIndex getIndex() const;

  // True if this is the most recently created expression
  bool hasLastIndex() const;

  // Return the number of children.  Note, that an application of a
  // user-defined function has the arity of that function (the number
  // of arguments), and the function name itself is part of the
  // operator.
  int arity() const;

  // Return the ith child.  As with arity, it's also the ith argument
  // in function application.
  const Expr& operator[](int i) const;

  //! Begin iterator
  iterator begin() const;
  //! End iterator
  iterator end() const;

  // Check if Expr is Null
  bool isNull() const;

  // Check if Expr is not Null
  bool isInitialized() const { return d_expr != NULL; }
  //! Get the memory manager index (it uniquely identifies the subclass)
  size_t getMMIndex() const;

  // Attributes

  // True if the find attribute has been set to something other than NULL.
  bool hasFind() const;

  // Return the attached find attribute for the expr.  Note that this
  // must be called repeatedly to get the root of the union-find tree.
  // It may also return a Null theorem if the attribute is not set.
  // Return by value, since a reference to the attribute may become
  // invalid at any point.
  Theorem getFind() const;

  // Return the notify list
  NotifyList* getNotify() const;

  //! Get the cached type.
  /*! Note that this does not compute the type.  For that, use
      Theory::getType() */
  const Type& lookupType() const;
  //! Look up the cached TCC (may return Null)
  const Expr& lookupTCC() const;
  //! Look up the cached subtyping predicate (may return Null)
  const Theorem& lookupSubtypePred() const;

  /*! @brief Return true if there is a valid cached value for calling
      simplify on this Expr. */
  bool validSimpCache() const;

  // Get the cached Simplify of this Expr.
  const Theorem& getSimpCache() const;

  // True if there is a pointer to the in-place simplification of current Expr
  //  bool hasSimpInPlace() const;

  // Return attached in-place simplification of current Expr
  //  Theorem getSimpInPlace() const;

  // Return true if there is a valid flag for whether Expr is atomic
  bool validIsAtomicFlag() const;

  // Get the isAtomic flag
  bool getIsAtomicFlag() const;

  // Get the RewriteNormal flag
  bool isRewriteNormal() const;

  //! Check if the generic flag is set
  bool getFlag() const;
  //! Set the generic flag
  void setFlag() const;
  //! Clear the generic flag in all Exprs
  void clearFlags() const;

  // Printing functions

  //! Print the expression to a string
  std::string toString() const;
  //! Print the expression to a string using the given output language
  std::string toString(InputLanguage lang) const;
  //! Print the expression in the specified format
  void print(InputLanguage lang) const;
  //! Print the expression as AST (lisp-like format)
  void print() const { print(AST_LANG); }
  /*! @brief Print only the top node of the expression as AST, and
    submit children to the ExprStream for pretty-printing */
  ExprStream& print(ExprStream& os) const;
  //! Set initial indentation to n.
  /*! The indentation will be reset to default unless the second
    argument is true.
    \return reference to itself, so one can write `os << e.indent(5)'
  */
  Expr& indent(int n, bool permanent = false);

  /////////////////////////////////////////////////////////////////////////////
  // Other Public methods                                                    //
  /////////////////////////////////////////////////////////////////////////////

  // Attributes

  //! Set the find attribute to e
  void setFind(const Theorem& e) const;

  // Set the simpInPlace attribute to e
  //  void setSimpInPlace(const Theorem& e) const;

  //! Add (e,i) to the notify list of this expression
  void addToNotify(Theory* i, const Expr& e) const;
  //! Remove (e,i) from the notify list of this expression
  void removeFromNotify(Theory* i, const Expr& e) const;

  //! Set the cached type
  void setType(const Type& t) const;
  //! Set the cached TCC
  void setTCC(const Expr& tcc) const;
  //! Set the cached subtyping predicate
  void setSubtypePred(const Theorem& pred) const;

  // Cache the result of a call to Simplify on this Expr
  void setSimpCache(const Theorem& e) const;

  // Set the isAtomicFlag for this Expr
  void setIsAtomicFlag(bool value) const;

  // Set or clear the RewriteNormal flag
  void setRewriteNormal() const;
  void clearRewriteNormal() const;

  //! Check if the current Expr (*this) is a subexpression of e
  bool subExprOf(const Expr& e) const;
  // Returns the maximum number of Boolean expressions on a path from
  // this to a leaf, including this.
  inline int getHeight() const;

  // Returns the index of the highest kid.
  inline int getHighestKid() const;

  // Gets/sets an expression that this expression was simplified from
  // (see newRWTheorem). This is the equivalent of SVC's Sigx.
  inline bool hasSimpFrom() const;
  inline const Expr& getSimpFrom() const;
  inline void setSimpFrom(const Expr& simpFrom);

  // Attributes for uninterpreted function symbols.  It is an error to
  // use these attributes with anything else but UFUNC.
  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;


  


  /////////////////////////////////////////////////////////////////////////////
  // Friend methods                                                          //
  /////////////////////////////////////////////////////////////////////////////

  friend std::ostream& operator<<(std::ostream& os, const Expr& e);

  // The master method which defines some fixed total ordering on all
  // Exprs.  If e1 < e2, e1==e2, and e1 > e2, it returns -1, 0, 1
  // respectively.  A Null expr is always "smaller" than any other
  // expr, but is equal to itself.
  friend int compare(const Expr& e1, const Expr& e2);

  friend bool operator==(const Expr& e1, const Expr& e2);
  friend bool operator!=(const Expr& e1, const Expr& e2);

  friend bool operator<(const Expr& e1, const Expr& e2);
  friend bool operator<=(const Expr& e1, const Expr& e2);
  friend bool operator>(const Expr& e1, const Expr& e2);
  friend bool operator>=(const Expr& e1, const Expr& e2);

  /*!@}*/ // end of group Expr

}; // end of class Expr

//! Printing NotifyList class
std::ostream& operator<<(std::ostream& os, const NotifyList& l); 

} // end of namespace CVCL

// Include expr_value.h here.  We cannot include it earlier, since it
// needs the definition of class Expr.  See comments in expr_value.h.
#ifndef DOXYGEN
#include "expr_op.h"
#include "expr_manager.h"
#include "expr_value.h"
#endif
namespace CVCL {

 // Private constructor for use in ExprManager
 inline Expr::Expr(ExprValue* expr, int i): d_expr(expr) {
   d_expr->incRefcount();
 }
 
 inline Expr::Expr(ExprValue* expr) {
   DebugAssert(expr != NULL, "Expr::Expr(ExprValue* NULL, int)");
   d_expr = expr->d_em->newExprValue(expr);
   d_expr->incRefcount();
 }
 
 // Copy constructor and assignment (copy the pointer and take care
 // of the refcount)
 inline Expr::Expr(const Expr& e) : d_expr(e.d_expr) {
   if(d_expr != NULL)
     d_expr->incRefcount();
 }
 
 inline Expr& Expr::operator=(const Expr& e) {
   if(&e == this) return *this; // Self-assignment
   if(d_expr != NULL) {
     d_expr->decRefcount();
   }
   d_expr = e.d_expr;
   if(d_expr != NULL)
     d_expr->incRefcount();
   return *this;
 }
 
  // Similar constructors, but from kinds rather than from an Op
 inline Expr::Expr(ExprManager *em, int kind) {
   ExprValue ev(em, kind);
   d_expr = em->newExprValue(&ev);
   d_expr->incRefcount();
 }

 inline Expr::Expr(ExprManager *em, int kind, const Expr& child) {
   std::vector<Expr> kids;
   kids.push_back(child);
   ExprNode ev(em, kind, kids);
   d_expr = em->newExprValue(&ev);
   d_expr->incRefcount();
 }

 inline Expr::Expr(ExprManager *em, int kind, const Expr& child0,
                   const Expr& child1) {
   std::vector<Expr> kids;
   kids.push_back(child0);
   kids.push_back(child1);
   ExprNode ev(em, kind, kids);
   d_expr = em->newExprValue(&ev);
   d_expr->incRefcount();
 }

 inline Expr::Expr(ExprManager *em, int kind, const Expr& child0,
                   const Expr& child1, const Expr& child2) {
   std::vector<Expr> kids;
   kids.push_back(child0);
   kids.push_back(child1);
   kids.push_back(child2);
   ExprNode ev(em, kind, kids);
   d_expr = em->newExprValue(&ev);
   d_expr->incRefcount();
 }

 inline Expr::Expr(ExprManager *em, int kind,
                   const std::vector<Expr>& children) {
   ExprNode ev(em, kind, children);
   d_expr = em->newExprValue(&ev);
   d_expr->incRefcount();
 }


 inline Expr Expr::eqExpr(const Expr& right) const {
   return Expr(getEM(), EQ, *this, right);
 }

 inline Expr Expr::notExpr() const {
   return Expr(getEM(), NOT, *this);
 }

 inline Expr Expr::negate() const {
   return isNot() ? (*this)[0] : this->notExpr();
 }

 inline Expr Expr::andExpr(const Expr& right) const {
   return Expr(getEM(), AND, *this, right);
 }

 inline Expr andExpr(const std::vector <Expr>& children) {
   DebugAssert(children.size()>0 && !children[0].isNull(),
               "Expr::andExpr(kids)");
   return Expr(children[0].getEM(), AND, children);
 }

 inline Expr Expr::orExpr(const Expr& right) const {
   return Expr(getEM(), OR, *this, right);
 }

 inline Expr orExpr(const std::vector <Expr>& children) {
   DebugAssert(children.size()>0 && !children[0].isNull(),
               "Expr::andExpr(kids)");
   return Expr(children[0].getEM(), OR, children);
 }

 inline Expr Expr::iteExpr(const Expr& thenpart, const Expr& elsepart) const {
   return Expr(getEM(), ITE, *this, thenpart, elsepart);
 }

 inline Expr Expr::iffExpr(const Expr& right) const {
   return Expr(getEM(), IFF, *this, right);
 }

 inline Expr Expr::impExpr(const Expr& right) const {
   return Expr(getEM(), IMPLIES, *this, right);
 }

 inline Expr Expr::skolemExpr(int i) const {
   ExprSkolem ev(getEM(), i, *this);
   return newExpr(&ev);
 }

 inline Expr Expr::boolVarExpr() const {
   BoolVarExprValue ev(getEM(), *this);
   return newExpr(&ev);
 }

 inline Expr Expr::rebuild(ExprManager* em) const {
   return em->rebuild(*this);
 }

 inline Expr::~Expr() {
   if(d_expr != NULL && !getEM()->d_disableGC) {
     d_expr->decRefcount();
   }
 }

 inline size_t Expr::hash(const Expr& e) { return e.getEM()->hash(e); }

 // Creating new Expr's.  These methods are basically the same as
 // constructors, but return value and can be nested.
 inline Expr newExpr(ExprValue* ev) {
   return Expr(ev);
 }

 inline Expr newExpr(ExprManager *em, const Expr& e) {
   return e.rebuild(em);
 }

 inline Expr newExpr(ExprManager *em, const Op& op) {
   return Expr(em, op);
 }
 inline Expr newExpr(ExprManager *em, const Op& op, const Expr& child) {
   return Expr(em, op, child);
 }
 inline Expr newExpr(ExprManager *em, const Op& op, const Expr& child0,
                     const Expr& child1) {
   return Expr(em, op, child0, child1);
 }
 inline Expr newExpr(ExprManager *em, const Op& op, const Expr& child0,
                     const Expr& child1, const Expr& child2) {
   return Expr(em, op, child0, child1, child2);
 }
 inline Expr newExpr(ExprManager *em, const Op& op,
                     const std::vector<Expr>& children) {
   return Expr(em, op, children);
 }

 inline Expr newExpr(ExprManager *em, int kind) {
   return Expr(em, kind);
 }
 inline Expr newExpr(ExprManager *em, int kind, const Expr& child) {
   return Expr(em, kind, child);
 }
 inline Expr newExpr(ExprManager *em, int kind, const Expr& child0,
                     const Expr& child1) {
   return Expr(em, kind, child0, child1);
 }
 inline Expr newExpr(ExprManager *em, int kind, const Expr& child0,
                     const Expr& child1, const Expr& child2) {
   return Expr(em, kind, child0, child1, child2);
 }
 inline Expr newExpr(ExprManager *em, int kind,
                     const std::vector<Expr>& children) {
   return Expr(em, kind, children);
 }

 inline Expr newClosureExpr(ExprManager *em, int kind,
                            const std::vector<Expr>& vars, const Expr& body) {
   ExprClosure ev(em, kind, vars, body);
   return newExpr(&ev);
 }

 inline Expr newClosureExpr(int kind, const std::vector<Expr>& vars,
                     const Expr& body) {
   ExprClosure ev(body.getEM(), kind, vars, body);
   return newExpr(&ev);
 }

 inline Expr newApplyExpr(ExprManager* em, const Expr& func,
                          const std::vector<Expr>& args) {
   ExprApply ev(em, func, args);
   return newExpr(&ev);
 }
 inline Expr newNamedExpr(ExprManager* em, int kind, const std::string& name) {
   NamedExprValue ev(em, kind, name, std::vector<Expr>());
   return newExpr(&ev);
 }
 inline Expr newNamedExpr(ExprManager* em, int kind, const std::string& name,
                          const std::vector<Expr>& kids) {
   NamedExprValue ev(em, kind, name, kids);
   return newExpr(&ev);
 }
 inline Expr newNamedExpr(int kind, const std::string& name,
                          const std::vector<Expr>& kids) {
   DebugAssert(kids.size() > 0 && !kids[0].isNull(), "newNamedExpr()");
   NamedExprValue ev(kids[0].getEM(), kind, name, kids);
   return newExpr(&ev);
 }
   
 // ExprManager is taken from the op or children
 inline Expr newExpr(const Op& op) {
   return Expr(op);
 }
 inline Expr newExpr(const Op& op, const Expr& child) {
   return Expr(op, child);
 }
 
 inline Expr newExpr(const Op& op, const Expr& child0, const Expr& child1) {
   return Expr(op, child0, child1);
 }
 inline Expr newExpr(const Op& op, const Expr& child0, const Expr& child1,
                     const Expr& child2) {
   return Expr(op, child0, child1, child2);
 }
 inline Expr newExpr(const Op& op, const std::vector<Expr>& children) {
   return Expr(op, children);
 }

 // Leaf nodes
 inline Expr newStringExpr(ExprManager *em, const std::string &s) {
   ExprString ev(em, s);
   return newExpr(&ev);
 }
 inline Expr newVarExpr(ExprManager *em, const std::string &s) {
   ExprVar ev(em, s);
   return newExpr(&ev);
 }
 inline Expr newBoundVarExpr(ExprManager *em, const std::string &name,
                             const std::string& uid) {
   ExprBoundVar ev(em, name, uid);
   return newExpr(&ev);
 }
 inline Expr newRatExpr(ExprManager *em, const Rational &r) {
   ExprRational ev(em, r);
   return newExpr(&ev);
 }

 inline Expr newSkolemExpr(const Expr& e, int index) {
   return e.skolemExpr(index);
 }

 inline Expr newBoolVarExpr(const Expr& e) {
   return e.boolVarExpr();
 }
 inline const Expr& falseExpr(ExprManager *em) {
   return em->falseExpr();
 }
 inline const Expr& trueExpr(ExprManager *em) {
   return em->trueExpr();
 }


  /////////////////////////////////////////////////////////////////////////////
  // Read-only (const) methods                                               //
  /////////////////////////////////////////////////////////////////////////////

 inline size_t Expr::hash() const { return getEM()->hash(*this); }

 // Core Expression Testers

 inline bool Expr::isVar() const { return d_expr->isVar(); }
 inline bool Expr::isBoolVar() const { return d_expr->isBoolVar(); }
 inline bool Expr::isString() const { return d_expr->isString(); }
 inline bool Expr::isClosure() const { return d_expr->isClosure(); }
 inline bool Expr::isQuantifier() const {
   return (isClosure() && (getKind() == FORALL || getKind() == EXISTS));
 }
 inline bool Expr::isLambda() const {
   return (isClosure() && getKind() == LAMBDA);
 }
 inline bool Expr::isApply() const { return d_expr->isApply(); }
 inline bool Expr::isType() const { return getEM()->isTypeKind(getKind()); }
//  inline bool Expr::isRecord() const { return d_expr->isRecord(); }
//  inline bool Expr::isRecordAccess() const { return d_expr->isField(); }
//  inline bool Expr::isTupleAccess() const { return d_expr->isTupleIndex(); }
 inline size_t Expr::isGeneric() const { return d_expr->isGeneric(); }
 inline bool Expr::isGeneric(size_t idx) const
   { return d_expr->isGeneric(idx); }

 inline int Expr::getHeight() const { return d_expr->getHeight(); }
 inline int Expr::getHighestKid() const { return d_expr->getHighestKid(); }

 inline bool Expr::hasSimpFrom() const
   { return !d_expr->getSimpFrom().isNull(); }
 inline const Expr& Expr::getSimpFrom() const
   { return hasSimpFrom() ? d_expr->getSimpFrom() : *this; }
 inline void Expr::setSimpFrom(const Expr& simpFrom)
   { d_expr->setSimpFrom(simpFrom); }

 // Leaf accessors

 inline const std::string& Expr::getName() const {
   DebugAssert(!isNull(), "Expr::getName() on Null expr");
   return d_expr->getName();
 }

 inline const std::string& Expr::getString() const {
    DebugAssert(isString(),
                "CVCL::Expr::getString(): not a string Expr:\n  "
                + toString(AST_LANG));
    return d_expr->getString();
 }

 inline const std::vector<Expr>& Expr::getVars() const {
    DebugAssert(isClosure(),
                "CVCL::Expr::getVars(): not a closure Expr:\n  "
                + toString(AST_LANG));
    return d_expr->getVars();
 }

 inline const Expr& Expr::getVar() const {
    DebugAssert(isBoolVar(),
                "CVCL::Expr::getVar(): not a BoolVar Expr:\n  "
                + toString(AST_LANG));
    return d_expr->getVar();
 }

 inline const Expr& Expr::getFun() const {
    DebugAssert(isApply(),
                "CVCL::Expr::getFun(): not an Apply Expr:\n  "
                + toString(AST_LANG));
    return d_expr->getFun();
 }

 inline const Expr& Expr::getBody() const {
    DebugAssert(isClosure(),
                "CVCL::Expr::getBody(): not a closure Expr:\n  "
                + toString(AST_LANG));
    return d_expr->getBody();
 }

//  inline const std::vector<std::string>& Expr::getRecordFields() const {
//    DebugAssert(isRecord(), "Expr::getRecordFields(): not a record Expr:\n  "
//             + toString(AST_LANG));
//    return d_expr->getFields();
//  }

//  inline const std::string& Expr::getRecordField() const {
//    DebugAssert(isRecordAccess(),
//             "Expr::getRecordField(): not a record access Expr:\n  "
//             + toString(AST_LANG));
//    return d_expr->getField();
//  }

//  inline int Expr::getFieldIndex(const std::string& fieldName) const
//    {
//      DebugAssert(isRecord(), "Expr::getFieldIndex : not a record");
//      const std::vector<std::string>& fields = getRecordFields();
//      DebugAssert(fields.size() == (unsigned int)arity(),
//        "Expr::getFieldIndex: number of fields differs from number of values");
//      for(int i=0; i<arity(); ++i)
//        {
//       if(fieldName == fields[i])
//         return i;
//        }
//      return -1;
       
//    }
//  inline int Expr::getTupleIndex() const {
//    DebugAssert(isTupleAccess(),
//             "Expr::getTupleIndex(): not a tuple access Expr:\n  "
//             + toString(AST_LANG));
//    return d_expr->getTupleIndex();
//  }


 inline const Expr& Expr::getExistential() const {
   DebugAssert(isSkolem(),
               "CVCL::Expr::getExistential() not a skolem variable");
   return d_expr->getExistential();
 }
 inline int Expr::getBoundIndex() const {
   DebugAssert(isSkolem(),
               "CVCL::Expr::getBoundIndex() not a skolem variable");
   return d_expr->getBoundIndex();
 }


 inline const Rational& Expr::getRational() const {
   DebugAssert(isRational(),
                "CVCL::Expr::getRational(): not a rational Expr:\n  "
                + toString(AST_LANG));
    return d_expr->getRational();
 }

 inline int Expr::getIntValue(int idx) const
   { return d_expr->getIntValue(idx); }
 inline const std::string& Expr::getStringValue(int idx) const
   { return d_expr->getStringValue(idx); }
 inline const Rational& Expr::getRatValue(int idx) const
   { return d_expr->getRatValue(idx); }
 inline const Expr& Expr::getExprValue(int idx) const
   { return d_expr->getExprValue(idx); }
 inline const Theorem& Expr::getTheoremValue(int idx) const
   { return d_expr->getTheoremValue(idx); }
 inline const CDO<int>& Expr::getCDIntValue(int idx) const
   { return d_expr->getCDIntValue(idx); }
 inline const CDO<Expr>& Expr::getCDExprValue(int idx) const
   { return d_expr->getCDExprValue(idx); }
 inline const CDO<Theorem>& Expr::getCDTheoremValue(int idx) const
   { return d_expr->getCDTheoremValue(idx); }
 inline const void* Expr::getOtherValue(int idx) const
   { return d_expr->getOtherValue(idx); }

 inline size_t Expr::getIntValueSize() const
   { return d_expr->getIntValueSize(); }
 inline size_t Expr::getStringValueSize() const
   { return d_expr->getStringValueSize(); }
 inline size_t Expr::getRatValueSize() const
   { return d_expr->getRatValueSize(); }
 inline size_t Expr::getExprValueSize() const
   { return d_expr->getExprValueSize(); }
 inline size_t Expr::getTheoremValueSize() const
   { return d_expr->getTheoremValueSize(); }
 inline size_t Expr::getCDIntValueSize() const
   { return d_expr->getCDIntValueSize(); }
 inline size_t Expr::getCDExprValueSize() const
   { return d_expr->getCDExprValueSize(); }
 inline size_t Expr::getCDTheoremValueSize() const
   {return d_expr->getCDTheoremValueSize();}
 inline size_t Expr::getOtherValueSize() const
   { return d_expr->getOtherValueSize(); }

 inline int& Expr::getIntAttr(int idx) const
   { return d_expr->getIntAttr(idx); }
 inline Expr& Expr::getExprAttr(int idx) const
   { return d_expr->getExprAttr(idx); }
 inline Theorem& Expr::getTheoremAttr(int idx) const
   { return d_expr->getTheoremAttr(idx); }
 inline CDO<int>& Expr::getCDIntAttr(int idx) const
   { return d_expr->getCDIntAttr(idx); }
 inline CDO<Expr>& Expr::getCDExprAttr(int idx) const
   { return d_expr->getCDExprAttr(idx); }
 inline CDO<Theorem>& Expr::getCDTheoremAttr(int idx) const
   { return d_expr->getCDTheoremAttr(idx); }
 inline void* Expr::getOtherAttr(int idx) const
   { return d_expr->getOtherAttr(idx); }

 inline size_t Expr::getIntAttrSize() const
   { return d_expr->getIntAttrSize(); }
 inline size_t Expr::getExprAttrSize() const
   { return d_expr->getExprAttrSize(); }
 inline size_t Expr::getTheoremAttrSize() const
   { return d_expr->getTheoremAttrSize(); }
 inline size_t Expr::getCDIntAttrSize() const
   { return d_expr->getCDIntAttrSize(); }
 inline size_t Expr::getCDExprAttrSize() const
   { return d_expr->getCDExprAttrSize(); }
 inline size_t Expr::getCDTheoremAttrSize() const
   {return d_expr->getCDTheoremAttrSize();}
 inline size_t Expr::getOtherAttrSize() const
   { return d_expr->getOtherAttrSize(); }

 inline const std::string& Expr::getUid() const {
    DebugAssert(getKind() == BOUND_VAR,
                "CVCL::Expr::getUid(): not a BOUND_VAR Expr:\n  "
                + toString(AST_LANG));
    return d_expr->getUid();
 }

 inline ExprManager* Expr::getEM() const {
   ASSERT_FATAL(d_expr != NULL,
                "CVCL::Expr:getEM: on Null Expr (not initialized)");
   return d_expr->d_em;
 }

 inline const std::vector<Expr>& Expr::getKids() const {
   DebugAssert(d_expr != NULL, "Expr::getKids on Null Expr");
   if(isNull()) return getEM()->getEmptyVector();
   else return d_expr->getKids();
 }

 inline int Expr::getKind() const {
    if(d_expr == NULL) return NULL_KIND; // FIXME: invent a better Null kind
    return d_expr->d_kind;
  }

 // Get the index field
 inline ExprIndex Expr::getIndex() const { return d_expr->d_index; }
 inline bool Expr::hasLastIndex() const { return d_expr->d_em->lastIndex() == getIndex(); }

//  inline bool Expr::hasOp() const {
//    if(d_expr == NULL) return false;
//    return d_expr->hasOp();
//  }

//  inline const Expr& Expr::getOpRef() const {
//    DebugAssert(!isNull(), "Expr::getOpRef() on Null expr");
//    return d_expr->getOpRef();
//  }

//  inline Expr Expr::getOp() const {
//    DebugAssert(!isNull(), "Expr::getOp() on Null expr");
//    return d_expr->getOp();
//  }

 inline int Expr::arity() const {
   if(isNull()) return 0;
   else return d_expr->arity();
 }

 inline bool Expr::isNull() const {
   return (d_expr == NULL) || (d_expr->d_kind == NULL_KIND);
 }

 inline size_t Expr::getMMIndex() const {
   DebugAssert(!isNull(), "Expr::getMMIndex()");
   return d_expr->getMMIndex();
 }

 // Attributes
 inline bool Expr::hasFind() const {
   DebugAssert(!isNull(), "hasFind called on NULL Expr");
   return (d_expr->d_find && !(d_expr->d_find->get().isNull()));
 }
 
 inline Theorem Expr::getFind() const {
   DebugAssert(hasFind(), "Should only be called if find is valid");
   return d_expr->d_find->get();
 }

 inline NotifyList* Expr::getNotify() const {
   if(isNull()) return NULL;
   else return d_expr->d_notifyList;
 }

 inline const Type& Expr::lookupType() const {
   static Type null;
   if(isNull()) return null;
   else return d_expr->d_type;
 }

 inline const Expr& Expr::lookupTCC() const {
   static Expr null;
   if(isNull()) return null;
   else return d_expr->d_tcc;
 }

 inline const Theorem& Expr::lookupSubtypePred() const {
   static Theorem null;
   if(isNull()) return null;
   else return d_expr->d_subtypePred;
 }

 inline bool Expr::validSimpCache() const {
   return d_expr->d_simpCacheTag == getEM()->getSimpCacheTag();
 }

 inline const Theorem& Expr::getSimpCache() const {
   return d_expr->d_simpCache;
 }

 inline bool Expr::validIsAtomicFlag() const {
   return d_expr->d_staticFlags & VALID_IS_ATOMIC;
 }

 inline bool Expr::getIsAtomicFlag() const {
   return d_expr->d_staticFlags & IS_ATOMIC;
 }

 inline bool Expr::isRewriteNormal() const {
   return d_expr->d_staticFlags & REWRITE_NORMAL;
 }

 inline bool Expr::getFlag() const {
   DebugAssert(!isNull(), "Expr::getFlag() on Null Expr");
   return (d_expr->d_flag == getEM()->getFlag());
 }

 inline void Expr::setFlag() const {
   DebugAssert(!isNull(), "Expr::setFlag() on Null Expr");
   d_expr->d_flag = getEM()->getFlag();
 }

 inline void Expr::clearFlags() const {
   DebugAssert(!isNull(), "Expr::clearFlags() on Null Expr");
   getEM()->clearFlags();
 }

 inline void Expr::setFind(const Theorem& e) const {
   DebugAssert(!isNull(), "Expr::setFind() on Null expr");
   DebugAssert(e.getLHS() == *this, "bad call to setFind");
   if (d_expr->d_find) d_expr->d_find->set(e);
   else {
     CDO<Theorem>* tmp = new CDO<Theorem>(getEM()->getCurrentContext(), e);
     d_expr->d_find = tmp;
     IF_DEBUG(tmp->setName("CDO[Expr.find]"));
   }
 }

 inline void Expr::setType(const Type& t) const {
   DebugAssert(!isNull(), "Expr::setType() on Null expr");
   d_expr->d_type = t;
 }

 inline void Expr::setTCC(const Expr& tcc) const {
   DebugAssert(!isNull(), "Expr::setTCC() on Null expr");
   d_expr->d_tcc = tcc;
 }

 inline void Expr::setSubtypePred(const Theorem& pred) const {
   DebugAssert(!isNull(), "Expr::setSubtypePred() on Null expr");
   d_expr->d_subtypePred = pred;
 }

 inline void Expr::setSimpCache(const Theorem& e) const {
   DebugAssert(!isNull(), "Expr::setSimpCache() on Null expr");
   d_expr->d_simpCache = e;
   d_expr->d_simpCacheTag = getEM()->getSimpCacheTag();
 }

 inline void Expr::setIsAtomicFlag(bool value) const {
   DebugAssert(!isNull(), "Expr::setIsAtomicFlag() on Null expr");
   d_expr->d_staticFlags = d_expr->d_staticFlags | VALID_IS_ATOMIC;
   if (value) d_expr->d_staticFlags = d_expr->d_staticFlags | IS_ATOMIC;
   else d_expr->d_staticFlags = d_expr->d_staticFlags & ~IS_ATOMIC;
 }

 inline void Expr::setRewriteNormal() const {
   DebugAssert(!isNull(), "Expr::setRewriteNormal() on Null expr");
   TRACE("setRewriteNormal", "setRewriteNormal(", *this, ")");
   d_expr->d_staticFlags = d_expr->d_staticFlags | REWRITE_NORMAL;
 }

 inline void Expr::clearRewriteNormal() const {
   DebugAssert(!isNull(), "Expr::clearRewriteNormal() on Null expr");
   d_expr->d_staticFlags = d_expr->d_staticFlags & ~REWRITE_NORMAL;
 }

 inline bool Expr::hasSig() const {
   return (!isNull()
           && d_expr->getSig() != NULL 
           && !(d_expr->getSig()->get().isNull()));
 }

 inline bool Expr::hasRep() const {
   return (!isNull()
           && d_expr->getRep() != NULL 
           && !(d_expr->getRep()->get().isNull()));
 }

 inline const Theorem& Expr::getSig() const {
   static Theorem nullThm;   
   DebugAssert(!isNull(), "Expr::getSig() on Null expr");
   if(d_expr->getSig() != NULL)
     return d_expr->getSig()->get();
   else
     return nullThm;
 }

 inline const Theorem& Expr::getRep() const {
   static Theorem nullThm;
   DebugAssert(!isNull(), "Expr::getRep() on Null expr");
   if(d_expr->getRep() != NULL)
     return d_expr->getRep()->get();
   else
     return nullThm;
 }

 inline void Expr::setSig(const Theorem& e) const {
   DebugAssert(!isNull(), "Expr::setSig() on Null expr");
   CDO<Theorem>* sig = d_expr->getSig();
   if(sig != NULL) sig->set(e);
   else {
     CDO<Theorem>* tmp = new CDO<Theorem>(getEM()->getCurrentContext(), e);
     d_expr->setSig(tmp);
     IF_DEBUG(tmp->setName("CDO[Expr.sig] in "+toString()));
   }
 }
 
 inline void Expr::setRep(const Theorem& e) const {
   DebugAssert(!isNull(), "Expr::setRep() on Null expr");
   CDO<Theorem>* rep = d_expr->getRep();
   if(rep != NULL) rep->set(e);
   else {
     CDO<Theorem>* tmp = new CDO<Theorem>(getEM()->getCurrentContext(), e);
     d_expr->setRep(tmp);
     IF_DEBUG(tmp->setName("CDO[Expr.rep] in "+toString()));
   }
 }
 
  inline bool operator==(const Expr& e1, const Expr& e2) {
    // Comparing pointers (equal expressions are always shared)
    return e1.d_expr == e2.d_expr;
  }

  inline bool operator!=(const Expr& e1, const Expr& e2)
    { return !(e1 == e2); }

  // compare() is defined in expr.cpp

  inline bool operator<(const Expr& e1, const Expr& e2)
    { return compare(e1,e2) < 0; }
  inline bool operator<=(const Expr& e1, const Expr& e2)
    { return compare(e1,e2) <= 0; }
  inline bool operator>(const Expr& e1, const Expr& e2)
    { return compare(e1,e2) > 0; }
  inline bool operator>=(const Expr& e1, const Expr& e2)
    { return compare(e1,e2) >= 0; }
  

} // end of namespace CVCL

#endif

---