Floating point infrastructure.

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

31 files changed, 5380 insertions, 20 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index f88dcb3a9..e66d590dc 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -20,7 +20,7 @@ AM_CPPFLAGS = \
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(FLAG_VISIBILITY_HIDDEN)
 
 SUBDIRS = lib options expr util prop/minisat prop/bvminisat . parser compat bindings main
-THEORIES = builtin booleans uf arith bv arrays datatypes sets strings quantifiers idl
+THEORIES = builtin booleans uf arith bv fp arrays datatypes sets strings quantifiers idl
 
 lib_LTLIBRARIES = libcvc4.la
 
@@ -407,7 +407,12 @@ libcvc4_la_SOURCES = \
 	theory/booleans/circuit_propagator.cpp \
 	theory/booleans/boolean_term_conversion_mode.h \
 	theory/booleans/boolean_term_conversion_mode.cpp \
-	theory/booleans/options_handlers.h
+	theory/booleans/options_handlers.h \
+	theory/fp/theory_fp.h \
+	theory/fp/theory_fp.cpp \
+	theory/fp/theory_fp_rewriter.h \
+	theory/fp/theory_fp_rewriter.cpp \
+	theory/fp/theory_fp_type_rules.h
 
 nodist_libcvc4_la_SOURCES = \
 	smt/smt_options.cpp \
@@ -491,7 +496,9 @@ EXTRA_DIST = \
 	theory/example/ecdata.h \
 	theory/example/ecdata.cpp \
 	theory/example/theory_uf_tim.h \
-	theory/example/theory_uf_tim.cpp
+	theory/example/theory_uf_tim.cpp \
+	theory/fp/kinds \
+	theory/fp/options_handlers.h
 
 svn_versioninfo.cpp: svninfo
 	$(AM_V_GEN)( \
diff --git a/src/cvc4.i b/src/cvc4.i
index 3ad08660c..56404ee65 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -297,6 +297,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %include "util/unsafe_interrupt_exception.i"
 %include "util/integer.i"
 %include "util/rational.i"
+//%include "util/floatingpoint.i"
 %include "util/language.i"
 %include "util/cardinality.i"
 %include "util/bool.i"
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());
diff --git a/src/options/Makefile.am b/src/options/Makefile.am
index 2be82469e..24b78836a 100644
--- a/src/options/Makefile.am
+++ b/src/options/Makefile.am
@@ -40,7 +40,9 @@ OPTIONS_FILES_SRCS = \
 	../theory/idl/options.cpp \
 	../theory/idl/options.h \
 	../theory/sets/options.cpp \
-	../theory/sets/options.h
+	../theory/sets/options.h \
+	../theory/fp/options.cpp \
+	../theory/fp/options.h
 
 OPTIONS_FILES = \
 	$(patsubst %.cpp,%,$(filter %.cpp,$(OPTIONS_FILES_SRCS)))
@@ -101,7 +103,9 @@ nodist_liboptions_la_SOURCES = \
 	../theory/idl/options.cpp \
 	../theory/idl/options.h \
 	../theory/sets/options.cpp \
-	../theory/sets/options.h
+	../theory/sets/options.h \
+	../theory/fp/options.cpp \
+	../theory/fp/options.h
 
 BUILT_SOURCES = \
 	exprs-builts \
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 511b67997..1a5442419 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -112,10 +112,13 @@ namespace CVC4 {
 #include "util/output.h"
 #include "util/rational.h"
 #include "util/hash.h"
+#include "util/floatingpoint.h"
 #include <vector>
 #include <set>
 #include <string>
 #include <sstream>
+// \todo Review the need for this header
+#include "math.h"
 
 using namespace CVC4;
 using namespace CVC4::parser;
@@ -949,7 +952,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
   std::string name;
   std::vector<Expr> args;
   std::vector< std::pair<std::string, Type> > sortedVarNames;
-  Expr f, f2;
+  Expr f, f2, f3, f4;
   std::string attr;
   Expr attexpr;
   std::vector<Expr> patexprs;
@@ -1243,13 +1246,30 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
       // valid GMP rational string
       expr = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); }
 
-  | LPAREN_TOK INDEX_TOK bvLit=SIMPLE_SYMBOL size=INTEGER_LITERAL RPAREN_TOK
-    { if(AntlrInput::tokenText($bvLit).find("bv") == 0) {
-        expr = MK_CONST( AntlrInput::tokenToBitvector($bvLit, $size) );
-      } else {
-        PARSER_STATE->parseError("Unexpected symbol `" + AntlrInput::tokenText($bvLit) + "'");
+  | LPAREN_TOK INDEX_TOK 
+    ( bvLit=SIMPLE_SYMBOL size=INTEGER_LITERAL 
+      { if(AntlrInput::tokenText($bvLit).find("bv") == 0) {
+           expr = MK_CONST( AntlrInput::tokenToBitvector($bvLit, $size) );
+        } else {
+           PARSER_STATE->parseError("Unexpected symbol `" + AntlrInput::tokenText($bvLit) + "'");
+        }
       }
-    }
+    | FP_PINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+      { expr = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
+                                      AntlrInput::tokenToUnsigned($sb),
+                                      +INFINITY)); }
+    | FP_NINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+      { expr = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
+                                      AntlrInput::tokenToUnsigned($sb),
+                                     -INFINITY)); }
+    | FP_NAN_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+      { expr = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
+                                      AntlrInput::tokenToUnsigned($sb),
+                                      NAN)); }
+    // NOTE: Theory parametric constants go here
+
+    )
+    RPAREN_TOK
 
   | HEX_LITERAL
     { assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
@@ -1263,6 +1283,16 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
 
   | str[s,false]
     { expr = MK_CONST( ::CVC4::String(s) ); }
+  | FP_RNE_TOK      { expr = MK_CONST(roundNearestTiesToEven); }
+  | FP_RNA_TOK      { expr = MK_CONST(roundNearestTiesToAway); }
+  | FP_RTP_TOK      { expr = MK_CONST(roundTowardPositive); }
+  | FP_RTN_TOK      { expr = MK_CONST(roundTowardNegative); }
+  | FP_RTZ_TOK      { expr = MK_CONST(roundTowardZero); }
+  | FP_RNE_FULL_TOK { expr = MK_CONST(roundNearestTiesToEven); }
+  | FP_RNA_FULL_TOK { expr = MK_CONST(roundNearestTiesToAway); }
+  | FP_RTP_FULL_TOK { expr = MK_CONST(roundTowardPositive); }
+  | FP_RTN_FULL_TOK { expr = MK_CONST(roundTowardNegative); }
+  | FP_RTZ_FULL_TOK { expr = MK_CONST(roundTowardZero); }
 
   | RENOSTR_TOK
     { std::vector< Expr > nvec; expr = MK_EXPR( CVC4::kind::REGEXP_EMPTY, nvec ); }
@@ -1427,8 +1457,50 @@ indexedFunctionName[CVC4::Expr& op]
         if(PARSER_STATE->strictModeEnabled()) {
           PARSER_STATE->parseError("bv2nat and int2bv are not part of SMT-LIB, and aren't available in SMT-LIB strict compliance mode");
         } }
+    | FP_PINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+      { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
+                                    AntlrInput::tokenToUnsigned($sb),
+                                    +INFINITY)); }
+    | FP_NINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+      { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
+                                    AntlrInput::tokenToUnsigned($sb),
+                                    -INFINITY)); }
+    | FP_NAN_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+      { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
+                                    AntlrInput::tokenToUnsigned($sb),
+                                    NAN)); }
+    | FP_PZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+      { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
+                                    AntlrInput::tokenToUnsigned($sb),
+                                    +0.0)); }
+    | FP_NZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+      { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
+                                    AntlrInput::tokenToUnsigned($sb),
+                                    -0.0)); }
+    | FP_TO_FP_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+      { op = MK_CONST(FloatingPointToFPGeneric(AntlrInput::tokenToUnsigned($eb),
+                                               AntlrInput::tokenToUnsigned($sb))); }
+    | FP_TO_FPBV_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+      { op = MK_CONST(FloatingPointToFPIEEEBitVector(AntlrInput::tokenToUnsigned($eb),
+                                                     AntlrInput::tokenToUnsigned($sb))); }
+    | FP_TO_FPFP_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+      { op = MK_CONST(FloatingPointToFPFloatingPoint(AntlrInput::tokenToUnsigned($eb),
+                                                     AntlrInput::tokenToUnsigned($sb))); }
+    | FP_TO_FPR_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+      { op = MK_CONST(FloatingPointToFPReal(AntlrInput::tokenToUnsigned($eb),
+                                            AntlrInput::tokenToUnsigned($sb))); }
+    | FP_TO_FPS_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+      { op = MK_CONST(FloatingPointToFPSignedBitVector(AntlrInput::tokenToUnsigned($eb),
+                                                       AntlrInput::tokenToUnsigned($sb))); }
+    | FP_TO_FPU_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+      { op = MK_CONST(FloatingPointToFPUnsignedBitVector(AntlrInput::tokenToUnsigned($eb),
+                                                         AntlrInput::tokenToUnsigned($sb))); }
+    | FP_TO_UBV_TOK m=INTEGER_LITERAL
+      { op = MK_CONST(FloatingPointToUBV(AntlrInput::tokenToUnsigned($m))); }
+    | FP_TO_SBV_TOK m=INTEGER_LITERAL
+      { op = MK_CONST(FloatingPointToSBV(AntlrInput::tokenToUnsigned($m))); }
     | badIndexedFunctionName
-   )
+    )
     RPAREN_TOK
   ;
 
@@ -1623,6 +1695,32 @@ builtinOp[CVC4::Kind& kind]
   
   | INST_CLOSURE_TOK  { $kind = CVC4::kind::INST_CLOSURE; }
 
+  | FP_TOK        { $kind = CVC4::kind::FLOATINGPOINT_FP; }
+  | FP_EQ_TOK     { $kind = CVC4::kind::FLOATINGPOINT_EQ; }
+  | FP_ABS_TOK    { $kind = CVC4::kind::FLOATINGPOINT_ABS; }
+  | FP_NEG_TOK    { $kind = CVC4::kind::FLOATINGPOINT_NEG; }
+  | FP_PLUS_TOK   { $kind = CVC4::kind::FLOATINGPOINT_PLUS; }
+  | FP_SUB_TOK    { $kind = CVC4::kind::FLOATINGPOINT_SUB; }
+  | FP_MUL_TOK    { $kind = CVC4::kind::FLOATINGPOINT_MULT; }
+  | FP_DIV_TOK    { $kind = CVC4::kind::FLOATINGPOINT_DIV; }
+  | FP_FMA_TOK    { $kind = CVC4::kind::FLOATINGPOINT_FMA; }
+  | FP_SQRT_TOK   { $kind = CVC4::kind::FLOATINGPOINT_SQRT; }
+  | FP_REM_TOK    { $kind = CVC4::kind::FLOATINGPOINT_REM; }
+  | FP_RTI_TOK    { $kind = CVC4::kind::FLOATINGPOINT_RTI; }
+  | FP_MIN_TOK    { $kind = CVC4::kind::FLOATINGPOINT_MIN; }
+  | FP_MAX_TOK    { $kind = CVC4::kind::FLOATINGPOINT_MAX; }
+  | FP_LEQ_TOK    { $kind = CVC4::kind::FLOATINGPOINT_LEQ; }
+  | FP_LT_TOK     { $kind = CVC4::kind::FLOATINGPOINT_LT; }
+  | FP_GEQ_TOK    { $kind = CVC4::kind::FLOATINGPOINT_GEQ; }
+  | FP_GT_TOK     { $kind = CVC4::kind::FLOATINGPOINT_GT; }
+  | FP_ISN_TOK    { $kind = CVC4::kind::FLOATINGPOINT_ISN; }
+  | FP_ISSN_TOK   { $kind = CVC4::kind::FLOATINGPOINT_ISSN; }
+  | FP_ISZ_TOK    { $kind = CVC4::kind::FLOATINGPOINT_ISZ; }
+  | FP_ISINF_TOK  { $kind = CVC4::kind::FLOATINGPOINT_ISINF; }
+  | FP_ISNAN_TOK  { $kind = CVC4::kind::FLOATINGPOINT_ISNAN; }
+  | FP_ISNEG_TOK  { $kind = CVC4::kind::FLOATINGPOINT_ISNEG; }
+  | FP_ISPOS_TOK  { $kind = CVC4::kind::FLOATINGPOINT_ISPOS; }
+  | FP_TO_REAL_TOK {$kind = CVC4::kind::FLOATINGPOINT_TO_REAL; }
   // NOTE: Theory operators go here
   ;
 
