Floating point infrastructure.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>

9 files changed, 3265 insertions, 0 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index c5249075b..7eb93b8ff 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -154,6 +154,12 @@ IntegerType ExprManager::integerType() const {
   return IntegerType(Type(d_nodeManager, new TypeNode(d_nodeManager->integerType())));
 }
 
+RoundingModeType ExprManager::roundingModeType() const {
+  NodeManagerScope nms(d_nodeManager);
+  return RoundingModeType(Type(d_nodeManager, new TypeNode(d_nodeManager->roundingModeType())));
+}
+
+
 Expr ExprManager::mkExpr(Kind kind, Expr child1) {
   const kind::MetaKind mk = kind::metaKindOf(kind);
   const unsigned n = 1 - (mk == kind::metakind::PARAMETERIZED ? 1 : 0);
@@ -573,6 +579,11 @@ SExprType ExprManager::mkSExprType(const std::vector<Type>& types) {
   return SExprType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSExprType(typeNodes))));
 }
 
+FloatingPointType ExprManager::mkFloatingPointType(unsigned exp, unsigned sig) const {
+  NodeManagerScope nms(d_nodeManager);
+  return FloatingPointType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFloatingPointType(exp,sig))));
+}
+
 BitVectorType ExprManager::mkBitVectorType(unsigned size) const {
   NodeManagerScope nms(d_nodeManager);
   return BitVectorType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkBitVectorType(size))));
diff --git a/src/expr/expr_manager_template.cpp.orig b/src/expr/expr_manager_template.cpp.orig
new file mode 100644
index 000000000..c5249075b
--- /dev/null
+++ b/src/expr/expr_manager_template.cpp.orig
@@ -0,0 +1,1027 @@
+/*********************                                                        */
+/*! \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 b/src/expr/expr_manager_template.h
index 2fabea0ff..8acb7489f 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -139,6 +139,9 @@ public:
   /** Get the type for integers */
   IntegerType integerType() const;
 
+  /** Get the type for rounding modes */
+  RoundingModeType roundingModeType() const;
+
   /**
    * Make a unary expression of a given kind (NOT, BVNOT, ...).
    * @param kind the kind of expression
@@ -361,6 +364,9 @@ public:
    */
   SExprType mkSExprType(const std::vector<Type>& types);
 
+  /** Make a type representing a floating-point type with the given parameters. */
+  FloatingPointType mkFloatingPointType(unsigned exp, unsigned sig) const;
+
   /** Make a type representing a bit-vector of the given size. */
   BitVectorType mkBitVectorType(unsigned size) const;
 
diff --git a/src/expr/expr_manager_template.h.orig b/src/expr/expr_manager_template.h.orig
new file mode 100644
index 000000000..2fabea0ff
--- /dev/null
+++ b/src/expr/expr_manager_template.h.orig
@@ -0,0 +1,572 @@
+/*********************                                                        */
+/*! \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 b/src/expr/node_manager.h
index f4c3a1999..f52c7732f 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -685,6 +685,9 @@ public:
   /** Get the (singleton) type for RegExp. */
   inline TypeNode regexpType();
 
+  /** Get the (singleton) type for rounding modes. */
+  inline TypeNode roundingModeType();
+
   /** Get the bound var list type. */
   inline TypeNode boundVarListType();
 
@@ -764,6 +767,11 @@ public:
    */
   inline TypeNode mkSExprType(const std::vector<TypeNode>& types);
 
+  /** Make the type of floating-point with <code>exp</code> bit exponent and
+      <code>sig</code> bit significand */
+  inline TypeNode mkFloatingPointType(unsigned exp, unsigned sig);  
+  inline TypeNode mkFloatingPointType(FloatingPointSize fs);
+
   /** Make the type of bitvectors of size <code>size</code> */
   inline TypeNode mkBitVectorType(unsigned size);
 
@@ -980,6 +988,11 @@ inline TypeNode NodeManager::regexpType() {
   return TypeNode(mkTypeConst<TypeConstant>(REGEXP_TYPE));
 }
 
+/** Get the (singleton) type for rounding modes. */
+inline TypeNode NodeManager::roundingModeType() {
+  return TypeNode(mkTypeConst<TypeConstant>(ROUNDINGMODE_TYPE));
+}
+
 /** Get the bound var list type. */
 inline TypeNode NodeManager::boundVarListType() {
   return TypeNode(mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE));
@@ -1066,6 +1079,14 @@ inline TypeNode NodeManager::mkBitVectorType(unsigned size) {
   return TypeNode(mkTypeConst<BitVectorSize>(BitVectorSize(size)));
 }
 
