Remove old .orig files that were added to the repository.

3 files changed, 0 insertions, 3097 deletions

diff --git a/src/expr/expr_manager_template.cpp.orig b/src/expr/expr_manager_template.cpp.orig
deleted file mode 100644
index c5249075b..000000000
--- a/src/expr/expr_manager_template.cpp.orig
+++ /dev/null
@@ -1,1027 +0,0 @@
-/*********************                                                        */
-/*! \file expr_manager_template.cpp
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Dejan Jovanovic, Christopher L. Conway
- ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** 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/node_manager.h"
-#include "expr/expr_manager.h"
-#include "expr/variable_type_map.h"
-#include "options/options.h"
-#include "util/statistics_registry.h"
-
-#include <map>
-
-${includes}
-
-// This is a hack, but an important one: if there's an error, the
-// compiler directs the user to the template file instead of the
-// generated one.  We don't want the user to modify the generated one,
-// since it'll get overwritten on a later build.
-#line 32 "${template}"
-
-#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* typeNode = Type::getTypeNode(type); \
-    TypeConstant type = typeNode->getKind() == kind::TYPE_CONSTANT ? typeNode->getConst<TypeConstant>() : LAST_TYPE; \
-    if (d_exprStatisticsVars[type] == NULL) { \
-      stringstream statName; \
-      if (type == LAST_TYPE) { \
-        statName << "expr::ExprManager::" << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") << ":Parameterized type"; \
-      } else { \
-        statName << "expr::ExprManager::" << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") << ":" << type; \
-      } \
-      d_exprStatisticsVars[type] = new IntStat(statName.str(), 0); \
-      d_nodeManager->getStatisticsRegistry()->registerStat_(d_exprStatisticsVars[type]); \
-    } \
-    ++ *(d_exprStatisticsVars[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(const Options& options) :
-  d_nodeManager(new NodeManager(this, options)) {
-#ifdef CVC4_STATISTICS_ON
-  for (unsigned i = 0; i < LAST_TYPE; ++ i) {
-    d_exprStatisticsVars[i] = NULL;
-  }
-  for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
-    d_exprStatistics[i] = NULL;
-  }
-#endif
-}
-
-ExprManager::~ExprManager() throw() {
-  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;
-  }
-}
-
-StatisticsRegistry* ExprManager::getStatisticsRegistry() throw() {
-  return d_nodeManager->getStatisticsRegistry();
-}
-
-const Options& ExprManager::getOptions() const {
-  return d_nodeManager->getOptions();
-}
-
-ResourceManager* ExprManager::getResourceManager() throw() {
-  return d_nodeManager->getResourceManager();
-}
-
-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())));
-}
-
-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())));
-}
-
-Expr ExprManager::mkExpr(Kind kind, Expr child1) {
-  const kind::MetaKind mk = kind::metaKindOf(kind);
-  const unsigned n = 1 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
-  CheckArgument(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().");
-  CheckArgument(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);
-  CheckArgument(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().");
-  CheckArgument(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);
-  CheckArgument(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().");
-  CheckArgument(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);
-  CheckArgument(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().");
-  CheckArgument(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);
-  CheckArgument(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().");
-  CheckArgument(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 kind::MetaKind mk = kind::metaKindOf(kind);
-  const unsigned n = children.size() - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
-  CheckArgument(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().");
-  CheckArgument(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;
-  CheckArgument(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().");
-  CheckArgument(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 unsigned n = 0;
-  Kind kind = NodeManager::operatorToKind(opExpr.getNode());
-  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
-                "This Expr constructor is for parameterized kinds only");
-  CheckArgument(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()));
-  } 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());
-  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
-                "This Expr constructor is for parameterized kinds only");
-  CheckArgument(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());
-  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
-                "This Expr constructor is for parameterized kinds only");
-  CheckArgument(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());
-  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
-                "This Expr constructor is for parameterized kinds only");
-  CheckArgument(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());
-  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
-                "This Expr constructor is for parameterized kinds only");
-  CheckArgument(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());
-  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
-                "This Expr constructor is for parameterized kinds only");
-  CheckArgument(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());
-  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
-                "This Expr constructor is for parameterized kinds only");
-  CheckArgument(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();
-}
-
-/** 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))));
-}
-
-TupleType ExprManager::mkTupleType(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 TupleType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes))));
-}
-
-RecordType ExprManager::mkRecordType(const Record& rec) {
-  NodeManagerScope nms(d_nodeManager);
-  return RecordType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkRecordType(rec))));
-}
-
-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))));
-}
-
-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))));
-}
-
-DatatypeType ExprManager::mkDatatypeType(const Datatype& datatype) {
-  // Not worth a special implementation; this doesn't need to be fast
-  // code anyway.
-  vector<Datatype> datatypes;
-  datatypes.push_back(datatype);
-  vector<DatatypeType> result = mkMutualDatatypeTypes(datatypes);
-  Assert(result.size() == 1);
-  return result.front();
-}
-
-std::vector<DatatypeType>
-ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
-  return mkMutualDatatypeTypes(datatypes, set<Type>());
-}
-
-std::vector<DatatypeType>
-ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
-                                   const std::set<Type>& unresolvedTypes) {
-  NodeManagerScope nms(d_nodeManager);
-  std::map<std::string, DatatypeType> nameResolutions;
-  std::vector<DatatypeType> dtts;
-
-  // First do some sanity checks, set up the final Type to be used for
-  // each datatype, and set up the "named resolutions" used to handle
-  // simple self- and mutual-recursion, for example in the definition
-  // "nat = succ(pred:nat) | zero", a named resolution can handle the
-  // pred selector.
-  for(std::vector<Datatype>::const_iterator i = datatypes.begin(),
-        i_end = datatypes.end();
-      i != i_end;
-      ++i) {
-    TypeNode* typeNode;
-    if( (*i).getNumParameters() == 0 ) {
-      typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i));
-    } else {
-      TypeNode cons = d_nodeManager->mkTypeConst(*i);
-      std::vector< TypeNode > params;
-      params.push_back( cons );
-      for( unsigned int ip = 0; ip < (*i).getNumParameters(); ++ip ) {
-        params.push_back( TypeNode::fromType( (*i).getParameter( ip ) ) );
-      }
-
-      typeNode = new TypeNode(d_nodeManager->mkTypeNode(kind::PARAMETRIC_DATATYPE, params));
-    }
-    Type type(d_nodeManager, typeNode);
-    DatatypeType dtt(type);
-    CheckArgument(nameResolutions.find((*i).getName()) == nameResolutions.end(),
-                  datatypes,
-                  "cannot construct two datatypes at the same time "
-                  "with the same name `%s'",
-                  (*i).getName().c_str());
-    nameResolutions.insert(std::make_pair((*i).getName(), dtt));
-    dtts.push_back(dtt);
-  }
-
-  // Second, set up the type substitution map for complex type
-  // resolution (e.g. if "list" is the type we're defining, and it has
-  // a selector of type "ARRAY INT OF list", this can't be taken care
-  // of using the named resolutions that we set up above.  A
-  // preliminary array type was set up, and now needs to have "list"
-  // substituted in it for the correct type.
-  //
-  // @TODO get rid of named resolutions altogether and handle
-  // everything with these resolutions?
-  std::vector< SortConstructorType > paramTypes;
-  std::vector< DatatypeType > paramReplacements;
-  std::vector<Type> placeholders;// to hold the "unresolved placeholders"
-  std::vector<Type> replacements;// to hold our final, resolved types
-  for(std::set<Type>::const_iterator i = unresolvedTypes.begin(),
-        i_end = unresolvedTypes.end();
-      i != i_end;
-      ++i) {
-    std::string name;
-    if( (*i).isSort() ) {
-      name = SortType(*i).getName();
-    } else {
-      Assert( (*i).isSortConstructor() );
-      name = SortConstructorType(*i).getName();
-    }
-    std::map<std::string, DatatypeType>::const_iterator resolver =
-      nameResolutions.find(name);
-    CheckArgument(resolver != nameResolutions.end(),
-                  unresolvedTypes,
-                  "cannot resolve type `%s'; it's not among "
-                  "the datatypes being defined", name.c_str());
-    // We will instruct the Datatype to substitute "*i" (the
-    // unresolved SortType used as a placeholder in complex types)
-    // with "(*resolver).second" (the DatatypeType we created in the
-    // first step, above).
-    if( (*i).isSort() ) {
-      placeholders.push_back(*i);
-      replacements.push_back( (*resolver).second );
-    } else {
-      Assert( (*i).isSortConstructor() );
-      paramTypes.push_back( SortConstructorType(*i) );
-      paramReplacements.push_back( (*resolver).second );
-    }
-  }
-
-  // Lastly, perform the final resolutions and checks.
-  for(std::vector<DatatypeType>::iterator i = dtts.begin(),
-        i_end = dtts.end();
-      i != i_end;
-      ++i) {
-    const Datatype& dt = (*i).getDatatype();
-    if(!dt.isResolved()) {
-      const_cast<Datatype&>(dt).resolve(this, nameResolutions,
-                                        placeholders, replacements,
-                                        paramTypes, paramReplacements);
-    }
-
-    // Now run some checks, including a check to make sure that no
-    // selector is function-valued.
-    checkResolvedDatatype(*i);
-  }
-
-  for(std::vector<NodeManagerListener*>::iterator i = d_nodeManager->d_listeners.begin(); i != d_nodeManager->d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewDatatypes(dtts);
-  }
-
-  return dtts;
-}
-
-void ExprManager::checkResolvedDatatype(DatatypeType dtt) const {
-  const Datatype& dt = dtt.getDatatype();
-
-  AssertArgument(dt.isResolved(), dtt, "datatype should have been resolved");
-
-  // for all constructors...
-  for(Datatype::const_iterator i = dt.begin(), i_end = dt.end();
-      i != i_end;
-      ++i) {
-    const DatatypeConstructor& c = *i;
-    Type testerType CVC4_UNUSED = c.getTester().getType();
-    Assert(c.isResolved() &&
-           testerType.isTester() &&
-           TesterType(testerType).getDomain() == dtt &&
-           TesterType(testerType).getRangeType() == booleanType(),
-           "malformed tester in datatype post-resolution");
-    Type ctorType CVC4_UNUSED = c.getConstructor().getType();
-    Assert(ctorType.isConstructor() &&
-           ConstructorType(ctorType).getArity() == c.getNumArgs() &&
-           ConstructorType(ctorType).getRangeType() == dtt,
-           "malformed constructor in datatype post-resolution");
-    // for all selectors...
-    for(DatatypeConstructor::const_iterator j = c.begin(), j_end = c.end();
-        j != j_end;
-        ++j) {
-      const DatatypeConstructorArg& a = *j;
-      Type selectorType = a.getSelector().getType();
-      Assert(a.isResolved() &&
-             selectorType.isSelector() &&
-             SelectorType(selectorType).getDomain() == dtt,
-             "malformed selector in datatype post-resolution");
-      // This next one's a "hard" check, performed in non-debug builds
-      // as well; the other ones should all be guaranteed by the
-      // CVC4::Datatype class, but this actually needs to be checked.
-      AlwaysAssert(!SelectorType(selectorType).getRangeType().d_typeNode->isFunctionLike(),
-                   "cannot put function-like things in datatypes");
-    }
-  }
-}
-
-ConstructorType ExprManager::mkConstructorType(const DatatypeConstructor& constructor, Type range) const {
-  NodeManagerScope nms(d_nodeManager);
-  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkConstructorType(constructor, *range.d_typeNode)));
-}
-
-SelectorType ExprManager::mkSelectorType(Type domain, Type range) const {
-  NodeManagerScope nms(d_nodeManager);
-  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSelectorType(*domain.d_typeNode, *range.d_typeNode)));
-}
-
-TesterType ExprManager::mkTesterType(Type domain) const {
-  NodeManagerScope nms(d_nodeManager);
-  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkTesterType(*domain.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) const {
-  NodeManagerScope nms(d_nodeManager);
-  return SortConstructorType(Type(d_nodeManager,
-              new TypeNode(d_nodeManager->mkSortConstructor(name, arity))));
-}
-
-/* - not in release 1.0
-Type ExprManager::mkPredicateSubtype(Expr lambda)
-  throw(TypeCheckingException) {
-  NodeManagerScope nms(d_nodeManager);
-  try {
-    return PredicateSubtype(Type(d_nodeManager,
-                new TypeNode(d_nodeManager->mkPredicateSubtype(lambda))));
-  } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(this, &e);
-  }
-}
-*/
-
-/* - not in release 1.0
-Type ExprManager::mkPredicateSubtype(Expr lambda, Expr witness)
-  throw(TypeCheckingException) {
-  NodeManagerScope nms(d_nodeManager);
-  try {
-    return PredicateSubtype(Type(d_nodeManager,
-                new TypeNode(d_nodeManager->mkPredicateSubtype(lambda, witness))));
-  } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(this, &e);
-  }
-}
-*/
-
-Type ExprManager::mkSubrangeType(const SubrangeBounds& bounds)
-  throw(TypeCheckingException) {
-  NodeManagerScope nms(d_nodeManager);
-  try {
-    return SubrangeType(Type(d_nodeManager,
-                new TypeNode(d_nodeManager->mkSubrangeType(bounds))));
-  } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(this, &e);
-  }
-}
-
-/**
- * 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 e, bool check) throw (TypeCheckingException) {
-  NodeManagerScope nms(d_nodeManager);
-  Type t;
-  try {
-    t = Type(d_nodeManager,
-             new TypeNode(d_nodeManager->getType(e.getNode(), check)));
-  } catch (const TypeCheckingExceptionPrivate& e) {
-    throw TypeCheckingException(this, &e);
-  }
-  return t;
-}
-
-Expr ExprManager::mkVar(const std::string& name, Type type, uint32_t flags) {
-  Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code.  Please use mkSkolem().");
-  NodeManagerScope nms(d_nodeManager);
-  Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode, flags);
-  Debug("nm") << "set " << name << " on " << *n << std::endl;
-  INC_STAT_VAR(type, false);
-  return Expr(this, n);
-}
-
-Expr ExprManager::mkVar(Type type, uint32_t flags) {
-  Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code.  Please use mkSkolem().");
-  NodeManagerScope nms(d_nodeManager);
-  INC_STAT_VAR(type, false);
-  return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode, flags));
-}
-
-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::mkAssociative(Kind kind,
-                                const std::vector<Expr>& children) {
-  CheckArgument( kind::isAssociative(kind), kind,
-                 "Illegal kind in mkAssociative: %s",
-                 kind::kindToString(kind).c_str());
-
-  NodeManagerScope nms(d_nodeManager);
-  const unsigned int max = maxArity(kind);
-  const unsigned int min = minArity(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);
-  }
-
-  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<Node> 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);
-
-    subChildren.clear();
-  }
-
-  /* If there's children left, "top off" the Expr. */
-  if(numChildren > 0) {
-    /* If the leftovers are too few, just copy them into newChildren;
-     * otherwise make a new sub-node  */
-    if(numChildren < min) {
-      for(; it != end; ++it) {
-        newChildren.push_back(it->getNode());
-      }
-    } else {
-      for(; it != end; ++it) {
-        subChildren.push_back(it->getNode());
-      }
-      Node subNode = d_nodeManager->mkNode(kind, subChildren);
-      newChildren.push_back(subNode);
-    }
-  }
-
-  /* It's inconceivable we could have enough children for this to fail
-   * (more than 2^32, in most cases?). */
-  AlwaysAssert( newChildren.size() <= max,
-                "Too many new children in mkAssociative" );
-
-  /* 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" );
-
-  return Expr(this, d_nodeManager->mkNodePtr(kind,newChildren) );
-}
-
-unsigned ExprManager::minArity(Kind kind) {
-  return metakind::getLowerBoundForKind(kind);
-}
-
-unsigned ExprManager::maxArity(Kind kind) {
-  return metakind::getUpperBoundForKind(kind);
-}
-
-NodeManager* ExprManager::getNodeManager() const {
-  return d_nodeManager;
-}
-
-Statistics ExprManager::getStatistics() const throw() {
-  return Statistics(*d_nodeManager->getStatisticsRegistry());
-}
-
-SExpr ExprManager::getStatistic(const std::string& name) const throw() {
-  return d_nodeManager->getStatisticsRegistry()->getStatistic(name);
-}
-
-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::SUBRANGE_TYPE) {
-    return to->mkSubrangeType(n.getSubrangeBounds());
-  }
-  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.orig b/src/expr/expr_manager_template.h.orig
deleted file mode 100644
index 2fabea0ff..000000000
--- a/src/expr/expr_manager_template.h.orig
+++ /dev/null
@@ -1,572 +0,0 @@
-/*********************                                                        */
-/*! \file expr_manager_template.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Dejan Jovanovic
- ** Minor contributors (to current version): Andrew Reynolds, Kshitij Bansal, Tim King, Christopher L. Conway
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** 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/kind.h"
-#include "expr/type.h"
-#include "expr/expr.h"
-#include "util/subrange_bound.h"
-#include "util/statistics.h"
-#include "util/sexpr.h"
-
-${includes}
-
-// This is a hack, but an important one: if there's an error, the
-// compiler directs the user to the template file instead of the
-// generated one.  We don't want the user to modify the generated one,
-// since it'll get overwritten on a later build.
-#line 38 "${template}"
-
-namespace CVC4 {
-
-class Expr;
-class SmtEngine;
-class NodeManager;
-class Options;
-class IntStat;
-struct ExprManagerMapCollection;
-class StatisticsRegistry;
-class ResourceManager;
-
-namespace expr {
-  namespace pickle {
-    class Pickler;
-  }/* CVC4::expr::pickle namespace */
-}/* CVC4::expr namespace */
-
-namespace stats {
-  StatisticsRegistry* getStatisticsRegistry(ExprManager*);
-}/* CVC4::stats namespace */
-
-class CVC4_PUBLIC ExprManager {
-private:
-  /** The internal node manager */
-  NodeManager* d_nodeManager;
-
-  /** Counts of expressions and variables created of a given kind */
-  IntStat* d_exprStatisticsVars[LAST_TYPE];
-  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;
-
-  /**
-   * Check some things about a newly-created DatatypeType.
-   */
-  void checkResolvedDatatype(DatatypeType dtt) 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;
-
-  /** Statistics reach in to get the StatisticsRegistry */
-  friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(ExprManager*);
-
-  /** Get the underlying statistics registry. */
-  StatisticsRegistry* getStatisticsRegistry() throw();
-
-  // undefined, private copy constructor and assignment op (disallow copy)
-  ExprManager(const ExprManager&) CVC4_UNDEFINED;
-  ExprManager& operator=(const ExprManager&) CVC4_UNDEFINED;
-
-public:
-
-  /**
-   * Creates an expression manager with default options.
-   */
-  ExprManager();
-
-  /**
-   * Creates an expression manager.
-   *
-   * @param options the earlyTypeChecking field is used to configure
-   * whether to do at Expr creation time.
-   */
-  explicit ExprManager(const Options& options);
-
-  /**
-   * 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() throw();
-
-  /** Get this expr manager's options */
-  const Options& getOptions() const;
-
-  /** Get this expr manager's resource manager */
-  ResourceManager* getResourceManager() throw();
-
-  /** Get the type for booleans */
-  BooleanType booleanType() const;
-
-  /** Get the type for strings. */
-  StringType stringType() const;
-
-  /** Get the type for reals. */
-  RealType realType() const;
-
-  /** Get the type for integers */
-  IntegerType integerType() 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);
-
-  /**
-   * 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);
-
-  /** 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 tuple type with types from
-   * <code>types[0..types.size()-1]</code>.  <code>types</code> must
-   * have at least one element.
-   */
-  TupleType mkTupleType(const std::vector<Type>& types);
-
-  /**
-   * Make a record type with types from the rec parameter.
-   */
-  RecordType mkRecordType(const Record& rec);
-
-  /**
-   * 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 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 a type representing the given datatype. */
-  DatatypeType mkDatatypeType(const Datatype& datatype);
-
-  /**
-   * Make a set of types representing the given datatypes, which may be
-   * mutually recursive.
-   */
-  std::vector<DatatypeType>
-  mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes);
-
-  /**
-   * Make a set of types representing the given datatypes, which may
-   * be mutually recursive.  unresolvedTypes is a set of SortTypes
-   * that were used as placeholders in the Datatypes for the Datatypes
-   * of the same name.  This is just a more complicated version of the
-   * above mkMutualDatatypeTypes() function, but is required to handle
-   * complex types.
-   *
-   * For example, unresolvedTypes might contain the single sort "list"
-   * (with that name reported from SortType::getName()).  The
-   * datatypes list might have the single datatype
-   *
-   *   DATATYPE
-   *     list = cons(car:ARRAY INT OF list, cdr:list) | nil;
-   *   END;
-   *
-   * To represent the Type of the array, the user had to create a
-   * placeholder type (an uninterpreted sort) to stand for "list" in
-   * the type of "car".  It is this placeholder sort that should be
-   * passed in unresolvedTypes.  If the datatype was of the simpler
-   * form:
-   *
-   *   DATATYPE
-   *     list = cons(car:list, cdr:list) | nil;
-   *   END;
-   *
-   * then no complicated Type needs to be created, and the above,
-   * simpler form of mkMutualDatatypeTypes() is enough.
-   */
-  std::vector<DatatypeType>
-  mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes,
-                        const std::set<Type>& unresolvedTypes);
-
-  /**
-   * Make a type representing a constructor with the given parameterization.
-   */
-  ConstructorType mkConstructorType(const DatatypeConstructor& constructor, Type range) const;
-
-  /** Make a type representing a selector with the given parameterization. */
-  SelectorType mkSelectorType(Type domain, Type range) const;
-
-  /** Make a type representing a tester with the given parameterization. */
-  TesterType mkTesterType(Type domain) const;
-
-  /** Bits for use in mkSort() flags. */
-  enum {
-    SORT_FLAG_NONE = 0,
-    SORT_FLAG_PLACEHOLDER = 1
-  };/* enum */
-
-  /** Make a new sort with the given name. */
-  SortType mkSort(const std::string& name, uint32_t flags = SORT_FLAG_NONE) const;
-
-  /** Make a sort constructor from a name and arity. */
-  SortConstructorType mkSortConstructor(const std::string& name,
-                                        size_t arity) const;
-
-  /**
-   * Make a predicate subtype type defined by the given LAMBDA
-   * expression.  A TypeCheckingException can be thrown if lambda is
-   * not a LAMBDA, or is ill-typed, or if CVC4 fails at proving that
-   * the resulting predicate subtype is inhabited.
-   */
-  // not in release 1.0
-  //Type mkPredicateSubtype(Expr lambda)
-  //  throw(TypeCheckingException);
-
-  /**
-   * Make a predicate subtype type defined by the given LAMBDA
-   * expression and whose non-emptiness is witnessed by the given
-   * witness.  A TypeCheckingException can be thrown if lambda is not
-   * a LAMBDA, or is ill-typed, or if the witness is not a witness or
-   * ill-typed.
-   */
-  // not in release 1.0
-  //Type mkPredicateSubtype(Expr lambda, Expr witness)
-  //  throw(TypeCheckingException);
-
-  /**
-   * Make an integer subrange type as defined by the argument.
-   */
-  Type mkSubrangeType(const SubrangeBounds& bounds)
-    throw(TypeCheckingException);
-
-  /** Get the type of an expression */
-  Type getType(Expr e, bool check = false)
-    throw(TypeCheckingException);
-
-  /** Bits for use in mkVar() flags. */
-  enum {
-    VAR_FLAG_NONE = 0,
-    VAR_FLAG_GLOBAL = 1,
-    VAR_FLAG_DEFINED = 2
-  };/* enum */
-
-  /**
-   * 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
-   * @param flags - VAR_FLAG_NONE - no flags;
-   * VAR_FLAG_GLOBAL - whether this variable is to be
-   * considered "global" or not.  Note that this information isn't
-   * used by the ExprManager, but is passed on to the ExprManager's
-   * event subscribers like the model-building service; if isGlobal
-   * is true, this newly-created variable will still available in
-   * models generated after an intervening pop.
-   * VAR_FLAG_DEFINED - if this is to be a "defined" symbol, e.g., for
-   * use with SmtEngine::defineFunction().  This keeps a declaration
-   * from being emitted in API dumps (since a subsequent definition is
-   * expected to be dumped instead).
-   */
-  Expr mkVar(const std::string& name, Type type, uint32_t flags = VAR_FLAG_NONE);
-
-  /**
-   * 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
-   * @param flags - VAR_FLAG_GLOBAL - whether this variable is to be considered "global"
-   * or not.  Note that this information isn't used by the ExprManager,
-   * but is passed on to the ExprManager's event subscribers like the
-   * model-building service; if isGlobal is true, this newly-created
-   * variable will still available in models generated after an
-   * intervening pop.
-   */
-  Expr mkVar(Type type, uint32_t flags = VAR_FLAG_NONE);
-
-  /**
-   * Create a new, fresh variable for use in a binder expression
-   * (the BOUND_VAR_LIST of a FORALL, EXISTS, or LAMBDA).  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, or LAMBDA).
-   * 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);
-
-  /** Get a reference to the statistics registry for this ExprManager */
-  Statistics getStatistics() const throw();
-
-  /** Get a reference to the statistics registry for this ExprManager */
-  SExpr getStatistic(const std::string& name) const throw();
-
-  /** 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);
-
-};/* class ExprManager */
-
-${mkConst_instantiations}
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__EXPR_MANAGER_H */
diff --git a/src/expr/node_manager.h.orig b/src/expr/node_manager.h.orig
deleted file mode 100644
index f4c3a1999..000000000
--- a/src/expr/node_manager.h.orig
+++ /dev/null
@@ -1,1498 +0,0 @@
-/*********************                                                        */
-/*! \file node_manager.h
- ** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Christopher L. Conway, Morgan Deters
- ** Minor contributors (to current version): ACSYS, Tianyi Liang, Kshitij Bansal, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief A manager for Nodes
- **
- ** A manager for Nodes.
- **
- ** Reviewed by Chris Conway, Apr 5 2010 (bug #65).
- **/
-
-#include "cvc4_private.h"
-
-/* circular dependency; force node.h first */
-//#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
-
-#include <vector>
-#include <string>
-#include <ext/hash_set>
-
-#include "expr/kind.h"
-#include "expr/metakind.h"
-#include "expr/node_value.h"
-#include "util/subrange_bound.h"
-#include "util/tls.h"
-#include "options/options.h"
-
-namespace CVC4 {
-
-class StatisticsRegistry;
-class ResourceManager;
-
-namespace expr {
-  namespace attr {
-    class AttributeUniqueId;
-    class AttributeManager;
-  }/* CVC4::expr::attr namespace */
-
-  class TypeChecker;
-}/* CVC4::expr namespace */
-
-/**
- * An interface that an interested party can implement and then subscribe
- * to NodeManager events via NodeManager::subscribeEvents(this).
- */
-class NodeManagerListener {
-public:
-  virtual ~NodeManagerListener() { }
-  virtual void nmNotifyNewSort(TypeNode tn, uint32_t flags) { }
-  virtual void nmNotifyNewSortConstructor(TypeNode tn) { }
-  virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort, uint32_t flags) { }
-  virtual void nmNotifyNewDatatypes(const std::vector<DatatypeType>& datatypes) { }
-  virtual void nmNotifyNewVar(TNode n, uint32_t flags) { }
-  virtual void nmNotifyNewSkolem(TNode n, const std::string& comment, uint32_t flags) { }
-  /**
-   * Notify a listener of a Node that's being GCed.  If this function stores a reference
-   * to the Node somewhere, very bad things will happen.
-   */
-  virtual void nmNotifyDeleteNode(TNode n) { }
-};/* class NodeManagerListener */
-
-class NodeManager {
-  template <unsigned nchild_thresh> friend class CVC4::NodeBuilder;
-  friend class NodeManagerScope;
-  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, uint32_t flags);
-  friend Expr ExprManager::mkVar(Type, uint32_t flags);
-
-  // friend so it can access NodeManager's d_listeners and notify clients
-  friend std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>&, const std::set<Type>&);
-
-  /** Predicate for use with STL algorithms */
-  struct NodeValueReferenceCountNonZero {
-    bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; }
-  };
-
-  typedef __gnu_cxx::hash_set<expr::NodeValue*,
-                              expr::NodeValuePoolHashFunction,
-                              expr::NodeValuePoolEq> NodeValuePool;
-  typedef __gnu_cxx::hash_set<expr::NodeValue*,
-                              expr::NodeValueIDHashFunction,
-                              expr::NodeValueEq> ZombieSet;
-
-  static CVC4_THREADLOCAL(NodeManager*) s_current;
-
-  Options* d_options;
-  StatisticsRegistry* d_statisticsRegistry;
-  ResourceManager* d_resourceManager;
-
-  NodeValuePool d_nodeValuePool;
-
-  size_t next_id;
-
-  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"
-   * contexts, like as a key in attribute tables), even though
-   * normally it's an error to have a TNode to a node value with a
-   * reference count of 0.  Being "under deletion" also enables
-   * assertions that inc() is not called on it.  (A poorly-behaving
-   * attribute cleanup function could otherwise create a "Node" that
-   * points to the node value that is in the process of being deleted,
-   * springing it back to life.)
-   */
-  expr::NodeValue* d_nodeUnderDeletion;
-
-  /**
-   * True iff we are in reclaimZombies().  This avoids unnecessary
-   * recursion; a NodeValue being deleted might zombify other
-   * NodeValues, but these shouldn't trigger a (recursive) call to
-   * reclaimZombies().
-   */
-  bool d_inReclaimZombies;
-
-  /**
-   * The set of zombie nodes.  We may want to revisit this design, as
-   * we might like to delete nodes in least-recently-used order.  But
-   * we also need to avoid processing a zombie twice.
-   */
-  ZombieSet d_zombies;
-
-  /**
-   * A set of operator singletons (w.r.t.  to this NodeManager
-   * instance) for operators.  Conceptually, Nodes with kind, say,
-   * PLUS, are APPLYs of a PLUS operator to arguments.  This array
-   * holds the set of operators for these things.  A PLUS operator is
-   * a Node with kind "BUILTIN", and if you call
-   * plusOperator->getConst<CVC4::Kind>(), you get kind::PLUS back.
-   */
-  Node d_operators[kind::LAST_KIND];
-
-  /**
-   * A list of subscribers for NodeManager events.
-   */
-  std::vector<NodeManagerListener*> d_listeners;
-
-  /**
-   * A map of tuple and record types to their corresponding datatype.
-   */
-  std::hash_map<TypeNode, TypeNode, TypeNodeHashFunction> d_tupleAndRecordTypes;
-
-  /**
-   * Keep a count of all abstract values produced by this NodeManager.
-   * Abstract values have a type attribute, so if multiple SmtEngines
-   * are attached to this NodeManager, we don't want their abstract
-   * values to overlap.
-   */
-  unsigned d_abstractValueCount;
-
-  /**
-   * A counter used to produce unique skolem names.
-   *
-   * Note that it is NOT incremented when skolems are created using
-   * SKOLEM_EXACT_NAME, so it is NOT a count of the skolems produced
-   * by this node manager.
-   */
-  unsigned d_skolemCounter;
-
-  /**
-   * Look up a NodeValue in the pool associated to this NodeManager.
-   * The NodeValue argument need not be a "completely-constructed"
-   * NodeValue.  In particular, "non-inlined" constants are permitted
-   * (see below).
-   *
-   * For non-CONSTANT metakinds, nv's d_kind and d_nchildren should be
-   * correctly set, and d_children[0..n-1] should be valid (extant)
-   * NodeValues for lookup.
-   *
-   * For CONSTANT metakinds, nv's d_kind should be set correctly.
-   * Normally a CONSTANT would have d_nchildren == 0 and the constant
-   * value inlined in the d_children space.  However, here we permit
-   * "non-inlined" NodeValues to avoid unnecessary copying.  For
-   * these, d_nchildren == 1, and d_nchildren is a pointer to the
-   * constant value.
-   *
-   * The point of this complex design is to permit efficient lookups
-   * (without fully constructing a NodeValue).  In the case that the
-   * argument is not fully constructed, and this function returns
-   * NULL, the caller should fully construct an equivalent one before
-   * calling poolInsert().  NON-FULLY-CONSTRUCTED NODEVALUES are not
-   * permitted in the pool!
-   */
-  inline expr::NodeValue* poolLookup(expr::NodeValue* nv) const;
-
-  /**
-   * Insert a NodeValue into the NodeManager's pool.
-   *
-   * It is an error to insert a NodeValue already in the pool.
-   * Enquire first with poolLookup().
-   */
-  inline void poolInsert(expr::NodeValue* nv);
-
-  /**
-   * Remove a NodeValue from the NodeManager's pool.
-   *
-   * It is an error to request the removal of a NodeValue from the
-   * pool that is not in the pool.
-   */
-  inline void poolRemove(expr::NodeValue* nv);
-
-  /**
-   * Determine if nv is currently being deleted by the NodeManager.
-   */
-  inline bool isCurrentlyDeleting(const expr::NodeValue* nv) const {
-    return d_nodeUnderDeletion == nv;
-  }
-
-  /**
-   * Register a NodeValue as a zombie.
-   */
-  inline void markForDeletion(expr::NodeValue* nv) {
-    Assert(nv->d_rc == 0);
-
-    // if d_reclaiming is set, make sure we don't call
-    // reclaimZombies(), because it's already running.
-    if(Debug.isOn("gc")) {
-      Debug("gc") << "zombifying node value " << nv
-                  << " [" << nv->d_id << "]: ";
-      nv->printAst(Debug("gc"));
-      Debug("gc") << (d_inReclaimZombies ? " [CURRENTLY-RECLAIMING]" : "")
-                  << std::endl;
-    }
-    d_zombies.insert(nv);// FIXME multithreading
-
-    if(safeToReclaimZombies()) {
-      if(d_zombies.size() > 5000) {
-        reclaimZombies();
-      }
-    }
-  }
-
-  /**
-   * Reclaim all zombies.
-   */
-  void reclaimZombies();
-
-  /**
-   * It is safe to collect zombies.
-   */
-  bool safeToReclaimZombies() const;
-
-  /**
-   * This template gives a mechanism to stack-allocate a NodeValue
-   * with enough space for N children (where N is a compile-time
-   * constant).  You use it like this:
-   *
-   *   NVStorage<4> nvStorage;
-   *   NodeValue& nvStack = reinterpret_cast<NodeValue&>(nvStorage);
-   *
-   * ...and then you can use nvStack as a NodeValue that you know has
-   * room for 4 children.
-   */
-  template <size_t N>
-  struct NVStorage {
-    expr::NodeValue nv;
-    expr::NodeValue* child[N];
-  };/* struct NodeManager::NVStorage<N> */
-
-  /* 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://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29
-   */
-  // bool containsDecision(TNode); // is "atomic"
-  // bool properlyContainsDecision(TNode); // all children are atomic
-
-  // undefined private copy constructor (disallow copy)
-  NodeManager(const NodeManager&) CVC4_UNDEFINED;
-
-  void init();
-
-  /**
-   * Create a variable with the given name and type.  NOTE that no
-   * lookup is done on the name.  If you mkVar("a", type) and then
-   * mkVar("a", type) again, you have two variables.  The NodeManager
-   * version of this is private to avoid internal uses of mkVar() from
-   * within CVC4.  Such uses should employ mkSkolem() instead.
-   */
-  Node mkVar(const std::string& name, const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
-  Node* mkVarPtr(const std::string& name, const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
-
-  /** Create a variable with the given type. */
-  Node mkVar(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
-  Node* mkVarPtr(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
-
-public:
-
-  explicit NodeManager(ExprManager* exprManager);
-  explicit NodeManager(ExprManager* exprManager, const Options& options);
-  ~NodeManager();
-
-  /** The node manager in the current public-facing CVC4 library context */
-  static NodeManager* currentNM() { return s_current; }
-  /** The resource manager associated with the current node manager */
-  static ResourceManager* currentResourceManager() { return s_current->d_resourceManager; }
-
-  /** Get this node manager's options (const version) */
-  const Options& getOptions() const {
-    return *d_options;
-  }
-
-  /** Get this node manager's options (non-const version) */
-  Options& getOptions() {
-    return *d_options;
-  }
-
-  /** Get this node manager's resource manager */
-  ResourceManager* getResourceManager() throw() { return d_resourceManager; }
-
-  /** Get this node manager's statistics registry */
-  StatisticsRegistry* getStatisticsRegistry() const throw() {
-    return d_statisticsRegistry;
-  }
-
-  /** Subscribe to NodeManager events */
-  void subscribeEvents(NodeManagerListener* listener) {
-    Assert(std::find(d_listeners.begin(), d_listeners.end(), listener) == d_listeners.end(), "listener already subscribed");
-    d_listeners.push_back(listener);
-  }
-
-  /** Unsubscribe from NodeManager events */
-  void unsubscribeEvents(NodeManagerListener* listener) {
-    std::vector<NodeManagerListener*>::iterator elt = std::find(d_listeners.begin(), d_listeners.end(), listener);
-    Assert(elt != d_listeners.end(), "listener not subscribed");
-    d_listeners.erase(elt);
-  }
-
-  /** Get a Kind from an operator expression */
-  static inline Kind operatorToKind(TNode n);
-
-  // general expression-builders
-
-  /** Create a node with one child. */
-  Node mkNode(Kind kind, TNode child1);
-  Node* mkNodePtr(Kind kind, TNode child1);
-
-  /** Create a node with two children. */
-  Node mkNode(Kind kind, TNode child1, TNode child2);
-  Node* mkNodePtr(Kind kind, TNode child1, TNode child2);
-
-  /** Create a node with three children. */
-  Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3);
-  Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3);
-
-  /** Create a node with four children. */
-  Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3,
-              TNode child4);
-  Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3,
-              TNode child4);
-
-  /** Create a node with five children. */
-  Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3,
-              TNode child4, TNode child5);
-  Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3,
-              TNode child4, TNode child5);
-
-  /** Create a node with an arbitrary number of children. */
-  template <bool ref_count>
-  Node mkNode(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
-  template <bool ref_count>
-  Node* mkNodePtr(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
-
-  /** Create a node (with no children) by operator. */
-  Node mkNode(TNode opNode);
-  Node* mkNodePtr(TNode opNode);
-
-  /** Create a node with one child by operator. */
-  Node mkNode(TNode opNode, TNode child1);
-  Node* mkNodePtr(TNode opNode, TNode child1);
-
-  /** Create a node with two children by operator. */
-  Node mkNode(TNode opNode, TNode child1, TNode child2);
-  Node* mkNodePtr(TNode opNode, TNode child1, TNode child2);
-
-  /** Create a node with three children by operator. */
-  Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3);
-  Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3);
-
-  /** Create a node with four children by operator. */
-  Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3,
-              TNode child4);
-  Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3,
-              TNode child4);
-
-  /** Create a node with five children by operator. */
-  Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3,
-              TNode child4, TNode child5);
-  Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3,
-              TNode child4, TNode child5);
-
-  /** Create a node by applying an operator to the children. */
-  template <bool ref_count>
-  Node mkNode(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children);
-  template <bool ref_count>
-  Node* mkNodePtr(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children);
-
-  Node mkBoundVar(const std::string& name, const TypeNode& type);
-  Node* mkBoundVarPtr(const std::string& name, const TypeNode& type);
-
-  Node mkBoundVar(const TypeNode& type);
-  Node* mkBoundVarPtr(const TypeNode& type);
-
-  /**
-   * Optional flags used to control behavior of NodeManager::mkSkolem().
-   * They should be composed with a bitwise OR (e.g.,
-   * "SKOLEM_NO_NOTIFY | SKOLEM_EXACT_NAME").  Of course, SKOLEM_DEFAULT
-   * cannot be composed in such a manner.
-   */
-  enum SkolemFlags {
-    SKOLEM_DEFAULT = 0,   /**< default behavior */
-    SKOLEM_NO_NOTIFY = 1, /**< do not notify subscribers */
-    SKOLEM_EXACT_NAME = 2,/**< do not make the name unique by adding the id */
-    SKOLEM_IS_GLOBAL = 4  /**< global vars appear in models even after a pop */
-  };/* enum SkolemFlags */
-
-  /**
-   * Create a skolem constant with the given name, type, and comment.
-   *
-   * @param prefix the name of the new skolem variable is the prefix
-   * appended with a unique ID.  This way a family of skolem variables
-   * can be made with unique identifiers, used in dump, tracing, and
-   * debugging output.  Use SKOLEM_EXECT_NAME flag if you don't want
-   * a unique ID appended and use prefix as the name.
-   *
-   * @param type the type of the skolem variable to create
-   *
-   * @param comment a comment for dumping output; if declarations are
-   * being dumped, this is included in a comment before the declaration
-   * and can be quite useful for debugging
-   *
-   * @param flags an optional mask of bits from SkolemFlags to control
-   * mkSkolem() behavior
-   */
-  Node mkSkolem(const std::string& prefix, const TypeNode& type,
-                const std::string& comment = "", int flags = SKOLEM_DEFAULT);
-
-  /** Create a instantiation constant with the given type. */
-  Node mkInstConstant(const TypeNode& type);
-
-  /** Make a new abstract value with the given type. */
-  Node mkAbstractValue(const TypeNode& type);
-
-  /**
-   * Create a constant of type T.  It will have the appropriate
-   * CONST_* kind defined for T.
-   */
-  template <class T>
-  Node mkConst(const T&);
-
-  template <class T>
-  TypeNode mkTypeConst(const T&);
-
-  template <class NodeClass, class T>
-  NodeClass mkConstInternal(const T&);
-
-  /** Create a node with children. */
-  TypeNode mkTypeNode(Kind kind, TypeNode child1);
-  TypeNode mkTypeNode(Kind kind, TypeNode child1, TypeNode child2);
-  TypeNode mkTypeNode(Kind kind, TypeNode child1, TypeNode child2,
-                      TypeNode child3);
-  TypeNode mkTypeNode(Kind kind, const std::vector<TypeNode>& children);
-
-  /**
-   * Determine whether Nodes of a particular Kind have operators.
-   * @returns true if Nodes of Kind k have operators.
-   */
-  static inline bool hasOperator(Kind k);
-
-  /**
-   * Get the (singleton) operator of an OPERATOR-kinded kind.  The
-   * returned node n will have kind BUILTIN, and calling
-   * n.getConst<CVC4::Kind>() will yield k.
-   */
-  inline TNode operatorOf(Kind k) {
-    AssertArgument( kind::metaKindOf(k) == kind::metakind::OPERATOR, k,
-                    "Kind is not an OPERATOR-kinded kind "
-                    "in NodeManager::operatorOf()" );
-    return d_operators[k];
-  }
-
-  /**
-   * Retrieve an attribute for a node.
-   *
-   * @param nv the node value
-   * @param attr an instance of the attribute kind to retrieve.
-   * @returns the attribute, if set, or a default-constructed
-   * <code>AttrKind::value_type</code> if not.
-   */
-  template <class AttrKind>
-  inline typename AttrKind::value_type getAttribute(expr::NodeValue* nv,
-                                                    const AttrKind& attr) const;
-
-  /**
-   * Check whether an attribute is set for a node.
-   *
-   * @param nv the node value
-   * @param attr an instance of the attribute kind to check
-   * @returns <code>true</code> iff <code>attr</code> is set for
-   * <code>nv</code>.
-   */
-  template <class AttrKind>
-  inline bool hasAttribute(expr::NodeValue* nv,
-                           const AttrKind& attr) const;
-
-  /**
-   * Check whether an attribute is set for a node, and, if so,
-   * retrieve it.
-   *
-   * @param nv the node value
-   * @param attr an instance of the attribute kind to check
-   * @param value a reference to an object of the attribute's value type.
-   * <code>value</code> will be set to the value of the attribute, if it is
-   * set for <code>nv</code>; otherwise, it will be set to the default
-   * value of the attribute.
-   * @returns <code>true</code> iff <code>attr</code> is set for
-   * <code>nv</code>.
-   */
-  template <class AttrKind>
-  inline bool getAttribute(expr::NodeValue* nv,
-                           const AttrKind& attr,
-                           typename AttrKind::value_type& value) const;
-
-  /**
-   * Set an attribute for a node.  If the node doesn't have the
-   * attribute, this function assigns one.  If the node has one, this
-   * overwrites it.
-   *
-   * @param nv the node value
-   * @param attr an instance of the attribute kind to set
-   * @param value the value of <code>attr</code> for <code>nv</code>
-   */
-  template <class AttrKind>
-  inline void setAttribute(expr::NodeValue* nv,
-                           const AttrKind& attr,
-                           const typename AttrKind::value_type& value);
-
-  /**
-   * Retrieve an attribute for a TNode.
-   *
-   * @param n the node
-   * @param attr an instance of the attribute kind to retrieve.
-   * @returns the attribute, if set, or a default-constructed
-   * <code>AttrKind::value_type</code> if not.
-   */
-  template <class AttrKind>
-  inline typename AttrKind::value_type
-  getAttribute(TNode n, const AttrKind& attr) const;
-
-  /**
-   * Check whether an attribute is set for a TNode.
-   *
-   * @param n the node
-   * @param attr an instance of the attribute kind to check
-   * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
-   */
-  template <class AttrKind>
-  inline bool hasAttribute(TNode n,
-                           const AttrKind& attr) const;
-
-  /**
-   * Check whether an attribute is set for a TNode and, if so, retieve
-   * it.
-   *
-   * @param n the node
-   * @param attr an instance of the attribute kind to check
-   * @param value a reference to an object of the attribute's value type.
-   * <code>value</code> will be set to the value of the attribute, if it is
-   * set for <code>nv</code>; otherwise, it will be set to the default value of
-   * the attribute.
-   * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
-   */
-  template <class AttrKind>
-  inline bool getAttribute(TNode n,
-                           const AttrKind& attr,
-                           typename AttrKind::value_type& value) const;
-
-  /**
-   * Set an attribute for a node.  If the node doesn't have the
-   * attribute, this function assigns one.  If the node has one, this
-   * overwrites it.
-   *
-   * @param n the node
-   * @param attr an instance of the attribute kind to set
-   * @param value the value of <code>attr</code> for <code>n</code>
-   */
-  template <class AttrKind>
-  inline void setAttribute(TNode n,
-                           const AttrKind& attr,
-                           const typename AttrKind::value_type& value);
-
-  /**
-   * Retrieve an attribute for a TypeNode.
-   *
-   * @param n the type node
-   * @param attr an instance of the attribute kind to retrieve.
-   * @returns the attribute, if set, or a default-constructed
-   * <code>AttrKind::value_type</code> if not.
-   */
-  template <class AttrKind>
-  inline typename AttrKind::value_type
-  getAttribute(TypeNode n, const AttrKind& attr) const;
-
-  /**
-   * Check whether an attribute is set for a TypeNode.
-   *
-   * @param n the type node
-   * @param attr an instance of the attribute kind to check
-   * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
-   */
-  template <class AttrKind>
-  inline bool hasAttribute(TypeNode n,
-                           const AttrKind& attr) const;
-
-  /**
-   * Check whether an attribute is set for a TypeNode and, if so, retieve
-   * it.
-   *
-   * @param n the type node
-   * @param attr an instance of the attribute kind to check
-   * @param value a reference to an object of the attribute's value type.
-   * <code>value</code> will be set to the value of the attribute, if it is
-   * set for <code>nv</code>; otherwise, it will be set to the default value of
-   * the attribute.
-   * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
-   */
-  template <class AttrKind>
-  inline bool getAttribute(TypeNode n,
-                           const AttrKind& attr,
-                           typename AttrKind::value_type& value) const;
-
-  /**
-   * Set an attribute for a type node.  If the node doesn't have the
-   * attribute, this function assigns one.  If the type node has one,
-   * this overwrites it.
-   *
-   * @param n the type node
-   * @param attr an instance of the attribute kind to set
-   * @param value the value of <code>attr</code> for <code>n</code>
-   */
-  template <class AttrKind>
-  inline void setAttribute(TypeNode n,
-                           const AttrKind& attr,
-                           const typename AttrKind::value_type& value);
-
-  /** Get the (singleton) type for Booleans. */
-  inline TypeNode booleanType();
-
-  /** Get the (singleton) type for integers. */
-  inline TypeNode integerType();
-
-  /** Get the (singleton) type for reals. */
-  inline TypeNode realType();
-
-  /** Get the (singleton) type for strings. */
-  inline TypeNode stringType();
-
-  /** Get the (singleton) type for RegExp. */
-  inline TypeNode regexpType();
-
-  /** Get the bound var list type. */
-  inline TypeNode boundVarListType();
-
-  /** Get the instantiation pattern type. */
-  inline TypeNode instPatternType();
-
-  /** Get the instantiation pattern type. */
-  inline TypeNode instPatternListType();
-
-  /**
-   * Get the (singleton) type for builtin operators (that is, the type
-   * of the Node returned from Node::getOperator() when the operator
-   * is built-in, like EQUAL). */
-  inline TypeNode builtinOperatorType();
-
-  /**
-   * Make a function type from domain to range.
-   *
-   * @param domain the domain type
-   * @param range the range type
-   * @returns the functional type domain -> range
-   */
-  inline TypeNode mkFunctionType(const TypeNode& domain, const TypeNode& range);
-
-  /**
-   * Make a function type with input types from
-   * argTypes. <code>argTypes</code> must have at least one element.
-   *
-   * @param argTypes the domain is a tuple (argTypes[0], ..., argTypes[n])
-   * @param range the range type
-   * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range
-   */
-  inline TypeNode mkFunctionType(const std::vector<TypeNode>& argTypes,
-                                 const TypeNode& 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.
-   */
-  inline TypeNode mkFunctionType(const std::vector<TypeNode>& 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.
-   */
-  inline TypeNode mkPredicateType(const std::vector<TypeNode>& sorts);
-
-  /**
-   * Make a tuple type with types from
-   * <code>types</code>. <code>types</code> must have at least one
-   * element.
-   *
-   * @param types a vector of types
-   * @returns the tuple type (types[0], ..., types[n])
-   */
-  inline TypeNode mkTupleType(const std::vector<TypeNode>& types);
-
-  /**
-   * Make a record type with the description from rec.
-   *
-   * @param rec a description of the record
-   * @returns the record type
-   */
-  inline TypeNode mkRecordType(const Record& rec);
-
-  /**
-   * Make a symbolic expression type with types from
-   * <code>types</code>. <code>types</code> may have any number of
-   * elements.
-   *
-   * @param types a vector of types
-   * @returns the symbolic expression type (types[0], ..., types[n])
-   */
-  inline TypeNode mkSExprType(const std::vector<TypeNode>& types);
-
-  /** Make the type of bitvectors of size <code>size</code> */
-  inline TypeNode mkBitVectorType(unsigned size);
-
-  /** Make the type of arrays with the given parameterization */
-  inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType);
-
-  /** Make the type of arrays with the given parameterization */
-  inline TypeNode mkSetType(TypeNode elementType);
-
-  /** Make a type representing a constructor with the given parameterization */
-  TypeNode mkConstructorType(const DatatypeConstructor& constructor, TypeNode range);
-
-  /** Make a type representing a selector with the given parameterization */
-  inline TypeNode mkSelectorType(TypeNode domain, TypeNode range);
-
-  /** Make a type representing a tester with given parameterization */
-  inline TypeNode mkTesterType(TypeNode domain);
-
-  /** Make a new (anonymous) sort of arity 0. */
-  TypeNode mkSort(uint32_t flags = ExprManager::SORT_FLAG_NONE);
-
-  /** Make a new sort with the given name of arity 0. */
-  TypeNode mkSort(const std::string& name, uint32_t flags = ExprManager::SORT_FLAG_NONE);
-
-  /** Make a new sort by parameterizing the given sort constructor. */
-  TypeNode mkSort(TypeNode constructor,
-                  const std::vector<TypeNode>& children,
-                  uint32_t flags = ExprManager::SORT_FLAG_NONE);
-
-  /** Make a new sort with the given name and arity. */
-  TypeNode mkSortConstructor(const std::string& name, size_t arity);
-
-  /**
-   * Make a predicate subtype type defined by the given LAMBDA
-   * expression.  A TypeCheckingExceptionPrivate can be thrown if
-   * lambda is not a LAMBDA, or is ill-typed, or if CVC4 fails at
-   * proving that the resulting predicate subtype is inhabited.
-   */
-  TypeNode mkPredicateSubtype(Expr lambda)
-    throw(TypeCheckingExceptionPrivate);
-
-  /**
-   * Make a predicate subtype type defined by the given LAMBDA
-   * expression and whose non-emptiness is witnessed by the given
-   * witness.  A TypeCheckingExceptionPrivate can be thrown if lambda
-   * is not a LAMBDA, or is ill-typed, or if the witness is not a
-   * witness or ill-typed.
-   */
-  TypeNode mkPredicateSubtype(Expr lambda, Expr witness)
-    throw(TypeCheckingExceptionPrivate);
-
-  /**
-   * Make an integer subrange type as defined by the argument.
-   */
-  TypeNode mkSubrangeType(const SubrangeBounds& bounds)
-    throw(TypeCheckingExceptionPrivate);
-
-  /**
-   * Given a tuple or record type, get the internal datatype used for
-   * it.  Makes the DatatypeType if necessary.
-   */
-  TypeNode getDatatypeForTupleRecord(TypeNode tupleRecordType);
-
-  /**
-   * Get the type for the given node 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 n the Node for which we want a type
-   * @param check whether we should check the type as we compute it
-   * (default: false)
-   */
-  TypeNode getType(TNode n, bool check = false)
-    throw(TypeCheckingExceptionPrivate, AssertionException);
-
-  /**
-   * 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(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);
-
-  /** Reclaims all zombies (if possible).*/
-  void reclaimAllZombies();
-
-  /** Size of the node pool. */
-  size_t poolSize() const;
-
-  /** Deletes a list of attributes from the NM's AttributeManager.*/
-  void deleteAttributes(const std::vector< const expr::attr::AttributeUniqueId* >& ids);
-
-  /**
-   * This function gives developers a hook into the NodeManager.
-   * This can be changed in node_manager.cpp without recompiling most of cvc4.
-   *
-   * debugHook is a debugging only function, and should not be present in
-   * any published code!
-   */
-  void debugHook(int debugFlag);
-};/* class NodeManager */
-
-/**
- * This class changes the "current" thread-global
- * <code>NodeManager</code> when it is created and reinstates the
- * previous thread-global <code>NodeManager</code> when it is
- * destroyed, effectively maintaining a set of nested
- * <code>NodeManager</code> scopes.  This is especially useful on
- * 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.
- *
- * The client must be careful to create and destroy
- * <code>NodeManagerScope</code> objects in a well-nested manner (such
- * as on the stack). You may create a <code>NodeManagerScope</code>
- * with <code>new</code> and destroy it with <code>delete</code>, or
- * place it as a data member of an object that is, but if the scope of
- * these <code>new</code>/<code>delete</code> pairs isn't properly
- * maintained, the incorrect "current" <code>NodeManager</code>
- * pointer may be restored after a delete.
- */
-class NodeManagerScope {
-  /** The old NodeManager, to be restored on destruction. */
-  NodeManager* d_oldNodeManager;
-
-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;
-    Options::s_current = nm ? nm->d_options : NULL;
-    Debug("current") << "node manager scope: "
-                     << NodeManager::s_current << "\n";
-  }
-
-  ~NodeManagerScope() {
-    NodeManager::s_current = d_oldNodeManager;
-    Options::s_current = d_oldNodeManager ? d_oldNodeManager->d_options : NULL;
-    Debug("current") << "node manager scope: "
-                     << "returning to " << NodeManager::s_current << "\n";
-  }
-};/* class NodeManagerScope */
-
-/** Get the (singleton) type for booleans. */
-inline TypeNode NodeManager::booleanType() {
-  return TypeNode(mkTypeConst<TypeConstant>(BOOLEAN_TYPE));
-}
-
-/** Get the (singleton) type for integers. */
-inline TypeNode NodeManager::integerType() {
-  return TypeNode(mkTypeConst<TypeConstant>(INTEGER_TYPE));
-}
-
-/** Get the (singleton) type for reals. */
-inline TypeNode NodeManager::realType() {
-  return TypeNode(mkTypeConst<TypeConstant>(REAL_TYPE));
-}
-
-/** Get the (singleton) type for strings. */
-inline TypeNode NodeManager::stringType() {
-  return TypeNode(mkTypeConst<TypeConstant>(STRING_TYPE));
-}
-
-/** Get the (singleton) type for regexps. */
-inline TypeNode NodeManager::regexpType() {
-  return TypeNode(mkTypeConst<TypeConstant>(REGEXP_TYPE));
-}
-
-/** Get the bound var list type. */
-inline TypeNode NodeManager::boundVarListType() {
-  return TypeNode(mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE));
-}
-
-/** Get the instantiation pattern type. */
-inline TypeNode NodeManager::instPatternType() {
-  return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_TYPE));
-}
-
-/** Get the instantiation pattern type. */
-inline TypeNode NodeManager::instPatternListType() {
-  return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_LIST_TYPE));
-}
-
-/** Get the (singleton) type for builtin operators. */
-inline TypeNode NodeManager::builtinOperatorType() {
-  return TypeNode(mkTypeConst<TypeConstant>(BUILTIN_OPERATOR_TYPE));
-}
-
-/** Make a function type from domain to range. */
-inline TypeNode NodeManager::mkFunctionType(const TypeNode& domain, const TypeNode& range) {
-  std::vector<TypeNode> sorts;
-  sorts.push_back(domain);
-  sorts.push_back(range);
-  return mkFunctionType(sorts);
-}
-
-inline TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& argTypes, const TypeNode& range) {
-  Assert(argTypes.size() >= 1);
-  std::vector<TypeNode> sorts(argTypes);
-  sorts.push_back(range);
-  return mkFunctionType(sorts);
-}
-
-inline TypeNode
-NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts) {
-  Assert(sorts.size() >= 2);
-  std::vector<TypeNode> sortNodes;
-  for (unsigned i = 0; i < sorts.size(); ++ i) {
-    CheckArgument(!sorts[i].isFunctionLike(), sorts,
-                  "cannot create higher-order function types");
-    sortNodes.push_back(sorts[i]);
-  }
-  return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
-}
-
-inline TypeNode
-NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) {
-  Assert(sorts.size() >= 1);
-  std::vector<TypeNode> sortNodes;
-  for (unsigned i = 0; i < sorts.size(); ++ i) {
-    CheckArgument(!sorts[i].isFunctionLike(), sorts,
-                  "cannot create higher-order function types");
-    sortNodes.push_back(sorts[i]);
-  }
-  sortNodes.push_back(booleanType());
-  return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
-}
-
-inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
-  std::vector<TypeNode> typeNodes;
-  for (unsigned i = 0; i < types.size(); ++ i) {
-    CheckArgument(!types[i].isFunctionLike(), types,
-                  "cannot put function-like types in tuples");
-    typeNodes.push_back(types[i]);
-  }
-  return mkTypeNode(kind::TUPLE_TYPE, typeNodes);
-}
-
-inline TypeNode NodeManager::mkRecordType(const Record& rec) {
-  return mkTypeConst(rec);
-}
-
-inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) {
-  std::vector<TypeNode> typeNodes;
-  for (unsigned i = 0; i < types.size(); ++ i) {
-    typeNodes.push_back(types[i]);
-  }
-  return mkTypeNode(kind::SEXPR_TYPE, typeNodes);
-}
-
-inline TypeNode NodeManager::mkBitVectorType(unsigned size) {
-  return TypeNode(mkTypeConst<BitVectorSize>(BitVectorSize(size)));
-}
-
-inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
-                                         TypeNode constituentType) {
-  CheckArgument(!indexType.isNull(), indexType,
-                "unexpected NULL index type");
-  CheckArgument(!constituentType.isNull(), constituentType,
-                "unexpected NULL constituent type");
-  CheckArgument(!indexType.isFunctionLike(), indexType,
-                "cannot index arrays by a function-like type");
-  CheckArgument(!constituentType.isFunctionLike(), constituentType,
-                "cannot store function-like types in arrays");
-  Debug("arrays") << "making array type " << indexType << " " << constituentType << std::endl;
-  return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType);
-}
-
-inline TypeNode NodeManager::mkSetType(TypeNode elementType) {
-  CheckArgument(!elementType.isNull(), elementType,
-                "unexpected NULL element type");
-  // TODO: Confirm meaning of isFunctionLike(). --K
-  CheckArgument(!elementType.isFunctionLike(), elementType,
-                "cannot store function-like types in sets");
-  Debug("sets") << "making sets type " << elementType << std::endl;
-  return mkTypeNode(kind::SET_TYPE, elementType);
-}
-
-inline TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) {
-  CheckArgument(!domain.isFunctionLike(), domain,
-                "cannot create higher-order function types");
-  CheckArgument(!range.isFunctionLike(), range,
-                "cannot create higher-order function types");
-  return mkTypeNode(kind::SELECTOR_TYPE, domain, range);
-}
-
-inline TypeNode NodeManager::mkTesterType(TypeNode domain) {
-  CheckArgument(!domain.isFunctionLike(), domain,
-                "cannot create higher-order function types");
-  return mkTypeNode(kind::TESTER_TYPE, domain );
-}
-
-inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const {
-  NodeValuePool::const_iterator find = d_nodeValuePool.find(nv);
-  if(find == d_nodeValuePool.end()) {
-    return NULL;
-  } else {
-    return *find;
-  }
-}
-
-inline void NodeManager::poolInsert(expr::NodeValue* nv) {
-  Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end(),
-         "NodeValue already in the pool!");
-  d_nodeValuePool.insert(nv);// FIXME multithreading
-}
-
-inline void NodeManager::poolRemove(expr::NodeValue* nv) {
-  Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end(),
-         "NodeValue is not in the pool!");
-
-  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(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
-#include "expr/metakind.h"
-#undef __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
-
-#include "expr/node_builder.h"
-
-namespace CVC4 {
-
-// general expression-builders
-
-inline bool NodeManager::hasOperator(Kind k) {
-  switch(kind::MetaKind mk = kind::metaKindOf(k)) {
-
-  case kind::metakind::INVALID:
-  case kind::metakind::VARIABLE:
-    return false;
-
-  case kind::metakind::OPERATOR:
-  case kind::metakind::PARAMETERIZED:
-    return true;
-
-  case kind::metakind::CONSTANT:
-    return false;
-
-  default:
-    Unhandled(mk);
-  }
-}
-
-inline Kind NodeManager::operatorToKind(TNode n) {
-  return kind::operatorToKind(n.d_nv);
-}
-
-inline Node NodeManager::mkNode(Kind kind, TNode child1) {
-  NodeBuilder<1> nb(this, kind);
-  nb << child1;
-  return nb.constructNode();
-}
-
-inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1) {
-  NodeBuilder<1> nb(this, kind);
-  nb << child1;
-  return nb.constructNodePtr();
-}
-
-inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2) {
-  NodeBuilder<2> nb(this, kind);
-  nb << child1 << child2;
-  return nb.constructNode();
-}
-
-inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2) {
-  NodeBuilder<2> nb(this, kind);
-  nb << child1 << child2;
-  return nb.constructNodePtr();
-}
-
-inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
-                                TNode child3) {
-  NodeBuilder<3> nb(this, kind);
-  nb << child1 << child2 << child3;
-  return nb.constructNode();
-}
-
-inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
-                                TNode child3) {
-  NodeBuilder<3> nb(this, kind);
-  nb << child1 << child2 << child3;
-  return nb.constructNodePtr();
-}
-
-inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
-                                TNode child3, TNode child4) {
-  NodeBuilder<4> nb(this, kind);
-  nb << child1 << child2 << child3 << child4;
-  return nb.constructNode();
-}
-
-inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
-                                TNode child3, TNode child4) {
-  NodeBuilder<4> nb(this, kind);
-  nb << child1 << child2 << child3 << child4;
-  return nb.constructNodePtr();
-}
-
-inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
-                                TNode child3, TNode child4, TNode child5) {
-  NodeBuilder<5> nb(this, kind);
-  nb << child1 << child2 << child3 << child4 << child5;
-  return nb.constructNode();
-}
-
-inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
-                                    TNode child3, TNode child4, TNode child5) {
-  NodeBuilder<5> nb(this, kind);
-  nb << child1 << child2 << child3 << child4 << child5;
-  return nb.constructNodePtr();
-}
-
-// N-ary version
-template <bool ref_count>
-inline Node NodeManager::mkNode(Kind kind,
-                                const std::vector<NodeTemplate<ref_count> >&
-                                children) {
-  NodeBuilder<> nb(this, kind);
-  nb.append(children);
-  return nb.constructNode();
-}
-
-template <bool ref_count>
-inline Node* NodeManager::mkNodePtr(Kind kind,
-                                const std::vector<NodeTemplate<ref_count> >&
-                                children) {
-  NodeBuilder<> nb(this, kind);
-  nb.append(children);
-  return nb.constructNodePtr();
-}
-
-// for operators
-inline Node NodeManager::mkNode(TNode opNode) {
-  NodeBuilder<1> nb(this, operatorToKind(opNode));
-  if(opNode.getKind() != kind::BUILTIN) {
-    nb << opNode;
-  }
-  return nb.constructNode();
-}
-
-inline Node* NodeManager::mkNodePtr(TNode opNode) {
-  NodeBuilder<1> nb(this, operatorToKind(opNode));
-  if(opNode.getKind() != kind::BUILTIN) {
-    nb << opNode;
-  }
-  return nb.constructNodePtr();
-}
-
-inline Node NodeManager::mkNode(TNode opNode, TNode child1) {
-  NodeBuilder<2> nb(this, operatorToKind(opNode));
-  if(opNode.getKind() != kind::BUILTIN) {
-    nb << opNode;
-  }
-  nb << child1;
-  return nb.constructNode();
-}
-
-inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1) {
-  NodeBuilder<2> nb(this, operatorToKind(opNode));
-  if(opNode.getKind() != kind::BUILTIN) {
-    nb << opNode;
-  }
-  nb << child1;
-  return nb.constructNodePtr();
-}
-
-inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2) {
-  NodeBuilder<3> nb(this, operatorToKind(opNode));
-  if(opNode.getKind() != kind::BUILTIN) {
-    nb << opNode;
-  }
-  nb << child1 << child2;
-  return nb.constructNode();
-}
-
-inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2) {
-  NodeBuilder<3> nb(this, operatorToKind(opNode));
-  if(opNode.getKind() != kind::BUILTIN) {
-    nb << opNode;
-  }
-  nb << child1 << child2;
-  return nb.constructNodePtr();
-}
-
-inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
-                                TNode child3) {
-  NodeBuilder<4> nb(this, operatorToKind(opNode));
-  if(opNode.getKind() != kind::BUILTIN) {
-    nb << opNode;
-  }
-  nb << child1 << child2 << child3;
-  return nb.constructNode();
-}
-
-inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
-                                TNode child3) {
-  NodeBuilder<4> nb(this, operatorToKind(opNode));
-  if(opNode.getKind() != kind::BUILTIN) {
-    nb << opNode;
-  }
-  nb << child1 << child2 << child3;
-  return nb.constructNodePtr();
-}
-
-inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
-                                TNode child3, TNode child4) {
-  NodeBuilder<5> nb(this, operatorToKind(opNode));
-  if(opNode.getKind() != kind::BUILTIN) {
-    nb << opNode;
-  }
-  nb << child1 << child2 << child3 << child4;
-  return nb.constructNode();
-}
-
-inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
-                                TNode child3, TNode child4) {
-  NodeBuilder<5> nb(this, operatorToKind(opNode));
-  if(opNode.getKind() != kind::BUILTIN) {
-    nb << opNode;
-  }
-  nb << child1 << child2 << child3 << child4;
-  return nb.constructNodePtr();
-}
-
-inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
-                                TNode child3, TNode child4, TNode child5) {
-  NodeBuilder<6> nb(this, operatorToKind(opNode));
-  if(opNode.getKind() != kind::BUILTIN) {
-    nb << opNode;
-  }
-  nb << child1 << child2 << child3 << child4 << child5;
-  return nb.constructNode();
-}
-
-inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
-                                    TNode child3, TNode child4, TNode child5) {
-  NodeBuilder<6> nb(this, operatorToKind(opNode));
-  if(opNode.getKind() != kind::BUILTIN) {
-    nb << opNode;
-  }
-  nb << child1 << child2 << child3 << child4 << child5;
-  return nb.constructNodePtr();
-}
-
-// N-ary version for operators
-template <bool ref_count>
-inline Node NodeManager::mkNode(TNode opNode,
-                                const std::vector<NodeTemplate<ref_count> >&
-                                children) {
-  NodeBuilder<> nb(this, operatorToKind(opNode));
-  if(opNode.getKind() != kind::BUILTIN) {
-    nb << opNode;
-  }
-  nb.append(children);
-  return nb.constructNode();
-}
-
-template <bool ref_count>
-inline Node* NodeManager::mkNodePtr(TNode opNode,
-                                    const std::vector<NodeTemplate<ref_count> >&
-                                    children) {
-  NodeBuilder<> nb(this, operatorToKind(opNode));
-  if(opNode.getKind() != kind::BUILTIN) {
-    nb << opNode;
-  }
-  nb.append(children);
-  return nb.constructNodePtr();
-}
-
-
-inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1) {
-  return (NodeBuilder<1>(this, kind) << child1).constructTypeNode();
-}
-
-inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1,
-                                        TypeNode child2) {
-  return (NodeBuilder<2>(this, kind) << child1 << child2).constructTypeNode();
-}
-
-inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1,
-                                        TypeNode child2, TypeNode child3) {
-  return (NodeBuilder<3>(this, kind) << child1 << child2 << child3).constructTypeNode();
-}
-
-// N-ary version for types
-inline TypeNode NodeManager::mkTypeNode(Kind kind,
-                                        const std::vector<TypeNode>& children) {
-  return NodeBuilder<>(this, kind).append(children).constructTypeNode();
-}
-
-template <class T>
-Node NodeManager::mkConst(const T& val) {
-  return mkConstInternal<Node, T>(val);
-}
-
-template <class T>
-TypeNode NodeManager::mkTypeConst(const T& val) {
-  return mkConstInternal<TypeNode, T>(val);
-}
-
-template <class NodeClass, class T>
-NodeClass NodeManager::mkConstInternal(const T& val) {
-
-  // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t;
-  NVStorage<1> nvStorage;
-  expr::NodeValue& nvStack = reinterpret_cast<expr::NodeValue&>(nvStorage);
-
-  nvStack.d_id = 0;
-  nvStack.d_kind = kind::metakind::ConstantMap<T>::kind;
-  nvStack.d_rc = 0;
-  nvStack.d_nchildren = 1;
-
-#if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6))
-#pragma GCC diagnostic push
-#pragma GCC diagnostic ignored "-Warray-bounds"
-#endif
-
-  nvStack.d_children[0] =
-    const_cast<expr::NodeValue*>(reinterpret_cast<const expr::NodeValue*>(&val));
-  expr::NodeValue* nv = poolLookup(&nvStack);
-
-#if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6))
-#pragma GCC diagnostic pop
-#endif
-
-  if(nv != NULL) {
-    return NodeClass(nv);
-  }
-
-  nv = (expr::NodeValue*)
-    std::malloc(sizeof(expr::NodeValue) + sizeof(T));
-  if(nv == NULL) {
-    throw std::bad_alloc();
-  }
-
-  nv->d_nchildren = 0;
-  nv->d_kind = kind::metakind::ConstantMap<T>::kind;
-  nv->d_id = next_id++;// FIXME multithreading
-  nv->d_rc = 0;
-
-  //OwningTheory::mkConst(val);
-  new (&nv->d_children) T(val);
-
-  poolInsert(nv);
-  if(Debug.isOn("gc")) {
-    Debug("gc") << "creating node value " << nv
-                << " [" << nv->d_id << "]: ";
-    nv->printAst(Debug("gc"));
-    Debug("gc") << std::endl;
-  }
-
-  return NodeClass(nv);
-}
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__NODE_MANAGER_H */