Delete Expr layer. (#6117)

13 files changed, 7 insertions, 4410 deletions

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 343d55800..3e8717986 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -27,7 +27,6 @@ libcvc4_add_sources(
   emptybag.h
   expr_iomanip.cpp
   expr_iomanip.h
-  expr_manager_scope.h
   kind_map.h
   lazy_proof.cpp
   lazy_proof.h
@@ -94,14 +93,11 @@ libcvc4_add_sources(
   term_context_stack.h
   term_conversion_proof_generator.cpp
   term_conversion_proof_generator.h
-  type.cpp
-  type.h
   type_checker.h
   type_matcher.cpp
   type_matcher.h
   type_node.cpp
   type_node.h
-  variable_type_map.h
   datatype_index.h
   datatype_index.cpp
   dtype.h
@@ -127,10 +123,6 @@ libcvc4_add_sources(GENERATED
   kind.h
   metakind.cpp
   metakind.h
-  expr.cpp
-  expr.h
-  expr_manager.cpp
-  expr_manager.h
   type_checker.cpp
   type_properties.h
 )
@@ -194,46 +186,6 @@ add_custom_command(
 )
 
 add_custom_command(
-  OUTPUT expr.h
-  COMMAND
-    ${mkexpr_script}
-    ${CMAKE_CURRENT_LIST_DIR}/expr_template.h
-    ${KINDS_FILES}
-    > ${CMAKE_CURRENT_BINARY_DIR}/expr.h
-  DEPENDS mkexpr expr_template.h kind.h ${KINDS_FILES}
-)
-
-add_custom_command(
-  OUTPUT expr.cpp
-  COMMAND
-    ${mkexpr_script}
-    ${CMAKE_CURRENT_LIST_DIR}/expr_template.cpp
-    ${KINDS_FILES}
-    > ${CMAKE_CURRENT_BINARY_DIR}/expr.cpp
-  DEPENDS mkexpr expr_template.cpp expr.h ${KINDS_FILES}
-)
-
-add_custom_command(
-  OUTPUT expr_manager.h
-  COMMAND
-    ${mkexpr_script}
-    ${CMAKE_CURRENT_LIST_DIR}/expr_manager_template.h
-    ${KINDS_FILES}
-    > ${CMAKE_CURRENT_BINARY_DIR}/expr_manager.h
-  DEPENDS mkexpr expr_manager_template.h expr.h ${KINDS_FILES}
-)
-
-add_custom_command(
-  OUTPUT expr_manager.cpp
-  COMMAND
-    ${mkexpr_script}
-    ${CMAKE_CURRENT_LIST_DIR}/expr_manager_template.cpp
-    ${KINDS_FILES}
-    > ${CMAKE_CURRENT_BINARY_DIR}/expr_manager.cpp
-  DEPENDS mkexpr expr_manager_template.cpp expr_manager.h ${KINDS_FILES}
-)
-
-add_custom_command(
   OUTPUT type_checker.cpp
   COMMAND
     ${mkexpr_script}
@@ -249,10 +201,6 @@ add_custom_target(gen-expr
     kind.h
     metakind.cpp
     metakind.h
-    expr.cpp
-    expr.h
-    expr_manager.cpp
-    expr_manager.h
     type_checker.cpp
     type_properties.h
 )
diff --git a/src/expr/expr_manager_scope.h b/src/expr/expr_manager_scope.h
deleted file mode 100644
index a737c669b..000000000
--- a/src/expr/expr_manager_scope.h
+++ /dev/null
@@ -1,69 +0,0 @@
-/*********************                                                        */
-/*! \file expr_manager_scope.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Christopher L. Conway, Mathias Preiner
- ** 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__EXPR_MANAGER_SCOPE_H
-#define CVC4__EXPR_MANAGER_SCOPE_H
-
-#include "expr/expr.h"
-#include "expr/node_manager.h"
-#include "expr/expr_manager.h"
-
-namespace CVC4 {
-
-/**
- * Creates a <code>NodeManagerScope</code> with the underlying
- * <code>NodeManager</code> of a given <code>Expr</code> or
- * <code>ExprManager</code>.  The <code>NodeManagerScope</code> is
- * destroyed when the <code>ExprManagerScope</code> is destroyed. See
- * <code>NodeManagerScope</code> for more information.
- */
-// NOTE: Here, it seems ExprManagerScope is redundant, since we have
-// NodeManagerScope already.  However, without this class, we'd need
-// Expr to be a friend of ExprManager, because in the implementation
-// of Expr functions, it needs to set the current NodeManager
-// correctly (and to do that it needs access to
-// ExprManager::getNodeManager()).  So, we make ExprManagerScope a
-// friend of ExprManager's, since its implementation is simple to
-// read and understand (and verify that it doesn't do any mischief).
-//
-// ExprManager::getNodeManager() can't just be made public, since
-// ExprManager is exposed to clients of the library and NodeManager is
-// not.  Similarly, ExprManagerScope shouldn't go in expr_manager.h,
-// since that's a public header.
-class ExprManagerScope {
-  NodeManagerScope d_nms;
-public:
-  inline ExprManagerScope(const Expr& e) :
-    d_nms(e.getExprManager() == NULL
-          ? NodeManager::currentNM()
-          : e.getExprManager()->getNodeManager()) {
-  }
-  inline ExprManagerScope(const Type& t) :
-    d_nms(t.getExprManager() == NULL
-          ? NodeManager::currentNM()
-          : t.getExprManager()->getNodeManager()) {
-  }
-  inline ExprManagerScope(const ExprManager& exprManager) :
-    d_nms(exprManager.getNodeManager()) {
-  }
-};/* class ExprManagerScope */
-
-}/* CVC4 namespace */
-
-#endif /* CVC4__EXPR_MANAGER_SCOPE_H */
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
deleted file mode 100644
index 414d8a611..000000000
--- a/src/expr/expr_manager_template.cpp
+++ /dev/null
@@ -1,908 +0,0 @@
-/*********************                                                        */
-/*! \file expr_manager_template.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Christopher L. Conway, Dejan Jovanovic
- ** 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 manager interface, implementation
- **
- ** Public-facing expression manager interface, implementation.
- **/
-
-#include "expr/expr_manager.h"
-
-#include <map>
-
-#include "expr/node_manager.h"
-#include "expr/variable_type_map.h"
-#include "expr/node_manager_attributes.h"
-#include "options/options.h"
-#include "util/statistics_registry.h"
-
-${includes}
-
-#ifdef CVC4_STATISTICS_ON
-  #define INC_STAT(kind) \
-  { \
-    if (d_exprStatistics[kind] == NULL) { \
-      stringstream statName; \
-      statName << "expr::ExprManager::" << kind; \
-      d_exprStatistics[kind] = new IntStat(statName.str(), 0); \
-      d_nodeManager->getStatisticsRegistry()->registerStat(d_exprStatistics[kind]); \
-    } \
-    ++ *(d_exprStatistics[kind]); \
-  }
-#define INC_STAT_VAR(type, bound_var)                                      \
-  {                                                                        \
-    TypeNode* isv_typeNode = Type::getTypeNode(type);                      \
-    TypeConstant isv_type = isv_typeNode->getKind() == kind::TYPE_CONSTANT \
-                                ? isv_typeNode->getConst<TypeConstant>()   \
-                                : LAST_TYPE;                               \
-    if (d_exprStatisticsVars[isv_type] == NULL)                            \
-    {                                                                      \
-      stringstream statName;                                               \
-      if (isv_type == LAST_TYPE)                                           \
-      {                                                                    \
-        statName << "expr::ExprManager::"                                  \
-                 << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE")          \
-                 << ":Parameterized isv_type";                             \
-      }                                                                    \
-      else                                                                 \
-      {                                                                    \
-        statName << "expr::ExprManager::"                                  \
-                 << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") << ":"   \
-                 << isv_type;                                              \
-      }                                                                    \
-      d_exprStatisticsVars[isv_type] = new IntStat(statName.str(), 0);     \
-      d_nodeManager->getStatisticsRegistry()->registerStat(                \
-          d_exprStatisticsVars[isv_type]);                                 \
-    }                                                                      \
-    ++*(d_exprStatisticsVars[isv_type]);                                   \
-  }
-#else
-  #define INC_STAT(kind)
-  #define INC_STAT_VAR(type, bound_var)
-#endif
-
-using namespace std;
-using namespace CVC4::kind;
-
-namespace CVC4 {
-
-ExprManager::ExprManager() :
-  d_nodeManager(new NodeManager(this)) {
-#ifdef CVC4_STATISTICS_ON
-  for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
-    d_exprStatistics[i] = NULL;
-  }
-  for (unsigned i = 0; i <= LAST_TYPE; ++ i) {
-    d_exprStatisticsVars[i] = NULL;
-  }
-#endif
-}
-
-ExprManager::~ExprManager()
-{
-  NodeManagerScope nms(d_nodeManager);
-
-  try {
-
-#ifdef CVC4_STATISTICS_ON
-    for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
-      if (d_exprStatistics[i] != NULL) {
-        d_nodeManager->getStatisticsRegistry()->unregisterStat(d_exprStatistics[i]);
-        delete d_exprStatistics[i];
-        d_exprStatistics[i] = NULL;
-      }
-    }
-    for (unsigned i = 0; i <= LAST_TYPE; ++ i) {
-      if (d_exprStatisticsVars[i] != NULL) {
-        d_nodeManager->getStatisticsRegistry()->unregisterStat(d_exprStatisticsVars[i]);
-        delete d_exprStatisticsVars[i];
-        d_exprStatisticsVars[i] = NULL;
-      }
-    }
-#endif
-
-    delete d_nodeManager;
-    d_nodeManager = NULL;
-  } catch(Exception& e) {
-    Warning() << "CVC4 threw an exception during cleanup." << std::endl
-              << e << std::endl;
-  }
-}
-
-BooleanType ExprManager::booleanType() const {
-  NodeManagerScope nms(d_nodeManager);
-  return BooleanType(Type(d_nodeManager, new TypeNode(d_nodeManager->booleanType())));
-}
-
-StringType ExprManager::stringType() const {
-  NodeManagerScope nms(d_nodeManager);
-  return StringType(Type(d_nodeManager, new TypeNode(d_nodeManager->stringType())));
-}
-
-RegExpType ExprManager::regExpType() const {
-  NodeManagerScope nms(d_nodeManager);
-  return RegExpType(Type(d_nodeManager, new TypeNode(d_nodeManager->regExpType())));
-}
-
-RealType ExprManager::realType() const {
-  NodeManagerScope nms(d_nodeManager);
-  return RealType(Type(d_nodeManager, new TypeNode(d_nodeManager->realType())));
-}
-
-IntegerType ExprManager::integerType() const {
-  NodeManagerScope nms(d_nodeManager);
-  return IntegerType(Type(d_nodeManager, new TypeNode(d_nodeManager->integerType())));
-}
-
-RoundingModeType ExprManager::roundingModeType() const {
-  NodeManagerScope nms(d_nodeManager);
-  return RoundingModeType(Type(d_nodeManager, new TypeNode(d_nodeManager->roundingModeType())));
-}
-
-
-Expr ExprManager::mkExpr(Kind kind, Expr child1) {
-  const kind::MetaKind mk = kind::metaKindOf(kind);
-  const unsigned n = 1 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
-  PrettyCheckArgument(
-      mk == kind::metakind::PARAMETERIZED ||
-      mk == kind::metakind::OPERATOR, kind,
-      "Only operator-style expressions are made with mkExpr(); "
-      "to make variables and constants, see mkVar(), mkBoundVar(), "
-      "and mkConst().");
-  PrettyCheckArgument(
-      n >= minArity(kind) && n <= maxArity(kind), kind,
-      "Exprs with kind %s must have at least %u children and "
-      "at most %u children (the one under construction has %u)",
-      kind::kindToString(kind).c_str(),
-      minArity(kind), maxArity(kind), n);
-  NodeManagerScope nms(d_nodeManager);
-  try {
-    INC_STAT(kind);
-    return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode()));
-  } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(this, &e);
-  }
-}
-
-Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2) {
-  const kind::MetaKind mk = kind::metaKindOf(kind);
-  const unsigned n = 2 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
-  PrettyCheckArgument(
-      mk == kind::metakind::PARAMETERIZED ||
-      mk == kind::metakind::OPERATOR, kind,
-      "Only operator-style expressions are made with mkExpr(); "
-      "to make variables and constants, see mkVar(), mkBoundVar(), "
-      "and mkConst().");
-  PrettyCheckArgument(
-      n >= minArity(kind) && n <= maxArity(kind), kind,
-      "Exprs with kind %s must have at least %u children and "
-      "at most %u children (the one under construction has %u)",
-      kind::kindToString(kind).c_str(),
-      minArity(kind), maxArity(kind), n);
-  NodeManagerScope nms(d_nodeManager);
-  try {
-    INC_STAT(kind);
-    return Expr(this, d_nodeManager->mkNodePtr(kind,
-                                               child1.getNode(),
-                                               child2.getNode()));
-  } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(this, &e);
-  }
-}
-
-Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3) {
-  const kind::MetaKind mk = kind::metaKindOf(kind);
-  const unsigned n = 3 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
-  PrettyCheckArgument(
-      mk == kind::metakind::PARAMETERIZED ||
-      mk == kind::metakind::OPERATOR, kind,
-      "Only operator-style expressions are made with mkExpr(); "
-      "to make variables and constants, see mkVar(), mkBoundVar(), "
-      "and mkConst().");
-  PrettyCheckArgument(
-      n >= minArity(kind) && n <= maxArity(kind), kind,
-      "Exprs with kind %s must have at least %u children and "
-      "at most %u children (the one under construction has %u)",
-      kind::kindToString(kind).c_str(),
-      minArity(kind), maxArity(kind), n);
-  NodeManagerScope nms(d_nodeManager);
-  try {
-    INC_STAT(kind);
-    return Expr(this, d_nodeManager->mkNodePtr(kind,
-                                               child1.getNode(),
-                                               child2.getNode(),
-                                               child3.getNode()));
-  } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(this, &e);
-  }
-}
-
-Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3,
-                         Expr child4) {
-  const kind::MetaKind mk = kind::metaKindOf(kind);
-  const unsigned n = 4 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
-  PrettyCheckArgument(
-      mk == kind::metakind::PARAMETERIZED ||
-      mk == kind::metakind::OPERATOR, kind,
-      "Only operator-style expressions are made with mkExpr(); "
-      "to make variables and constants, see mkVar(), mkBoundVar(), "
-      "and mkConst().");
-  PrettyCheckArgument(
-      n >= minArity(kind) && n <= maxArity(kind), kind,
-      "Exprs with kind %s must have at least %u children and "
-      "at most %u children (the one under construction has %u)",
-      kind::kindToString(kind).c_str(),
-      minArity(kind), maxArity(kind), n);
-  NodeManagerScope nms(d_nodeManager);
-  try {
-    INC_STAT(kind);
-    return Expr(this, d_nodeManager->mkNodePtr(kind,
-                                               child1.getNode(),
-                                               child2.getNode(),
-                                               child3.getNode(),
-                                               child4.getNode()));
-  } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(this, &e);
-  }
-}
-
-Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3,
-                         Expr child4, Expr child5) {
-  const kind::MetaKind mk = kind::metaKindOf(kind);
-  const unsigned n = 5 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
-  PrettyCheckArgument(
-      mk == kind::metakind::PARAMETERIZED ||
-      mk == kind::metakind::OPERATOR, kind,
-      "Only operator-style expressions are made with mkExpr(); "
-      "to make variables and constants, see mkVar(), mkBoundVar(), "
-      "and mkConst().");
-  PrettyCheckArgument(
-      n >= minArity(kind) && n <= maxArity(kind), kind,
-      "Exprs with kind %s must have at least %u children and "
-      "at most %u children (the one under construction has %u)",
-      kind::kindToString(kind).c_str(),
-      minArity(kind), maxArity(kind), n);
-  NodeManagerScope nms(d_nodeManager);
-  try {
-    INC_STAT(kind);
-    return Expr(this, d_nodeManager->mkNodePtr(kind,
-                                               child1.getNode(),
-                                               child2.getNode(),
-                                               child3.getNode(),
-                                               child4.getNode(),
-                                               child5.getNode()));
-  } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(this, &e);
-  }
-}
-
-Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children)
-{
-  const size_t nchildren = children.size();
-  const kind::MetaKind mk = kind::metaKindOf(kind);
-  PrettyCheckArgument(
-      mk == kind::metakind::PARAMETERIZED || mk == kind::metakind::OPERATOR,
-      kind,
-      "Only operator-style expressions are made with mkExpr(); "
-      "to make variables and constants, see mkVar(), mkBoundVar(), "
-      "and mkConst().");
-  PrettyCheckArgument(
-      mk != kind::metakind::PARAMETERIZED || nchildren > 0,
-      kind,
-      "Terms with kind %s must have an operator expression as first argument",
-      kind::kindToString(kind).c_str());
-  const size_t n = nchildren - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
-  PrettyCheckArgument(n >= minArity(kind) && n <= maxArity(kind),
-                      kind,
-                      "Exprs with kind %s must have at least %u children and "
-                      "at most %u children (the one under construction has %u)",
-                      kind::kindToString(kind).c_str(),
-                      minArity(kind),
-                      maxArity(kind),
-                      n);
-
-  NodeManagerScope nms(d_nodeManager);
-
-  vector<Node> nodes;
-  vector<Expr>::const_iterator it = children.begin();
-  vector<Expr>::const_iterator it_end = children.end();
-  while(it != it_end) {
-    nodes.push_back(it->getNode());
-    ++it;
-  }
-  try {
-    INC_STAT(kind);
-    return Expr(this, d_nodeManager->mkNodePtr(kind, nodes));
-  } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(this, &e);
-  }
-}
-
-Expr ExprManager::mkExpr(Kind kind, Expr child1,
-                         const std::vector<Expr>& otherChildren) {
-  const kind::MetaKind mk = kind::metaKindOf(kind);
-  const unsigned n =
-      otherChildren.size() - (mk == kind::metakind::PARAMETERIZED ? 1 : 0) + 1;
-  PrettyCheckArgument(
-      mk == kind::metakind::PARAMETERIZED ||
-      mk == kind::metakind::OPERATOR, kind,
-      "Only operator-style expressions are made with mkExpr(); "
-      "to make variables and constants, see mkVar(), mkBoundVar(), "
-      "and mkConst().");
-  PrettyCheckArgument(
-      n >= minArity(kind) && n <= maxArity(kind), kind,
-      "Exprs with kind %s must have at least %u children and "
-      "at most %u children (the one under construction has %u)",
-      kind::kindToString(kind).c_str(),
-      minArity(kind), maxArity(kind), n);
-
-  NodeManagerScope nms(d_nodeManager);
-
-  vector<Node> nodes;
-  nodes.push_back(child1.getNode());
-
-  vector<Expr>::const_iterator it = otherChildren.begin();
-  vector<Expr>::const_iterator it_end = otherChildren.end();
-  while(it != it_end) {
-    nodes.push_back(it->getNode());
-    ++it;
-  }
-  try {
-    INC_STAT(kind);
-    return Expr(this, d_nodeManager->mkNodePtr(kind, nodes));
-  } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(this, &e);
-  }
-}
-
-Expr ExprManager::mkExpr(Expr opExpr) {
-  const Kind kind = NodeManager::operatorToKind(opExpr.getNode());
-  PrettyCheckArgument(
-      opExpr.getKind() == kind::BUILTIN ||
-      kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
-      "This Expr constructor is for parameterized kinds only");
-  NodeManagerScope nms(d_nodeManager);
-  try {
-    INC_STAT(kind);
-    return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode()));
-  } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(this, &e);
-  }
-}
-
-Expr ExprManager::mkExpr(Expr opExpr, Expr child1) {
-  const unsigned n = 1;
-  Kind kind = NodeManager::operatorToKind(opExpr.getNode());
-  PrettyCheckArgument(
-      (opExpr.getKind() == kind::BUILTIN ||
-       kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr,
-      "This Expr constructor is for parameterized kinds only");
-  PrettyCheckArgument(
-      n >= minArity(kind) && n <= maxArity(kind), kind,
-      "Exprs with kind %s must have at least %u children and "
-      "at most %u children (the one under construction has %u)",
-      kind::kindToString(kind).c_str(),
-      minArity(kind), maxArity(kind), n);
-  NodeManagerScope nms(d_nodeManager);
-  try {
-    INC_STAT(kind);
-    return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), child1.getNode()));
-  } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(this, &e);
-  }
-}
-
-Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2) {
-  const unsigned n = 2;
-  Kind kind = NodeManager::operatorToKind(opExpr.getNode());
-  PrettyCheckArgument(
-      (opExpr.getKind() == kind::BUILTIN ||
-       kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr,
-      "This Expr constructor is for parameterized kinds only");
-  PrettyCheckArgument(
-      n >= minArity(kind) && n <= maxArity(kind), kind,
-      "Exprs with kind %s must have at least %u children and "
-      "at most %u children (the one under construction has %u)",
-      kind::kindToString(kind).c_str(),
-      minArity(kind), maxArity(kind), n);
-  NodeManagerScope nms(d_nodeManager);
-  try {
-    INC_STAT(kind);
-    return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(),
-                                               child1.getNode(),
-                                               child2.getNode()));
-  } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(this, &e);
-  }
-}
-
-Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3) {
-  const unsigned n = 3;
-  Kind kind = NodeManager::operatorToKind(opExpr.getNode());
-  PrettyCheckArgument(
-      (opExpr.getKind() == kind::BUILTIN ||
-       kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr,
-                "This Expr constructor is for parameterized kinds only");
-  PrettyCheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
-                "Exprs with kind %s must have at least %u children and "
-                "at most %u children (the one under construction has %u)",
-                kind::kindToString(kind).c_str(),
-                minArity(kind), maxArity(kind), n);
-  NodeManagerScope nms(d_nodeManager);
-  try {
-    INC_STAT(kind);
-    return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(),
-                                               child1.getNode(),
-                                               child2.getNode(),
-                                               child3.getNode()));
-  } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(this, &e);
-  }
-}
-
-Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
-                         Expr child4) {
-  const unsigned n = 4;
-  Kind kind = NodeManager::operatorToKind(opExpr.getNode());
-  PrettyCheckArgument(
-      (opExpr.getKind() == kind::BUILTIN ||
-       kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr,
-      "This Expr constructor is for parameterized kinds only");
-
-  PrettyCheckArgument(
-      n >= minArity(kind) && n <= maxArity(kind), kind,
-      "Exprs with kind %s must have at least %u children and "
-      "at most %u children (the one under construction has %u)",
-      kind::kindToString(kind).c_str(),
-      minArity(kind), maxArity(kind), n);
-
-  NodeManagerScope nms(d_nodeManager);
-  try {
-    INC_STAT(kind);
-    return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(),
-                                               child1.getNode(),
-                                               child2.getNode(),
-                                               child3.getNode(),
-                                               child4.getNode()));
-  } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(this, &e);
-  }
-}
-
-Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
-                         Expr child4, Expr child5) {
-  const unsigned n = 5;
-  Kind kind = NodeManager::operatorToKind(opExpr.getNode());
-  PrettyCheckArgument(
-      (opExpr.getKind() == kind::BUILTIN ||
-       kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr,
-      "This Expr constructor is for parameterized kinds only");
-  PrettyCheckArgument(
-      n >= minArity(kind) && n <= maxArity(kind), kind,
-      "Exprs with kind %s must have at least %u children and "
-      "at most %u children (the one under construction has %u)",
-      kind::kindToString(kind).c_str(),
-      minArity(kind), maxArity(kind), n);
-  NodeManagerScope nms(d_nodeManager);
-  try {
-    INC_STAT(kind);
-    return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(),
-                                               child1.getNode(),
-                                               child2.getNode(),
-                                               child3.getNode(),
-                                               child4.getNode(),
-                                               child5.getNode()));
-  } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(this, &e);
-  }
-}
-
-Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) {
-  const unsigned n = children.size();
-  Kind kind = NodeManager::operatorToKind(opExpr.getNode());
-  PrettyCheckArgument(
-      (opExpr.getKind() == kind::BUILTIN ||
-       kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED), opExpr,
-      "This Expr constructor is for parameterized kinds only");
-  PrettyCheckArgument(
-      n >= minArity(kind) && n <= maxArity(kind), kind,
-      "Exprs with kind %s must have at least %u children and "
-      "at most %u children (the one under construction has %u)",
-      kind::kindToString(kind).c_str(),
-      minArity(kind), maxArity(kind), n);
-
-  NodeManagerScope nms(d_nodeManager);
-
-  vector<Node> nodes;
-  vector<Expr>::const_iterator it = children.begin();
-  vector<Expr>::const_iterator it_end = children.end();
-  while(it != it_end) {
-    nodes.push_back(it->getNode());
-    ++it;
-  }
-  try {
-    INC_STAT(kind);
-    return Expr(this,d_nodeManager->mkNodePtr(opExpr.getNode(), nodes));
-  } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(this, &e);
-  }
-}
-
-bool ExprManager::hasOperator(Kind k) {
-  return NodeManager::hasOperator(k);
-}
-
-Expr ExprManager::operatorOf(Kind k) {
-  NodeManagerScope nms(d_nodeManager);
-
-  return d_nodeManager->operatorOf(k).toExpr();
-}
-
-Kind ExprManager::operatorToKind(Expr e) {
-  NodeManagerScope nms(d_nodeManager);
-
-  return d_nodeManager->operatorToKind( e.getNode() );
-}
-
-/** Make a function type from domain to range. */
-FunctionType ExprManager::mkFunctionType(Type domain, Type range) {
-  NodeManagerScope nms(d_nodeManager);
-  return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(*domain.d_typeNode, *range.d_typeNode))));
-}
-
-/** Make a function type with input types from argTypes. */
-FunctionType ExprManager::mkFunctionType(const std::vector<Type>& argTypes, Type range) {
-  NodeManagerScope nms(d_nodeManager);
-  Assert(argTypes.size() >= 1);
-  std::vector<TypeNode> argTypeNodes;
-  for (unsigned i = 0, i_end = argTypes.size(); i < i_end; ++ i) {
-    argTypeNodes.push_back(*argTypes[i].d_typeNode);
-  }
-  return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(argTypeNodes, *range.d_typeNode))));
-}
-
-FunctionType ExprManager::mkFunctionType(const std::vector<Type>& sorts) {
-  NodeManagerScope nms(d_nodeManager);
-  Assert(sorts.size() >= 2);
-  std::vector<TypeNode> sortNodes;
-  for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) {
-     sortNodes.push_back(*sorts[i].d_typeNode);
-  }
-  return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(sortNodes))));
-}
-
-FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) {
-  NodeManagerScope nms(d_nodeManager);
-  Assert(sorts.size() >= 1);
-  std::vector<TypeNode> sortNodes;
-  for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) {
-     sortNodes.push_back(*sorts[i].d_typeNode);
-  }
-  return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes))));
-}
-
-SExprType ExprManager::mkSExprType(const std::vector<Type>& types) {
-  NodeManagerScope nms(d_nodeManager);
-  std::vector<TypeNode> typeNodes;
-  for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) {
-     typeNodes.push_back(*types[i].d_typeNode);
-  }
-  return SExprType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSExprType(typeNodes))));
-}
-
-FloatingPointType ExprManager::mkFloatingPointType(unsigned exp, unsigned sig) const {
-  NodeManagerScope nms(d_nodeManager);
-  return FloatingPointType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFloatingPointType(exp,sig))));
-}
-
-BitVectorType ExprManager::mkBitVectorType(unsigned size) const {
-  NodeManagerScope nms(d_nodeManager);
-  return BitVectorType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkBitVectorType(size))));
-}
-
-ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const {
-  NodeManagerScope nms(d_nodeManager);
-  return ArrayType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode))));
-}
-
-SetType ExprManager::mkSetType(Type elementType) const {
-  NodeManagerScope nms(d_nodeManager);
-  return SetType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSetType(*elementType.d_typeNode))));
-}
-
-SequenceType ExprManager::mkSequenceType(Type elementType) const
-{
-  NodeManagerScope nms(d_nodeManager);
-  return SequenceType(Type(
-      d_nodeManager,
-      new TypeNode(d_nodeManager->mkSequenceType(*elementType.d_typeNode))));
-}
-
-SortType ExprManager::mkSort(const std::string& name, uint32_t flags) const {
-  NodeManagerScope nms(d_nodeManager);
-  return SortType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name, flags))));
-}
-
-SortConstructorType ExprManager::mkSortConstructor(const std::string& name,
-                                                   size_t arity,
-                                                   uint32_t flags) const
-{
-  NodeManagerScope nms(d_nodeManager);
-  return SortConstructorType(
-      Type(d_nodeManager,
-           new TypeNode(d_nodeManager->mkSortConstructor(name, arity, flags))));
-}
-
-/**
- * Get the type for the given Expr and optionally do type checking.
- *
- * Initial type computation will be near-constant time if
- * type checking is not requested. Results are memoized, so that
- * subsequent calls to getType() without type checking will be
- * constant time.
- *
- * Initial type checking is linear in the size of the expression.
- * Again, the results are memoized, so that subsequent calls to
- * getType(), with or without type checking, will be constant
- * time.
- *
- * NOTE: A TypeCheckingException can be thrown even when type
- * checking is not requested. getType() will always return a
- * valid and correct type and, thus, an exception will be thrown
- * when no valid or correct type can be computed (e.g., if the
- * arguments to a bit-vector operation aren't bit-vectors). When
- * type checking is not requested, getType() will do the minimum
- * amount of checking required to return a valid result.
- *
- * @param e the Expr for which we want a type
- * @param check whether we should check the type as we compute it
- * (default: false)
- */
-Type ExprManager::getType(Expr expr, bool check)
-{
-  NodeManagerScope nms(d_nodeManager);
-  Type t;
-  try {
-    t = Type(d_nodeManager,
-             new TypeNode(d_nodeManager->getType(expr.getNode(), check)));
-  } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(this, &e);
-  }
-  return t;
-}
-
-Expr ExprManager::mkVar(const std::string& name, Type type)
-{
-  NodeManagerScope nms(d_nodeManager);
-  Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode);
-  Debug("nm") << "set " << name << " on " << *n << std::endl;
-  INC_STAT_VAR(type, false);
-  return Expr(this, n);
-}
-
-Expr ExprManager::mkVar(Type type)
-{
-  NodeManagerScope nms(d_nodeManager);
-  INC_STAT_VAR(type, false);
-  return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode));
-}
-
-Expr ExprManager::mkBoundVar(const std::string& name, Type type)
-{
-  NodeManagerScope nms(d_nodeManager);
-  Node* n = d_nodeManager->mkBoundVarPtr(name, *type.d_typeNode);
-  Debug("nm") << "set " << name << " on " << *n << std::endl;
-  INC_STAT_VAR(type, true);
-  return Expr(this, n);
-}
-
-Expr ExprManager::mkBoundVar(Type type)
-{
-  NodeManagerScope nms(d_nodeManager);
-  INC_STAT_VAR(type, true);
-  return Expr(this, d_nodeManager->mkBoundVarPtr(*type.d_typeNode));
-}
-
-Expr ExprManager::mkNullaryOperator(Type type, Kind k){
-  NodeManagerScope nms(d_nodeManager);
-  Node n = d_nodeManager->mkNullaryOperator(*type.d_typeNode, k); 
-  return n.toExpr();
-}
-
-Expr ExprManager::mkAssociative(Kind kind,
-                                const std::vector<Expr>& children) {
-  PrettyCheckArgument(
-      kind::isAssociative(kind), kind,
-      "Illegal kind in mkAssociative: %s",
-      kind::kindToString(kind).c_str());
-
-  const unsigned int max = maxArity(kind);
-  unsigned int numChildren = children.size();
-
-  /* If the number of children is within bounds, then there's nothing to do. */
-  if( numChildren <= max ) {
-    return mkExpr(kind,children);
-  }
-  NodeManagerScope nms(d_nodeManager);
-  const unsigned int min = minArity(kind);
-
-  std::vector<Expr>::const_iterator it = children.begin() ;
-  std::vector<Expr>::const_iterator end = children.end() ;
-
-  /* The new top-level children and the children of each sub node */
-  std::vector<Expr> newChildren;
-  std::vector<Node> subChildren;
-
-  while( it != end && numChildren > max ) {
-    /* Grab the next max children and make a node for them. */
-    for( std::vector<Expr>::const_iterator next = it + max;
-         it != next;
-         ++it, --numChildren ) {
-      subChildren.push_back(it->getNode());
-    }
-    Node subNode = d_nodeManager->mkNode(kind,subChildren);
-    newChildren.push_back(subNode.toExpr());
-
-    subChildren.clear();
-  }
-
-  // add the leftover children
-  if(numChildren > 0) {
-    for (; it != end; ++it)
-    {
-      newChildren.push_back(*it);
-    }
-  }
-
-  /* It would be really weird if this happened (it would require
-   * min > 2, for one thing), but let's make sure. */
-  AlwaysAssert(newChildren.size() >= min)
-      << "Too few new children in mkAssociative";
-
-  // recurse
-  return mkAssociative(kind, newChildren);
-}
-
-Expr ExprManager::mkLeftAssociative(Kind kind,
-                                    const std::vector<Expr>& children)
-{
-  NodeManagerScope nms(d_nodeManager);
-  Node n = children[0];
-  for (unsigned i = 1, size = children.size(); i < size; i++)
-  {
-    n = d_nodeManager->mkNode(kind, n, children[i].getNode());
-  }
-  return n.toExpr();
-}
-
-Expr ExprManager::mkRightAssociative(Kind kind,
-                                     const std::vector<Expr>& children)
-{
-  NodeManagerScope nms(d_nodeManager);
-  Node n = children[children.size() - 1];
-  for (unsigned i = children.size() - 1; i > 0;)
-  {
-    n = d_nodeManager->mkNode(kind, children[--i].getNode(), n);
-  }
-  return n.toExpr();
-}
-
-Expr ExprManager::mkChain(Kind kind, const std::vector<Expr>& children)
-{
-  if (children.size() == 2)
-  {
-    // if this is the case exactly 1 pair will be generated so the
-    // AND is not required
-    return mkExpr(kind, children[0], children[1]);
-  }
-  std::vector<Expr> cchildren;
-  for (size_t i = 0, nargsmo = children.size() - 1; i < nargsmo; i++)
-  {
-    cchildren.push_back(mkExpr(kind, children[i], children[i + 1]));
-  }
-  return mkExpr(kind::AND, cchildren);
-}
-
-unsigned ExprManager::minArity(Kind kind) {
-  return metakind::getMinArityForKind(kind);
-}
-
-unsigned ExprManager::maxArity(Kind kind) {
-  return metakind::getMaxArityForKind(kind);
-}
-
-bool ExprManager::isNAryKind(Kind fun)
-{
-  return ExprManager::maxArity(fun) == expr::NodeValue::MAX_CHILDREN;
-}
-
-NodeManager* ExprManager::getNodeManager() const {
-  return d_nodeManager;
-}
-Statistics ExprManager::getStatistics() const
-{
-  return Statistics(*d_nodeManager->getStatisticsRegistry());
-}
-
-SExpr ExprManager::getStatistic(const std::string& name) const
-{
-  return d_nodeManager->getStatisticsRegistry()->getStatistic(name);
-}
-
-void ExprManager::safeFlushStatistics(int fd) const {
-  d_nodeManager->getStatisticsRegistry()->safeFlushInformation(fd);
-}
-
-namespace expr {
-
-Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap);
-
-TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, ExprManagerMapCollection& vmap) {
-  Debug("export") << "type: " << n << " " << n.getId() << std::endl;
-  if(theory::kindToTheoryId(n.getKind()) == theory::THEORY_DATATYPES) {
-    throw ExportUnsupportedException
-      ("export of types belonging to theory of DATATYPES kinds unsupported");
-  }
-  if(n.getMetaKind() == kind::metakind::PARAMETERIZED &&
-     n.getKind() != kind::SORT_TYPE) {
-    throw ExportUnsupportedException
-      ("export of PARAMETERIZED-kinded types (other than SORT_KIND) not supported");
-  }
-  if(n.getKind() == kind::TYPE_CONSTANT) {
-    return to->mkTypeConst(n.getConst<TypeConstant>());
-  } else if(n.getKind() == kind::BITVECTOR_TYPE) {
-    return to->mkBitVectorType(n.getConst<BitVectorSize>());
-  }
-  else if (n.getKind() == kind::FLOATINGPOINT_TYPE)
-  {
-    return to->mkFloatingPointType(n.getConst<FloatingPointSize>());
-  }
-  else if (n.getNumChildren() == 0)
-  {
-    std::stringstream msg;
-    msg << "export of type " << n << " not supported";
-    throw ExportUnsupportedException(msg.str().c_str());
-  }
-  Type from_t = from->toType(n);
-  Type& to_t = vmap.d_typeMap[from_t];
-  if(! to_t.isNull()) {
-    Debug("export") << "+ mapped `" << from_t << "' to `" << to_t << "'" << std::endl;
-    return *Type::getTypeNode(to_t);
-  }
-  NodeBuilder<> children(to, n.getKind());
-  if(n.getKind() == kind::SORT_TYPE) {
-    Debug("export") << "type: operator: " << n.getOperator() << std::endl;
-    // make a new sort tag in target node manager
-    Node sortTag = NodeBuilder<0>(to, kind::SORT_TAG);
-    children << sortTag;
-  }
-  for(TypeNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) {
-    Debug("export") << "type: child: " << *i << std::endl;
-    children << exportTypeInternal(*i, from, to, vmap);
-  }
-  TypeNode out = children.constructTypeNode();// FIXME thread safety
-  to_t = to->toType(out);
-  return out;
-}/* exportTypeInternal() */
-
-}/* CVC4::expr namespace */
-
-Type ExprManager::exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap) {
-  Assert(t.d_nodeManager != em->d_nodeManager)
-      << "Can't export a Type to the same ExprManager";
-  NodeManagerScope ems(t.d_nodeManager);
-  return Type(em->d_nodeManager,
-              new TypeNode(expr::exportTypeInternal(*t.d_typeNode, t.d_nodeManager, em->d_nodeManager, vmap)));
-}
-
-${mkConst_implementations}
-
-}/* CVC4 namespace */
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
deleted file mode 100644
index 37c3a7255..000000000
--- a/src/expr/expr_manager_template.h
+++ /dev/null
@@ -1,463 +0,0 @@
-/*********************                                                        */
-/*! \file expr_manager_template.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Dejan Jovanovic, Andrew Reynolds
- ** 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 manager interface
- **
- ** Public-facing expression manager interface.
- **/
-
-#include "cvc4_public.h"
-
-#ifndef CVC4__EXPR_MANAGER_H
-#define CVC4__EXPR_MANAGER_H
-
-#include <vector>
-
-#include "expr/expr.h"
-#include "expr/kind.h"
-#include "expr/type.h"
-#include "util/statistics.h"
-
-${includes}
-
-namespace CVC4 {
-
-namespace api {
-class Solver;
-}
-
-class Expr;
-class SmtEngine;
-class NodeManager;
-class Options;
-class IntStat;
-struct ExprManagerMapCollection;
-class ResourceManager;
-
-class CVC4_PUBLIC ExprManager {
- private:
-  friend api::Solver;
-  /** The internal node manager */
-  NodeManager* d_nodeManager;
-
-  /** Counts of expressions and variables created of a given kind */
-  IntStat* d_exprStatisticsVars[LAST_TYPE + 1];
-  IntStat* d_exprStatistics[kind::LAST_KIND];
-
-  /**
-   * Returns the internal node manager.  This should only be used by
-   * internal users, i.e. the friend classes.
-   */
-  NodeManager* getNodeManager() const;
-
-  /**
-   * SmtEngine will use all the internals, so it will grab the
-   * NodeManager.
-   */
-  friend class SmtEngine;
-
-  /** ExprManagerScope reaches in to get the NodeManager */
-  friend class ExprManagerScope;
-
-  /** NodeManager reaches in to get the NodeManager */
-  friend class NodeManager;
-
-  // undefined, private copy constructor and assignment op (disallow copy)
-  ExprManager(const ExprManager&) = delete;
-  ExprManager& operator=(const ExprManager&) = delete;
-  /** Creates an expression manager. */
-  ExprManager();
- public:
-  /**
-   * Destroys the expression manager. No will be deallocated at this point, so
-   * any expression references that used to be managed by this expression
-   * manager and are left-over are bad.
-   */
-  ~ExprManager();
-
-  /** Get the type for booleans */
-  BooleanType booleanType() const;
-
-  /** Get the type for strings. */
-  StringType stringType() const;
-
-  /** Get the type for regular expressions. */
-  RegExpType regExpType() const;
-
-  /** Get the type for reals. */
-  RealType realType() const;
-
-  /** Get the type for integers */
-  IntegerType integerType() const;
-
-  /** Get the type for rounding modes */
-  RoundingModeType roundingModeType() const;
-
-  /**
-   * Make a unary expression of a given kind (NOT, BVNOT, ...).
-   * @param kind the kind of expression
-   * @param child1 kind the kind of expression
-   * @return the expression
-   */
-  Expr mkExpr(Kind kind, Expr child1);
-
-  /**
-   * Make a binary expression of a given kind (AND, PLUS, ...).
-   * @param kind the kind of expression
-   * @param child1 the first child of the new expression
-   * @param child2 the second child of the new expression
-   * @return the expression
-   */
-  Expr mkExpr(Kind kind, Expr child1, Expr child2);
-
-  /**
-   * Make a 3-ary expression of a given kind (AND, PLUS, ...).
-   * @param kind the kind of expression
-   * @param child1 the first child of the new expression
-   * @param child2 the second child of the new expression
-   * @param child3 the third child of the new expression
-   * @return the expression
-   */
-  Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3);
-
-  /**
-   * Make a 4-ary expression of a given kind (AND, PLUS, ...).
-   * @param kind the kind of expression
-   * @param child1 the first child of the new expression
-   * @param child2 the second child of the new expression
-   * @param child3 the third child of the new expression
-   * @param child4 the fourth child of the new expression
-   * @return the expression
-   */
-  Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
-
-  /**
-   * Make a 5-ary expression of a given kind (AND, PLUS, ...).
-   * @param kind the kind of expression
-   * @param child1 the first child of the new expression
-   * @param child2 the second child of the new expression
-   * @param child3 the third child of the new expression
-   * @param child4 the fourth child of the new expression
-   * @param child5 the fifth child of the new expression
-   * @return the expression
-   */
-  Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4,
-              Expr child5);
-
-  /**
-   * Make an n-ary expression of given kind given a vector of its
-   * children
-   *
-   * @param kind the kind of expression to build
-   * @param children the subexpressions
-   * @return the n-ary expression
-   */
-  Expr mkExpr(Kind kind, const std::vector<Expr>& children);
-
-  /**
-   * Make an n-ary expression of given kind given a first arg and
-   * a vector of its remaining children (this can be useful where the
-   * kind is parameterized operator, so the first arg is really an
-   * arg to the kind to construct an operator)
-   *
-   * @param kind the kind of expression to build
-   * @param child1 the first subexpression
-   * @param otherChildren the remaining subexpressions
-   * @return the n-ary expression
-   */
-  Expr mkExpr(Kind kind, Expr child1, const std::vector<Expr>& otherChildren);
-
-  /**
-   * Make a nullary parameterized expression with the given operator.
-   *
-   * @param opExpr the operator expression
-   * @return the nullary expression
-   */
-  Expr mkExpr(Expr opExpr);
-
-  /**
-   * Make a unary parameterized expression with the given operator.
-   *
-   * @param opExpr the operator expression
-   * @param child1 the subexpression
-   * @return the unary expression
-   */
-  Expr mkExpr(Expr opExpr, Expr child1);
-
-  /**
-   * Make a binary parameterized expression with the given operator.
-   *
-   * @param opExpr the operator expression
-   * @param child1 the first subexpression
-   * @param child2 the second subexpression
-   * @return the binary expression
-   */
-  Expr mkExpr(Expr opExpr, Expr child1, Expr child2);
-
-  /**
-   * Make a ternary parameterized expression with the given operator.
-   *
-   * @param opExpr the operator expression
-   * @param child1 the first subexpression
-   * @param child2 the second subexpression
-   * @param child3 the third subexpression
-   * @return the ternary expression
-   */
-  Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3);
-
-  /**
-   * Make a quaternary parameterized expression with the given operator.
-   *
-   * @param opExpr the operator expression
-   * @param child1 the first subexpression
-   * @param child2 the second subexpression
-   * @param child3 the third subexpression
-   * @param child4 the fourth subexpression
-   * @return the quaternary expression
-   */
-  Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4);
-
-  /**
-   * Make a quinary parameterized expression with the given operator.
-   *
-   * @param opExpr the operator expression
-   * @param child1 the first subexpression
-   * @param child2 the second subexpression
-   * @param child3 the third subexpression
-   * @param child4 the fourth subexpression
-   * @param child5 the fifth subexpression
-   * @return the quinary expression
-   */
-  Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4,
-              Expr child5);
-
-  /**
-   * Make an n-ary expression of given operator to apply and a vector
-   * of its children
-   *
-   * @param opExpr the operator expression
-   * @param children the subexpressions
-   * @return the n-ary expression
-   */
-  Expr mkExpr(Expr opExpr, const std::vector<Expr>& children);
-
-  /** Create a constant of type T */
-  template <class T>
-  Expr mkConst(const T&);
-
-  /**
-   * Create an Expr by applying an associative operator to the children.
-   * If <code>children.size()</code> is greater than the max arity for
-   * <code>kind</code>, then the expression will be broken up into
-   * suitably-sized chunks, taking advantage of the associativity of
-   * <code>kind</code>. For example, if kind <code>FOO</code> has max arity
-   * 2, then calling <code>mkAssociative(FOO,a,b,c)</code> will return
-   * <code>(FOO (FOO a b) c)</code> or <code>(FOO a (FOO b c))</code>.
-   * The order of the arguments will be preserved in a left-to-right
-   * traversal of the resulting tree.
-   */
-  Expr mkAssociative(Kind kind, const std::vector<Expr>& children);
-
-  /**
-   * Create an Expr by applying an binary left-associative operator to the
-   * children. For example, mkLeftAssociative( f, { a, b, c } ) returns
-   * f( f( a, b ), c ).
-   */
-  Expr mkLeftAssociative(Kind kind, const std::vector<Expr>& children);
-  /**
-   * Create an Expr by applying an binary right-associative operator to the
-   * children. For example, mkRightAssociative( f, { a, b, c } ) returns
-   * f( a, f( b, c ) ).
-   */
-  Expr mkRightAssociative(Kind kind, const std::vector<Expr>& children);
-
-  /** make chain
-   *
-   * Given a kind k and arguments t_1, ..., t_n, this returns the
-   * conjunction of:
-   *  (k t_1 t_2) .... (k t_{n-1} t_n)
-   * It is expected that k is a kind denoting a predicate, and args is a list
-   * of terms of size >= 2 such that the terms above are well-typed.
-   */
-  Expr mkChain(Kind kind, const std::vector<Expr>& children);
-
-  /**
-   * Determine whether Exprs of a particular Kind have operators.
-   * @returns true if Exprs of Kind k have operators.
-   */
-  static bool hasOperator(Kind k);
-
-  /**
-   * Get the (singleton) operator of an OPERATOR-kinded kind.  The
-   * returned Expr e will have kind BUILTIN, and calling
-   * e.getConst<CVC4::Kind>() will yield k.
-   */
-  Expr operatorOf(Kind k);
-  
-  /** Get a Kind from an operator expression */
-  Kind operatorToKind(Expr e);
-  
-  /** Make a function type from domain to range. */
-  FunctionType mkFunctionType(Type domain, Type range);
-
-  /**
-   * Make a function type with input types from argTypes.
-   * <code>argTypes</code> must have at least one element.
-   */
-  FunctionType mkFunctionType(const std::vector<Type>& argTypes, Type range);
-
-  /**
-   * Make a function type with input types from
-   * <code>sorts[0..sorts.size()-2]</code> and result type
-   * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
-   * at least 2 elements.
-   */
-  FunctionType mkFunctionType(const std::vector<Type>& sorts);
-
-  /**
-   * Make a predicate type with input types from
-   * <code>sorts</code>. The result with be a function type with range
-   * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
-   * element.
-   */
-  FunctionType mkPredicateType(const std::vector<Type>& sorts);
-
-  /**
-   * Make a symbolic expressiontype with types from
-   * <code>types[0..types.size()-1]</code>.  <code>types</code> may
-   * have any number of elements.
-   */
-  SExprType mkSExprType(const std::vector<Type>& types);
-
-  /** Make a type representing a floating-point type with the given parameters. */
-  FloatingPointType mkFloatingPointType(unsigned exp, unsigned sig) const;
-
-  /** Make a type representing a bit-vector of the given size. */
-  BitVectorType mkBitVectorType(unsigned size) const;
-
-  /** Make the type of arrays with the given parameterization. */
-  ArrayType mkArrayType(Type indexType, Type constituentType) const;
-
-  /** Make the type of set with the given parameterization. */
-  SetType mkSetType(Type elementType) const;
-
-  /** Make the type of sequence with the given parameterization. */
-  SequenceType mkSequenceType(Type elementType) const;
-
-  /** Make a new sort with the given name. */
-  SortType mkSort(const std::string& name, uint32_t flags) const;
-
-  /** Make a sort constructor from a name and arity. */
-  SortConstructorType mkSortConstructor(const std::string& name,
-                                        size_t arity,
-                                        uint32_t flags) const;
-
-  /**
-   * Get the type of an expression.
-   *
-   * Throws a TypeCheckingException on failures or if a Type cannot be
-   * computed.
-   */
-  Type getType(Expr e, bool check = false);
-
-  /**
-   * Create a new, fresh variable.  This variable is guaranteed to be
-   * distinct from every variable thus far in the ExprManager, even
-   * if it shares a name with another; this is to support any kind of
-   * scoping policy on top of ExprManager.  The SymbolTable class
-   * can be used to store and lookup symbols by name, if desired.
-   *
-   * @param name a name to associate to the fresh new variable
-   * @param type the type for the new variable
-   */
-  Expr mkVar(const std::string& name, Type type);
-
-  /**
-   * Create a (nameless) new, fresh variable.  This variable is guaranteed
-   * to be distinct from every variable thus far in the ExprManager.
-   *
-   * @param type the type for the new variable
-   */
-  Expr mkVar(Type type);
-
-  /**
-   * Create a new, fresh variable for use in a binder expression
-   * (the BOUND_VAR_LIST of a FORALL, EXISTS, LAMBDA, or WITNESS).  It is
-   * an error for this bound variable to exist outside of a binder,
-   * and it should also only be used in a single binder expression.
-   * That is, two distinct FORALL expressions should use entirely
-   * disjoint sets of bound variables (however, a single FORALL
-   * expression can be used in multiple places in a formula without
-   * a problem).  This newly-created bound variable is guaranteed to
-   * be distinct from every variable thus far in the ExprManager, even
-   * if it shares a name with another; this is to support any kind of
-   * scoping policy on top of ExprManager.  The SymbolTable class
-   * can be used to store and lookup symbols by name, if desired.
-   *
-   * @param name a name to associate to the fresh new bound variable
-   * @param type the type for the new bound variable
-   */
-  Expr mkBoundVar(const std::string& name, Type type);
-
-  /**
-   * Create a (nameless) new, fresh variable for use in a binder
-   * expression (the BOUND_VAR_LIST of a FORALL, EXISTS, LAMBDA, or WITNESS).
-   * It is an error for this bound variable to exist outside of a
-   * binder, and it should also only be used in a single binder
-   * expression.  That is, two distinct FORALL expressions should use
-   * entirely disjoint sets of bound variables (however, a single FORALL
-   * expression can be used in multiple places in a formula without
-   * a problem).  This newly-created bound variable is guaranteed to
-   * be distinct from every variable thus far in the ExprManager.
-   *
-   * @param type the type for the new bound variable
-   */
-  Expr mkBoundVar(Type type);
-
-  /**
-   * Create unique variable of type 
-   */
-  Expr mkNullaryOperator( Type type, Kind k);
-
-  /** Get a reference to the statistics registry for this ExprManager */
-  Statistics getStatistics() const;
-
-  /** Get a reference to the statistics registry for this ExprManager */
-  SExpr getStatistic(const std::string& name) const;
-
-  /**
-   * Flushes statistics for this ExprManager to a file descriptor. Safe to use
-   * in a signal handler.
-   */
-  void safeFlushStatistics(int fd) const;
-
-  /** Export an expr to a different ExprManager */
-  //static Expr exportExpr(const Expr& e, ExprManager* em);
-  /** Export a type to a different ExprManager */
-  static Type exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap);
-
-  /** Returns the minimum arity of the given kind. */
-  static unsigned minArity(Kind kind);
-
-  /** Returns the maximum arity of the given kind. */
-  static unsigned maxArity(Kind kind);
-
-  /** Whether a kind is n-ary. The test is based on n-ary kinds having their
-   * maximal arity as the maximal possible number of children of a node.
-   **/
-  static bool isNAryKind(Kind fun);
-};/* class ExprManager */
-
-${mkConst_instantiations}
-
-}/* CVC4 namespace */
-
-#endif /* CVC4__EXPR_MANAGER_H */
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 */
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
deleted file mode 100644
index 2676c12b0..000000000
--- a/src/expr/expr_template.h
+++ /dev/null
@@ -1,622 +0,0 @@
-/*********************                                                        */
-/*! \file expr_template.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Dejan Jovanovic, Aina Niemetz
- ** 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.
- **
- ** Public-facing expression interface.
- **/
-
-#include "cvc4_public.h"
-
-// putting the constant-payload #includes up here allows circularity
-// (some of them may require a completely-defined Expr type).  This
-// way, those #includes can forward-declare some stuff to get Expr's
-// getConst<> template instantiations correct, and then #include
-// "expr.h" safely, then go on to completely declare their own stuff.
-${includes}
-
-#ifndef CVC4__EXPR_H
-#define CVC4__EXPR_H
-
-#include <iosfwd>
-#include <iterator>
-#include <string>
-#include <map>
-#include <set>
-#include <unordered_map>
-#include <unordered_set>
-
-#include "base/exception.h"
-#include "options/language.h"
-#include "util/hash.h"
-
-namespace CVC4 {
-
-// The internal expression representation
-template <bool ref_count>
-class NodeTemplate;
-
-class NodeManager;
-
-class Expr;
-class ExprManager;
-class SmtEngine;
-class Type;
-class TypeCheckingException;
-class TypeCheckingExceptionPrivate;
-
-namespace api {
-class Solver;
-}
-
-namespace prop {
-  class TheoryProxy;
-}/* CVC4::prop namespace */
-
-struct ExprManagerMapCollection;
-
-struct ExprHashFunction;
-
-namespace smt {
-  class SmtEnginePrivate;
-}/* CVC4::smt namespace */
-
-namespace expr {
-  class ExportPrivate;
-}/* CVC4::expr namespace */
-
-/**
- * Exception thrown in the case of type-checking errors.
- */
-class CVC4_PUBLIC TypeCheckingException : public Exception {
- private:
-  friend class SmtEngine;
-  friend class smt::SmtEnginePrivate;
-
-  /** The expression responsible for the error */
-  Expr* d_expr;
-
- protected:
-  TypeCheckingException() : Exception() {}
-  TypeCheckingException(ExprManager* em,
-                        const TypeCheckingExceptionPrivate* exc);
-
- public:
-  TypeCheckingException(const Expr& expr, std::string message);
-
-  /** Copy constructor */
-  TypeCheckingException(const TypeCheckingException& t);
-
-  /** Destructor */
-  ~TypeCheckingException() override;
-
-  /**
-   * Get the Expr that caused the type-checking to fail.
-   *
-   * @return the expr
-   */
-  Expr getExpression() const;
-
-  /**
-   * Returns the message corresponding to the type-checking failure.
-   * We prefer toStream() to toString() because that keeps the expr-depth
-   * and expr-language settings present in the stream.
-   */
-  void toStream(std::ostream& out) const override;
-
-  friend class ExprManager;
-};/* class TypeCheckingException */
-
-/**
- * Exception thrown in case of failure to export
- */
-class CVC4_PUBLIC ExportUnsupportedException : public Exception {
- public:
-  ExportUnsupportedException() : Exception("export unsupported") {}
-  ExportUnsupportedException(const char* msg) : Exception(msg) {}
-};/* class DatatypeExportUnsupportedException */
-
-std::ostream& operator<<(std::ostream& out,
-                         const TypeCheckingException& e) CVC4_PUBLIC;
-
-/**
- * Output operator for expressions
- * @param out the stream to output to
- * @param e the expression to output
- * @return the stream
- */
-std::ostream& operator<<(std::ostream& out, const Expr& e) CVC4_PUBLIC;
-
-/**
- * Serialize a vector of expressions to given stream.
- *
- * @param out the output stream to use
- * @param container the vector of expressions to output to the stream
- * @return the stream
- */
-std::ostream& operator<<(std::ostream& out,
-                         const std::vector<Expr>& container) CVC4_PUBLIC;
-
-/**
- * Serialize a set of expressions to the given stream.
- *
- * @param out the output stream to use
- * @param container the set of expressions to output to the stream
- * @return the stream
- */
-std::ostream& operator<<(std::ostream& out,
-                         const std::set<Expr>& container) CVC4_PUBLIC;
-
-/**
- * Serialize an unordered_set of expressions to the given stream.
- *
- * @param out the output stream to use
- * @param container the unordered_set of expressions to output to the stream
- * @return the stream
- */
-std::ostream& operator<<(
-    std::ostream& out,
-    const std::unordered_set<Expr, ExprHashFunction>& container) CVC4_PUBLIC;
-
-/**
- * Serialize a map of expressions to the given stream.
- *
- * @param out the output stream to use
- * @param container the map of expressions to output to the stream
- * @return the stream
- */
-template <typename V>
-std::ostream& operator<<(std::ostream& out,
-                         const std::map<Expr, V>& container) CVC4_PUBLIC;
-
-/**
- * Serialize an unordered_map of expressions to the given stream.
- *
- * @param out the output stream to use
- * @param container the unordered_map of expressions to output to the stream
- * @return the stream
- */
-template <typename V>
-std::ostream& operator<<(
-    std::ostream& out,
-    const std::unordered_map<Expr, V, ExprHashFunction>& container) CVC4_PUBLIC;
-
-// for hash_maps, hash_sets..
-struct ExprHashFunction {
-  size_t operator()(CVC4::Expr e) const;
-};/* struct ExprHashFunction */
-
-/**
- * Class encapsulating CVC4 expressions and methods for constructing new
- * expressions.
- */
-class CVC4_PUBLIC Expr {
-  friend class ExprManager;
-  friend class NodeManager;
-  friend class SmtEngine;
-  friend class TypeCheckingException;
-  friend class api::Solver;
-  friend class expr::ExportPrivate;
-  friend class prop::TheoryProxy;
-  friend class smt::SmtEnginePrivate;
-  friend std::ostream& CVC4::operator<<(std::ostream& out, const Expr& e);
-
-  /** The internal expression representation */
-  NodeTemplate<true>* d_node;
-
-  /** The responsible expression manager */
-  ExprManager* d_exprManager;
-
-  /**
-   * Constructor for internal purposes.
-   *
-   * @param em the expression manager that handles this expression
-   * @param node the actual expression node pointer
-   */
-  Expr(ExprManager* em, NodeTemplate<true>* node);
-
-public:
-
-  /** Default constructor, makes a null expression. */
-  Expr();
-
-  /**
-   * Copy constructor, makes a copy of a given expression
-   *
-   * @param e the expression to copy
-   */
-  Expr(const Expr& e);
-
-  /** Destructor */
-  ~Expr();
-
-  /**
-   * Assignment operator, makes a copy of the given expression. If the
-   * expression managers of the two expressions differ, the expression of
-   * the given expression will be used.
-   *
-   * @param e the expression to assign
-   * @return the reference to this expression after assignment
-   */
-  Expr& operator=(const Expr& e);
-
-  /**
-   * Syntactic comparison operator. Returns true if expressions belong to the
-   * same expression manager and are syntactically identical.
-   *
-   * @param e the expression to compare to
-   * @return true if expressions are syntactically the same, false otherwise
-   */
-  bool operator==(const Expr& e) const;
-
-  /**
-   * Syntactic disequality operator.
-   *
-   * @param e the expression to compare to
-   * @return true if expressions differ syntactically, false otherwise
-   */
-  bool operator!=(const Expr& e) const;
-
-  /**
-   * Order comparison operator. The only invariant on the order of expressions
-   * is that the expressions that were created sooner will be smaller in the
-   * ordering than all the expressions created later. Null expression is the
-   * smallest element of the ordering. The behavior of the operator is
-   * undefined if the expressions come from two different expression managers.
-   *
-   * @param e the expression to compare to
-   * @return true if this expression is smaller than the given one
-   */
-  bool operator<(const Expr& e) const;
-
-  /**
-   * Order comparison operator. The only invariant on the order of expressions
-   * is that the expressions that were created sooner will be smaller in the
-   * ordering than all the expressions created later. Null expression is the
-   * smallest element of the ordering. The behavior of the operator is
-   * undefined if the expressions come from two different expression managers.
-   *
-   * @param e the expression to compare to
-   * @return true if this expression is greater than the given one
-   */
-  bool operator>(const Expr& e) const;
-
-  /**
-   * Order comparison operator. The only invariant on the order of expressions
-   * is that the expressions that were created sooner will be smaller in the
-   * ordering than all the expressions created later. Null expression is the
-   * smallest element of the ordering. The behavior of the operator is
-   * undefined if the expressions come from two different expression managers.
-   *
-   * @param e the expression to compare to
-   * @return true if this expression is smaller or equal to the given one
-   */
-  bool operator<=(const Expr& e) const { return !(*this > e); }
-
-  /**
-   * Order comparison operator. The only invariant on the order of expressions
-   * is that the expressions that were created sooner will be smaller in the
-   * ordering than all the expressions created later. Null expression is the
-   * smallest element of the ordering. The behavior of the operator is
-   * undefined if the expressions come from two different expression managers.
-   *
-   * @param e the expression to compare to
-   * @return true if this expression is greater or equal to the given one
-   */
-  bool operator>=(const Expr& e) const { return !(*this < e); }
-
-  /**
-   * Get the ID of this expression (used for the comparison operators).
-   *
-   * @return an identifier uniquely identifying the value this
-   * expression holds.
-   */
-  uint64_t getId() const;
-
-  /**
-   * Returns the kind of the expression (AND, PLUS ...).
-   *
-   * @return the kind of the expression
-   */
-  Kind getKind() const;
-
-  /**
-   * Returns the number of children of this expression.
-   *
-   * @return the number of children
-   */
-  size_t getNumChildren() const;
-
-  /**
-   * Returns the i'th child of this expression.
-   *
-   * @param i the index of the child to retrieve
-   * @return the child
-   */
-  Expr operator[](unsigned i) const;
-
-  /**
-   * Returns the children of this Expr.
-   */
-  std::vector<Expr> getChildren() const {
-    return std::vector<Expr>(begin(), end());
-  }
-
-  /**
-   * Returns the Boolean negation of this Expr.
-   */
-  Expr notExpr() const;
-
-  /**
-   * Returns the conjunction of this expression and
-   * the given expression.
-   */
-  Expr andExpr(const Expr& e) const;
-
-  /**
-   * Returns the disjunction of this expression and
-   * the given expression.
-   */
-  Expr orExpr(const Expr& e) const;
-
-  /**
-   * Returns the exclusive disjunction of this expression and
-   * the given expression.
-   */
-  Expr xorExpr(const Expr& e) const;
-
-  /**
-   * Returns the Boolean equivalence of this expression and
-   * the given expression.
-   */
-  Expr eqExpr(const Expr& e) const;
-
-  /**
-   * Returns the implication of this expression and
-   * the given expression.
-   */
-  Expr impExpr(const Expr& e) const;
-
-  /**
-   * Returns the if-then-else expression with this expression
-   * as the Boolean condition and the given expressions as
-   * the "then" and "else" expressions.
-   */
-  Expr iteExpr(const Expr& then_e, const Expr& else_e) const;
-
-  /**
-   * Iterator type for the children of an Expr.
-   */
-  class const_iterator : public std::iterator<std::input_iterator_tag, Expr> {
-    ExprManager* d_exprManager;
-    void* d_iterator;
-
-    explicit const_iterator(ExprManager*, void*);
-
-    friend class Expr;// to access void* constructor
-
-  public:
-    const_iterator();
-    const_iterator(const const_iterator& it);
-    const_iterator& operator=(const const_iterator& it);
-    ~const_iterator();
-    bool operator==(const const_iterator& it) const;
-    bool operator!=(const const_iterator& it) const {
-      return !(*this == it);
-    }
-    const_iterator& operator++();
-    const_iterator operator++(int);
-    Expr operator*() const;
-  };/* class Expr::const_iterator */
-
-  /**
-   * Returns an iterator to the first child of this Expr.
-   */
-  const_iterator begin() const;
-
-  /**
-   * Returns an iterator to one-off-the-last child of this Expr.
-   */
-  const_iterator end() const;
-
-  /**
-   * Check if this is an expression that has an operator.
-   *
-   * @return true if this expression has an operator
-   */
-  bool hasOperator() const;
-
-  /**
-   * Get the operator of this expression.
-   *
-   * @throws IllegalArgumentException if it has no operator
-   * @return the operator of this expression
-   */
-  Expr getOperator() const;
-
-  /**
-   * Check if this is an expression is parameterized.
-   *
-   * @return true if this expression is parameterized.
-   *
-   * In detail, an expression that is parameterized is one that has an operator
-   * that must be provided in addition to its kind to construct it. For example,
-   * say we want to re-construct an Expr e where its children a1, ..., an are
-   * replaced by b1 ... bn. Then there are two cases:
-   * (1) If e is parametric, call:
-   *   ExprManager::mkExpr(e.getKind(), e.getOperator(), b1, ..., bn )
-   * (2) If e is not parametric, call:
-   *   ExprManager::mkExpr(e.getKind(), b1, ..., bn )
-   */
-  bool isParameterized() const;
-
-  /**
-   * Get the type for this Expr and optionally do type checking.
-   *
-   * Initial type computation will be near-constant time if
-   * type checking is not requested. Results are memoized, so that
-   * subsequent calls to getType() without type checking will be
-   * constant time.
-   *
-   * Initial type checking is linear in the size of the expression.
-   * Again, the results are memoized, so that subsequent calls to
-   * getType(), with or without type checking, will be constant
-   * time.
-   *
-   * NOTE: A TypeCheckingException can be thrown even when type
-   * checking is not requested. getType() will always return a
-   * valid and correct type and, thus, an exception will be thrown
-   * when no valid or correct type can be computed (e.g., if the
-   * arguments to a bit-vector operation aren't bit-vectors). When
-   * type checking is not requested, getType() will do the minimum
-   * amount of checking required to return a valid result.
-   *
-   * @param check whether we should check the type as we compute it
-   * (default: false)
-   */
-  Type getType(bool check = false) const;
-
-  /**
-   * Substitute "replacement" in for "e".
-   */
-  Expr substitute(Expr e, Expr replacement) const;
-
-  /**
-   * Substitute "replacements" in for "exes".
-   */
-  Expr substitute(const std::vector<Expr> exes,
-                  const std::vector<Expr>& replacements) const;
-
-  /**
-   * Substitute pairs of (ex,replacement) from the given map.
-   */
-  Expr substitute(const std::unordered_map<Expr, Expr, ExprHashFunction> map) const;
-
-  /**
-   * Returns the string representation of the expression.
-   * @return a string representation of the expression
-   */
-  std::string toString() const;
-
-  /**
-   * Outputs the string representation of the expression to the stream.
-   *
-   * @param out the stream to serialize this expression to
-   * @param toDepth the depth to which to print this expression, or -1
-   * to print it fully
-   * @param dag the dagification threshold to use (0 == off)
-   * @param language the language in which to output
-   */
-  void toStream(std::ostream& out,
-                int toDepth = -1,
-                size_t dag = 1,
-                OutputLanguage language = language::output::LANG_AUTO) const;
-
-  /**
-   * Check if this is a null expression.
-   *
-   * @return true if a null expression
-   */
-  bool isNull() const;
-
-  /**
-   * Check if this is an expression representing a variable.
-   *
-   * @return true if a variable expression
-   */
-  bool isVariable() const;
-
-  /**
-   * Check if this is an expression representing a constant.
-   *
-   * @return true if a constant expression
-   */
-  bool isConst() const;
-
-  /**
-   * Check if this expression contains a free variable.
-   *
-   * @return true if this node contains a free variable.
-   */
-  bool hasFreeVariable() const;
-
-  /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance)..
-   *
-   * It has been decided for now to hold off on implementations of
-   * these functions, as they may only be needed in CNF conversion,
-   * where it's pointless to do a lazy isAtomic determination by
-   * searching through the DAG, and storing it, since the result will
-   * only be used once.  For more details see the 4/27/2010 CVC4
-   * developer's meeting notes at:
-   *
-   * http://cvc4.cs.stanford.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29
-   */
-  // bool containsDecision(); // is "atomic"
-  // bool properlyContainsDecision(); // maybe not atomic but all children are
-
-  /** Extract a constant of type T */
-  template <class T>
-  const T& getConst() const;
-
-  /**
-   * Returns the expression reponsible for this expression.
-   */
-  ExprManager* getExprManager() const;
-
-  /**
-   * Maps this Expr into one for a different ExprManager, using
-   * variableMap for the translation and extending it with any new
-   * mappings.
-   */
-  Expr exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap, uint32_t flags = 0) const;
-
-  /**
-   * Very basic pretty printer for Expr.
-   * This is equivalent to calling e.getNode().printAst(...)
-   * @param out output stream to print to.
-   * @param indent number of spaces to indent the formula by.
-   */
-  void printAst(std::ostream& out, int indent = 0) const;
-
-private:
-
-  /**
-   * Pretty printer for use within gdb
-   * This is not intended to be used outside of gdb.
-   * This writes to the ostream Warning() and immediately flushes
-   * the ostream.
-   */
-  void debugPrint();
-
-  /**
-   * Returns the actual internal node.
-   * @return the internal node
-   */
-  NodeTemplate<true> getNode() const;
-
-  /**
-   * Returns the actual internal node as a TNode.
-   * @return the internal node
-   */
-  NodeTemplate<false> getTNode() const;
-  template <bool ref_count> friend class NodeTemplate;
-
-};/* class Expr */
-
-${getConst_instantiations}
-
-inline size_t ExprHashFunction::operator()(CVC4::Expr e) const {
-  return (size_t) e.getId();
-}
-
-}/* CVC4 namespace */
-
-#endif /* CVC4__EXPR_H */
diff --git a/src/expr/node.h b/src/expr/node.h
index 7e6324822..bb8c5618c 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -23,6 +23,7 @@
 #define CVC4__NODE_H
 
 #include <iostream>