+inline TypeNode NodeManager::mkFloatingPointType(unsigned exp, unsigned sig) {
+  return TypeNode(mkTypeConst<FloatingPointSize>(FloatingPointSize(exp,sig)));
+}
+
+inline TypeNode NodeManager::mkFloatingPointType(FloatingPointSize fs) {
+  return TypeNode(mkTypeConst<FloatingPointSize>(fs));
+}
+
 inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
                                          TypeNode constituentType) {
   CheckArgument(!indexType.isNull(), indexType,
diff --git a/src/expr/node_manager.h.orig b/src/expr/node_manager.h.orig
new file mode 100644
index 000000000..f4c3a1999
--- /dev/null
+++ b/src/expr/node_manager.h.orig
@@ -0,0 +1,1498 @@
+/*********************                                                        */
+/*! \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 */
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 5810e1f4f..46705a849 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -223,12 +223,24 @@ bool Type::isString() const {
   return d_typeNode->isString();
 }
 
+/** Is this the rounding mode type? */
+bool Type::isRoundingMode() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isRoundingMode();
+}
+
 /** Is this the bit-vector type? */
 bool Type::isBitVector() const {
   NodeManagerScope nms(d_nodeManager);
   return d_typeNode->isBitVector();
 }
 
+/** Is this the floating-point type? */
+bool Type::isFloatingPoint() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isFloatingPoint();
+}
+
 /** Is this a datatype type? */
 bool Type::isDatatype() const {
   NodeManagerScope nms(d_nodeManager);
@@ -436,11 +448,21 @@ StringType::StringType(const Type& t) throw(IllegalArgumentException) :
   CheckArgument(isNull() || isString(), this);
 }
 
+RoundingModeType::RoundingModeType(const Type& t) throw(IllegalArgumentException) :
+  Type(t) {
+  CheckArgument(isNull() || isRoundingMode(), this);
+}
+
 BitVectorType::BitVectorType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
   CheckArgument(isNull() || isBitVector(), this);
 }
 
+FloatingPointType::FloatingPointType(const Type& t) throw(IllegalArgumentException) :
+  Type(t) {
+  CheckArgument(isNull() || isFloatingPoint(), this);
+}
+
 DatatypeType::DatatypeType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
   CheckArgument(isNull() || isDatatype(), this);
@@ -520,6 +542,14 @@ unsigned BitVectorType::getSize() const {
   return d_typeNode->getBitVectorSize();
 }
 
+unsigned FloatingPointType::getExponentSize() const {
+  return d_typeNode->getFloatingPointExponentSize();
+}
+
+unsigned FloatingPointType::getSignificandSize() const {
+  return d_typeNode->getFloatingPointSignificandSize();
+}
+
 Type ArrayType::getIndexType() const {
   return makeType(d_typeNode->getArrayIndexType());
 }
diff --git a/src/expr/type.h b/src/expr/type.h
index 7674ff9d0..8a5a987d5 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -47,6 +47,7 @@ class BooleanType;
 class IntegerType;
 class RealType;
 class StringType;
+class RoundingModeType;
 class BitVectorType;
 class ArrayType;
 class SetType;
@@ -259,12 +260,24 @@ public:
   bool isString() const;
 
   /**
+   * Is this the rounding mode type?
+   * @return true if the type is the rounding mode type
+   */
+  bool isRoundingMode() const;
+
+  /**
    * Is this the bit-vector type?
    * @return true if the type is a bit-vector type
    */
   bool isBitVector() const;
 
   /**
+   * Is this the floating-point type?
+   * @return true if the type is a floating-point type
+   */
+  bool isFloatingPoint() const;
+
+  /**
    * Is this a function type?
    * @return true if the type is a function type
    */
