From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 15 Jan 2019 16:54:02 +0000 (-0600)
Subject:  Fix unsound double abs rewrite rule for FP (#2792)
X-Git-Tag: cvc5-1.0.0~4287
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=da504025a3a77e9a3201af33ee6f96f937802807;p=cvc5.git

 Fix unsound double abs rewrite rule for FP (#2792)
---

diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index 21644161e..875471ded 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -76,9 +76,12 @@ namespace rewrite {
 
   RewriteResponse compactAbs (TNode node, bool) {
     Assert(node.getKind() == kind::FLOATINGPOINT_ABS);
-    if (node[0].getKind() == kind::FLOATINGPOINT_NEG ||
-	node[0].getKind() == kind::FLOATINGPOINT_ABS) {
-      return RewriteResponse(REWRITE_AGAIN, node[0][0]);
+    if (node[0].getKind() == kind::FLOATINGPOINT_NEG
+        || node[0].getKind() == kind::FLOATINGPOINT_ABS)
+    {
+      Node ret =
+          NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_ABS, node[0][0]);
+      return RewriteResponse(REWRITE_AGAIN, ret);
     }
 
     return RewriteResponse(REWRITE_DONE, node);
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e6e28336e..dbefe3af2 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -444,6 +444,8 @@ set(regress_0_tests
   regress0/fmf/sort-infer-typed-082718.smt2
   regress0/fmf/syn002-si-real-int.smt2
   regress0/fmf/tail_rec.smt2
+  regress0/fp/abs-unsound.smt2
+  regress0/fp/abs-unsound2.smt2
   regress0/fp/ext-rew-test.smt2
   regress0/fp/simple.smt2
   regress0/fuzz_1.smt
diff --git a/test/regress/regress0/fp/abs-unsound.smt2 b/test/regress/regress0/fp/abs-unsound.smt2
new file mode 100644
index 000000000..4ac53b830
--- /dev/null
+++ b/test/regress/regress0/fp/abs-unsound.smt2
@@ -0,0 +1,11 @@
+; REQUIRES: symfpu
+; EXPECT: sat
+(set-logic QF_FP)
+(set-info :status sat)
+(declare-fun x () (_ FloatingPoint 3 5))
+(declare-fun y () (_ FloatingPoint 3 5))
+
+(assert (not (= (fp.abs (fp.abs x)) x)))
+(assert (not (= (fp.abs (fp.neg y)) y)))
+
+(check-sat)
diff --git a/test/regress/regress0/fp/abs-unsound2.smt2 b/test/regress/regress0/fp/abs-unsound2.smt2
new file mode 100644
index 000000000..a6172b157
--- /dev/null
+++ b/test/regress/regress0/fp/abs-unsound2.smt2
@@ -0,0 +1,9 @@
+; REQUIRES: symfpu
+; EXPECT: unsat
+(set-logic QF_FP)
+(set-info :status unsat)
+(declare-fun x () (_ FloatingPoint 3 5))
+
+(assert (fp.isNegative (fp.abs (fp.neg x))))
+
+(check-sat)