@@ -1706,6 +1804,17 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
           PARSER_STATE->parseError("Illegal bitvector size: 0");
         }
         t = EXPR_MANAGER->mkBitVectorType(numerals.front());
+      } else if ( name == "FloatingPoint" ) {
+        if( numerals.size() != 2 ) {
+          PARSER_STATE->parseError("Illegal floating-point type.");
+        }
+        if(!validExponentSize(numerals[0])) {
+          PARSER_STATE->parseError("Illegal floating-point exponent size");
+        }
+        if(!validSignificandSize(numerals[1])) {
+          PARSER_STATE->parseError("Illegal floating-point significand size");
+        }
+        t = EXPR_MANAGER->mkFloatingPointType(numerals[0],numerals[1]);
       } else {
         std::stringstream ss;
         ss << "unknown indexed symbol `" << name << "'";
@@ -2035,6 +2144,56 @@ EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset';
 // tokenized and handled directly when
 // processing a term
 
+FP_TOK : 'fp';
+FP_PINF_TOK : '+oo';
+FP_NINF_TOK : '-oo';
+FP_PZERO_TOK : '+zero';
+FP_NZERO_TOK : '-zero';
+FP_NAN_TOK : 'NaN';
+FP_EQ_TOK : 'fp.eq';
+FP_ABS_TOK : 'fp.abs';
+FP_NEG_TOK : 'fp.neg';
+FP_PLUS_TOK : 'fp.add';
+FP_SUB_TOK : 'fp.sub';
+FP_MUL_TOK : 'fp.mul';
+FP_DIV_TOK : 'fp.div';
+FP_FMA_TOK : 'fp.fma';
+FP_SQRT_TOK : 'fp.sqrt';
+FP_REM_TOK : 'fp.rem';
+FP_RTI_TOK : 'fp.roundToIntegral';
+FP_MIN_TOK : 'fp.min';
+FP_MAX_TOK : 'fp.max';
+FP_LEQ_TOK : 'fp.leq';
+FP_LT_TOK : 'fp.lt';
+FP_GEQ_TOK : 'fp.geq';
+FP_GT_TOK : 'fp.gt';
+FP_ISN_TOK : 'fp.isNormal';
+FP_ISSN_TOK : 'fp.isSubnormal';
+FP_ISZ_TOK : 'fp.isZero';
+FP_ISINF_TOK : 'fp.isInfinite';
+FP_ISNAN_TOK : 'fp.isNaN';
+FP_ISNEG_TOK : 'fp.isNegative';
+FP_ISPOS_TOK : 'fp.isPositive';
+FP_TO_FP_TOK : 'to_fp';
+FP_TO_FPBV_TOK : 'to_fp_bv';
+FP_TO_FPFP_TOK : 'to_fp_fp';
+FP_TO_FPR_TOK : 'to_fp_real';
+FP_TO_FPS_TOK : 'to_fp_signed';
+FP_TO_FPU_TOK : 'to_fp_unsigned';
+FP_TO_UBV_TOK : 'fp.to_ubv';
+FP_TO_SBV_TOK : 'fp.to_sbv';
+FP_TO_REAL_TOK : 'fp.to_real';
+FP_RNE_TOK : 'RNE';
+FP_RNA_TOK : 'RNA';
+FP_RTP_TOK : 'RTP';
+FP_RTN_TOK : 'RTN';
+FP_RTZ_TOK : 'RTZ';
+FP_RNE_FULL_TOK : 'roundNearestTiesToEven';
+FP_RNA_FULL_TOK : 'roundNearestTiesToAway';
+FP_RTP_FULL_TOK : 'roundTowardPositive';
+FP_RTN_FULL_TOK : 'roundTowardNegative';
+FP_RTZ_FULL_TOK : 'roundTowardZero';
+
 /**
  * A sequence of printable ASCII characters (except backslash) that starts
  * and ends with | and does not otherwise contain |.
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 62814ca25..7740d0b94 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -95,6 +95,41 @@ void Smt2::addStringOperators() {
   Parser::addOperator(kind::STRING_LENGTH);
 }
 
+void Smt2::addFloatingPointOperators() {
+  Parser::addOperator(kind::FLOATINGPOINT_FP);
+  Parser::addOperator(kind::FLOATINGPOINT_EQ);
+  Parser::addOperator(kind::FLOATINGPOINT_ABS);
+  Parser::addOperator(kind::FLOATINGPOINT_NEG);
+  Parser::addOperator(kind::FLOATINGPOINT_PLUS);
+  Parser::addOperator(kind::FLOATINGPOINT_SUB);
+  Parser::addOperator(kind::FLOATINGPOINT_MULT);
+  Parser::addOperator(kind::FLOATINGPOINT_DIV);
+  Parser::addOperator(kind::FLOATINGPOINT_FMA);
+  Parser::addOperator(kind::FLOATINGPOINT_SQRT);
+  Parser::addOperator(kind::FLOATINGPOINT_REM);
+  Parser::addOperator(kind::FLOATINGPOINT_RTI);
+  Parser::addOperator(kind::FLOATINGPOINT_MIN);
+  Parser::addOperator(kind::FLOATINGPOINT_MAX);
+  Parser::addOperator(kind::FLOATINGPOINT_LEQ);
+  Parser::addOperator(kind::FLOATINGPOINT_LT);
+  Parser::addOperator(kind::FLOATINGPOINT_GEQ);
+  Parser::addOperator(kind::FLOATINGPOINT_GT);
+  Parser::addOperator(kind::FLOATINGPOINT_ISN);
+  Parser::addOperator(kind::FLOATINGPOINT_ISSN);
+  Parser::addOperator(kind::FLOATINGPOINT_ISZ);  
+  Parser::addOperator(kind::FLOATINGPOINT_ISINF);
+  Parser::addOperator(kind::FLOATINGPOINT_ISNAN);
+  Parser::addOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR);
+  Parser::addOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT);
+  Parser::addOperator(kind::FLOATINGPOINT_TO_FP_REAL);
+  Parser::addOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR);
+  Parser::addOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR);
+  Parser::addOperator(kind::FLOATINGPOINT_TO_UBV);
+  Parser::addOperator(kind::FLOATINGPOINT_TO_SBV);
+  Parser::addOperator(kind::FLOATINGPOINT_TO_REAL);
+}
+
+
 void Smt2::addTheory(Theory theory) {
   switch(theory) {
   case THEORY_ARRAYS:
@@ -172,6 +207,15 @@ void Smt2::addTheory(Theory theory) {
     Parser::addOperator(kind::APPLY_UF);
     break;
 
+  case THEORY_FP:
+    defineType("RoundingMode", getExprManager()->roundingModeType());
+    defineType("Float16", getExprManager()->mkFloatingPointType(5, 11));
+    defineType("Float32", getExprManager()->mkFloatingPointType(8, 24));
+    defineType("Float64", getExprManager()->mkFloatingPointType(11, 53));
+    defineType("Float128", getExprManager()->mkFloatingPointType(15, 113));
+    addFloatingPointOperators();
+    break;
+
   default:
     std::stringstream ss;
     ss << "internal error: unsupported theory " << theory;
@@ -222,6 +266,8 @@ bool Smt2::isTheoryEnabled(Theory theory) const {
     return d_logic.isTheoryEnabled(theory::THEORY_STRINGS);
   case THEORY_UF:
     return d_logic.isTheoryEnabled(theory::THEORY_UF);
+  case THEORY_FP:
+    return d_logic.isTheoryEnabled(theory::THEORY_FP);
   default:
     std::stringstream ss;
     ss << "internal error: unsupported theory " << theory;
@@ -301,6 +347,11 @@ void Smt2::setLogic(const std::string& name) {
   if(d_logic.isQuantified()) {
     addTheory(THEORY_QUANTIFIERS);
   }
+
+  if (d_logic.isTheoryEnabled(theory::THEORY_FP)) {
+    addTheory(THEORY_FP);
+  }
+
 }/* Smt2::setLogic() */
 
 void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 8c23c8657..82498b624 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -51,7 +51,8 @@ public:
     THEORY_QUANTIFIERS,
     THEORY_SETS,
     THEORY_STRINGS,
-    THEORY_UF
+    THEORY_UF,
+    THEORY_FP
   };
 
 private:
@@ -219,6 +220,8 @@ private:
 
   void addStringOperators();
 