@@ -413,6 +426,19 @@ public:
 };/* class StringType */
 
 /**
+ * Singleton class encapsulating the rounding mode type.
+ */
+class CVC4_PUBLIC RoundingModeType : public Type {
+
+public:
+
+  /** Construct from the base type */
+  RoundingModeType(const Type& type = Type()) throw(IllegalArgumentException);
+};/* class RoundingModeType */
+
+
+
+/**
  * Class encapsulating a function type.
  */
 class CVC4_PUBLIC FunctionType : public Type {
@@ -610,6 +636,31 @@ public:
 
 
 /**
+ * Class encapsulating the floating point type.
+ */
+class CVC4_PUBLIC FloatingPointType : public Type {
+
+public:
+
+  /** Construct from the base type */
+  FloatingPointType(const Type& type = Type()) throw(IllegalArgumentException);
+
+  /**
+   * Returns the size of the floating-point exponent type.
+   * @return the width of the floating-point exponent type (> 0)
+   */
+  unsigned getExponentSize() const;
+
+  /**
+   * Returns the size of the floating-point significand type.
+   * @return the width of the floating-point significand type (> 0)
+   */
+  unsigned getSignificandSize() const;
+
+};/* class FloatingPointType */
+
+
+/**
  * Class encapsulating the datatype type
  */
 class CVC4_PUBLIC DatatypeType : public Type {
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 289395a34..5129b7581 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -463,6 +463,9 @@ public:
   /** Is this the String type? */
   bool isString() const;
 
+  /** Is this the Rounding Mode type? */
+  bool isRoundingMode() const;
+
   /** Is this an array type? */
   bool isArray() const;
 
@@ -560,6 +563,13 @@ public:
   /** Is this a regexp type */
   bool isRegExp() const;
 
+  /** Is this a floating-point type */
+  bool isFloatingPoint() const;
+
+  /** Is this a floating-point type of with <code>exp</code> exponent bits
+      and <code>sig</code> significand bits */
+  bool isFloatingPoint(unsigned exp, unsigned sig) const;
+
   /** Is this a bit-vector type */
   bool isBitVector() const;
 
@@ -590,6 +600,12 @@ public:
   /** Get the Datatype specification from a datatype type */
   const Datatype& getDatatype() const;
 
+  /** Get the exponent size of this floating-point type */
+  unsigned getFloatingPointExponentSize() const;
+
+  /** Get the significand size of this floating-point type */
+  unsigned getFloatingPointSignificandSize() const;
+
   /** Get the size of this bit-vector type */
   unsigned getBitVectorSize() const;
 
@@ -852,6 +868,11 @@ inline bool TypeNode::isString() const {
 inline bool TypeNode::isRegExp() const {
   return getKind() == kind::TYPE_CONSTANT &&
     getConst<TypeConstant>() == REGEXP_TYPE;
+ }
+
+inline bool TypeNode::isRoundingMode() const {
+  return getKind() == kind::TYPE_CONSTANT &&
+    getConst<TypeConstant>() == ROUNDINGMODE_TYPE;
 }
 
 inline bool TypeNode::isArray() const {
@@ -939,6 +960,12 @@ inline bool TypeNode::isSubrange() const {
     ( isPredicateSubtype() && getSubtypeParentType().isSubrange() );
 }
 
+/** Is this a floating-point type */
+inline bool TypeNode::isFloatingPoint() const {
+  return getKind() == kind::FLOATINGPOINT_TYPE ||
+    ( isPredicateSubtype() && getSubtypeParentType().isFloatingPoint() );
+}
+
 /** Is this a bit-vector type */
 inline bool TypeNode::isBitVector() const {
   return getKind() == kind::BITVECTOR_TYPE ||
@@ -973,6 +1000,16 @@ inline bool TypeNode::isTester() const {
   return getKind() == kind::TESTER_TYPE;
 }
 
+/** Is this a floating-point type of with <code>exp</code> exponent bits
+    and <code>sig</code> significand bits */
+inline bool TypeNode::isFloatingPoint(unsigned exp, unsigned sig) const {
+  return
+    ( getKind() == kind::FLOATINGPOINT_TYPE && 
+      getConst<FloatingPointSize>().exponent() == exp &&
+      getConst<FloatingPointSize>().significand() == sig ) ||
+    ( isPredicateSubtype() && getSubtypeParentType().isFloatingPoint(exp,sig) );
+}
+
 /** Is this a bit-vector type of size <code>size</code> */
 inline bool TypeNode::isBitVector(unsigned size) const {
   return
@@ -990,6 +1027,18 @@ inline const Datatype& TypeNode::getDatatype() const {
   }
 }
 
+/** Get the exponent size of this floating-point type */
+inline unsigned TypeNode::getFloatingPointExponentSize() const {
+  Assert(isFloatingPoint());
+  return getConst<FloatingPointSize>().exponent();
+}
+
+/** Get the significand size of this floating-point type */
+inline unsigned TypeNode::getFloatingPointSignificandSize() const {
+ Assert(isFloatingPoint());
+ return getConst<FloatingPointSize>().significand();
+}
+
 /** Get the size of this bit-vector type */
 inline unsigned TypeNode::getBitVectorSize() const {
   Assert(isBitVector());