Floating point infrastructure.

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

8 files changed, 1356 insertions, 0 deletions

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 */