+  void addFloatingPointOperators();
+
 };/* class Smt2 */
 
 }/* CVC4::parser namespace */
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 4f12ed012..b3b548450 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -42,6 +42,7 @@ namespace smt2 {
 static string smtKindString(Kind k) throw();
 
 static void printBvParameterizedOp(std::ostream& out, TNode n) throw();
+static void printFpParameterizedOp(std::ostream& out, TNode n) throw();
 
 void Smt2Printer::toStream(std::ostream& out, TNode n,
                            int toDepth, bool types, size_t dag) const throw() {
@@ -140,6 +141,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       case REAL_TYPE: out << "Real"; break;
       case INTEGER_TYPE: out << "Int"; break;
       case STRING_TYPE: out << "String"; break;
+      case ROUNDINGMODE_TYPE: out << "RoundingMode"; break;
       default:
         // fall back on whatever operator<< does on underlying type; we
         // might luck out and be SMT-LIB v2 compliant
@@ -149,6 +151,12 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     case kind::BITVECTOR_TYPE:
       out << "(_ BitVec " << n.getConst<BitVectorSize>().size << ")";
       break;
+    case kind::FLOATINGPOINT_TYPE:
+      out << "(_ FloatingPoint "
+	  << n.getConst<FloatingPointSize>().exponent() << " "
+	  << n.getConst<FloatingPointSize>().significand()
+	  << ")";
+      break;
     case kind::CONST_BITVECTOR: {
       const BitVector& bv = n.getConst<BitVector>();
       const Integer& x = bv.getValue();
@@ -163,6 +171,20 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       // }
       break;
     }
+    case kind::CONST_FLOATINGPOINT:
+      out << n.getConst<FloatingPoint>().getLiteral();
+      break;
+    case kind::CONST_ROUNDINGMODE:
+      switch (n.getConst<RoundingMode>()) {
+      case roundNearestTiesToEven : out << "roundNearestTiesToEven"; break;
+      case roundNearestTiesToAway : out << "roundNearestTiesToAway"; break;
+      case roundTowardPositive : out << "roundTowardPositive"; break;
+      case roundTowardNegative : out << "roundTowardNegative"; break;
+      case roundTowardZero : out << "roundTowardZero"; break;
+      default :
+	Unreachable("Invalid value of rounding mode constant (%d)",n.getConst<RoundingMode>());
+      }
+      break;
     case kind::CONST_BOOLEAN:
       // the default would print "1" or "0" for bool, that's not correct
       // for our purposes
@@ -448,7 +470,49 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::SET_TYPE:
   case kind::SINGLETON: out << smtKindString(k) << " "; break;
 
-   // datatypes
+    // fp theory
+  case kind::FLOATINGPOINT_FP:
+  case kind::FLOATINGPOINT_EQ:
+  case kind::FLOATINGPOINT_ABS:
+  case kind::FLOATINGPOINT_NEG:
+  case kind::FLOATINGPOINT_PLUS:
+  case kind::FLOATINGPOINT_SUB:
+  case kind::FLOATINGPOINT_MULT:
+  case kind::FLOATINGPOINT_DIV:
+  case kind::FLOATINGPOINT_FMA:
+  case kind::FLOATINGPOINT_SQRT:
+  case kind::FLOATINGPOINT_REM:
+  case kind::FLOATINGPOINT_RTI:
+  case kind::FLOATINGPOINT_MIN:
+  case kind::FLOATINGPOINT_MAX:
+  case kind::FLOATINGPOINT_LEQ:
+  case kind::FLOATINGPOINT_LT:
+  case kind::FLOATINGPOINT_GEQ:
+  case kind::FLOATINGPOINT_GT:
+  case kind::FLOATINGPOINT_ISN:
+  case kind::FLOATINGPOINT_ISSN:
+  case kind::FLOATINGPOINT_ISZ:
+  case kind::FLOATINGPOINT_ISINF:
+  case kind::FLOATINGPOINT_ISNAN:
+  case kind::FLOATINGPOINT_ISNEG:
+  case kind::FLOATINGPOINT_ISPOS:
+  case kind::FLOATINGPOINT_TO_REAL:
+    out << smtKindString(k) << ' '; break;
+
+  case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
+  case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT:
+  case kind::FLOATINGPOINT_TO_FP_REAL:
+  case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
+  case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
+  case kind::FLOATINGPOINT_TO_FP_GENERIC:
+  case kind::FLOATINGPOINT_TO_UBV:
+  case kind::FLOATINGPOINT_TO_SBV:
+    printFpParameterizedOp(out, n);
+    out << ' ';
+    stillNeedToPrintParams = false;
+    break;
+
+    // datatypes
   case kind::APPLY_TYPE_ASCRIPTION: {
       TypeNode t = TypeNode::fromType(n.getOperator().getConst<AscriptionType>().getType());
       if(t.getKind() == kind::TYPE_CONSTANT &&
@@ -657,6 +721,46 @@ static string smtKindString(Kind k) throw() {
   case kind::SET_TYPE: return "Set";
   case kind::SINGLETON: return "singleton";
   case kind::INSERT: return "insert";
+
+    // fp theory
+  case kind::FLOATINGPOINT_FP: return "fp";
+  case kind::FLOATINGPOINT_EQ: return "fp.eq";
+  case kind::FLOATINGPOINT_ABS: return "fp.abs";
+  case kind::FLOATINGPOINT_NEG: return "fp.neg";
+  case kind::FLOATINGPOINT_PLUS: return "fp.add";
+  case kind::FLOATINGPOINT_SUB: return "fp.sub";
+  case kind::FLOATINGPOINT_MULT: return "fp.mul";
+  case kind::FLOATINGPOINT_DIV: return "fp.div";
+  case kind::FLOATINGPOINT_FMA: return "fp.fma";
+  case kind::FLOATINGPOINT_SQRT: return "fp.sqrt";
+  case kind::FLOATINGPOINT_REM: return "fp.rem";
+  case kind::FLOATINGPOINT_RTI: return "fp.roundToIntegral";
+  case kind::FLOATINGPOINT_MIN: return "fp.min";
+  case kind::FLOATINGPOINT_MAX: return "fp.max";
+
+  case kind::FLOATINGPOINT_LEQ: return "fp.leq";
+  case kind::FLOATINGPOINT_LT: return "fp.lt";
+  case kind::FLOATINGPOINT_GEQ: return "fp.geq";
+  case kind::FLOATINGPOINT_GT: return "fp.gt";
+
+  case kind::FLOATINGPOINT_ISN: return "fp.isNormal";
+  case kind::FLOATINGPOINT_ISSN: return "fp.isSubnormal";
+  case kind::FLOATINGPOINT_ISZ: return "fp.isZero";  
+  case kind::FLOATINGPOINT_ISINF: return "fp.isInfinite";
+  case kind::FLOATINGPOINT_ISNAN: return "fp.isNaN";
+  case kind::FLOATINGPOINT_ISNEG: return "fp.isNegative";
+  case kind::FLOATINGPOINT_ISPOS: return "fp.isPositive";
+
+  case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: return "to_fp";
+  case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: return "to_fp";
+  case kind::FLOATINGPOINT_TO_FP_REAL: return "to_fp";
+  case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: return "to_fp";
+  case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: return "to_fp_unsigned";
+  case kind::FLOATINGPOINT_TO_FP_GENERIC: return "to_fp_unsigned";
+  case kind::FLOATINGPOINT_TO_UBV: return "fp.to_ubv";
+  case kind::FLOATINGPOINT_TO_SBV: return "fp.to_sbv";
+  case kind::FLOATINGPOINT_TO_REAL: return "fp.to_real";
+
   default:
     ; /* fall through */
   }
@@ -703,6 +807,58 @@ static void printBvParameterizedOp(std::ostream& out, TNode n) throw() {
   out << ")";
 }
 
+static void printFpParameterizedOp(std::ostream& out, TNode n) throw() {
+  out << "(_ ";
+  switch(n.getKind()) {
+  case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
+    //out << "to_fp_bv "
+    out << "to_fp "
+        << n.getOperator().getConst<FloatingPointToFPIEEEBitVector>().t.exponent() << ' '
+        << n.getOperator().getConst<FloatingPointToFPIEEEBitVector>().t.significand();
+    break;
+  case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT:
+    //out << "to_fp_fp "
+    out << "to_fp "
+        << n.getOperator().getConst<FloatingPointToFPFloatingPoint>().t.exponent() << ' '
+        << n.getOperator().getConst<FloatingPointToFPFloatingPoint>().t.significand();
+    break;
+  case kind::FLOATINGPOINT_TO_FP_REAL:
+    //out << "to_fp_real "
+    out << "to_fp "
+        << n.getOperator().getConst<FloatingPointToFPReal>().t.exponent() << ' '
+        << n.getOperator().getConst<FloatingPointToFPReal>().t.significand();
+    break;
+  case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
+    //out << "to_fp_signed "
+    out << "to_fp "
+        << n.getOperator().getConst<FloatingPointToFPSignedBitVector>().t.exponent() << ' '
+        << n.getOperator().getConst<FloatingPointToFPSignedBitVector>().t.significand();
+    break;
+  case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
+    out << "to_fp_unsigned "
+        << n.getOperator().getConst<FloatingPointToFPUnsignedBitVector>().t.exponent() << ' '
+        << n.getOperator().getConst<FloatingPointToFPUnsignedBitVector>().t.significand();
+    break;
+  case kind::FLOATINGPOINT_TO_FP_GENERIC:
+    out << "to_fp "
+        << n.getOperator().getConst<FloatingPointToFPGeneric>().t.exponent() << ' '
+        << n.getOperator().getConst<FloatingPointToFPGeneric>().t.significand();
+    break;
+  case kind::FLOATINGPOINT_TO_UBV:
+    out << "fp.to_ubv "
+        << n.getOperator().getConst<FloatingPointToUBV>().bvs.size;
+    break;
+  case kind::FLOATINGPOINT_TO_SBV:
+    out << "fp.to_sbv "
+        << n.getOperator().getConst<FloatingPointToSBV>().bvs.size;
+    break;
+  default:
+    out << n.getKind();
+  }
+  out << ")";
+}
+
+
 template <class T>
 static bool tryToStream(std::ostream& out, const Command* c) throw();
 template <class T>
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index ba3845d7a..7ab590d89 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -846,7 +846,17 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
                     k != kind::TUPLE_UPDATE &&
                     k != kind::RECORD_SELECT &&
                     k != kind::RECORD_UPDATE &&
-                    k != kind::DIVISIBLE) {
+                    k != kind::DIVISIBLE &&
+		    // Theory parametric functions go here
+		    k != kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR &&
+		    k != kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT &&
+		    k != kind::FLOATINGPOINT_TO_FP_REAL &&
+		    k != kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR &&
+		    k != kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR &&
+		    k != kind::FLOATINGPOINT_TO_UBV &&
+		    k != kind::FLOATINGPOINT_TO_SBV &&
+		    k != kind::FLOATINGPOINT_TO_REAL
+		    ) {
             Debug("bt") << "rewriting: " << top.getOperator() << endl;
             result.top() << rewriteBooleanTermsRec(top.getOperator(), theory::THEORY_BUILTIN, quantBoolVars);
             Debug("bt") << "got: " << result.top().getOperator() << endl;
diff --git a/src/theory/fp/kinds b/src/theory/fp/kinds
new file mode 100644
index 000000000..983d5aa5c
--- /dev/null
+++ b/src/theory/fp/kinds
@@ -0,0 +1,238 @@
+# kinds                                                               -*- sh -*-
+#
+# For documentation on this file format, please refer to
+# src/theory/builtin/kinds.
+#
+
+theory THEORY_FP ::CVC4::theory::fp::TheoryFp "theory/fp/theory_fp.h"
+typechecker "theory/fp/theory_fp_type_rules.h"
+rewriter ::CVC4::theory::fp::TheoryFpRewriter "theory/fp/theory_fp_rewriter.h"
+
+properties check
+
+# Theory content goes here.
+
+# constants...
+constant CONST_FLOATINGPOINT \
+    ::CVC4::FloatingPoint \
+    ::CVC4::FloatingPointHashFunction \
+    "util/floatingpoint.h" \
+    "a floating-point literal"
+typerule CONST_FLOATINGPOINT    ::CVC4::theory::fp::FloatingPointConstantTypeRule
+
+
+constant CONST_ROUNDINGMODE \
+    ::CVC4::RoundingMode \
+    ::CVC4::RoundingModeHashFunction \
+    "util/floatingpoint.h" \
+    "a floating-point rounding mode"    
+typerule CONST_ROUNDINGMODE    ::CVC4::theory::fp::RoundingModeConstantTypeRule
+
+
+
+# types...
+sort ROUNDINGMODE_TYPE \
+    5 \
+    well-founded \
+    "NodeManager::currentNM()->mkConst<RoundingMode>(RoundingMode())" \
+    "expr/node_manager.h" \
+    "floating-point rounding mode"
+
+constant FLOATINGPOINT_TYPE \
+    ::CVC4::FloatingPointSize \
+    ::CVC4::FloatingPointSizeHashFunction \
+    "util/floatingpoint.h" \
+    "floating-point type"
+#cardinality FLOATINGPOINT_TYPE "function" "header"
+#enumerator FLOATINGPOINT_TYPE "function" "header"
+#well-founded FLOATINGPOINT_TYPE true "function" "header"
+
+
+# operators...
+operator FLOATINGPOINT_FP 3 "construct a floating-point literal from bit vectors"
+typerule FLOATINGPOINT_FP    ::CVC4::theory::fp::FloatingPointFPTypeRule
+
+
+
+operator FLOATINGPOINT_EQ 2: "floating-point equality"
+typerule FLOATINGPOINT_EQ    ::CVC4::theory::fp::FloatingPointTestTypeRule
+
+operator FLOATINGPOINT_ABS 1 "floating-point absolute value"
+typerule FLOATINGPOINT_ABS   ::CVC4::theory::fp::FloatingPointOperationTypeRule
+
+operator FLOATINGPOINT_NEG 1 "floating-point negation"
+typerule FLOATINGPOINT_NEG   ::CVC4::theory::fp::FloatingPointOperationTypeRule
+
+operator FLOATINGPOINT_PLUS 3 "floating-point addition"
+typerule FLOATINGPOINT_PLUS   ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule
+
+operator FLOATINGPOINT_SUB 3 "floating-point sutraction"
+typerule FLOATINGPOINT_SUB   ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule
+
+operator FLOATINGPOINT_MULT 3 "floating-point multiply"
+typerule FLOATINGPOINT_MULT   ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule
+
+operator FLOATINGPOINT_DIV 3 "floating-point division"
+typerule FLOATINGPOINT_DIV   ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule
+
+operator FLOATINGPOINT_FMA 4 "floating-point fused multiply and add"
+typerule FLOATINGPOINT_FMA   ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule
+
+operator FLOATINGPOINT_SQRT 2 "floating-point square root"
+typerule FLOATINGPOINT_SQRT   ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule
+
+operator FLOATINGPOINT_REM 2 "floating-point remainder"
+typerule FLOATINGPOINT_REM   ::CVC4::theory::fp::FloatingPointOperationTypeRule
+
+operator FLOATINGPOINT_RTI 2 "floating-point round to integral"
+typerule FLOATINGPOINT_RTI   ::CVC4::theory::fp::FloatingPointRoundingOperationTypeRule
+
+operator FLOATINGPOINT_MIN 2 "floating-point minimum"
+typerule FLOATINGPOINT_MIN   ::CVC4::theory::fp::FloatingPointOperationTypeRule
+
+operator FLOATINGPOINT_MAX 2 "floating-point maximum"
+typerule FLOATINGPOINT_MAX   ::CVC4::theory::fp::FloatingPointOperationTypeRule
+
+
+operator FLOATINGPOINT_LEQ 2 "floating-point less than or equal"
+typerule FLOATINGPOINT_LEQ   ::CVC4::theory::fp::FloatingPointTestTypeRule
+
+operator FLOATINGPOINT_LT 2 "floating-point less than"
+typerule FLOATINGPOINT_LT   ::CVC4::theory::fp::FloatingPointTestTypeRule
+
+operator FLOATINGPOINT_GEQ 2 "floating-point greater than or equal"
+typerule FLOATINGPOINT_GEQ   ::CVC4::theory::fp::FloatingPointTestTypeRule
+
+operator FLOATINGPOINT_GT 2 "floating-point greater than"
+typerule FLOATINGPOINT_GT   ::CVC4::theory::fp::FloatingPointTestTypeRule
+
+
+
+operator FLOATINGPOINT_ISN 1 "floating-point is normal"
+typerule FLOATINGPOINT_ISN   ::CVC4::theory::fp::FloatingPointTestTypeRule
+
+operator FLOATINGPOINT_ISSN 1 "floating-point is sub-normal"
+typerule FLOATINGPOINT_ISSN   ::CVC4::theory::fp::FloatingPointTestTypeRule
+
+operator FLOATINGPOINT_ISZ 1 "floating-point is zero"
+typerule FLOATINGPOINT_ISZ   ::CVC4::theory::fp::FloatingPointTestTypeRule
+
+operator FLOATINGPOINT_ISINF 1 "floating-point is infinite"
+typerule FLOATINGPOINT_ISINF   ::CVC4::theory::fp::FloatingPointTestTypeRule
+
+operator FLOATINGPOINT_ISNAN 1 "floating-point is NaN"
+typerule FLOATINGPOINT_ISNAN   ::CVC4::theory::fp::FloatingPointTestTypeRule
+
+operator FLOATINGPOINT_ISNEG 1 "floating-point is negative"
+typerule FLOATINGPOINT_ISNEG   ::CVC4::theory::fp::FloatingPointTestTypeRule
+
+operator FLOATINGPOINT_ISPOS 1 "floating-point is positive"
+typerule FLOATINGPOINT_ISPOS   ::CVC4::theory::fp::FloatingPointTestTypeRule
+
+
+
+constant FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP \
+    ::CVC4::FloatingPointToFPIEEEBitVector \
+    "::CVC4::FloatingPointConvertSortHashFunction<0x1>" \
+    "util/floatingpoint.h" \
+    "operator for to_fp from bit vector"
+typerule FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule
+
+parameterized FLOATINGPOINT_TO_FP_IEEE_BITVECTOR FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP 1 "convert an IEEE-754 bit vector to floating-point"
+typerule FLOATINGPOINT_TO_FP_IEEE_BITVECTOR   ::CVC4::theory::fp::FloatingPointToFPIEEEBitVectorTypeRule
+
+
+
+constant FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP \
+    ::CVC4::FloatingPointToFPFloatingPoint \
+    "::CVC4::FloatingPointConvertSortHashFunction<0x2>" \
+    "util/floatingpoint.h" \
+    "operator for to_fp from floating point"
+typerule FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule
+
+parameterized FLOATINGPOINT_TO_FP_FLOATINGPOINT FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP 2 "convert between floating-point sorts"
+typerule FLOATINGPOINT_TO_FP_FLOATINGPOINT   ::CVC4::theory::fp::FloatingPointToFPFloatingPointTypeRule
+
+
+
+
+constant FLOATINGPOINT_TO_FP_REAL_OP \
+    ::CVC4::FloatingPointToFPReal \
+    "::CVC4::FloatingPointConvertSortHashFunction<0x4>" \
+    "util/floatingpoint.h" \
+    "operator for to_fp from real"
+typerule FLOATINGPOINT_TO_FP_REAL_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule
+
+parameterized FLOATINGPOINT_TO_FP_REAL FLOATINGPOINT_TO_FP_REAL_OP 2 "convert a real to floating-point"
+typerule FLOATINGPOINT_TO_FP_REAL   ::CVC4::theory::fp::FloatingPointToFPRealTypeRule
+
+
+
+constant FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP \
+    ::CVC4::FloatingPointToFPSignedBitVector \
+    "::CVC4::FloatingPointConvertSortHashFunction<0x8>" \
+    "util/floatingpoint.h" \
+    "operator for to_fp from signed bit vector"
+typerule FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule
+
+parameterized FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP 2 "convert a signed bit vector to floating-point"
+typerule FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR   ::CVC4::theory::fp::FloatingPointToFPSignedBitVectorTypeRule
+
+
+
+constant FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP \
+    ::CVC4::FloatingPointToFPUnsignedBitVector \
+    "::CVC4::FloatingPointConvertSortHashFunction<0x10>" \
+    "util/floatingpoint.h" \
+    "operator for to_fp from unsigned bit vector"
+typerule FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule
+
+
+parameterized FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP 2 "convert an unsigned bit vector to floating-point"
+typerule FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR   ::CVC4::theory::fp::FloatingPointToFPUnsignedBitVectorTypeRule
+
+
+
+constant FLOATINGPOINT_TO_FP_GENERIC_OP \
+    ::CVC4::FloatingPointToFPGeneric \
+    "::CVC4::FloatingPointConvertSortHashFunction<0x11>" \
+    "util/floatingpoint.h" \
+    "operator for a generic to_fp"
+typerule FLOATINGPOINT_TO_FP_GENERIC_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule
+
+
+parameterized FLOATINGPOINT_TO_FP_GENERIC FLOATINGPOINT_TO_FP_GENERIC_OP 1:2 "a generic conversion to floating-point, used in parsing only"
+typerule FLOATINGPOINT_TO_FP_GENERIC   ::CVC4::theory::fp::FloatingPointToFPGenericTypeRule
+
+
+
+
+
+constant FLOATINGPOINT_TO_UBV_OP \
+    ::CVC4::FloatingPointToUBV \
+    "::CVC4::FloatingPointToBVHashFunction<0x1>" \
+    "util/floatingpoint.h" \
+    "operator for to_ubv"
+typerule FLOATINGPOINT_TO_UBV_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule
+
+parameterized FLOATINGPOINT_TO_UBV FLOATINGPOINT_TO_UBV_OP 2 "convert a floating-point value to an unsigned bit vector"
+typerule FLOATINGPOINT_TO_UBV   ::CVC4::theory::fp::FloatingPointToUBVTypeRule
+
+
+
+constant FLOATINGPOINT_TO_SBV_OP \
+    ::CVC4::FloatingPointToSBV \
+    "::CVC4::FloatingPointToBVHashFunction<0x2>" \
+    "util/floatingpoint.h" \
+    "operator for to_sbv"
+typerule FLOATINGPOINT_TO_SBV_OP ::CVC4::theory::fp::FloatingPointParametricOpTypeRule
+
+parameterized FLOATINGPOINT_TO_SBV FLOATINGPOINT_TO_SBV_OP 2 "convert a floating-point value to a signed bit vector"
+typerule FLOATINGPOINT_TO_SBV   ::CVC4::theory::fp::FloatingPointToSBVTypeRule
+
+
+operator FLOATINGPOINT_TO_REAL 1 "floating-point to real"
+typerule FLOATINGPOINT_TO_REAL   ::CVC4::theory::fp::FloatingPointToRealTypeRule
+
+
+endtheory
diff --git a/src/theory/fp/options b/src/theory/fp/options
new file mode 100644
index 000000000..3fee94d1d
--- /dev/null
+++ b/src/theory/fp/options
@@ -0,0 +1,8 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module FP "theory/fp/options.h" Fp
+
+endmodule
diff --git a/src/theory/fp/options_handlers.h b/src/theory/fp/options_handlers.h
new file mode 100644
index 000000000..f1a86e396
--- /dev/null
+++ b/src/theory/fp/options_handlers.h
@@ -0,0 +1,14 @@
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__FP__OPTIONS_HANDLERS_H
+#define __CVC4__THEORY__FP__OPTIONS_HANDLERS_H
+
+namespace CVC4 {
+namespace theory {
+namespace fp {
+
+}/* CVC4::theory::fp namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__FP__OPTIONS_HANDLERS_H */
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
new file mode 100644
index 000000000..6400fec38
--- /dev/null
+++ b/src/theory/fp/theory_fp.cpp
@@ -0,0 +1,104 @@
+#include "theory/fp/theory_fp.h"
+
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+namespace fp {
+
+namespace removeToFPGeneric {
+  
+  Node removeToFPGeneric (TNode node) {
+    Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC);
+    
+    FloatingPointToFPGeneric info = node.getOperator().getConst<FloatingPointToFPGeneric>();
+    
+    size_t children = node.getNumChildren();
+    
+    Node op;
+    
+    if (children == 1) {
+      op = NodeManager::currentNM()->mkConst(FloatingPointToFPIEEEBitVector(info.t.exponent(),
+									    info.t.significand()));
+      return NodeManager::currentNM()->mkNode(op, node[0]);
+      
+    } else {
+      Assert(children == 2);
+      Assert(node[0].getType().isRoundingMode());
+      
+      TypeNode t = node[1].getType();
+      
+      if (t.isFloatingPoint()) {
+	op = NodeManager::currentNM()->mkConst(FloatingPointToFPFloatingPoint(info.t.exponent(),
+									      info.t.significand()));
+      } else if (t.isReal()) {
+	op = NodeManager::currentNM()->mkConst(FloatingPointToFPReal(info.t.exponent(),
+								     info.t.significand()));
+      } else if (t.isBitVector()) {
+	op = NodeManager::currentNM()->mkConst(FloatingPointToFPSignedBitVector(info.t.exponent(),
+										info.t.significand()));
+	
+      } else {
+	throw TypeCheckingExceptionPrivate(node, "cannot rewrite to_fp generic due to incorrect type of second argument");
+      }
+      
+      return NodeManager::currentNM()->mkNode(op, node[0], node[1]);
+    }
+    
+    Unreachable("to_fp generic not rewritten");
+  }
+}
+
+
+/** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
+TheoryFp::TheoryFp(context::Context* c,
+                           context::UserContext* u,
+                           OutputChannel& out,
+                           Valuation valuation,
+                           const LogicInfo& logicInfo) :
+  Theory(THEORY_FP, c, u, out, valuation, logicInfo) {
+}/* TheoryFp::TheoryFp() */
+
+
+Node TheoryFp::expandDefinition(LogicRequest &, Node node) {
+  Trace("fp-expandDefinition") << "TheoryFp::expandDefinition(): " << node << std::endl;
+
+  if (node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC) {
+    Node res(removeToFPGeneric::removeToFPGeneric(node));
+
+    Trace("fp-expandDefinition") << "TO_FP_GENERIC rewritten to " << res << std::endl;
+
+    return res;
+  } else {
+    return node;
+  }
+}
+
+
+void TheoryFp::check(Effort level) {
+  if (done() && !fullEffort(level)) {
+    return;
+  }
+
+  while(!done()) {
+    // Get all the assertions
+    Assertion assertion = get();
+    TNode fact = assertion.assertion;
+
+    Debug("fp") << "TheoryFp::check(): processing " << fact << std::endl;
+
+    // Do the work
+    switch(fact.getKind()) {
+
+    /* cases for all the theory's kinds go here... */
+
+    default:
+      Unhandled(fact.getKind());
+    }
+  }
+
+}/* TheoryFp::check() */
+
+}/* CVC4::theory::fp namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
new file mode 100644
index 000000000..6fb41685f
--- /dev/null
+++ b/src/theory/fp/theory_fp.h
@@ -0,0 +1,36 @@
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__FP__THEORY_FP_H
+#define __CVC4__THEORY__FP__THEORY_FP_H
+
+#include "theory/theory.h"
+
+namespace CVC4 {
+namespace theory {
+namespace fp {
+
+class TheoryFp : public Theory {
+public:
+
+  /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
+  TheoryFp(context::Context* c,
+               context::UserContext* u,
+               OutputChannel& out,
+               Valuation valuation,
+               const LogicInfo& logicInfo);
+
+  Node expandDefinition(LogicRequest &, Node node);
+
+  void check(Effort);
+
+  std::string identify() const {
+    return "THEORY_FP";
+  }
+
+};/* class TheoryFp */
+
+}/* CVC4::theory::fp namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__FP__THEORY_FP_H */
diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
new file mode 100644
index 000000000..0c41e8ff7
--- /dev/null
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -0,0 +1,478 @@
+/*********************                                                        */
+/*! \file theory_fp_rewriter.cpp
+ ** \verbatim
+ ** Original author: Martin Brain
+ ** Major contributors: 
+ ** Minor contributors (to current version): 
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013  University of Oxford
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Rewrite rules for floating point theories. ]]
+ **
+ ** \todo [[ Constant folding
+ **          Push negations up through arithmetic operators (include max and min? maybe not due to +0/-0)
+ **          classifications to normal tests (maybe)
+ **          (= x (fp.neg x)) --> (isNaN x)
+ **          (fp.eq x (fp.neg x)) --> (isZero x)   (previous and reorganise should be sufficient)
+ **          (fp.eq x const) --> various = depending on const 
+ **          (fp.abs (fp.neg x)) --> (fp.abs x)
+ **          (fp.isPositive (fp.neg x)) --> (fp.isNegative x)
+ **          (fp.isNegative (fp.neg x)) --> (fp.isPositive x)
+ **          (fp.isPositive (fp.abs x)) --> (not (isNaN x))
+ **          (fp.isNegative (fp.abs x)) --> false
+ **       ]]
+ **/
+
+#include "theory/fp/theory_fp_rewriter.h"
+
+#include "util/cvc4_assert.h"
+
+#include <algorithm>
+
+namespace CVC4 {
+namespace theory {
+namespace fp {
+
+namespace rewrite {
+  /** Rewrite rules **/
+
+  RewriteResponse notFP (TNode node, bool) {
+    Unreachable("non floating-point kind (%d) in floating point rewrite?",node.getKind());
+  }
+
+  RewriteResponse identity (TNode node, bool) {
+    return RewriteResponse(REWRITE_DONE, node);
+  }
+
+  RewriteResponse type (TNode node, bool) {
+    Unreachable("sort kind (%d) found in expression?",node.getKind());
+    return RewriteResponse(REWRITE_DONE, node);
+  }
+
+  RewriteResponse removeDoubleNegation (TNode node, bool) {
+    Assert(node.getKind() == kind::FLOATINGPOINT_NEG);
+    if (node[0].getKind() == kind::FLOATINGPOINT_NEG) {
+      RewriteResponse(REWRITE_AGAIN, node[0][0]);
+    }
+
+    return RewriteResponse(REWRITE_DONE, node);
+  }
+
+  RewriteResponse convertSubtractionToAddition (TNode node, bool) {
+    Assert(node.getKind() == kind::FLOATINGPOINT_SUB);
+    Node negation = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_NEG,node[2]);
+    Node addition = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_PLUS,node[0],node[1],negation);
+    return RewriteResponse(REWRITE_DONE, addition);
+  }
+
+
+  /* Implies (fp.eq x x) --> (not (isNaN x))
+   */
+
+  RewriteResponse ieeeEqToEq (TNode node, bool) {
+    Assert(node.getKind() == kind::FLOATINGPOINT_EQ);
+    NodeManager *nm = NodeManager::currentNM();
+
+    return RewriteResponse(REWRITE_DONE,
+			   nm->mkNode(kind::AND,
+				      nm->mkNode(kind::AND,
+						 nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[0])),
+						 nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[1]))),
+				      nm->mkNode(kind::OR,
+						 nm->mkNode(kind::EQUAL, node[0], node[1]),
+						 nm->mkNode(kind::AND,
+							    nm->mkNode(kind::FLOATINGPOINT_ISZ, node[0]),
+							    nm->mkNode(kind::FLOATINGPOINT_ISZ, node[1])))));
+  }
+
+
+  RewriteResponse geqToleq (TNode node, bool) {
+    Assert(node.getKind() == kind::FLOATINGPOINT_GEQ);
+    return RewriteResponse(REWRITE_DONE,NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_LEQ,node[1],node[0]));
+  }
+
+  RewriteResponse gtTolt (TNode node, bool) {
+    Assert(node.getKind() == kind::FLOATINGPOINT_GT);
+    return RewriteResponse(REWRITE_DONE,NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_LT,node[1],node[0]));
+  }
+
+  RewriteResponse removed (TNode node, bool) {  
+    Unreachable("kind (%d) should have been removed?",node.getKind());
+    return RewriteResponse(REWRITE_DONE, node);
+  }
+
+  RewriteResponse variable (TNode node, bool) {  
+    // We should only get floating point and rounding mode variables to rewrite.
+    TypeNode tn = node.getType(true);
+    Assert(tn.isFloatingPoint() || tn.isRoundingMode());
+ 
+    // Not that we do anything with them...
+    return RewriteResponse(REWRITE_DONE, node);
+  }
+
+  RewriteResponse equal (TNode node, bool isPreRewrite) {  
+    // We should only get equalities of floating point or rounding mode types.
+    Assert(node.getKind() == kind::EQUAL);
+
+    TypeNode tn = node[0].getType(true);
+
+    Assert(tn.isFloatingPoint() || tn.isRoundingMode());
+    Assert(tn == node[1].getType(true));   // Should be ensured by the typing rules
+
+    if (node[0] == node[1]) {
+      return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
+    } else if (!isPreRewrite && (node[0] > node[1])) {
+	Node normal = NodeManager::currentNM()->mkNode(kind::EQUAL,node[1],node[0]);
+	return RewriteResponse(REWRITE_DONE, normal);
+    } else {
+      return RewriteResponse(REWRITE_DONE, node);
+    }
+  }
+
+  RewriteResponse convertFromRealLiteral (TNode node, bool) {
+    Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_REAL);
+
+    // \todo Honour the rounding mode and work for something other than doubles!
+
+    if (node[1].getKind() == kind::CONST_RATIONAL) {
+      TNode op = node.getOperator();
+      const FloatingPointToFPReal &param = op.getConst<FloatingPointToFPReal>();
+      Node lit =
+	NodeManager::currentNM()->mkConst(FloatingPoint(param.t.exponent(),
+							param.t.significand(),
+							node[1].getConst<Rational>().getDouble()));
+      
+      return RewriteResponse(REWRITE_DONE, lit);
+    } else {
+      return RewriteResponse(REWRITE_DONE, node);
+    }
+  }
+
+  RewriteResponse convertFromIEEEBitVectorLiteral (TNode node, bool) {
+    Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR);
+
+    // \todo Handle arbitrary length bit vectors without using strings!
+
+    if (node[0].getKind() == kind::CONST_BITVECTOR) {
+      TNode op = node.getOperator();
+      const FloatingPointToFPIEEEBitVector &param = op.getConst<FloatingPointToFPIEEEBitVector>();
+      const BitVector &bv = node[0].getConst<BitVector>();
+      std::string bitString(bv.toString());
+
+      Node lit =
+	NodeManager::currentNM()->mkConst(FloatingPoint(param.t.exponent(),
+							param.t.significand(),
+							bitString));
+
+      return RewriteResponse(REWRITE_DONE, lit);
+    } else {
+      return RewriteResponse(REWRITE_DONE, node);
+    }
+  }
+
+  RewriteResponse convertFromLiteral (TNode node, bool) {
+    Assert(node.getKind() == kind::FLOATINGPOINT_FP);
+
+    // \todo Handle arbitrary length bit vectors without using strings!
+
+    if ((node[0].getKind() == kind::CONST_BITVECTOR) &&
+	(node[1].getKind() == kind::CONST_BITVECTOR) &&
+	(node[2].getKind() == kind::CONST_BITVECTOR)) {
+
+      BitVector bv(node[0].getConst<BitVector>());
+      bv = bv.concat(node[1].getConst<BitVector>());
+      bv = bv.concat(node[2].getConst<BitVector>());
+
+      std::string bitString(bv.toString());
+      std::reverse(bitString.begin(), bitString.end());
+
+      // +1 to support the hidden bit
+      Node lit =
+	NodeManager::currentNM()->mkConst(FloatingPoint(node[1].getConst<BitVector>().getSize(),
+							node[2].getConst<BitVector>().getSize() + 1,
+							bitString));
+
+      return RewriteResponse(REWRITE_DONE, lit);
+    } else {
+      return RewriteResponse(REWRITE_DONE, node);
+    }
+  }
+
+  // Note these cannot be assumed to be symmetric for +0/-0, thus no symmetry reorder
+  RewriteResponse compactMinMax (TNode node, bool isPreRewrite) {
+    Kind k = node.getKind();
+
+    Assert((k == kind::FLOATINGPOINT_MIN) || (k == kind::FLOATINGPOINT_MAX));
+
+    if (node[0] == node[1]) {
+      return RewriteResponse(REWRITE_DONE, node[0]);
+    } else {
+      return RewriteResponse(REWRITE_DONE, node);
+    }
+  }
+
+
+  RewriteResponse reorderFPEquality (TNode node, bool isPreRewrite) {
+    Assert(node.getKind() == kind::FLOATINGPOINT_EQ);
+    Assert(!isPreRewrite);    // Likely redundant in pre-rewrite
+
+    if (node[0] > node[1]) {
+      Node normal = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_EQ,node[1],node[0]);
+      return RewriteResponse(REWRITE_DONE, normal);
+    } else {
+      return RewriteResponse(REWRITE_DONE, node);
+    } 
+  }
+
+  RewriteResponse reorderBinaryOperation (TNode node, bool isPreRewrite) {
+    Kind k = node.getKind();
+    Assert((k == kind::FLOATINGPOINT_PLUS) || (k == kind::FLOATINGPOINT_MULT));
+    Assert(!isPreRewrite);    // Likely redundant in pre-rewrite
+
+    if (node[1] > node[2]) {
+      Node normal = NodeManager::currentNM()->mkNode(k,node[0],node[2],node[1]);
+      return RewriteResponse(REWRITE_DONE, normal);
+    } else {
+      return RewriteResponse(REWRITE_DONE, node);
+    } 
+  }
+
+  RewriteResponse reorderFMA (TNode node, bool isPreRewrite) {
+    Assert(node.getKind() == kind::FLOATINGPOINT_FMA);
+    Assert(!isPreRewrite);    // Likely redundant in pre-rewrite
+
+    if (node[1] > node[2]) {
+      Node normal = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_FMA,node[0],node[2],node[1],node[3]);
+      return RewriteResponse(REWRITE_DONE, normal);
+    } else {
+      return RewriteResponse(REWRITE_DONE, node);
+    } 
+  }
+
+  RewriteResponse removeSignOperations (TNode node, bool isPreRewrite) {
+    Assert(node.getKind() == kind::FLOATINGPOINT_ISN   ||
+	   node.getKind() == kind::FLOATINGPOINT_ISSN  ||
+	   node.getKind() == kind::FLOATINGPOINT_ISZ   ||
+	   node.getKind() == kind::FLOATINGPOINT_ISINF ||
+	   node.getKind() == kind::FLOATINGPOINT_ISNAN);
+    Assert(node.getNumChildren() == 1);
+
+    Kind childKind(node[0].getKind());
+
+    if ((childKind == kind::FLOATINGPOINT_NEG) ||
+	(childKind == kind::FLOATINGPOINT_ABS)) {
+
+      Node rewritten = NodeManager::currentNM()->mkNode(node.getKind(),node[0][0]);
+      return RewriteResponse(REWRITE_AGAIN, rewritten);
+    } else {
+      return RewriteResponse(REWRITE_DONE, node);
+    } 
+  }
+
+
+}; /* CVC4::theory::fp::rewrite */
+
+RewriteFunction TheoryFpRewriter::preRewriteTable[kind::LAST_KIND]; 
+RewriteFunction TheoryFpRewriter::postRewriteTable[kind::LAST_KIND]; 
+
+
+  /**
+   * Initialize the rewriter.
+   */
+  void TheoryFpRewriter::init() {
+
+    /* Set up the pre-rewrite dispatch table */
+    for (unsigned i = 0; i < kind::LAST_KIND; ++i) {
+      preRewriteTable[i] = rewrite::notFP;
+    }
+
+    /******** Constants ********/
+    /* No rewriting possible for constants */
+    preRewriteTable[kind::CONST_FLOATINGPOINT] = rewrite::identity;
+    preRewriteTable[kind::CONST_ROUNDINGMODE] = rewrite::identity; 
+
+    /******** Sorts(?) ********/
+    /* These kinds should only appear in types */
+    //preRewriteTable[kind::ROUNDINGMODE_TYPE] = rewrite::type;
+    preRewriteTable[kind::FLOATINGPOINT_TYPE] = rewrite::type;
+      
+    /******** Operations ********/
+    preRewriteTable[kind::FLOATINGPOINT_FP] = rewrite::identity;
+    preRewriteTable[kind::FLOATINGPOINT_ABS] = rewrite::identity;
+    preRewriteTable[kind::FLOATINGPOINT_NEG] = rewrite::removeDoubleNegation;
+    preRewriteTable[kind::FLOATINGPOINT_PLUS] = rewrite::identity;
+    preRewriteTable[kind::FLOATINGPOINT_SUB] = rewrite::convertSubtractionToAddition;
+    preRewriteTable[kind::FLOATINGPOINT_MULT] = rewrite::identity;
+    preRewriteTable[kind::FLOATINGPOINT_DIV] = rewrite::identity;
+    preRewriteTable[kind::FLOATINGPOINT_FMA] = rewrite::identity;
+    preRewriteTable[kind::FLOATINGPOINT_SQRT] = rewrite::identity;
+    preRewriteTable[kind::FLOATINGPOINT_REM] = rewrite::identity;
+    preRewriteTable[kind::FLOATINGPOINT_RTI] = rewrite::identity;
+    preRewriteTable[kind::FLOATINGPOINT_MIN] = rewrite::compactMinMax;
+    preRewriteTable[kind::FLOATINGPOINT_MAX] = rewrite::compactMinMax;
+
+    /******** Comparisons ********/
+    preRewriteTable[kind::FLOATINGPOINT_EQ] = rewrite::ieeeEqToEq;
+    preRewriteTable[kind::FLOATINGPOINT_LEQ] = rewrite::identity;
+    preRewriteTable[kind::FLOATINGPOINT_LT] = rewrite::identity;
+    preRewriteTable[kind::FLOATINGPOINT_GEQ] = rewrite::geqToleq;
+    preRewriteTable[kind::FLOATINGPOINT_GT] = rewrite::gtTolt;
+
+    /******** Classifications ********/
+    preRewriteTable[kind::FLOATINGPOINT_ISN] = rewrite::identity;
+    preRewriteTable[kind::FLOATINGPOINT_ISSN] = rewrite::identity;
+    preRewriteTable[kind::FLOATINGPOINT_ISZ] = rewrite::identity;  
+    preRewriteTable[kind::FLOATINGPOINT_ISINF] = rewrite::identity;
+    preRewriteTable[kind::FLOATINGPOINT_ISNAN] = rewrite::identity;
+    preRewriteTable[kind::FLOATINGPOINT_ISNEG] = rewrite::identity;
+    preRewriteTable[kind::FLOATINGPOINT_ISPOS] = rewrite::identity;
+
+    /******** Conversions ********/
+    preRewriteTable[kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR] = rewrite::identity;
+    preRewriteTable[kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT] = rewrite::identity;
+    preRewriteTable[kind::FLOATINGPOINT_TO_FP_REAL] = rewrite::identity;
+    preRewriteTable[kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR] = rewrite::identity;
+    preRewriteTable[kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR] = rewrite::identity;
+    preRewriteTable[kind::FLOATINGPOINT_TO_FP_GENERIC] = rewrite::removed;
+    preRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity;
+    preRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity;
+    preRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity;
+
+    /******** Variables ********/
+    preRewriteTable[kind::VARIABLE] = rewrite::variable;
+    preRewriteTable[kind::BOUND_VARIABLE] = rewrite::variable;
+
+    preRewriteTable[kind::EQUAL] = rewrite::equal;
+
+
+
+
+    /* Set up the post-rewrite dispatch table */
+    for (unsigned i = 0; i < kind::LAST_KIND; ++i) {
+      postRewriteTable[i] = rewrite::notFP;
+    }
+
+    /******** Constants ********/
+    /* No rewriting possible for constants */
+    postRewriteTable[kind::CONST_FLOATINGPOINT] = rewrite::identity;
+    postRewriteTable[kind::CONST_ROUNDINGMODE] = rewrite::identity; 
+
+    /******** Sorts(?) ********/
+    /* These kinds should only appear in types */
+    //postRewriteTable[kind::ROUNDINGMODE_TYPE] = rewrite::type;
+    postRewriteTable[kind::FLOATINGPOINT_TYPE] = rewrite::type;
+      
+    /******** Operations ********/
+    postRewriteTable[kind::FLOATINGPOINT_FP] = rewrite::convertFromLiteral;
+    postRewriteTable[kind::FLOATINGPOINT_ABS] = rewrite::identity;
+    postRewriteTable[kind::FLOATINGPOINT_NEG] = rewrite::removeDoubleNegation;
+    postRewriteTable[kind::FLOATINGPOINT_PLUS] = rewrite::reorderBinaryOperation;
+    postRewriteTable[kind::FLOATINGPOINT_SUB] = rewrite::removed;
+    postRewriteTable[kind::FLOATINGPOINT_MULT] = rewrite::reorderBinaryOperation;
+    postRewriteTable[kind::FLOATINGPOINT_DIV] = rewrite::identity;
+    postRewriteTable[kind::FLOATINGPOINT_FMA] = rewrite::reorderFMA;
+    postRewriteTable[kind::FLOATINGPOINT_SQRT] = rewrite::identity;
+    postRewriteTable[kind::FLOATINGPOINT_REM] = rewrite::identity;
+    postRewriteTable[kind::FLOATINGPOINT_RTI] = rewrite::identity;
+    postRewriteTable[kind::FLOATINGPOINT_MIN] = rewrite::compactMinMax;
+    postRewriteTable[kind::FLOATINGPOINT_MAX] = rewrite::compactMinMax;
+
+    /******** Comparisons ********/
+    postRewriteTable[kind::FLOATINGPOINT_EQ] = rewrite::removed;
+    postRewriteTable[kind::FLOATINGPOINT_LEQ] = rewrite::identity;
+    postRewriteTable[kind::FLOATINGPOINT_LT] = rewrite::identity;
+    postRewriteTable[kind::FLOATINGPOINT_GEQ] = rewrite::removed;
+    postRewriteTable[kind::FLOATINGPOINT_GT] = rewrite::removed;
+
+    /******** Classifications ********/
+    postRewriteTable[kind::FLOATINGPOINT_ISN] = rewrite::removeSignOperations;
+    postRewriteTable[kind::FLOATINGPOINT_ISSN] = rewrite::removeSignOperations;
+    postRewriteTable[kind::FLOATINGPOINT_ISZ] = rewrite::removeSignOperations;
+    postRewriteTable[kind::FLOATINGPOINT_ISINF] = rewrite::removeSignOperations;
+    postRewriteTable[kind::FLOATINGPOINT_ISNAN] = rewrite::removeSignOperations;
+    postRewriteTable[kind::FLOATINGPOINT_ISNEG] = rewrite::identity;
+    postRewriteTable[kind::FLOATINGPOINT_ISPOS] = rewrite::identity;
+
+    /******** Conversions ********/
+    postRewriteTable[kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR] = rewrite::convertFromIEEEBitVectorLiteral;
+    postRewriteTable[kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT] = rewrite::identity;
+    postRewriteTable[kind::FLOATINGPOINT_TO_FP_REAL] = rewrite::convertFromRealLiteral;
+    postRewriteTable[kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR] = rewrite::identity;
+    postRewriteTable[kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR] = rewrite::identity;
+    postRewriteTable[kind::FLOATINGPOINT_TO_FP_GENERIC] = rewrite::removed;
+    postRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity;
+    postRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity;
+    postRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity;
+
+    /******** Variables ********/
+    postRewriteTable[kind::VARIABLE] = rewrite::variable;
+    postRewriteTable[kind::BOUND_VARIABLE] = rewrite::variable;
+
+    postRewriteTable[kind::EQUAL] = rewrite::equal;
+
+
+  }
+
+
+
+
+  /**
+   * Rewrite a node into the normal form for the theory of fp
+   * in pre-order (really topological order)---meaning that the
+   * children may not be in the normal form.  This is an optimization
+   * for theories with cancelling terms (e.g., 0 * (big-nasty-expression)
+   * in arithmetic rewrites to 0 without the need to look at the big
+   * nasty expression).  Since it's only an optimization, the
+   * implementation here can do nothing.
+   */
+
+  RewriteResponse TheoryFpRewriter::preRewrite(TNode node) {
+    Trace("fp-rewrite") << "TheoryFpRewriter::preRewrite(): " << node << std::endl;
+    RewriteResponse res = preRewriteTable [node.getKind()] (node, true);
+    if (res.node != node) {
+      Debug("fp-rewrite") << "TheoryFpRewriter::preRewrite(): before " << node << std::endl;
+      Debug("fp-rewrite") << "TheoryFpRewriter::preRewrite(): after  " << res.node << std::endl;
+    }
+    return res;
+  }
+
+
+  /**
+   * Rewrite a node into the normal form for the theory of fp.
+   * Called in post-order (really reverse-topological order) when
+   * traversing the expression DAG during rewriting.  This is the
+   * main function of the rewriter, and because of the ordering,
+   * it can assume its children are all rewritten already.
+   *
+   * This function can return one of three rewrite response codes
+   * along with the rewritten node:
+   *
+   *   REWRITE_DONE indicates that no more rewriting is needed.
+   *   REWRITE_AGAIN means that the top-level expression should be
+   *     rewritten again, but that its children are in final form.
+   *   REWRITE_AGAIN_FULL means that the entire returned expression
+   *     should be rewritten again (top-down with preRewrite(), then
+   *     bottom-up with postRewrite()).
+   *
+   * Even if this function returns REWRITE_DONE, if the returned
+   * expression belongs to a different theory, it will be fully
+   * rewritten by that theory's rewriter.
+   */
+
+  RewriteResponse TheoryFpRewriter::postRewrite(TNode node) {
+    Trace("fp-rewrite") << "TheoryFpRewriter::postRewrite(): " << node << std::endl;
+    RewriteResponse res = postRewriteTable [node.getKind()] (node, false);
+    if (res.node != node) {
+      Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): before " << node << std::endl;
+      Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): after  " << res.node << std::endl;
+    }
+    return res;
+  }
+
+
+}/* CVC4::theory::fp namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
diff --git a/src/theory/fp/theory_fp_rewriter.h b/src/theory/fp/theory_fp_rewriter.h
new file mode 100644
index 000000000..8a8f1c933
--- /dev/null
+++ b/src/theory/fp/theory_fp_rewriter.h
@@ -0,0 +1,48 @@
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__FP__THEORY_FP_REWRITER_H
+#define __CVC4__THEORY__FP__THEORY_FP_REWRITER_H
+
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace fp {
+
+typedef RewriteResponse (*RewriteFunction) (TNode, bool);
+
+class TheoryFpRewriter {
+ protected :
+  static RewriteFunction preRewriteTable[kind::LAST_KIND];
+  static RewriteFunction postRewriteTable[kind::LAST_KIND];
+
+ public:
+
+  static RewriteResponse preRewrite(TNode node);
+  static RewriteResponse postRewrite(TNode node);
+
+
+  /**
+   * Rewrite an equality, in case special handling is required.
+   */
+  static Node rewriteEquality(TNode equality) {
+    // often this will suffice
+    return postRewrite(equality).node;
+  }
+
+  static void init();
+
+  /**
+   * Shut down the rewriter.
+   */
+  static inline void shutdown() {
+    // nothing to do
+  }
+
+};/* class TheoryFpRewriter */
+
+}/* CVC4::theory::fp namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__FP__THEORY_FP_REWRITER_H */
diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h
new file mode 100644
index 000000000..2c9a67984
--- /dev/null
+++ b/src/theory/fp/theory_fp_type_rules.h
@@ -0,0 +1,430 @@
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H
+#define __CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H
+
+namespace CVC4 {
+namespace theory {
+namespace fp {
+
+#define TRACE(FUNCTION) Trace("fp-type") << FUNCTION "::computeType(" << check << "): " << n << std::endl
+
+
+class FloatingPointConstantTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    TRACE("FloatingPointConstantTypeRule");
+
+    const FloatingPoint &f = n.getConst<FloatingPoint>();
+    
+    if (check) {
+      if (!(validExponentSize(f.t.exponent()))) {
+        throw TypeCheckingExceptionPrivate(n, "constant with invalid exponent size");
+      }
+      if (!(validSignificandSize(f.t.significand()))) {
+        throw TypeCheckingExceptionPrivate(n, "constant with invalid significand size");
+      }
+    }
+    return nodeManager->mkFloatingPointType(f.t);
+  }
+};
+
+
+class RoundingModeConstantTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    TRACE("RoundingModeConstantTypeRule");
+
+    // Nothing to check!
+    return nodeManager->roundingModeType();
+  }
+};
+
+
+
+class FloatingPointFPTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    TRACE("FloatingPointFPTypeRule");
+
+    TypeNode signType = n[0].getType(check);
+    TypeNode exponentType = n[1].getType(check);
+    TypeNode significandType = n[2].getType(check);
+
+    if (!signType.isBitVector() ||
+	!exponentType.isBitVector() ||
+	!significandType.isBitVector()) {
+      throw TypeCheckingExceptionPrivate(n, "arguments to fp must be bit vectors");
+    }
+
+    unsigned signBits = signType.getBitVectorSize();
+    unsigned exponentBits = exponentType.getBitVectorSize();
+    unsigned significandBits = significandType.getBitVectorSize();
+
+    if (check) {
+
+      if (signBits != 1) {
+	throw TypeCheckingExceptionPrivate(n, "sign bit vector in fp must be 1 bit long");
+      } else if (!(validExponentSize(exponentBits))) {
+	throw TypeCheckingExceptionPrivate(n, "exponent bit vector in fp is an invalid size");
+      } else if (!(validSignificandSize(significandBits))) {
+	throw TypeCheckingExceptionPrivate(n, "significand bit vector in fp is an invalid size");
+      }
+    }
+
+    // The +1 is for the implicit hidden bit
+    return nodeManager->mkFloatingPointType(exponentBits,significandBits + 1);
+  }
+
+};
+
+
+class FloatingPointTestTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    TRACE("FloatingPointTestTypeRule");
+
+    if (check) {
+      TypeNode firstOperand = n[0].getType(check);
+
+      if (!firstOperand.isFloatingPoint()) {
+	throw TypeCheckingExceptionPrivate(n, "floating-point test applied to a non floating-point sort");
+      }
+
+      size_t children = n.getNumChildren();
+      for (size_t i = 1; i < children; ++i) {
+	if (!(n[i].getType(check) == firstOperand)) {
+	  throw TypeCheckingExceptionPrivate(n, "floating-point test applied to mixed sorts");
+	}
+      }
+    }
+
+    return nodeManager->booleanType();
+  }
+};
+
+
+class FloatingPointOperationTypeRule {
+public :
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    TRACE("FloatingPointOperationTypeRule");
+
+    TypeNode firstOperand = n[0].getType(check);
+
+    if (check) {
+      if (!firstOperand.isFloatingPoint()) {
+	throw TypeCheckingExceptionPrivate(n, "floating-point operation applied to a non floating-point sort");
+      }
+
+      size_t children = n.getNumChildren();
+      for (size_t i = 1; i < children; ++i) {
+	if (!(n[i].getType(check) == firstOperand)) {
+	  throw TypeCheckingExceptionPrivate(n, "floating-point test applied to mixed sorts");
+	}
+      }
+    }
+
+    return firstOperand;
+  }
+};
+
+
+class FloatingPointRoundingOperationTypeRule {
+public :
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    TRACE("FloatingPointRoundingOperationTypeRule");
+
+    if (check) {
+      TypeNode roundingModeType = n[0].getType(check);
+
+      if (!roundingModeType.isRoundingMode()) {
+	throw TypeCheckingExceptionPrivate(n, "first argument must be a rounding mode");
+      }
+    }
+
+
+    TypeNode firstOperand = n[1].getType(check);
+
+    if (check) {
+      if (!firstOperand.isFloatingPoint()) {
+	throw TypeCheckingExceptionPrivate(n, "floating-point operation applied to a non floating-point sort");
+      }
+
+      size_t children = n.getNumChildren();
+      for (size_t i = 2; i < children; ++i) {
+	if (!(n[i].getType(check) == firstOperand)) {
+	  throw TypeCheckingExceptionPrivate(n, "floating-point test applied to mixed sorts");
+	}
+      }
+    }
+
+    return firstOperand;
+  }
+};
+
+class FloatingPointParametricOpTypeRule {
+public :
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    TRACE("FloatingPointParametricOpTypeRule");
+
+    return nodeManager->builtinOperatorType();
+  }
+};
+
+class FloatingPointToFPIEEEBitVectorTypeRule {
+public :
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    TRACE("FloatingPointToFPIEEEBitVectorTypeRule");
+
+    FloatingPointToFPIEEEBitVector info = n.getOperator().getConst<FloatingPointToFPIEEEBitVector>();
+
+    if (check) {
+      TypeNode operandType = n[0].getType(check);
+      
+      if (!(operandType.isBitVector())) {
+	throw TypeCheckingExceptionPrivate(n, "conversion to floating-point from bit vector used with sort other than bit vector");
+      } else if (!(operandType.getBitVectorSize() == info.t.exponent() + info.t.significand())) {
+	throw TypeCheckingExceptionPrivate(n, "conversion to floating-point from bit vector used with bit vector length that does not match floating point parameters");
+      }
+    }
+
+    return nodeManager->mkFloatingPointType(info.t);
+  }
+};
+
+
+class FloatingPointToFPFloatingPointTypeRule {
+public :
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    TRACE("FloatingPointToFPFloatingPointTypeRule");
+
+    FloatingPointToFPFloatingPoint info = n.getOperator().getConst<FloatingPointToFPFloatingPoint>();
+
+    if (check) {
+      TypeNode roundingModeType = n[0].getType(check);
+
+      if (!roundingModeType.isRoundingMode()) {
+	throw TypeCheckingExceptionPrivate(n, "first argument must be a rounding mode");
+      }
+
+
+      TypeNode operandType = n[1].getType(check);
+      
+      if (!(operandType.isFloatingPoint())) {
+	throw TypeCheckingExceptionPrivate(n, "conversion to floating-point from floating-point used with sort other than floating-point");
+      }
+    }
+
+    return nodeManager->mkFloatingPointType(info.t);
+  }
+};
+
+
+class FloatingPointToFPRealTypeRule {
+public :
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    TRACE("FloatingPointToFPRealTypeRule");
+
+    FloatingPointToFPReal info = n.getOperator().getConst<FloatingPointToFPReal>();
+
+    if (check) {
+      TypeNode roundingModeType = n[0].getType(check);
+
+      if (!roundingModeType.isRoundingMode()) {
+	throw TypeCheckingExceptionPrivate(n, "first argument must be a rounding mode");
+      }
+
+
+      TypeNode operandType = n[1].getType(check);
+      
+      if (!(operandType.isReal())) {
+	throw TypeCheckingExceptionPrivate(n, "conversion to floating-point from real used with sort other than real");
+      }
+    }
+
+    return nodeManager->mkFloatingPointType(info.t);
+  }
+};
+
+
+class FloatingPointToFPSignedBitVectorTypeRule {
+public :
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    TRACE("FloatingPointToFPSignedBitVectorTypeRule");
+
+    FloatingPointToFPSignedBitVector info = n.getOperator().getConst<FloatingPointToFPSignedBitVector>();
+
+    if (check) {
+      TypeNode roundingModeType = n[0].getType(check);
+
+      if (!roundingModeType.isRoundingMode()) {
+	throw TypeCheckingExceptionPrivate(n, "first argument must be a rounding mode");
+      }
+
+
+      TypeNode operandType = n[1].getType(check);
+      
+      if (!(operandType.isBitVector())) {
+	throw TypeCheckingExceptionPrivate(n, "conversion to floating-point from signed bit vector used with sort other than bit vector");
+      }
+    }
+
+    return nodeManager->mkFloatingPointType(info.t);
+  }
+};
+
+
+class FloatingPointToFPUnsignedBitVectorTypeRule {
+public :
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    TRACE("FloatingPointToFPUnsignedBitVectorTypeRule");
+
+    FloatingPointToFPUnsignedBitVector info = n.getOperator().getConst<FloatingPointToFPUnsignedBitVector>();
+
+    if (check) {
+      TypeNode roundingModeType = n[0].getType(check);
+
+      if (!roundingModeType.isRoundingMode()) {
+	throw TypeCheckingExceptionPrivate(n, "first argument must be a rounding mode");
+      }
+
+
+      TypeNode operandType = n[1].getType(check);
+      
+      if (!(operandType.isBitVector())) {
+	throw TypeCheckingExceptionPrivate(n, "conversion to floating-point from unsigned bit vector used with sort other than bit vector");
+      }
+    }
+
+    return nodeManager->mkFloatingPointType(info.t);
+  }
+};
+
+
+
+class FloatingPointToFPGenericTypeRule {
+public :
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    TRACE("FloatingPointToFPGenericTypeRule");
+
+    FloatingPointToFPGeneric info = n.getOperator().getConst<FloatingPointToFPGeneric>();
+
+    if (check) {
+      /* As this is a generic kind intended only for parsing,
+       * the checking here is light.  For better checking, use
+       * expandDefinitions first.
+       */
+
+      size_t children = n.getNumChildren();
+      for (size_t i = 0; i < children; ++i) {
+	n[i].getType(check);
+      }
+    }
+
+    return nodeManager->mkFloatingPointType(info.t);
+  }
+};
+
+
+
+class FloatingPointToUBVTypeRule {
+public :
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    TRACE("FloatingPointToUBVTypeRule");
+
+    FloatingPointToUBV info = n.getOperator().getConst<FloatingPointToUBV>();
+
+    if (check) {
+      TypeNode roundingModeType = n[0].getType(check);
+
+      if (!roundingModeType.isRoundingMode()) {
+	throw TypeCheckingExceptionPrivate(n, "first argument must be a rounding mode");
+      }
+
+
+      TypeNode operandType = n[1].getType(check);
+      
+      if (!(operandType.isFloatingPoint())) {
+	throw TypeCheckingExceptionPrivate(n, "conversion to unsigned bit vector used with a sort other than floating-point");
+      }
+    }
+
+    return nodeManager->mkBitVectorType(info.bvs);
+  }
+};
+
+
+class FloatingPointToSBVTypeRule {
+public :
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    TRACE("FloatingPointToSBVTypeRule");
+
+    FloatingPointToSBV info = n.getOperator().getConst<FloatingPointToSBV>();
+
+    if (check) {
+      TypeNode roundingModeType = n[0].getType(check);
+
+      if (!roundingModeType.isRoundingMode()) {
+	throw TypeCheckingExceptionPrivate(n, "first argument must be a rounding mode");
+      }
+
+
+      TypeNode operandType = n[1].getType(check);
+      
+      if (!(operandType.isFloatingPoint())) {
+	throw TypeCheckingExceptionPrivate(n, "conversion to signed bit vector used with a sort other than floating-point");
+      }
+    }
+
+    return nodeManager->mkBitVectorType(info.bvs);
+  }
+};
+
+
+
+class FloatingPointToRealTypeRule {
+public :
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    TRACE("FloatingPointToRealTypeRule");
+
+    if (check) {
+      TypeNode roundingModeType = n[0].getType(check);
+
+      if (!roundingModeType.isRoundingMode()) {
+	throw TypeCheckingExceptionPrivate(n, "first argument must be a rounding mode");
+      }
+
+      TypeNode operand = n[1].getType(check);
+
+      if (!operand.isFloatingPoint()) {
+	throw TypeCheckingExceptionPrivate(n, "floating-point to real applied to a non floating-point sort");
+      }
+    }
+
+    return nodeManager->realType();
+  }
+};
+
+
+
+}/* CVC4::theory::fp namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H */
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 4ea30d5c9..635262a1e 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -107,6 +107,10 @@ std::string LogicInfo::getLogicString() const {
         ss << "BV";
         ++seen;
       }
