diff options
author | Martin <martin.brain@cs.ox.ac.uk> | 2018-11-21 21:59:51 +0000 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-11-21 13:59:51 -0800 |
commit | 3072a39f6bda5a5ce0dd538e0f1a1bd1b744d122 (patch) | |
tree | 8d29ca399ae4947864c75179fb7238c789e364b1 /src/theory/fp | |
parent | 2c05402119dba7e90e24621c5768514ab2f5042c (diff) |
Obvious rewrites to floating-point < and <=. (#2706)
Diffstat (limited to 'src/theory/fp')
-rw-r--r-- | src/theory/fp/theory_fp_rewriter.cpp | 37 |
1 files changed, 33 insertions, 4 deletions
diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index 372db40b1..f77291a05 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -283,6 +283,33 @@ namespace rewrite { return RewriteResponse(REWRITE_DONE, working); } + RewriteResponse leqId(TNode node, bool isPreRewrite) + { + Assert(node.getKind() == kind::FLOATINGPOINT_LEQ); + + if (node[0] == node[1]) + { + NodeManager *nm = NodeManager::currentNM(); + return RewriteResponse( + isPreRewrite ? REWRITE_DONE : REWRITE_AGAIN_FULL, + nm->mkNode(kind::NOT, + nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[0]))); + } + return RewriteResponse(REWRITE_DONE, node); + } + + RewriteResponse ltId(TNode node, bool isPreRewrite) + { + Assert(node.getKind() == kind::FLOATINGPOINT_LT); + + if (node[0] == node[1]) + { + return RewriteResponse(REWRITE_DONE, + NodeManager::currentNM()->mkConst(false)); + } + return RewriteResponse(REWRITE_DONE, node); + } + }; /* CVC4::theory::fp::rewrite */ @@ -985,8 +1012,10 @@ RewriteFunction TheoryFpRewriter::constantFoldTable[kind::LAST_KIND]; /******** Comparisons ********/ preRewriteTable[kind::FLOATINGPOINT_EQ] = rewrite::then<rewrite::breakChain,rewrite::ieeeEqToEq>; - preRewriteTable[kind::FLOATINGPOINT_LEQ] = rewrite::breakChain; - preRewriteTable[kind::FLOATINGPOINT_LT] = rewrite::breakChain; + preRewriteTable[kind::FLOATINGPOINT_LEQ] = + rewrite::then<rewrite::breakChain, rewrite::leqId>; + preRewriteTable[kind::FLOATINGPOINT_LT] = + rewrite::then<rewrite::breakChain, rewrite::ltId>; preRewriteTable[kind::FLOATINGPOINT_GEQ] = rewrite::then<rewrite::breakChain,rewrite::geqToleq>; preRewriteTable[kind::FLOATINGPOINT_GT] = rewrite::then<rewrite::breakChain,rewrite::gtTolt>; @@ -1068,8 +1097,8 @@ RewriteFunction TheoryFpRewriter::constantFoldTable[kind::LAST_KIND]; /******** Comparisons ********/ postRewriteTable[kind::FLOATINGPOINT_EQ] = rewrite::removed; - postRewriteTable[kind::FLOATINGPOINT_LEQ] = rewrite::identity; - postRewriteTable[kind::FLOATINGPOINT_LT] = rewrite::identity; + postRewriteTable[kind::FLOATINGPOINT_LEQ] = rewrite::leqId; + postRewriteTable[kind::FLOATINGPOINT_LT] = rewrite::ltId; postRewriteTable[kind::FLOATINGPOINT_GEQ] = rewrite::removed; postRewriteTable[kind::FLOATINGPOINT_GT] = rewrite::removed; |