+#include <map>
 #include <string>
 #include <unordered_map>
 #include <unordered_set>
@@ -32,7 +33,6 @@
 #include "base/check.h"
 #include "base/exception.h"
 #include "base/output.h"
-#include "expr/expr.h"
 #include "expr/expr_iomanip.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
@@ -170,8 +170,6 @@ class NodeTemplate {
    */
   friend class expr::NodeValue;
 
-  friend class expr::ExportPrivate;
-
   /** A convenient null-valued encapsulated pointer */
   static NodeTemplate s_null;
 
@@ -269,14 +267,6 @@ public:
   NodeTemplate(const NodeTemplate& node);
 
   /**
-   * Allow Exprs to become Nodes.  This permits flexible translation of
-   * Exprs -> Nodes inside the CVC4 library without exposing a toNode()
-   * function in the public interface, or requiring lots of "friend"
-   * relationships.
-   */
-  NodeTemplate(const Expr& e);
-
-  /**
    * Assignment operator for nodes, copies the relevant information from node
    * to this node.
    * @param node the node to copy
@@ -415,23 +405,6 @@ public:
   // bool containsDecision(); // is "atomic"
   // bool properlyContainsDecision(); // maybe not atomic but all children are
 
-
-  /**
-   * Convert this Node into an Expr using the currently-in-scope
-   * manager.  Essentially this is like an "operator Expr()" but we
-   * don't want it to compete with implicit conversions between e.g.
-   * Node and TNode, and we want internal-to-external interface
-   * (Node -> Expr) points to be explicit.  We could write an
-   * explicit Expr(Node) constructor---but that dirties the public
-   * interface.
-   */
-  inline Expr toExpr() const;
-
-  /**
-   * Convert an Expr into a Node.
-   */
-  static inline Node fromExpr(const Expr& e);
-
   /**
    * Returns true if this node represents a constant
    * @return true if const
@@ -1104,18 +1077,6 @@ NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate& e) {
 }
 
 template <bool ref_count>
-NodeTemplate<ref_count>::NodeTemplate(const Expr& e) {
-  Assert(e.d_node != NULL) << "Expecting a non-NULL expression value!";
-  Assert(e.d_node->d_nv != NULL) << "Expecting a non-NULL expression value!";
-  d_nv = e.d_node->d_nv;
-  // shouldn't ever fail
-  Assert(d_nv->d_rc > 0) << "Node constructed from Expr with rc == 0";
-  if(ref_count) {
-    d_nv->inc();
-  }
-}
-
-template <bool ref_count>
 NodeTemplate<ref_count>::~NodeTemplate() {
   Assert(d_nv != NULL) << "Expecting a non-NULL expression value!";
   if(ref_count) {
@@ -1459,18 +1420,6 @@ NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin,
   }
 }
 
-template <bool ref_count>
-inline Expr NodeTemplate<ref_count>::toExpr() const {
-  assertTNodeNotExpired();
-  return NodeManager::currentNM()->toExpr(*this);
-}
-
-// intentionally not defined for TNode
-template <>
-inline Node NodeTemplate<true>::fromExpr(const Expr& e) {
-  return NodeManager::fromExpr(e);
-}
-
 #ifdef CVC4_DEBUG
 /**
  * Pretty printer for use within gdb.  This is not intended to be used
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index c34aa0a87..2d5ed36fb 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -94,14 +94,13 @@ namespace attr {
 // attribute that stores the canonical bound variable list for function types
 typedef expr::Attribute<attr::LambdaBoundVarListTag, Node> LambdaBoundVarListAttr;
 
-NodeManager::NodeManager(ExprManager* exprManager)
+NodeManager::NodeManager()
     : d_statisticsRegistry(new StatisticsRegistry()),
       d_skManager(new SkolemManager),
       d_bvManager(new BoundVarManager),
       next_id(0),
       d_attrManager(new expr::attr::AttributeManager()),
-      d_exprManager(exprManager),
-      d_nodeUnderDeletion(NULL),
+      d_nodeUnderDeletion(nullptr),
       d_inReclaimZombies(false),
       d_abstractValueCount(0),
       d_skolemCounter(0)
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index d113c1458..348200b6e 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -22,8 +22,6 @@
 //#include "expr/attribute.h"
 #include "expr/node.h"
 #include "expr/type_node.h"
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
 
 #ifndef CVC4__NODE_MANAGER_H
 #define CVC4__NODE_MANAGER_H
@@ -90,9 +88,6 @@ class NodeManager
   friend class api::Solver;
   friend class expr::NodeValue;
   friend class expr::TypeChecker;
-  // friends so they can access mkVar() here, which is private
-  friend Expr ExprManager::mkVar(const std::string&, Type);
-  friend Expr ExprManager::mkVar(Type);
 
   template <unsigned nchild_thresh>
   friend class NodeBuilder;
@@ -134,9 +129,6 @@ class NodeManager
 
   expr::attr::AttributeManager* d_attrManager;
 
-  /** The associated ExprManager */
-  ExprManager* d_exprManager;
-
   /**
    * The node value we're currently freeing.  This unique node value
    * is permitted to have outstanding TNodes to it (in "soft"
@@ -292,14 +284,10 @@ class NodeManager
     // `d_zombies` uses the node id to hash and compare nodes. If `d_zombies`
     // already contains a node value with the same id as `nv`, but the pointers
     // are different, then the wrong `NodeManager` was in scope for one of the
-    // two nodes when it reached refcount zero. This can happen for example if
-    // you create a node with a `NodeManager` n1 and then call `Node::toExpr()`
-    // on that node while a different `NodeManager` n2 is in scope. When that
-    // `Expr` is deleted and the node reaches refcount zero in the `Expr`'s
-    // destructor, then `markForDeletion()` will be called on n2.
+    // two nodes when it reached refcount zero.
     Assert(d_zombies.find(nv) == d_zombies.end() || *d_zombies.find(nv) == nv);
 
-    d_zombies.insert(nv);  // FIXME multithreading
+    d_zombies.insert(nv);
 
     if(safeToReclaimZombies()) {
       if(d_zombies.size() > 5000) {
@@ -392,8 +380,7 @@ class NodeManager
   Node* mkVarPtr(const TypeNode& type);
 
  public:
-
-  explicit NodeManager(ExprManager* exprManager);
+  explicit NodeManager();
   ~NodeManager();
 
   /** The node manager in the current public-facing CVC4 library context */
@@ -1103,37 +1090,6 @@ class NodeManager
    */
   TypeNode getType(TNode n, bool check = false);
 
-  /**
-   * Convert a node to an expression.  Uses the ExprManager
-   * associated to this NodeManager.
-   */
-  inline Expr toExpr(TNode n);
-
-  /**
-   * Convert an expression to a node.
-   */
-  static inline Node fromExpr(const Expr& e);
-
-  /**
-   * Convert a node manager to an expression manager.
-   */
-  inline ExprManager* toExprManager();
-
-  /**
-   * Convert an expression manager to a node manager.
-   */
-  static inline NodeManager* fromExprManager(ExprManager* exprManager);
-
-  /**
-   * Convert a type node to a type.
-   */
-  inline Type toType(const TypeNode& tn);
-
-  /**
-   * Convert a type to a type node.
-   */
-  static inline TypeNode fromType(Type t);
-
   /** Reclaim zombies while there are more than k nodes in the pool (if possible).*/
   void reclaimZombiesUntil(uint32_t k);
 
@@ -1165,8 +1121,7 @@ class NodeManager
  * public-interface calls into the CVC4 library, where CVC4's notion
  * of the "current" <code>NodeManager</code> should be set to match
  * the calling context.  See, for example, the implementations of
- * public calls in the <code>ExprManager</code> and
- * <code>SmtEngine</code> classes.
+ * public calls in the <code>SmtEngine</code> class.
  *
  * The client must be careful to create and destroy
  * <code>NodeManagerScope</code> objects in a well-nested manner (such
@@ -1183,10 +1138,6 @@ class NodeManagerScope {
 public:
  NodeManagerScope(NodeManager* nm) : d_oldNodeManager(NodeManager::s_current)
  {
-   // There are corner cases where nm can be NULL and it's ok.
-   // For example, if you write { Expr e; }, then when the null
-   // Expr is destructed, there's no active node manager.
-   // Assert(nm != NULL);
    NodeManager::s_current = nm;
    Debug("current") << "node manager scope: " << NodeManager::s_current << "\n";
   }
@@ -1274,31 +1225,6 @@ inline void NodeManager::poolRemove(expr::NodeValue* nv) {
   d_nodeValuePool.erase(nv);// FIXME multithreading
 }
 
-inline Expr NodeManager::toExpr(TNode n) {
-  return Expr(d_exprManager, new Node(n));
-}
-
-inline Node NodeManager::fromExpr(const Expr& e) {
-  return e.getNode();
-}
-
-inline ExprManager* NodeManager::toExprManager() {
-  return d_exprManager;
-}
-
-inline NodeManager* NodeManager::fromExprManager(ExprManager* exprManager) {
-  return exprManager->getNodeManager();
-}
-
-inline Type NodeManager::toType(const TypeNode& tn)
-{
-  return Type(this, new TypeNode(tn));
-}
-
-inline TypeNode NodeManager::fromType(Type t) {
-  return *Type::getTypeNode(t);
-}
-
 }/* CVC4 namespace */
 
 #define CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
deleted file mode 100644
index baf3ddf8c..000000000
--- a/src/expr/type.cpp
+++ /dev/null
@@ -1,681 +0,0 @@
-/*********************                                                        */
-/*! \file type.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Dejan Jovanovic, Andrew Reynolds
- ** 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 Implementation of expression types
- **
- ** Implementation of expression types.
- **/
-#include "expr/type.h"
-
-#include <iostream>
-#include <sstream>
-#include <string>
-#include <vector>
-
-#include "base/exception.h"
-#include "expr/node_manager.h"
-#include "expr/node_manager_attributes.h"
-#include "expr/type_node.h"
-
-using namespace std;
-
-namespace CVC4 {
-
-ostream& operator<<(ostream& out, const Type& t) {
-  NodeManagerScope nms(t.d_nodeManager);
-  return out << *Type::getTypeNode(t);
-}
-
-Type Type::makeType(const TypeNode& typeNode) const {
-  return Type(d_nodeManager, new TypeNode(typeNode));
-}
-
-Type::Type(NodeManager* nm, TypeNode* node)
-    : d_typeNode(node), d_nodeManager(nm) {
-  // This does not require a NodeManagerScope as this is restricted to be an
-  // internal only pointer initialization call.
-}
-
-Type::Type() : d_typeNode(new TypeNode), d_nodeManager(NULL) {
-  // This does not require a NodeManagerScope as `new TypeNode` is backed by a
-  // static expr::NodeValue::null().
-}
-
-Type::Type(const Type& t) : d_typeNode(NULL), d_nodeManager(t.d_nodeManager) {
-  NodeManagerScope nms(d_nodeManager);
-  d_typeNode = new TypeNode(*t.d_typeNode);
-}
-
-Type::~Type() {
-  NodeManagerScope nms(d_nodeManager);
-  delete d_typeNode;
-}
-
-bool Type::isNull() const {
-  return d_typeNode->isNull();
-}
-
-Cardinality Type::getCardinality() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->getCardinality();
-}
-
-bool Type::isFinite() const
-{
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isFinite();
-}
-
-bool Type::isInterpretedFinite() const
-{
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isInterpretedFinite();
-}
-
-bool Type::isWellFounded() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isWellFounded();
-}
-
-bool Type::isFirstClass() const
-{
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isFirstClass();
-}
-
-bool Type::isFunctionLike() const
-{
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isFunctionLike();
-}
-
-Expr Type::mkGroundTerm() const {
-  NodeManagerScope nms(d_nodeManager);
-  Expr ret = d_typeNode->mkGroundTerm().toExpr();
-  if (ret.isNull())
-  {
-    IllegalArgument(this, "Cannot construct ground term!");
-  }
-  return ret;
-}
-
-Expr Type::mkGroundValue() const
-{
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->mkGroundValue().toExpr();
-}
-
-bool Type::isSubtypeOf(Type t) const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isSubtypeOf(*t.d_typeNode);
-}
-
-bool Type::isComparableTo(Type t) const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isComparableTo(*t.d_typeNode);
-}
-
-Type Type::getBaseType() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->getBaseType().toType();
-}
-
-Type& Type::operator=(const Type& t) {
-  PrettyCheckArgument(d_typeNode != NULL, this, "Unexpected NULL typenode pointer!");
-  PrettyCheckArgument(t.d_typeNode != NULL, t, "Unexpected NULL typenode pointer!");
-
-  if(this != &t) {
-    if(d_nodeManager == t.d_nodeManager) {
-      NodeManagerScope nms(d_nodeManager);
-      *d_typeNode = *t.d_typeNode;
-    } else {
-      // This happens more than you think---every time you set to or
-      // from the null Type.  It's tricky because each node manager
-      // must be in play at the right time.
-
-      NodeManagerScope nms1(d_nodeManager);
-      *d_typeNode = TypeNode::null();
-
-      NodeManagerScope nms2(t.d_nodeManager);
-      *d_typeNode = *t.d_typeNode;
-
-      d_nodeManager = t.d_nodeManager;
-    }
-  }
-  return *this;
-}
-
-bool Type::operator==(const Type& t) const {
-  NodeManagerScope nms(d_nodeManager);
-  return *d_typeNode == *t.d_typeNode;
-}
-
-bool Type::operator!=(const Type& t) const {
-  NodeManagerScope nms(d_nodeManager);
-  return *d_typeNode != *t.d_typeNode;
-}
-
-bool Type::operator<(const Type& t) const {
-  NodeManagerScope nms(d_nodeManager);
-  return *d_typeNode < *t.d_typeNode;
-}
-
-bool Type::operator<=(const Type& t) const {
-  NodeManagerScope nms(d_nodeManager);
-  return *d_typeNode <= *t.d_typeNode;
-}
-
-bool Type::operator>(const Type& t) const {
-  NodeManagerScope nms(d_nodeManager);
-  return *d_typeNode > *t.d_typeNode;
-}
-
-bool Type::operator>=(const Type& t) const {
-  NodeManagerScope nms(d_nodeManager);
-  return *d_typeNode >= *t.d_typeNode;
-}
-
-Type Type::substitute(const Type& type, const Type& replacement) const {
-  NodeManagerScope nms(d_nodeManager);
-  return makeType(d_typeNode->substitute(*type.d_typeNode,
-                                         *replacement.d_typeNode));
-}
-
-Type Type::substitute(const std::vector<Type>& types,
-                      const std::vector<Type>& replacements) const {
-  NodeManagerScope nms(d_nodeManager);
-
-  vector<TypeNode> typesNodes, replacementsNodes;
-
-  for(vector<Type>::const_iterator i = types.begin(),
-        iend = types.end();
-      i != iend;
-      ++i) {
-    typesNodes.push_back(*(*i).d_typeNode);
-  }
-
-  for(vector<Type>::const_iterator i = replacements.begin(),
-        iend = replacements.end();
-      i != iend;
-      ++i) {
-    replacementsNodes.push_back(*(*i).d_typeNode);
-  }
-
-  return makeType(d_typeNode->substitute(typesNodes.begin(),
-                                         typesNodes.end(),
-                                         replacementsNodes.begin(),
-                                         replacementsNodes.end()));
-}
-
-ExprManager* Type::getExprManager() const {
-  return d_nodeManager->toExprManager();
-}
-
-Type Type::exportTo(ExprManager* exprManager, ExprManagerMapCollection& vmap) const {
-  return ExprManager::exportType(*this, exprManager, vmap);
-}
-
-void Type::toStream(std::ostream& out) const {
-  NodeManagerScope nms(d_nodeManager);
-  out << *d_typeNode;
-  return;
-}
-
-string Type::toString() const {
-  NodeManagerScope nms(d_nodeManager);
-  stringstream ss;
-  ss << *d_typeNode;
-  return ss.str();
-}
-
-/** Is this the Boolean type? */
-bool Type::isBoolean() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isBoolean();
-}
-
-/** Is this the integer type? */
-bool Type::isInteger() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isInteger();
-}
-
-/** Is this the real type? */
-bool Type::isReal() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isReal();
-}
-
-/** Is this the string type? */
-bool Type::isString() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isString();
-}
-
-/** Is this the regexp type? */
-bool Type::isRegExp() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isRegExp();
-}
-
-/** Is this the rounding mode type? */
-bool Type::isRoundingMode() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isRoundingMode();
-}
-
-/** Is this the bit-vector type? */
-bool Type::isBitVector() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isBitVector();
-}
-
-/** Is this the floating-point type? */
-bool Type::isFloatingPoint() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isFloatingPoint();
-}
-
-/** Is this a datatype type? */
-bool Type::isDatatype() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isDatatype();
-}
-
-/** Is this the Constructor type? */
-bool Type::isConstructor() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isConstructor();
-}
-
-/** Is this the Selector type? */
-bool Type::isSelector() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isSelector();
-}
-
-/** Is this the Tester type? */
-bool Type::isTester() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isTester();
-}
-
-/** Is this a function type? */
-bool Type::isFunction() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isFunction();
-}
-
-/**
- * Is this a predicate type? NOTE: all predicate types are also
- * function types.
- */
-bool Type::isPredicate() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isPredicate();
-}
-
-/** Is this a tuple type? */
-bool Type::isTuple() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isTuple();
-}
-
-/** Is this a record type? */
-bool Type::isRecord() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isRecord();
-}
-
-/** Is this a symbolic expression type? */
-bool Type::isSExpr() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isSExpr();
-}
-
-/** Is this an array type? */
-bool Type::isArray() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isArray();
-}
-
-/** Is this a Set type? */
-bool Type::isSet() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isSet();
-}
-
-bool Type::isSequence() const
-{
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isSequence();
-}
-
-/** Is this a sort kind */
-bool Type::isSort() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isSort();
-}
-
-/** Cast to a sort type */
-bool Type::isSortConstructor() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isSortConstructor();
-}
-
-size_t FunctionType::getArity() const {
-  return d_typeNode->getNumChildren() - 1;
-}
-
-vector<Type> FunctionType::getArgTypes() const {
-  NodeManagerScope nms(d_nodeManager);
-  vector<Type> args;
-  vector<TypeNode> argNodes = d_typeNode->getArgTypes();
-  vector<TypeNode>::iterator it = argNodes.begin();
-  vector<TypeNode>::iterator it_end = argNodes.end();
-  for(; it != it_end; ++ it) {
-    args.push_back(makeType(*it));
-  }
-  return args;
-}
-
-Type FunctionType::getRangeType() const {
-  NodeManagerScope nms(d_nodeManager);
-  PrettyCheckArgument(isNull() || isFunction(), this);
-  return makeType(d_typeNode->getRangeType());
-}
-
-vector<Type> SExprType::getTypes() const {
-  NodeManagerScope nms(d_nodeManager);
-  vector<Type> types;
-  vector<TypeNode> typeNodes = d_typeNode->getSExprTypes();
-  vector<TypeNode>::iterator it = typeNodes.begin();
-  vector<TypeNode>::iterator it_end = typeNodes.end();
-  for(; it != it_end; ++ it) {
-    types.push_back(makeType(*it));
-  }
-  return types;
-}
-
-string SortType::getName() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->getAttribute(expr::VarNameAttr());
-}
-
-bool SortType::isParameterized() const {
-  return false;
-}
-
-/** Get the parameter types */
-std::vector<Type> SortType::getParamTypes() const {
-  vector<Type> params;
-  return params;
-}
-
-string SortConstructorType::getName() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->getAttribute(expr::VarNameAttr());
-}
-
-size_t SortConstructorType::getArity() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->getAttribute(expr::SortArityAttr());
-}
-
-SortType SortConstructorType::instantiate(const std::vector<Type>& params) const {
-  NodeManagerScope nms(d_nodeManager);
-  vector<TypeNode> paramsNodes;
-  for(vector<Type>::const_iterator i = params.begin(),
-        iend = params.end();
-      i != iend;
-      ++i) {
-    paramsNodes.push_back(*getTypeNode(*i));
-  }
-  return SortType(makeType(d_nodeManager->mkSort(*d_typeNode, paramsNodes)));
-}
-
-BooleanType::BooleanType(const Type& t) : Type(t)
-{
-  PrettyCheckArgument(isNull() || isBoolean(), this);
-}
-
-IntegerType::IntegerType(const Type& t) : Type(t)
-{
-  PrettyCheckArgument(isNull() || isInteger(), this);
-}
-
-RealType::RealType(const Type& t) : Type(t)
-{
-  PrettyCheckArgument(isNull() || isReal(), this);
-}
-
-StringType::StringType(const Type& t) : Type(t)
-{
-  PrettyCheckArgument(isNull() || isString(), this);
-}
-
-RegExpType::RegExpType(const Type& t) : Type(t)
-{
-  PrettyCheckArgument(isNull() || isRegExp(), this);
-}
-
-RoundingModeType::RoundingModeType(const Type& t) : Type(t)
-{
-  PrettyCheckArgument(isNull() || isRoundingMode(), this);
-}
-
-BitVectorType::BitVectorType(const Type& t) : Type(t)
-{
-  PrettyCheckArgument(isNull() || isBitVector(), this);
-}
-
-FloatingPointType::FloatingPointType(const Type& t) : Type(t)
-{
-  PrettyCheckArgument(isNull() || isFloatingPoint(), this);
-}
-
-DatatypeType::DatatypeType(const Type& t) : Type(t)
-{
-  PrettyCheckArgument(isNull() || isDatatype(), this);
-}
-
-ConstructorType::ConstructorType(const Type& t) : Type(t)
-{
-  PrettyCheckArgument(isNull() || isConstructor(), this);
-}
-
-SelectorType::SelectorType(const Type& t) : Type(t)
-{
-  PrettyCheckArgument(isNull() || isSelector(), this);
-}
-
-TesterType::TesterType(const Type& t) : Type(t)
-{
-  PrettyCheckArgument(isNull() || isTester(), this);
-}
-
-FunctionType::FunctionType(const Type& t) : Type(t)
-{
-  PrettyCheckArgument(isNull() || isFunction(), this);
-}
-
-SExprType::SExprType(const Type& t) : Type(t)
-{
-  PrettyCheckArgument(isNull() || isSExpr(), this);
-}
-
-ArrayType::ArrayType(const Type& t) : Type(t)
-{
-  PrettyCheckArgument(isNull() || isArray(), this);
-}
-
-SetType::SetType(const Type& t) : Type(t)
-{
-  PrettyCheckArgument(isNull() || isSet(), this);
-}
-
-SequenceType::SequenceType(const Type& t) : Type(t)
-{
-  PrettyCheckArgument(isNull() || isSequence(), this);
-}
-
-SortType::SortType(const Type& t) : Type(t)
-{
-  PrettyCheckArgument(isNull() || isSort(), this);
-}
-
-SortConstructorType::SortConstructorType(const Type& t)
-    : Type(t) {
-  PrettyCheckArgument(isNull() || isSortConstructor(), this);
-}
-
-unsigned BitVectorType::getSize() const {
-  return d_typeNode->getBitVectorSize();
-}
-
-unsigned FloatingPointType::getExponentSize() const {
-  return d_typeNode->getFloatingPointExponentSize();
-}
-
-unsigned FloatingPointType::getSignificandSize() const {
-  return d_typeNode->getFloatingPointSignificandSize();
-}
-
-Type ArrayType::getIndexType() const {
-  return makeType(d_typeNode->getArrayIndexType());
-}
-
-Type ArrayType::getConstituentType() const {
-  return makeType(d_typeNode->getArrayConstituentType());
-}
-
-Type SetType::getElementType() const {
-  return makeType(d_typeNode->getSetElementType());
-}
-
-Type SequenceType::getElementType() const
-{
-  return makeType(d_typeNode->getSequenceElementType());
-}
-
-DatatypeType ConstructorType::getRangeType() const {
-  return DatatypeType(makeType(d_typeNode->getConstructorRangeType()));
-}
-
-size_t ConstructorType::getArity() const {
-  return d_typeNode->getNumChildren() - 1;
-}
-
-std::vector<Type> ConstructorType::getArgTypes() const {
-  NodeManagerScope nms(d_nodeManager);
-  vector<Type> args;
-  vector<TypeNode> argNodes = d_typeNode->getArgTypes();
-  vector<TypeNode>::iterator it = argNodes.begin();
-  vector<TypeNode>::iterator it_end = argNodes.end();
-  for(; it != it_end; ++ it) {
-    args.push_back(makeType(*it));
-  }
-  return args;
-}
-
-bool DatatypeType::isParametric() const {
-  return d_typeNode->isParametricDatatype();
-}
-
-bool DatatypeType::isInstantiated() const {
-  return d_typeNode->isInstantiatedDatatype();
-}
-
-bool DatatypeType::isParameterInstantiated(unsigned n) const {
-  return d_typeNode->isParameterInstantiatedDatatype(n);
-}
-
-size_t DatatypeType::getArity() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->getNumChildren() - 1;
-}
-
-std::vector<Type> DatatypeType::getParamTypes() const {
-  NodeManagerScope nms(d_nodeManager);
-  vector<Type> params;
-  vector<TypeNode> paramNodes = d_typeNode->getParamTypes();
-  vector<TypeNode>::iterator it = paramNodes.begin();
-  vector<TypeNode>::iterator it_end = paramNodes.end();
-  for(; it != it_end; ++it) {
-    params.push_back(makeType(*it));
-  }
-  return params;
-}
-
-DatatypeType DatatypeType::instantiate(const std::vector<Type>& params) const {
-  NodeManagerScope nms(d_nodeManager);
-  TypeNode cons = d_nodeManager->mkTypeConst( (*d_typeNode)[0].getConst<DatatypeIndexConstant>() );
-  vector<TypeNode> paramsNodes;
-  paramsNodes.push_back( cons );
-  for(vector<Type>::const_iterator i = params.begin(),
-        iend = params.end();
-      i != iend;
-      ++i) {
-    paramsNodes.push_back(*getTypeNode(*i));
-  }
-  return DatatypeType(makeType(d_nodeManager->mkTypeNode(kind::PARAMETRIC_DATATYPE, paramsNodes)));
-}
-
-/** Get the length of a tuple type */
-size_t DatatypeType::getTupleLength() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->getTupleLength();
-}
-
-/** Get the constituent types of a tuple type */
-std::vector<Type> DatatypeType::getTupleTypes() const {
-  NodeManagerScope nms(d_nodeManager);
-  std::vector< TypeNode > vec = d_typeNode->getTupleTypes();
-  std::vector< Type > vect;
-  for( unsigned i=0; i<vec.size(); i++ ){
-    vect.push_back( vec[i].toType() );
-  }
-  return vect;
-}
-
-DatatypeType SelectorType::getDomain() const {
-  return DatatypeType(makeType((*d_typeNode)[0]));
-}
-
-Type SelectorType::getRangeType() const {
-  return makeType((*d_typeNode)[1]);
-}
-
-DatatypeType TesterType::getDomain() const {
-  return DatatypeType(makeType((*d_typeNode)[0]));
-}
-
-BooleanType TesterType::getRangeType() const {
-  return BooleanType(makeType(d_nodeManager->booleanType()));
-}
-
-/* - not in release 1.0
-Expr PredicateSubtype::getPredicate() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->getSubtypePredicate().toExpr();
-}
-
-Type PredicateSubtype::getParentType() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->getSubtypeParentType().toType();
-}
-*/
-
-size_t TypeHashFunction::operator()(const Type& t) const {
-  return TypeNodeHashFunction()(NodeManager::fromType(t));
-}
-
-}/* CVC4 namespace */
diff --git a/src/expr/type.h b/src/expr/type.h
deleted file mode 100644
index 8f8ccc1bf..000000000
--- a/src/expr/type.h
+++ /dev/null
@@ -1,695 +0,0 @@
-/*********************                                                        */
-/*! \file type.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Dejan Jovanovic, Andrew Reynolds
- ** 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 Interface for expression types.
- **
- ** Interface for expression types
- **/
-
-#include "cvc4_public.h"
-
-#ifndef CVC4__TYPE_H
-#define CVC4__TYPE_H
-
-#include <climits>
-#include <string>
-#include <vector>
-
-#include "util/cardinality.h"
-
-namespace CVC4 {
-
-class NodeManager;
-class CVC4_PUBLIC ExprManager;
-class Expr;
-class TypeNode;
-struct CVC4_PUBLIC ExprManagerMapCollection;
-
-class SmtEngine;
-
-template <bool ref_count>
-class NodeTemplate;
-
-class BooleanType;
-class IntegerType;
-class RealType;
-class StringType;
-class RegExpType;
-class RoundingModeType;
-class BitVectorType;
-class ArrayType;
-class SetType;
-class DatatypeType;
-class ConstructorType;
-class SelectorType;
-class TesterType;
-class FunctionType;
-class SExprType;
-class SortType;
-class SortConstructorType;
-class Type;
-
-/** Hash function for Types */
-struct CVC4_PUBLIC TypeHashFunction {
-  /** Return a hash code for type t */
-  size_t operator()(const CVC4::Type& t) const;
-};/* struct TypeHashFunction */
-
-/**
- * Output operator for types
- * @param out the stream to output to
- * @param t the type to output
- * @return the stream
- */
-std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC;
-
-namespace expr {
-  TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* nm, ExprManagerMapCollection& vmap);
-}/* CVC4::expr namespace */
-
-/**
- * Class encapsulating CVC4 expression types.
- */
-class CVC4_PUBLIC Type {
-
-  friend class SmtEngine;
-  friend class ExprManager;
-  friend class NodeManager;
-  friend class TypeNode;
-  friend std::ostream& CVC4::operator<<(std::ostream& out, const Type& t);
-  friend TypeNode expr::exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* nm, ExprManagerMapCollection& vmap);
-
-protected:
-
-  /** The internal expression representation */
-  TypeNode* d_typeNode;
-
-  /** The responsible expression manager */
-  NodeManager* d_nodeManager;
-
-  /**
-   * Construct a new type given the typeNode, for internal use only.
-   * @param typeNode the TypeNode to use
-   * @return the Type corresponding to the TypeNode
-   */
-  Type makeType(const TypeNode& typeNode) const;
-
-  /**
-   * Constructor for internal purposes.
-   * @param em the expression manager that handles this expression
-   * @param typeNode the actual TypeNode pointer for this type
-   */
-  Type(NodeManager* em, TypeNode* typeNode);
-
-  /** Accessor for derived classes */
-  static TypeNode* getTypeNode(const Type& t) { return t.d_typeNode; }
- public:
-  /** Force a virtual destructor for safety. */
-  virtual ~Type();
-
-  /** Default constructor */
-  Type();
-
-  /**
-   * Copy constructor.
-   * @param t the type to make a copy of
-   */
-  Type(const Type& t);
-
-  /**
-   * Check whether this is a null type
-   * @return true if type is null
-   */
-  bool isNull() const;
-
-  /**
-   * Return the cardinality of this type.
-   */
-  Cardinality getCardinality() const;
-
-  /**
-   * Is this type finite? This assumes uninterpreted sorts have infinite
-   * cardinality.
-   */
-  bool isFinite() const;
-
-  /**
-   * Is this type interpreted as being finite.
-   * If finite model finding is enabled, this assumes all uninterpreted sorts
-   *   are interpreted as finite.
-   */
-  bool isInterpretedFinite() const;
-
-  /**
-   * Is this a well-founded type?
-   */
-  bool isWellFounded() const;
-
-  /**
-   * Is this a first-class type?
-   *
-   * First-class types are types for which:
-   * (1) we handle equalities between terms of that type, and
-   * (2) they are allowed to be parameters of parametric types (e.g. index or
-   * element types of arrays).
-   *
-   * Examples of types that are not first-class include constructor types,
-   * selector types, tester types, regular expressions and SExprs.
-   */
-  bool isFirstClass() const;
-
-  /**
-   * Is this a function-LIKE type?
-   *
-   * Anything function-like except arrays (e.g., datatype selectors) is
-   * considered a function here. Function-like terms can not be the argument
-   * or return value for any term that is function-like.
-   * This is mainly to avoid higher order.
-   *
-   * Note that arrays are explicitly not considered function-like here.
-   *
-   * @return true if this is a function-like type
-   */
-  bool isFunctionLike() const;
-
-  /**
-   * Construct and return a ground term for this Type.  Throws an
-   * exception if this type is not well-founded.
-   */
-  Expr mkGroundTerm() const;
-
-  /**
-   * Construct and return a ground value for this Type.  Throws an
-   * exception if this type is not well-founded.
-   *
-   * This is the same as mkGroundTerm, but constructs a constant value instead
-   * of a canonical ground term. These two notions typically coincide. However,
-   * for uninterpreted sorts, they do not: mkGroundTerm returns a fresh variable
-   * whereas mkValue returns an uninterpreted constant. The motivation for
-   * mkGroundTerm is that unintepreted constants should never appear in lemmas.
-   * The motivation for mkGroundValue is for e.g. type enumeration and model
-   * construction.
-   */
-  Expr mkGroundValue() const;
-
-  /**
-   * Is this type a subtype of the given type?
-   */
-  bool isSubtypeOf(Type t) const;
-
-  /**
-   * Is this type comparable to the given type (i.e., do they share
-   * a common ancestor in the subtype tree)?
-   */
-  bool isComparableTo(Type t) const;
-
-  /**
-   * Get the most general base type of this type.
-   */
-  Type getBaseType() const;
-
-  /**
-   * Substitution of Types.
-   */
-  Type substitute(const Type& type, const Type& replacement) const;
-
-  /**
-   * Simultaneous substitution of Types.
-   */
-  Type substitute(const std::vector<Type>& types,
-                  const std::vector<Type>& replacements) const;
-
-  /**
-   * Get this type's ExprManager.
-   */
-  ExprManager* getExprManager() const;
-
-  /**
-   * Exports this type into a different ExprManager.
-   */
-  Type exportTo(ExprManager* exprManager, ExprManagerMapCollection& vmap) const;
-
-  /**
-   * Assignment operator.
-   * @param t the type to assign to this type
-   * @return this type after assignment.
-   */
-  Type& operator=(const Type& t);
-
-  /**
-   * Comparison for structural equality.
-   * @param t the type to compare to
-   * @returns true if the types are equal
-   */
-  bool operator==(const Type& t) const;
-
-  /**
-   * Comparison for structural disequality.
-   * @param t the type to compare to
-   * @returns true if the types are not equal
-   */
-  bool operator!=(const Type& t) const;
-
-  /**
-   * An ordering on Types so they can be stored in maps, etc.
-   */
-  bool operator<(const Type& t) const;
-
-  /**
-   * An ordering on Types so they can be stored in maps, etc.
-   */
-  bool operator<=(const Type& t) const;
-
-  /**
-   * An ordering on Types so they can be stored in maps, etc.
-   */
-  bool operator>(const Type& t) const;
-
-  /**
-   * An ordering on Types so they can be stored in maps, etc.
-   */
-  bool operator>=(const Type& t) const;
-
-  /**
-   * Is this the Boolean type?
-   * @return true if the type is a Boolean type
-   */
-  bool isBoolean() const;
-
-  /**
-   * Is this the integer type?
-   * @return true if the type is a integer type
-   */
-  bool isInteger() const;
-
-  /**
-   * Is this the real type?
-   * @return true if the type is a real type
-   */
-  bool isReal() const;
-
-  /**
-   * Is this the string type?
-   * @return true if the type is the string type
-   */
-  bool isString() const;
-
-  /**
-   * Is this the regexp type?
-   * @return true if the type is the regexp type
-   */
-  bool isRegExp() const;
-
-  /**
-   * Is this the rounding mode type?
-   * @return true if the type is the rounding mode type
-   */
-  bool isRoundingMode() const;
-
-  /**
-   * Is this the bit-vector type?
-   * @return true if the type is a bit-vector type
-   */
-  bool isBitVector() const;
-
-  /**
-   * Is this the floating-point type?
-   * @return true if the type is a floating-point type
-   */
-  bool isFloatingPoint() const;
-
-  /**
-   * Is this a function type?
-   * @return true if the type is a function type
-   */
-  bool isFunction() const;
-
-  /**
-   * Is this a predicate type, i.e. if it's a function type mapping to Boolean.
-   * All predicate types are also function types.
-   * @return true if the type is a predicate type
-   */
-  bool isPredicate() const;
-
-  /**
-   * Is this a tuple type?
-   * @return true if the type is a tuple type
-   */
-  bool isTuple() const;
-
-  /**
-   * Is this a record type?
-   * @return true if the type is a record type
-   */
-  bool isRecord() const;
-
-  /**
-   * Is this a symbolic expression type?
-   * @return true if the type is a symbolic expression type
-   */
-  bool isSExpr() const;
-
-  /**
-   * Is this an array type?
-   * @return true if the type is a array type
-   */
-  bool isArray() const;
-
-  /**
-   * Is this a Set type?
-   * @return true if the type is a Set type
-   */
-  bool isSet() const;
-
-  /**
-   * Is this a Sequence type?
-   * @return true if the type is a Sequence type
-   */
-  bool isSequence() const;
-
-  /**
-   * Is this a datatype type?
-   * @return true if the type is a datatype type
-   */
-  bool isDatatype() const;
-
-  /**
-   * Is this a constructor type?
-   * @return true if the type is a constructor type
-   */
-  bool isConstructor() const;
-
-  /**
-   * Is this a selector type?
-   * @return true if the type is a selector type
-   */
-  bool isSelector() const;
-
-  /**
-   * Is this a tester type?
-   * @return true if the type is a tester type
-   */
-  bool isTester() const;
-
-  /**
-   * Is this a sort kind?
-   * @return true if this is a sort kind
-   */
-  bool isSort() const;
-
-  /**
-   * Is this a sort constructor kind?
-   * @return true if this is a sort constructor kind
-   */
-  bool isSortConstructor() const;
-
-  /**
-   * Is this a predicate subtype?
-   * @return true if this is a predicate subtype
-   */
-  // not in release 1.0
-  //bool isPredicateSubtype() const;
-
-  /**
-   * Is this an integer subrange type?
-   * @return true if this is an integer subrange type
-   */
-  //bool isSubrange() const;
-
-  /**
-   * Outputs a string representation of this type to the stream.
-   * @param out the stream to output to
-   */
-  void toStream(std::ostream& out) const;
-
-  /**
-   * Constructs a string representation of this type.
-   */
-  std::string toString() const;
-};/* class Type */
-
-/** Singleton class encapsulating the Boolean type. */
-class CVC4_PUBLIC BooleanType : public Type {
- public:
-  /** Construct from the base type */
-  BooleanType(const Type& type = Type());
-};/* class BooleanType */
-
-/** Singleton class encapsulating the integer type. */
-class CVC4_PUBLIC IntegerType : public Type {
- public:
-  /** Construct from the base type */
-  IntegerType(const Type& type = Type());
-};/* class IntegerType */
-
-/** Singleton class encapsulating the real type. */
-class CVC4_PUBLIC RealType : public Type {
- public:
-  /** Construct from the base type */
-  RealType(const Type& type = Type());
-};/* class RealType */
-
-/** Singleton class encapsulating the string type. */
-class CVC4_PUBLIC StringType : public Type {
- public:
-  /** Construct from the base type */
-  StringType(const Type& type);
-};/* class StringType */
-
-/** Singleton class encapsulating the string type. */
-class CVC4_PUBLIC RegExpType : public Type {
- public:
-  /** Construct from the base type */
-  RegExpType(const Type& type);
-};/* class RegExpType */
-
-/** Singleton class encapsulating the rounding mode type. */
-class CVC4_PUBLIC RoundingModeType : public Type {
- public:
-  /** Construct from the base type */
-  RoundingModeType(const Type& type = Type());
-};/* class RoundingModeType */
-
-/** Class encapsulating a function type. */
-class CVC4_PUBLIC FunctionType : public Type {
- public:
-  /** Construct from the base type */
-  FunctionType(const Type& type = Type());
-
-  /** Get the arity of the function type */
-  size_t getArity() const;
-
-  /** Get the argument types */
-  std::vector<Type> getArgTypes() const;
-
-  /** Get the range type (i.e., the type of the result). */
-  Type getRangeType() const;
-};/* class FunctionType */
-
-/** Class encapsulating a sexpr type. */
-class CVC4_PUBLIC SExprType : public Type {
- public:
-  /** Construct from the base type */
-  SExprType(const Type& type = Type());
-
-  /** Get the constituent types */
-  std::vector<Type> getTypes() const;
-};/* class SExprType */
-
-/** Class encapsulating an array type. */
-class CVC4_PUBLIC ArrayType : public Type {
- public:
-  /** Construct from the base type */
-  ArrayType(const Type& type = Type());
-
-  /** Get the index type */
-  Type getIndexType() const;
-
-  /** Get the constituent type */
-  Type getConstituentType() const;
-};/* class ArrayType */
-
-/** Class encapsulating a set type. */
-class CVC4_PUBLIC SetType : public Type {
- public:
-  /** Construct from the base type */
-  SetType(const Type& type = Type());
-
-  /** Get the element type */
-  Type getElementType() const;
-}; /* class SetType */
-
-/** Class encapsulating a sequence type. */
-class CVC4_PUBLIC SequenceType : public Type
-{
- public:
-  /** Construct from the base type */
-  SequenceType(const Type& type = Type());
-
-  /** Get the element type */
-  Type getElementType() const;
-}; /* class SetType */
-
-/** Class encapsulating a user-defined sort. */
-class CVC4_PUBLIC SortType : public Type {
- public:
-  /** Construct from the base type */
-  SortType(const Type& type = Type());
-
-  /** Get the name of the sort */
-  std::string getName() const;
-
-  /** Is this type parameterized? */
-  bool isParameterized() const;
-
-  /** Get the parameter types */
-  std::vector<Type> getParamTypes() const;
-
-};/* class SortType */
-
-/** Class encapsulating a user-defined sort constructor. */
-class CVC4_PUBLIC SortConstructorType : public Type {
- public:
-  /** Construct from the base type */
-  SortConstructorType(const Type& type = Type());
-
-  /** Get the name of the sort constructor */
-  std::string getName() const;
-
-  /** Get the arity of the sort constructor */
-  size_t getArity() const;
-
-  /** Instantiate a sort using this sort constructor */
-  SortType instantiate(const std::vector<Type>& params) const;
-
-};/* class SortConstructorType */
-
-/** Class encapsulating the bit-vector type. */
-class CVC4_PUBLIC BitVectorType : public Type {
- public:
-  /** Construct from the base type */
-  BitVectorType(const Type& type = Type());
-
-  /**
-   * Returns the size of the bit-vector type.
-   * @return the width of the bit-vector type (> 0)
-   */
-  unsigned getSize() const;
-
-};/* class BitVectorType */
-
-/** Class encapsulating the floating point type. */
-class CVC4_PUBLIC FloatingPointType : public Type {
- public:
-  /** Construct from the base type */
-  FloatingPointType(const Type& type = Type());
-
-  /**
-   * Returns the size of the floating-point exponent type.
-   * @return the width of the floating-point exponent type (> 0)
-   */
-  unsigned getExponentSize() const;
-
-  /**
-   * Returns the size of the floating-point significand type.
-   * @return the width of the floating-point significand type (> 0)
-   */
-  unsigned getSignificandSize() const;
-
-};/* class FloatingPointType */
-
-/** Class encapsulating the datatype type */
-class CVC4_PUBLIC DatatypeType : public Type {
- public:
-  /** Construct from the base type */
-  DatatypeType(const Type& type = Type());
-
-  /** Is this datatype parametric? */
-  bool isParametric() const;
-  /**
-   * Has this datatype been fully instantiated ?
-   *
-   * @return true if this datatype is not parametric or, if it is, it
-   * has been fully instantiated
-   */
-  bool isInstantiated() const;
-
-  /** Has this datatype been instantiated for parameter `n` ? */
-  bool isParameterInstantiated(unsigned n) const;
-
-  /** Get the parameter types */
-  std::vector<Type> getParamTypes() const;
-
-  /** Get the arity of the datatype constructor */
-  size_t getArity() const;
-
-  /** Instantiate a datatype using this datatype constructor */
-  DatatypeType instantiate(const std::vector<Type>& params) const;
-
-  /** Get the length of a tuple type */
-  size_t getTupleLength() const;
-
-  /** Get the constituent types of a tuple type */
-  std::vector<Type> getTupleTypes() const;
-
-};/* class DatatypeType */
-
-/** Class encapsulating the constructor type. */
-class CVC4_PUBLIC ConstructorType : public Type {
- public:
-  /** Construct from the base type */
-  ConstructorType(const Type& type = Type());
-
-  /** Get the range type */
-  DatatypeType getRangeType() const;
-
-  /** Get the argument types */
-  std::vector<Type> getArgTypes() const;
-
-  /** Get the number of constructor arguments */
-  size_t getArity() const;
-
-};/* class ConstructorType */
-
-/** Class encapsulating the Selector type. */
-class CVC4_PUBLIC SelectorType : public Type {
- public:
-  /** Construct from the base type */
-  SelectorType(const Type& type = Type());
-
-  /** Get the domain type for this selector (the datatype type) */
-  DatatypeType getDomain() const;
-
-  /** Get the range type for this selector (the field type) */
-  Type getRangeType() const;
-
-};/* class SelectorType */
-
-/** Class encapsulating the Tester type. */
-class CVC4_PUBLIC TesterType : public Type {
- public:
-  /** Construct from the base type */
-  TesterType(const Type& type = Type());
-
-  /** Get the type that this tester tests (the datatype type) */
-  DatatypeType getDomain() const;
-
-  /**
-   * Get the range type for this tester (included for sake of
-   * interface completeness), but doesn't give useful information).
-   */
-  BooleanType getRangeType() const;
-
-};/* class TesterType */
-
-}/* CVC4 namespace */
-
-#endif /* CVC4__TYPE_H */
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 63c26f5e9..15cfeede6 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -404,17 +404,6 @@ public:
   }
 
   /**
-   * Convert this TypeNode into a Type using the currently-in-scope
-   * manager.
-   */
-  inline Type toType() const;
-
-  /**
-   * Convert a Type into a TypeNode.
-   */
-  inline static TypeNode fromType(const Type& t);
-
-  /**
    * Returns the cardinality of this type.
    *
    * @return a finite or infinite cardinality
@@ -772,16 +761,6 @@ typedef TypeNode::HashFunction TypeNodeHashFunction;
 
 namespace CVC4 {
 
-inline Type TypeNode::toType() const
-{
-  return NodeManager::currentNM()->toType(*this);
-}
-
-inline TypeNode TypeNode::fromType(const Type& t) {
-  NodeManagerScope scope(t.d_nodeManager);
-  return NodeManager::fromType(t);
-}
-
 inline TypeNode
 TypeNode::substitute(const TypeNode& type,
                      const TypeNode& replacement) const {
diff --git a/src/expr/variable_type_map.h b/src/expr/variable_type_map.h
deleted file mode 100644
index afccac13f..000000000
--- a/src/expr/variable_type_map.h
+++ /dev/null
@@ -1,63 +0,0 @@
-/*********************                                                        */
-/*! \file variable_type_map.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Tim King, Mathias Preiner
- ** 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 [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_public.h"
-
-#ifndef CVC4__VARIABLE_TYPE_MAP_H
-#define CVC4__VARIABLE_TYPE_MAP_H
-
-#include <unordered_map>
-
-#include "expr/expr.h"
-
-namespace CVC4 {
-
-class Expr;
-struct ExprHashFunction;
-class Type;
-struct TypeHashFunction;
-
-class CVC4_PUBLIC VariableTypeMap {
-  /**
-   * A map Expr -> Expr, intended to be used for a mapping of variables
-   * between two ExprManagers.
-   */
-  std::unordered_map<Expr, Expr, ExprHashFunction> d_variables;
-
-  /**
-   * A map Type -> Type, intended to be used for a mapping of types
-   * between two ExprManagers.
-   */
-  std::unordered_map<Type, Type, TypeHashFunction> d_types;
-
-public:
-  Expr& operator[](Expr e) { return d_variables[e]; }
-  Type& operator[](Type t) { return d_types[t]; }
-
-};/* class VariableTypeMap */
-
-typedef std::unordered_map<uint64_t, uint64_t> VarMap;
-
-struct CVC4_PUBLIC ExprManagerMapCollection {
-  VariableTypeMap d_typeMap;
-  VarMap d_to;
-  VarMap d_from;
-};/* struct ExprManagerMapCollection */
-
-}/* CVC4 namespace */
-
-#endif /* CVC4__VARIABLE_MAP_H */