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

7 files changed, 54 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;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 685ac8b4e..3f1ff1307 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -581,6 +581,7 @@ set(regress_0_tests
   regress0/fp/issue3619.smt2
   regress0/fp/issue4277-assign-func.smt2
   regress0/fp/issue5511.smt2
+  regress0/fp/issue5734.smt2
   regress0/fp/issue6164.smt2
   regress0/fp/rti_3_5_bug.smt2
   regress0/fp/simple.smt2
diff --git a/test/regress/regress0/fp/issue3582.smt2 b/test/regress/regress0/fp/issue3582.smt2
index c06cdb110..2de76b680 100644
--- a/test/regress/regress0/fp/issue3582.smt2
+++ b/test/regress/regress0/fp/issue3582.smt2
@@ -1,3 +1,4 @@
+; REQUIRES: symfpu
 ; EXPECT: unsat
 (set-logic QF_FP)
 (declare-fun bv () (_ BitVec 1))
diff --git a/test/regress/regress0/fp/issue5511.smt2 b/test/regress/regress0/fp/issue5511.smt2
index 911db54ee..d4393486c 100644
--- a/test/regress/regress0/fp/issue5511.smt2
+++ b/test/regress/regress0/fp/issue5511.smt2
@@ -1,3 +1,4 @@
+; REQUIRES: symfpu
 ; EXPECT: sat
 (set-logic QF_FP)
 (declare-fun a () (_ FloatingPoint 53 11))
diff --git a/test/regress/regress0/fp/issue5734.smt2 b/test/regress/regress0/fp/issue5734.smt2
new file mode 100644
index 000000000..2ad9ac921
--- /dev/null
+++ b/test/regress/regress0/fp/issue5734.smt2
@@ -0,0 +1,7 @@
+; REQUIRES: symfpu
+; EXPECT: sat
+(set-logic QF_FP)
+(declare-fun a () RoundingMode)
+(declare-fun b () (_ FloatingPoint 8 24))
+(assert (= b (fp.add a b (fp.add a ((_ to_fp 8 24) a ((_ to_fp 8 24) a 0)) b))))
+(check-sat)
diff --git a/test/regress/regress0/fp/issue6164.smt2 b/test/regress/regress0/fp/issue6164.smt2
index 3ec9f1594..056a98afc 100644
--- a/test/regress/regress0/fp/issue6164.smt2
+++ b/test/regress/regress0/fp/issue6164.smt2
@@ -1,3 +1,4 @@
+; REQUIRES: symfpu
 ; EXPECT: sat
 ; EXPECT: ((((_ to_fp 5 11) roundNearestTiesToAway (/ 1 10)) (fp #b0 #b01011 #b1001100110)))
 (set-logic ALL)