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 372db40b188b467beb2ba65b3d4a00e3b581f15b..f77291a059f54fb0d895eb27968a9a54ef5af01a 100644 (file)
--- 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;