From: Martin <martin.brain@cs.ox.ac.uk>
Date: Wed, 21 Nov 2018 21:59:51 +0000 (+0000)
Subject: Obvious rewrites to floating-point < and <=. (#2706)
X-Git-Tag: cvc5-1.0.0~4359
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3072a39f6bda5a5ce0dd538e0f1a1bd1b744d122;p=cvc5.git

Obvious rewrites to floating-point < and <=. (#2706)
---

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;