diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-01-15 10:54:02 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-01-15 10:54:02 -0600 |
| commit | da504025a3a77e9a3201af33ee6f96f937802807 (patch) | |
| tree | cd23822d9806e5f0cc29fe871b0c1cf24a89921d | |
| parent | 448ee080458373fbd3aabe97396101d98d68f0c0 (diff) | |
Fix unsound double abs rewrite rule for FP (#2792)
| -rw-r--r-- | src/theory/fp/theory_fp_rewriter.cpp | 9 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | test/regress/regress0/fp/abs-unsound.smt2 | 11 | ||||
| -rw-r--r-- | test/regress/regress0/fp/abs-unsound2.smt2 | 9 |
4 files changed, 28 insertions, 3 deletions
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) |