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

diff --git a/src/theory/fp/fp_expand_defs.cpp b/src/theory/fp/fp_expand_defs.cpp
index 1fc893a3064f63ca61d7770fea66e7f1a09b83a1..dac0d51362a5bdd7bbee7ad83ac2d34f32ef1905 100644 (file)
--- 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 74e1ff52616583a488e3f86bc1053119ac778a8c..628c00c300756a28f0c32eea48ca78a91b8e4aab 100644 (file)
--- 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 685ac8b4ee431afd6113c2d0c7adbb934f5f6cac..3f1ff1307b8787c4e6601e4670f2dd0c1d7f3749 100644 (file)
--- 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 c06cdb1105d2212c09269777ad0c832063b05a56..2de76b68078847ec0eb5e334664c56e9c3a6314c 100644 (file)
--- 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 911db54eeb2db48ae738e4a3765415a866c06833..d4393486c23705b1f75c5e30dc9bf2e220246beb 100644 (file)
--- 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 (file)
index 0000000..2ad9ac9
--- /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 3ec9f159475b03378b6ab4afdceb605a64abff78..056a98afc6822331a2f1709f4769da92e04e8204 100644 (file)
--- 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)