diff options
author | Martin <martin.brain@diffblue.com> | 2017-09-15 04:04:20 +0100 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2017-09-14 20:04:20 -0700 |
commit | 190e5aa70862f40ba96b7dc7add3f11a8143c66f (patch) | |
tree | f039ee87fa11000355da09e9fd156452e8eecdb9 /src/theory/fp | |
parent | e27d7b41dba65c1611bfb536ffe958fa7cad3848 (diff) |
Make floating-point comparison operators chainable (#1101)
Floating-point comparison operators are chainable according to the standard.
Diffstat (limited to 'src/theory/fp')
-rw-r--r-- | src/theory/fp/kinds | 8 | ||||
-rw-r--r-- | src/theory/fp/theory_fp_rewriter.cpp | 48 |
2 files changed, 47 insertions, 9 deletions
diff --git a/src/theory/fp/kinds b/src/theory/fp/kinds index 983d5aa5c..a1b28d885 100644 --- a/src/theory/fp/kinds +++ b/src/theory/fp/kinds @@ -94,16 +94,16 @@ operator FLOATINGPOINT_MAX 2 "floating-point maximum" typerule FLOATINGPOINT_MAX ::CVC4::theory::fp::FloatingPointOperationTypeRule -operator FLOATINGPOINT_LEQ 2 "floating-point less than or equal" +operator FLOATINGPOINT_LEQ 2: "floating-point less than or equal" typerule FLOATINGPOINT_LEQ ::CVC4::theory::fp::FloatingPointTestTypeRule -operator FLOATINGPOINT_LT 2 "floating-point less than" +operator FLOATINGPOINT_LT 2: "floating-point less than" typerule FLOATINGPOINT_LT ::CVC4::theory::fp::FloatingPointTestTypeRule -operator FLOATINGPOINT_GEQ 2 "floating-point greater than or equal" +operator FLOATINGPOINT_GEQ 2: "floating-point greater than or equal" typerule FLOATINGPOINT_GEQ ::CVC4::theory::fp::FloatingPointTestTypeRule -operator FLOATINGPOINT_GT 2 "floating-point greater than" +operator FLOATINGPOINT_GT 2: "floating-point greater than" typerule FLOATINGPOINT_GT ::CVC4::theory::fp::FloatingPointTestTypeRule diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index ba4bf9228..747aaeac6 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -37,6 +37,16 @@ namespace fp { namespace rewrite { /** Rewrite rules **/ + template <RewriteFunction first, RewriteFunction second> + RewriteResponse then (TNode node, bool isPreRewrite) { + RewriteResponse result(first(node, isPreRewrite)); + + if (result.status == REWRITE_DONE) { + return second(result.node, isPreRewrite); + } else { + return result; + } + } RewriteResponse notFP (TNode node, bool) { Unreachable("non floating-point kind (%d) in floating point rewrite?",node.getKind()); @@ -67,6 +77,34 @@ namespace rewrite { return RewriteResponse(REWRITE_DONE, addition); } + RewriteResponse breakChain (TNode node, bool isPreRewrite) { + Assert(isPreRewrite); // Should be run first + + Kind k = node.getKind(); + Assert(k == kind::FLOATINGPOINT_EQ || + k == kind::FLOATINGPOINT_GEQ || + k == kind::FLOATINGPOINT_LEQ || + k == kind::FLOATINGPOINT_GT || + k == kind::FLOATINGPOINT_LT); + + + size_t children = node.getNumChildren(); + if (children > 2) { + + NodeBuilder<> conjunction(kind::AND); + + for (size_t i = 0; i < children - 1; ++i) { + for (size_t j = i + 1; j < children; ++j) { + conjunction << NodeManager::currentNM()->mkNode(k, node[i], node[j]); + } + } + return RewriteResponse(REWRITE_AGAIN_FULL, conjunction); + + } else { + return RewriteResponse(REWRITE_DONE, node); + } + } + /* Implies (fp.eq x x) --> (not (isNaN x)) */ @@ -314,11 +352,11 @@ RewriteFunction TheoryFpRewriter::postRewriteTable[kind::LAST_KIND]; preRewriteTable[kind::FLOATINGPOINT_MAX] = rewrite::compactMinMax; /******** Comparisons ********/ - preRewriteTable[kind::FLOATINGPOINT_EQ] = rewrite::ieeeEqToEq; - preRewriteTable[kind::FLOATINGPOINT_LEQ] = rewrite::identity; - preRewriteTable[kind::FLOATINGPOINT_LT] = rewrite::identity; - preRewriteTable[kind::FLOATINGPOINT_GEQ] = rewrite::geqToleq; - preRewriteTable[kind::FLOATINGPOINT_GT] = rewrite::gtTolt; + 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_GEQ] = rewrite::then<rewrite::breakChain,rewrite::geqToleq>; + preRewriteTable[kind::FLOATINGPOINT_GT] = rewrite::then<rewrite::breakChain,rewrite::gtTolt>; /******** Classifications ********/ preRewriteTable[kind::FLOATINGPOINT_ISN] = rewrite::identity; |