From: Martin Date: Fri, 15 Sep 2017 03:04:20 +0000 (+0100) Subject: Make floating-point comparison operators chainable (#1101) X-Git-Tag: cvc5-1.0.0~5634 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=190e5aa70862f40ba96b7dc7add3f11a8143c66f;p=cvc5.git Make floating-point comparison operators chainable (#1101) Floating-point comparison operators are chainable according to the standard. --- 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 + 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; + preRewriteTable[kind::FLOATINGPOINT_LEQ] = rewrite::breakChain; + preRewriteTable[kind::FLOATINGPOINT_LT] = rewrite::breakChain; + preRewriteTable[kind::FLOATINGPOINT_GEQ] = rewrite::then; + preRewriteTable[kind::FLOATINGPOINT_GT] = rewrite::then; /******** Classifications ********/ preRewriteTable[kind::FLOATINGPOINT_ISN] = rewrite::identity;