Delete Expr layer. (#6117)

1 files changed, 0 insertions, 703 deletions

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
deleted file mode 100644
index 745588a9a..000000000
--- a/src/expr/expr_template.cpp
+++ /dev/null
@@ -1,703 +0,0 @@
-/*********************                                                        */
-/*! \file expr_template.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Mathias Preiner, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Public-facing expression interface, implementation.
- **
- ** Public-facing expression interface, implementation.
- **/
-#include "expr/expr.h"
-
-#include <iostream>
-#include <iterator>
-#include <utility>
-#include <vector>
-
-#include "base/check.h"
-#include "expr/expr_manager_scope.h"
-#include "expr/node.h"
-#include "expr/node_algorithm.h"
-#include "expr/node_manager_attributes.h"
-#include "expr/variable_type_map.h"
-
-${includes}
-
-using namespace CVC4::kind;
-using namespace std;
-
-namespace CVC4 {
-
-class ExprManager;
-
-std::ostream& operator<<(std::ostream& out, const TypeCheckingException& e) {
-  return out << e.getMessage() << ": " << e.getExpression();
-}
-
-std::ostream& operator<<(std::ostream& out, const Expr& e) {
-  if(e.isNull()) {
-    return out << "null";
-  } else {
-    ExprManagerScope ems(*e.getExprManager());
-    return out << e.getNode();
-  }
-}
-
-std::ostream& operator<<(std::ostream& out, const std::vector<Expr>& container)
-{
-  container_to_stream(out, container);
-  return out;
-}
-
-std::ostream& operator<<(std::ostream& out, const std::set<Expr>& container)
-{
-  container_to_stream(out, container);
-  return out;
-}
-
-std::ostream& operator<<(
-    std::ostream& out,
-    const std::unordered_set<Expr, ExprHashFunction>& container)
-{
-  container_to_stream(out, container);
-  return out;
-}
-
-template <typename V>
-std::ostream& operator<<(std::ostream& out, const std::map<Expr, V>& container)
-{
-  container_to_stream(out, container);
-  return out;
-}
-
-template <typename V>
-std::ostream& operator<<(
-    std::ostream& out,
-    const std::unordered_map<Expr, V, ExprHashFunction>& container)
-{
-  container_to_stream(out, container);
-  return out;
-}
-
-TypeCheckingException::TypeCheckingException(const TypeCheckingException& t)
-    : Exception(t.d_msg), d_expr(new Expr(t.getExpression()))
-{
-}
-
-TypeCheckingException::TypeCheckingException(const Expr& expr,
-                                             std::string message)
-    : Exception(message), d_expr(new Expr(expr))
-{
-}
-
-TypeCheckingException::TypeCheckingException(
-    ExprManager* em, const TypeCheckingExceptionPrivate* exc)
-    : Exception(exc->getMessage()),
-      d_expr(new Expr(em, new Node(exc->getNode())))
-{
-}
-
-TypeCheckingException::~TypeCheckingException() { delete d_expr; }
-
-void TypeCheckingException::toStream(std::ostream& os) const
-{
-  os << "Error during type checking: " << d_msg << endl
-     << "The ill-typed expression: " << *d_expr;
-}
-
-Expr TypeCheckingException::getExpression() const { return *d_expr; }
-
-Expr::Expr() :
-  d_node(new Node),
-  d_exprManager(NULL) {
-  // We do not need to wrap this in an ExprManagerScope as `new Node` is backed
-  // by NodeValue::null which is a static outside of a NodeManager.
-}
-
-Expr::Expr(ExprManager* em, Node* node) :
-  d_node(node),
-  d_exprManager(em) {
-  // We do not need to wrap this in an ExprManagerScope as this only initializes
-  // pointers
-}
-
-Expr::Expr(const Expr& e) :
-  d_node(NULL),
-  d_exprManager(e.d_exprManager) {
-  ExprManagerScope ems(*this);
-  d_node = new Node(*e.d_node);
-}
-
-Expr::~Expr() {
-  ExprManagerScope ems(*this);
-  delete d_node;
-}
-
-ExprManager* Expr::getExprManager() const {
-  return d_exprManager;
-}
-
-namespace expr {
-
-static Node exportConstant(TNode n, NodeManager* to, ExprManagerMapCollection& vmap);
-
-class ExportPrivate {
-private:
-  typedef std::unordered_map <NodeTemplate<false>, NodeTemplate<true>, TNodeHashFunction> ExportCache;
-  ExprManager* d_from;
-  ExprManager* d_to;
-  ExprManagerMapCollection& d_vmap;
-  uint32_t d_flags;
-  ExportCache d_exportCache;
-
- public:
-  ExportPrivate(ExprManager* from,
-                ExprManager* to,
-                ExprManagerMapCollection& vmap,
-                uint32_t flags)
-      : d_from(from), d_to(to), d_vmap(vmap), d_flags(flags)
-  {
-  }
-  Node exportInternal(TNode n) {
-
-    if(n.isNull()) return Node::null();
-    if(theory::kindToTheoryId(n.getKind()) == theory::THEORY_DATATYPES) {
-      throw ExportUnsupportedException
-        ("export of node belonging to theory of DATATYPES kinds unsupported");
-    }
-
-    if(n.getMetaKind() == metakind::CONSTANT) {
-      if(n.getKind() == kind::EMPTYSET) {
-        Type type = d_from->exportType(
-            n.getConst< ::CVC4::EmptySet>().getType().toType(), d_to, d_vmap);
-        return d_to->mkConst(::CVC4::EmptySet(TypeNode::fromType(type)));
-      }
-      return exportConstant(n, NodeManager::fromExprManager(d_to), d_vmap);
-    } else if(n.getMetaKind() == metakind::NULLARY_OPERATOR ){
-      Expr from_e(d_from, new Node(n));
-      Type type = d_from->exportType(from_e.getType(), d_to, d_vmap);
-      return d_to->mkNullaryOperator(type, n.getKind());  // FIXME thread safety
-    } else if(n.getMetaKind() == metakind::VARIABLE) {
-      Expr from_e(d_from, new Node(n));
-      Expr& to_e = d_vmap.d_typeMap[from_e];
-      if(! to_e.isNull()) {
-        Debug("export") << "+ mapped `" << from_e << "' to `" << to_e << "'" << std::endl;
-        return to_e.getNode();
-      } else {
-        // construct new variable in other manager:
-        // to_e is a ref, so this inserts from_e -> to_e
-        std::string name;
-        Type type = d_from->exportType(from_e.getType(), d_to, d_vmap);
-        if(Node::fromExpr(from_e).getAttribute(VarNameAttr(), name)) {
-          if (n.getKind() == kind::BOUND_VARIABLE)
-          {
-            // bound vars are only available at the Node level (not the Expr
-            // level)
-            TypeNode typeNode = TypeNode::fromType(type);
-            NodeManager* to_nm = NodeManager::fromExprManager(d_to);
-            Node nn = to_nm->mkBoundVar(name, typeNode);  // FIXME thread safety
-
-            // Make sure that the correct `NodeManager` is in scope while
-            // converting the node to an expression.
-            NodeManagerScope to_nms(to_nm);
-            to_e = nn.toExpr();
-          } else if(n.getKind() == kind::VARIABLE) {
-            // Temporarily set the node manager to nullptr; this gets around
-            // a check that mkVar isn't called internally
-            NodeManagerScope nullScope(nullptr);
-            to_e = d_to->mkVar(name,
-                               type);  // FIXME thread safety
-          } else if(n.getKind() == kind::SKOLEM) {
-            // skolems are only available at the Node level (not the Expr level)
-            TypeNode typeNode = TypeNode::fromType(type);
-            NodeManager* to_nm = NodeManager::fromExprManager(d_to);
-            Node nn =
-                to_nm->mkSkolem(name,
-                                typeNode,
-                                "is a skolem variable imported from another "
-                                "ExprManager");  // FIXME thread safety
-
-            // Make sure that the correct `NodeManager` is in scope while
-            // converting the node to an expression.
-            NodeManagerScope to_nms(to_nm);
-            to_e = nn.toExpr();
-          } else {
-            Unhandled();
-          }
-
-          Debug("export") << "+ exported var `" << from_e << "'[" << from_e.getId() << "] with name `" << name << "' and type `" << from_e.getType() << "' to `" << to_e << "'[" << to_e.getId() << "] with type `" << type << "'" << std::endl;
-        } else {
-          if (n.getKind() == kind::BOUND_VARIABLE)
-          {
-            // bound vars are only available at the Node level (not the Expr
-            // level)
-            TypeNode typeNode = TypeNode::fromType(type);
-            NodeManager* to_nm = NodeManager::fromExprManager(d_to);
-            Node nn = to_nm->mkBoundVar(typeNode);  // FIXME thread safety
-
-            // Make sure that the correct `NodeManager` is in scope while
-            // converting the node to an expression.
-            NodeManagerScope to_nms(to_nm);
-            to_e = nn.toExpr();
-          }
-          else
-          {
-            // Temporarily set the node manager to nullptr; this gets around
-            // a check that mkVar isn't called internally
-            NodeManagerScope nullScope(nullptr);
-            to_e = d_to->mkVar(type);  // FIXME thread safety
-          }
-          Debug("export") << "+ exported unnamed var `" << from_e << "' with type `" << from_e.getType() << "' to `" << to_e << "' with type `" << type << "'" << std::endl;
-        }
-        uint64_t to_int = (uint64_t)(to_e.getNode().d_nv);
-        uint64_t from_int = (uint64_t)(from_e.getNode().d_nv);
-        d_vmap.d_from[to_int] = from_int;
-        d_vmap.d_to[from_int] = to_int;
-        d_vmap.d_typeMap[to_e] = from_e;  // insert other direction too
-
-        // Make sure that the expressions are associated with the correct
-        // `ExprManager`s.
-        Assert(from_e.getExprManager() == d_from);
-        Assert(to_e.getExprManager() == d_to);
-        return Node::fromExpr(to_e);
-      }
-    } else {
-      if (d_exportCache.find(n) != d_exportCache.end())
-      {
-        return d_exportCache[n];
-      }
-
-      std::vector<Node> children;
-      Debug("export") << "n: " << n << std::endl;
-      if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
-        Debug("export") << "+ parameterized, op is " << n.getOperator() << std::endl;
-        children.reserve(n.getNumChildren() + 1);
-        children.push_back(exportInternal(n.getOperator()));
-      } else {
-        children.reserve(n.getNumChildren());
-      }
-      for(TNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) {
-        Debug("export") << "+ child: " << *i << std::endl;
-        children.push_back(exportInternal(*i));
-      }
-      if(Debug.isOn("export")) {
-        Debug("export") << "children for export from " << n << std::endl;
-
-        // `n` belongs to the `from` ExprManager, so begin ExprManagerScope
-        // after printing `n`
-        ExprManagerScope ems(*d_to);
-        for(std::vector<Node>::iterator i = children.begin(), i_end = children.end(); i != i_end; ++i) {
-          Debug("export") << "  child: " << *i << std::endl;
-        }
-      }
-
-      // FIXME thread safety
-      Node ret =
-          NodeManager::fromExprManager(d_to)->mkNode(n.getKind(), children);
-
-      d_exportCache[n] = ret;
-      return ret;
-    }
-  }/* exportInternal() */
-
-};
-
-}/* CVC4::expr namespace */
-
-Expr Expr::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap,
-                    uint32_t flags /* = 0 */) const {
-  Assert(d_exprManager != exprManager)
-      << "No sense in cloning an Expr in the same ExprManager";
-  ExprManagerScope ems(*this);
-  return Expr(exprManager, new Node(expr::ExportPrivate(d_exprManager, exprManager, variableMap, flags).exportInternal(*d_node)));
-}
-
-Expr& Expr::operator=(const Expr& e) {
-  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
-  Assert(e.d_node != NULL) << "Unexpected NULL expression pointer!";
-
-  if(this != &e) {
-    if(d_exprManager == e.d_exprManager) {
-      ExprManagerScope ems(*this);
-      *d_node = *e.d_node;
-    } else {
-      // This happens more than you think---every time you set to or
-      // from the null Expr.  It's tricky because each node manager
-      // must be in play at the right time.
-
-      ExprManagerScope ems1(*this);
-      *d_node = Node::null();
-
-      ExprManagerScope ems2(e);
-      *d_node = *e.d_node;
-
-      d_exprManager = e.d_exprManager;
-    }
-  }
-  return *this;
-}
-
-bool Expr::operator==(const Expr& e) const {
-  if(d_exprManager != e.d_exprManager) {
-    return false;
-  }
-  ExprManagerScope ems(*this);
-  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
-  Assert(e.d_node != NULL) << "Unexpected NULL expression pointer!";
-  return *d_node == *e.d_node;
-}
-
-bool Expr::operator!=(const Expr& e) const {
-  return !(*this == e);
-}
-
-bool Expr::operator<(const Expr& e) const {
-  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
-  Assert(e.d_node != NULL) << "Unexpected NULL expression pointer!";
-  if(isNull() && !e.isNull()) {
-    return true;
-  }
-  ExprManagerScope ems(*this);
-  return *d_node < *e.d_node;
-}
-
-bool Expr::operator>(const Expr& e) const {
-  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
-  Assert(e.d_node != NULL) << "Unexpected NULL expression pointer!";
-  if(isNull() && !e.isNull()) {
-    return true;
-  }
-  ExprManagerScope ems(*this);
-  return *d_node > *e.d_node;
-}
-
-uint64_t Expr::getId() const
-{
-  ExprManagerScope ems(*this);
-  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
-  return d_node->getId();
-}
-
-Kind Expr::getKind() const {
-  ExprManagerScope ems(*this);
-  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
-  return d_node->getKind();
-}
-
-size_t Expr::getNumChildren() const {
-  ExprManagerScope ems(*this);
-  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
-  return d_node->getNumChildren();
-}
-
-Expr Expr::operator[](unsigned i) const {
-  ExprManagerScope ems(*this);
-  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
-  Assert(i >= 0 && i < d_node->getNumChildren()) << "Child index out of bounds";
-  return Expr(d_exprManager, new Node((*d_node)[i]));
-}
-
-bool Expr::hasOperator() const {
-  ExprManagerScope ems(*this);
-  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
-  return d_node->hasOperator();
-}
-
-Expr Expr::getOperator() const {
-  ExprManagerScope ems(*this);
-  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
-  PrettyCheckArgument(d_node->hasOperator(), *this,
-                      "Expr::getOperator() called on an Expr with no operator");
-  return Expr(d_exprManager, new Node(d_node->getOperator()));
-}
-
-bool Expr::isParameterized() const
-{
-  ExprManagerScope ems(*this);
-  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
-  return d_node->getMetaKind() == kind::metakind::PARAMETERIZED;
-}
-
-Type Expr::getType(bool check) const
-{
-  ExprManagerScope ems(*this);
-  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
-  PrettyCheckArgument(!d_node->isNull(), this,
-                      "Can't get type of null expression!");
-  return d_exprManager->getType(*this, check);
-}
-
-Expr Expr::substitute(Expr e, Expr replacement) const {
-  ExprManagerScope ems(*this);
-  return Expr(d_exprManager, new Node(d_node->substitute(TNode(*e.d_node), TNode(*replacement.d_node))));
-}
-
-template <class Iterator>
-class NodeIteratorAdaptor : public std::iterator<std::input_iterator_tag, Node> {
-  Iterator d_iterator;
-public:
-  NodeIteratorAdaptor(Iterator i) : d_iterator(i) {
-  }
-  NodeIteratorAdaptor& operator++() { ++d_iterator; return *this; }
-  NodeIteratorAdaptor operator++(int) { NodeIteratorAdaptor i(d_iterator); ++d_iterator; return i; }
-  bool operator==(NodeIteratorAdaptor i) { return d_iterator == i.d_iterator; }
-  bool operator!=(NodeIteratorAdaptor i) { return !(*this == i); }
-  Node operator*() { return Node::fromExpr(*d_iterator); }
-};/* class NodeIteratorAdaptor */
-
-template <class Iterator>
-static inline NodeIteratorAdaptor<Iterator> mkNodeIteratorAdaptor(Iterator i) {
-  return NodeIteratorAdaptor<Iterator>(i);
-}
-
-Expr Expr::substitute(const std::vector<Expr> exes,
-                      const std::vector<Expr>& replacements) const {
-  ExprManagerScope ems(*this);
-  return Expr(d_exprManager,
-              new Node(d_node->substitute(mkNodeIteratorAdaptor(exes.begin()),
-                                          mkNodeIteratorAdaptor(exes.end()),
-                                          mkNodeIteratorAdaptor(replacements.begin()),
-                                          mkNodeIteratorAdaptor(replacements.end()))));
-}
-
-template <class Iterator>
-class NodePairIteratorAdaptor : public std::iterator<std::input_iterator_tag, pair<Node, Node> > {
-  Iterator d_iterator;
-public:
-  NodePairIteratorAdaptor(Iterator i) : d_iterator(i) {
-  }
-  NodePairIteratorAdaptor& operator++() { ++d_iterator; return *this; }
-  NodePairIteratorAdaptor operator++(int) { NodePairIteratorAdaptor i(d_iterator); ++d_iterator; return i; }
-  bool operator==(NodePairIteratorAdaptor i) { return d_iterator == i.d_iterator; }
-  bool operator!=(NodePairIteratorAdaptor i) { return !(*this == i); }
-  pair<Node, Node> operator*() { return make_pair(Node::fromExpr((*d_iterator).first), Node::fromExpr((*d_iterator).second)); }
-};/* class NodePairIteratorAdaptor */
-
-template <class Iterator>
-static inline NodePairIteratorAdaptor<Iterator> mkNodePairIteratorAdaptor(Iterator i) {
-  return NodePairIteratorAdaptor<Iterator>(i);
-}
-
-Expr Expr::substitute(const std::unordered_map<Expr, Expr, ExprHashFunction> map) const {
-  ExprManagerScope ems(*this);
-  return Expr(d_exprManager, new Node(d_node->substitute(mkNodePairIteratorAdaptor(map.begin()), mkNodePairIteratorAdaptor(map.end()))));
-}
-
-Expr::const_iterator::const_iterator()
-    : d_exprManager(nullptr), d_iterator(nullptr) {}
-
-Expr::const_iterator::const_iterator(ExprManager* em, void* v)
-    : d_exprManager(em), d_iterator(v) {}
-
-Expr::const_iterator::const_iterator(const const_iterator& it)
-    : d_exprManager(nullptr), d_iterator(nullptr) {
-  if (it.d_iterator != nullptr) {
-    d_exprManager = it.d_exprManager;
-    ExprManagerScope ems(*d_exprManager);
-    d_iterator =
-        new Node::iterator(*reinterpret_cast<Node::iterator*>(it.d_iterator));
-  }
-}
-
-Expr::const_iterator& Expr::const_iterator::operator=(const const_iterator& it) {
-  if(d_iterator != NULL) {
-    ExprManagerScope ems(*d_exprManager);
-    delete reinterpret_cast<Node::iterator*>(d_iterator);
-  }
-  d_exprManager = it.d_exprManager;
-  ExprManagerScope ems(*d_exprManager);
-  d_iterator = new Node::iterator(*reinterpret_cast<Node::iterator*>(it.d_iterator));
-  return *this;
-}
-Expr::const_iterator::~const_iterator() {
-  if(d_iterator != NULL) {
-    ExprManagerScope ems(*d_exprManager);
-    delete reinterpret_cast<Node::iterator*>(d_iterator);
-  }
-}
-bool Expr::const_iterator::operator==(const const_iterator& it) const {
-  if(d_iterator == NULL || it.d_iterator == NULL) {
-    return false;
-  }
-  return *reinterpret_cast<Node::iterator*>(d_iterator) ==
-    *reinterpret_cast<Node::iterator*>(it.d_iterator);
-}
-Expr::const_iterator& Expr::const_iterator::operator++() {
-  Assert(d_iterator != NULL);
-  ExprManagerScope ems(*d_exprManager);
-  ++*reinterpret_cast<Node::iterator*>(d_iterator);
-  return *this;
-}
-Expr::const_iterator Expr::const_iterator::operator++(int) {
-  Assert(d_iterator != NULL);
-  ExprManagerScope ems(*d_exprManager);
-  const_iterator it = *this;
-  ++*reinterpret_cast<Node::iterator*>(d_iterator);
-  return it;
-}
-Expr Expr::const_iterator::operator*() const {
-  Assert(d_iterator != NULL);
-  ExprManagerScope ems(*d_exprManager);
-  return (**reinterpret_cast<Node::iterator*>(d_iterator)).toExpr();
-}
-
-Expr::const_iterator Expr::begin() const {
-  ExprManagerScope ems(*d_exprManager);
-  return Expr::const_iterator(d_exprManager, new Node::iterator(d_node->begin()));
-}
-
-Expr::const_iterator Expr::end() const {
-  ExprManagerScope ems(*d_exprManager);
-  return Expr::const_iterator(d_exprManager, new Node::iterator(d_node->end()));
-}
-
-std::string Expr::toString() const {
-  ExprManagerScope ems(*this);
-  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
-  return d_node->toString();
-}
-
-bool Expr::isNull() const {
-  ExprManagerScope ems(*this);
-  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
-  return d_node->isNull();
-}
-
-bool Expr::isVariable() const {
-  ExprManagerScope ems(*this);
-  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
-  return d_node->getMetaKind() == kind::metakind::VARIABLE;
-}
-
-bool Expr::isConst() const {
-  ExprManagerScope ems(*this);
-  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
-  return d_node->isConst();
-}
-
-bool Expr::hasFreeVariable() const
-{
-  ExprManagerScope ems(*this);
-  Assert(d_node != NULL) << "Unexpected NULL expression pointer!";
-  return expr::hasFreeVar(*d_node);
-}
-
-void Expr::toStream(std::ostream& out,
-                    int depth,
-                    size_t dag,
-                    OutputLanguage language) const
-{
-  ExprManagerScope ems(*this);
-  d_node->toStream(out, depth, dag, language);
-}
-
-Node Expr::getNode() const { return *d_node; }
-TNode Expr::getTNode() const { return *d_node; }
-Expr Expr::notExpr() const {
-  Assert(d_exprManager != NULL)
-      << "Don't have an expression manager for this expression!";
-  return d_exprManager->mkExpr(NOT, *this);
-}
-
-Expr Expr::andExpr(const Expr& e) const {
-  Assert(d_exprManager != NULL)
-      << "Don't have an expression manager for this expression!";
-  PrettyCheckArgument(d_exprManager == e.d_exprManager, e,
-                      "Different expression managers!");
-  return d_exprManager->mkExpr(AND, *this, e);
-}
-
-Expr Expr::orExpr(const Expr& e) const {
-  Assert(d_exprManager != NULL)
-      << "Don't have an expression manager for this expression!";
-  PrettyCheckArgument(d_exprManager == e.d_exprManager, e,
-                      "Different expression managers!");
-  return d_exprManager->mkExpr(OR, *this, e);
-}
-
-Expr Expr::xorExpr(const Expr& e) const {
-  Assert(d_exprManager != NULL)
-      << "Don't have an expression manager for this expression!";
-  PrettyCheckArgument(d_exprManager == e.d_exprManager, e,
-                      "Different expression managers!");
-  return d_exprManager->mkExpr(XOR, *this, e);
-}
-
-Expr Expr::eqExpr(const Expr& e) const
-{
-  Assert(d_exprManager != NULL)
-      << "Don't have an expression manager for this expression!";
-  PrettyCheckArgument(d_exprManager == e.d_exprManager, e,
-                      "Different expression managers!");
-  return d_exprManager->mkExpr(EQUAL, *this, e);
-}
-
-Expr Expr::impExpr(const Expr& e) const {
-  Assert(d_exprManager != NULL)
-      << "Don't have an expression manager for this expression!";
-  PrettyCheckArgument(d_exprManager == e.d_exprManager, e,
-                      "Different expression managers!");
-  return d_exprManager->mkExpr(IMPLIES, *this, e);
-}
-
-Expr Expr::iteExpr(const Expr& then_e,
-                           const Expr& else_e) const {
-  Assert(d_exprManager != NULL)
-      << "Don't have an expression manager for this expression!";
-  PrettyCheckArgument(d_exprManager == then_e.d_exprManager, then_e,
-                      "Different expression managers!");
-  PrettyCheckArgument(d_exprManager == else_e.d_exprManager, else_e,
-                      "Different expression managers!");
-  return d_exprManager->mkExpr(ITE, *this, then_e, else_e);
-}
-
-void Expr::printAst(std::ostream & o, int indent) const {
-  ExprManagerScope ems(*this);
-  getNode().printAst(o, indent);
-}
-
-void Expr::debugPrint() {
-#ifndef CVC4_MUZZLE
-  printAst(Warning());
-  Warning().flush();
-#endif /* ! CVC4_MUZZLE */
-}
-
-${getConst_implementations}
-
-namespace expr {
-
-static Node exportConstant(TNode n, NodeManager* to, ExprManagerMapCollection& vmap) {
-  Assert(n.isConst());
-  Debug("export") << "constant: " << n << std::endl;
-
-  if(n.getKind() == kind::STORE_ALL) {
-    // Special export for ArrayStoreAll.
-    //
-    // Ultimately we'll need special cases also for RecordUpdate,
-    // TupleUpdate, AscriptionType, and other constant-metakinded
-    // expressions that embed types.  For now datatypes aren't supported
-    // for export so those don't matter.
-    ExprManager* toEm = to->toExprManager();
-    const ArrayStoreAll& asa = n.getConst<ArrayStoreAll>();
-    return to->mkConst(ArrayStoreAll(
-        TypeNode::fromType(asa.getType().toType().exportTo(toEm, vmap)),
-        Node::fromExpr(asa.getValue().toExpr().exportTo(toEm, vmap))));
-  }
-
-  switch(n.getKind()) {
-${exportConstant_cases}
-
-default: Unhandled() << n.getKind();
-  }
-
-}/* exportConstant() */
-
-}/* CVC4::expr namespace */
-}/* CVC4 namespace */