+      if(d_theories[THEORY_FP]) {
+        ss << "FP";
+        ++seen;
+      }
       if(d_theories[THEORY_DATATYPES]) {
         ss << "DT";
         ++seen;
@@ -206,6 +210,10 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
         enableTheory(THEORY_BV);
         p += 2;
       }
+      if(!strncmp(p, "FP", 2)) {
+        enableTheory(THEORY_FP);
+        p += 2;
+      }
       if(!strncmp(p, "DT", 2)) {
         enableTheory(THEORY_DATATYPES);
         p += 2;
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index cca98db60..df787d049 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -100,6 +100,8 @@ libutil_la_SOURCES = \
 	didyoumean.cpp \
 	unsat_core.h \
 	unsat_core.cpp \
+	floatingpoint.h \
+	floatingpoint.cpp \
 	resource_manager.h \
 	resource_manager.cpp \
 	unsafe_interrupt_exception.h
@@ -164,7 +166,8 @@ EXTRA_DIST = \
 	resource_manager.i \
 	unsafe_interrupt_exception.i \
 	proof.i \
-	unsat_core.i
+	unsat_core.i \
+	floatingpoint.i
 
 DISTCLEANFILES = \
 	integer.h.tmp \
diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp
new file mode 100644
index 000000000..1aed6331e
--- /dev/null
+++ b/src/util/floatingpoint.cpp
@@ -0,0 +1,38 @@
+/*********************                                                        */
+/*! \file floatingpoint.cpp
+ ** \verbatim
+ ** Original author: Martin Brain
+ ** Major contributors:
+ ** Minor contributors (to current version):
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013  University of Oxford
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Implementations of the utility functions for working with floating point theories. ]]
+ **
+ **/
+
+#include "util/cvc4_assert.h"
+#include "util/floatingpoint.h"
+
+namespace CVC4 {
+
+  FloatingPointSize::FloatingPointSize (unsigned _e, unsigned _s) : e(_e), s(_s)
+  {
+    CheckArgument(validExponentSize(_e),_e,"Invalid exponent size : %d",_e);
+    CheckArgument(validSignificandSize(_s),_s,"Invalid significand size : %d",_s);
+  }
+
+  FloatingPointSize::FloatingPointSize (const FloatingPointSize &old) : e(old.e), s(old.s)
+  {
+    CheckArgument(validExponentSize(e),e,"Invalid exponent size : %d",e);
+    CheckArgument(validSignificandSize(s),s,"Invalid significand size : %d",s);
+  }
+
+  void FloatingPointLiteral::unfinished (void) const {
+    Unimplemented("Floating-point literals not yet implemented.");
+  }
+
+}/* CVC4 namespace */
+
diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h
new file mode 100644
index 000000000..e0678d389
--- /dev/null
+++ b/src/util/floatingpoint.h
@@ -0,0 +1,293 @@
+/*********************                                                        */
+/*! \file floatingpoint.h
+ ** \verbatim
+ ** Original author: Martin Brain
+ ** Major contributors:
+ ** Minor contributors (to current version):
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013  University of Oxford
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Utility functions for working with floating point theories. ]]
+ **
+ ** [[ This file contains the data structures used by the constant and
+ **    parametric types of the floating point theory. ]]
+ **/
+
+#include <fenv.h>
+
+#include "cvc4_public.h"
+
+#include "util/bitvector.h"
+
+
+#ifndef __CVC4__FLOATINGPOINT_H
+#define __CVC4__FLOATINGPOINT_H
+
+
+
+namespace CVC4 {
+
+
+  // Inline these!
+  inline bool CVC4_PUBLIC validExponentSize (unsigned e) { return e >= 2; }
+  inline bool CVC4_PUBLIC validSignificandSize (unsigned s) { return s >= 2; }
+
+  /**
+   * Floating point sorts are parameterised by two non-zero constants
+   * giving the width (in bits) of the exponent and significand
+   * (including the hidden bit).
+   */
+  class CVC4_PUBLIC FloatingPointSize {
+    /*
+      Class invariants:
+      * VALIDEXPONENTSIZE(e)
+      * VALIDSIGNIFCANDSIZE(s)
+     */
+
+  private :
+    unsigned e;
+    unsigned s;
+
+  public :
+    FloatingPointSize (unsigned _e, unsigned _s);
+    FloatingPointSize (const FloatingPointSize &old);
+
+    inline unsigned exponent (void) const {
+      return this->e;
+    }
+
+    inline unsigned significand (void) const {
+      return this->s;
+    }
+
+    bool operator ==(const FloatingPointSize& fps) const {
+      return (e == fps.e) && (s == fps.s);
+    }
+
+  }; /* class FloatingPointSize */
+
+
+
+#define ROLL(X,N) (((X) << (N)) | ((X) >> (8*sizeof((X)) - (N)) ))
+
+  struct CVC4_PUBLIC FloatingPointSizeHashFunction {
+    inline size_t operator() (const FloatingPointSize& fpt) const {
+      return size_t(ROLL(fpt.exponent(), 4*sizeof(unsigned)) |
+		    fpt.significand());
+    }
+  }; /* struct FloatingPointSizeHashFunction */
+
+
+
+
+
+
+
+
+
+
+  /**
+   * A concrete instance of the rounding mode sort
+   */
+  enum CVC4_PUBLIC RoundingMode {
+    roundNearestTiesToEven = FE_TONEAREST,
+    roundNearestTiesToAway,
+    roundTowardPositive = FE_UPWARD,
+    roundTowardNegative = FE_DOWNWARD,
+    roundTowardZero = FE_TOWARDZERO
+  }; /* enum RoundingMode */
+
+  struct CVC4_PUBLIC RoundingModeHashFunction {
+    inline size_t operator() (const RoundingMode& rm) const {
+      return size_t(rm);
+    }
+  }; /* struct RoundingModeHashFunction */
+
+
+
+
+
+
+
+
+
+
+  /**
+   * A concrete floating point number
+   */
+
+  class CVC4_PUBLIC FloatingPointLiteral {
+  public :
+    // This intentional left unfinished as the choice of literal
+    // representation is solver specific.
+    void unfinished (void) const;
+
+    FloatingPointLiteral(unsigned, unsigned, double) { unfinished(); }
+    FloatingPointLiteral(unsigned, unsigned, const std::string &) { unfinished(); }
+    FloatingPointLiteral(const FloatingPointLiteral &) { unfinished(); }
+
+    bool operator == (const FloatingPointLiteral &op) const {
+      unfinished();
+      return false;
+    }
+
+    size_t hash (void) const {
+      unfinished();
+      return 23;
+    }
+  };
+
+  class CVC4_PUBLIC FloatingPoint {
+  protected :
+    FloatingPointLiteral fpl;
+
+  public :
+    FloatingPointSize t;
+
+    FloatingPoint (unsigned e, unsigned s, double d) : fpl(e,s,d), t(e,s) {}
+    FloatingPoint (unsigned e, unsigned s, const std::string &bitString) : fpl(e,s,bitString), t(e,s) {}
+    FloatingPoint (const FloatingPoint &fp) : fpl(fp.fpl), t(fp.t) {}
+
+    bool operator ==(const FloatingPoint& fp) const {
+      return ( (t == fp.t) && fpl == fp.fpl );
+    }
+
+    const FloatingPointLiteral & getLiteral (void) const {
+      return this->fpl;
+    }
+
+  }; /* class FloatingPoint */
+
+
+  struct CVC4_PUBLIC FloatingPointHashFunction {
+    inline size_t operator() (const FloatingPoint& fp) const {
+      FloatingPointSizeHashFunction h;
+      return h(fp.t) ^ fp.getLiteral().hash();
+    }
+  }; /* struct FloatingPointHashFunction */
+
+
+
+
+
+
+
+  /**
+   * The parameter type for the conversions to floating point.
+   */
+  class CVC4_PUBLIC FloatingPointConvertSort {
+  public :
+    FloatingPointSize t;
+
+    FloatingPointConvertSort (unsigned _e, unsigned _s)
+      : t(_e,_s) {}
+
+    bool operator ==(const FloatingPointConvertSort& fpcs) const {
+      return t == fpcs.t;
+    }
+
+  };
+
+  /**
+   * As different conversions are different parameterised kinds, there
+   * is a need for different (C++) types for each one.
+   */
+
+  class CVC4_PUBLIC FloatingPointToFPIEEEBitVector : public FloatingPointConvertSort {
+  public : FloatingPointToFPIEEEBitVector (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+  };
+  class CVC4_PUBLIC FloatingPointToFPFloatingPoint : public FloatingPointConvertSort {
+  public : FloatingPointToFPFloatingPoint (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+  };
+  class CVC4_PUBLIC FloatingPointToFPReal : public FloatingPointConvertSort {
+  public : FloatingPointToFPReal (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+  };
+  class CVC4_PUBLIC FloatingPointToFPSignedBitVector : public FloatingPointConvertSort {
+  public : FloatingPointToFPSignedBitVector (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+  };
+  class CVC4_PUBLIC FloatingPointToFPUnsignedBitVector : public FloatingPointConvertSort {
+  public : FloatingPointToFPUnsignedBitVector (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+  };
+  class CVC4_PUBLIC FloatingPointToFPGeneric : public FloatingPointConvertSort {
+  public : FloatingPointToFPGeneric (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+  };
+
+
+
+  template <unsigned key>
+  struct CVC4_PUBLIC FloatingPointConvertSortHashFunction {
+    inline size_t operator() (const FloatingPointConvertSort& fpcs) const {
+      FloatingPointSizeHashFunction f;
+      return f(fpcs.t) ^ (0x00005300 | (key << 24));
+    }
+  }; /* struct FloatingPointConvertSortHashFunction */
+
+
+
+
+
+
+
+
+  /**
+   * The parameter type for the conversion to bit vector.
+   */
+  class CVC4_PUBLIC FloatingPointToBV {
+  public :
+    BitVectorSize bvs;
+
+    FloatingPointToBV (unsigned s)
+      : bvs(s) {}
+    operator unsigned () const { return bvs; }
+  };
+
+  class CVC4_PUBLIC FloatingPointToUBV : public FloatingPointToBV {
+  public : FloatingPointToUBV (unsigned _s) : FloatingPointToBV(_s) {}
+  };
+  class CVC4_PUBLIC FloatingPointToSBV : public FloatingPointToBV {
+  public : FloatingPointToSBV (unsigned _s) : FloatingPointToBV(_s) {}
+  };
+
+
+  template <unsigned key>
+  struct CVC4_PUBLIC FloatingPointToBVHashFunction {
+    inline size_t operator() (const FloatingPointToBV& fptbv) const {
+      UnsignedHashFunction< ::CVC4::BitVectorSize > f;
+      return 	(key ^ 0x46504256) ^ f(fptbv.bvs);
+    }
+  }; /* struct FloatingPointToBVHashFunction */
+
+
+
+
+
+
+  inline std::ostream& operator <<(std::ostream& os, const FloatingPointLiteral& fp) CVC4_PUBLIC;
+  inline std::ostream& operator <<(std::ostream& os, const FloatingPointLiteral& fp) {
+    fp.unfinished();
+    return os;
+  }
+
+  inline std::ostream& operator <<(std::ostream& os, const FloatingPoint& fp) CVC4_PUBLIC;
+  inline std::ostream& operator <<(std::ostream& os, const FloatingPoint& fp) {
+    return os << fp.getLiteral();
+  }
+
+  inline std::ostream& operator <<(std::ostream& os, const FloatingPointSize& fps) CVC4_PUBLIC;
+  inline std::ostream& operator <<(std::ostream& os, const FloatingPointSize& fps) {
+    return os << "(_ FloatingPoint " << fps.exponent() << " " << fps.significand() << ")";
+  }
+
+  inline std::ostream& operator <<(std::ostream& os, const FloatingPointConvertSort& fpcs) CVC4_PUBLIC;
+  inline std::ostream& operator <<(std::ostream& os, const FloatingPointConvertSort& fpcs) {
+    return os << "(_ to_fp " << fpcs.t.exponent() << " " << fpcs.t.significand() << ")";
+  }
+
+
+
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__FLOATINGPOINT_H */
diff --git a/src/util/floatingpoint.i b/src/util/floatingpoint.i
new file mode 100644
index 000000000..c66cc311d
--- /dev/null
+++ b/src/util/floatingpoint.i
@@ -0,0 +1,5 @@
+%{
+#include "util/floatingpoint.h"
+%}
+
+%include "util/floatingpoint.h"
diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index 007378528..efc7c5582 100644
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -512,13 +512,13 @@ public:
     info.arithOnlyLinear();
     info.disableIntegers();
     info.lock();
-    TS_ASSERT_EQUALS( info.getLogicString(), "AUFBVDTLRA" );
+    TS_ASSERT_EQUALS( info.getLogicString(), "AUFBVFPDTLRA" );
 
     info = info.getUnlockedCopy();
     TS_ASSERT( !info.isLocked() );
     info.disableQuantifiers();
     info.lock();
-    TS_ASSERT_EQUALS( info.getLogicString(), "QF_AUFBVDTLRA" );
+    TS_ASSERT_EQUALS( info.getLogicString(), "QF_AUFBVFPDTLRA" );
 
     info = info.getUnlockedCopy();
     TS_ASSERT( !info.isLocked() );
@@ -527,12 +527,13 @@ public:
     info.enableIntegers();
     info.disableReals();
     info.lock();
-    TS_ASSERT_EQUALS( info.getLogicString(), "QF_AUFLIA" );
+    TS_ASSERT_EQUALS( info.getLogicString(), "QF_AUFFPLIA" );
 
     info = info.getUnlockedCopy();
     TS_ASSERT( !info.isLocked() );
     info.disableTheory(THEORY_ARITH);
     info.disableTheory(THEORY_UF);
+    info.disableTheory(THEORY_FP);
     info.lock();
     TS_ASSERT_EQUALS( info.getLogicString(), "QF_AX" );
     TS_ASSERT( info.isPure( THEORY_ARRAY ) );