FP: Move removal of generic to_fp operations to rewriter. (#6480)

2 files changed, 43 insertions, 48 deletions

diff --git a/src/theory/fp/fp_expand_defs.cpp b/src/theory/fp/fp_expand_defs.cpp
index 1fc893a30..dac0d5136 100644
--- a/src/theory/fp/fp_expand_defs.cpp
+++ b/src/theory/fp/fp_expand_defs.cpp
@@ -21,48 +21,6 @@ namespace cvc5 {
 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;
-  NodeManager* nm = NodeManager::currentNM();
-
-  if (children == 1)
-  {
-    op = nm->mkConst(FloatingPointToFPIEEEBitVector(info));
-    return nm->mkNode(op, node[0]);
-  }
-  Assert(children == 2);
-  Assert(node[0].getType().isRoundingMode());
-
-  TypeNode t = node[1].getType();
-
-  if (t.isFloatingPoint())
-  {
-    op = nm->mkConst(FloatingPointToFPFloatingPoint(info));
-  }
-  else if (t.isReal())
-  {
-    op = nm->mkConst(FloatingPointToFPReal(info));
-  }
-  else
-  {
-    Assert(t.isBitVector());
-    op = nm->mkConst(FloatingPointToFPSignedBitVector(info));
-  }
-
-  return nm->mkNode(op, node[0], node[1]);
-}
-}  // namespace removeToFPGeneric
-
 FpExpandDefs::FpExpandDefs(context::UserContext* u)
     :
 
@@ -251,11 +209,7 @@ TrustNode FpExpandDefs::expandDefinition(Node node)
   Node res = node;
   Kind kind = node.getKind();
 
-  if (kind == kind::FLOATINGPOINT_TO_FP_GENERIC)
-  {
-    res = removeToFPGeneric::removeToFPGeneric(node);
-  }
-  else if (kind == kind::FLOATINGPOINT_MIN)
+  if (kind == kind::FLOATINGPOINT_MIN)
   {
     res = NodeManager::currentNM()->mkNode(
         kind::FLOATINGPOINT_MIN_TOTAL, node[0], node[1], minUF(node));
diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index 74e1ff526..628c00c30 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -77,6 +77,46 @@ namespace rewrite {
                   << ") found in expression?";
   }
 
+  RewriteResponse removeToFPGeneric(TNode node, bool isPreRewrite)
+  {
+    Assert(!isPreRewrite);
+    Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC);
+
+    FloatingPointToFPGeneric info =
+        node.getOperator().getConst<FloatingPointToFPGeneric>();
+
+    uint32_t children = node.getNumChildren();
+
+    Node op;
+    NodeManager* nm = NodeManager::currentNM();
+
+    if (children == 1)
+    {
+      op = nm->mkConst(FloatingPointToFPIEEEBitVector(info));
+      return RewriteResponse(REWRITE_AGAIN, nm->mkNode(op, node[0]));
+    }
+    Assert(children == 2);
+    Assert(node[0].getType().isRoundingMode());
+
+    TypeNode t = node[1].getType();
+
+    if (t.isFloatingPoint())
+    {
+      op = nm->mkConst(FloatingPointToFPFloatingPoint(info));
+    }
+    else if (t.isReal())
+    {
+      op = nm->mkConst(FloatingPointToFPReal(info));
+    }
+    else
+    {
+      Assert(t.isBitVector());
+      op = nm->mkConst(FloatingPointToFPSignedBitVector(info));
+    }
+
+    return RewriteResponse(REWRITE_AGAIN, nm->mkNode(op, node[0], node[1]));
+  }
+
   RewriteResponse removeDoubleNegation(TNode node, bool isPreRewrite)
   {
     Assert(node.getKind() == kind::FLOATINGPOINT_NEG);
@@ -1233,7 +1273,8 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u)
       rewrite::toFPSignedBV;
   d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR] =
       rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_GENERIC] = rewrite::identity;
+  d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_GENERIC] =
+      rewrite::removeToFPGeneric;
   d_postRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity;
   d_postRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity;
   d_postRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity;