diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-12-19 11:58:52 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-12-19 11:58:52 -0600 |
| commit | 6b46621c4076ace3b0703e29fbdadca04f7635cb (patch) | |
| tree | b9d46b8d2453fac49e119fa22811ad610195cca6 /src/theory/fp | |
| parent | f6f26013ce73db50502dc5452c08e304ab2e3ac3 (diff) | |
Fix issues with REWRITE_DONE in floating point rewriter (#2762)
Diffstat (limited to 'src/theory/fp')
| -rw-r--r-- | src/theory/fp/theory_fp_rewriter.cpp | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index f77291a05..21644161e 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -175,8 +175,9 @@ namespace rewrite { if (node[0] == node[1]) { return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); } else if (!isPreRewrite && (node[0] > node[1])) { - Node normal = NodeManager::currentNM()->mkNode(kind::EQUAL,node[1],node[0]); - return RewriteResponse(REWRITE_DONE, normal); + Node normal = + NodeManager::currentNM()->mkNode(kind::EQUAL, node[1], node[0]); + return RewriteResponse(REWRITE_DONE, normal); } else { return RewriteResponse(REWRITE_DONE, node); } @@ -191,7 +192,7 @@ namespace rewrite { (k == kind::FLOATINGPOINT_MIN_TOTAL) || (k == kind::FLOATINGPOINT_MAX_TOTAL)); #endif if (node[0] == node[1]) { - return RewriteResponse(REWRITE_DONE, node[0]); + return RewriteResponse(REWRITE_AGAIN, node[0]); } else { return RewriteResponse(REWRITE_DONE, node); } @@ -249,7 +250,7 @@ namespace rewrite { (childKind == kind::FLOATINGPOINT_ABS)) { Node rewritten = NodeManager::currentNM()->mkNode(node.getKind(),node[0][0]); - return RewriteResponse(REWRITE_AGAIN, rewritten); + return RewriteResponse(REWRITE_AGAIN_FULL, rewritten); } else { return RewriteResponse(REWRITE_DONE, node); } @@ -276,8 +277,11 @@ namespace rewrite { // Lift negation out of the LHS so it can be cancelled out if (working[0].getKind() == kind::FLOATINGPOINT_NEG) { NodeManager * nm = NodeManager::currentNM(); - working = nm->mkNode(kind::FLOATINGPOINT_NEG, - nm->mkNode(kind::FLOATINGPOINT_REM, working[0][0], working[1])); + working = nm->mkNode( + kind::FLOATINGPOINT_NEG, + nm->mkNode(kind::FLOATINGPOINT_REM, working[0][0], working[1])); + // in contrast to other rewrites here, this requires rewrite again full + return RewriteResponse(REWRITE_AGAIN_FULL, working); } return RewriteResponse(REWRITE_DONE, working); |