From 9d3898044d5e140ae6e6b4eb36ca1c2cd19ba2f8 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 18 Feb 2020 07:50:45 -0800
Subject: [PATCH] =?UTF-8?q?[sledge]=20Canonize=20e=20/=20-1=20to=20-1?=
 =?UTF-8?q?=C3=97e?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Summary: Strengthen arithmetic canonizer, and add previously failing test.

Reviewed By: jvillard

Differential Revision: D19950366

fbshipit-source-id: 0d6eb0428
---
 sledge/src/llair/term.ml             | 2 ++
 sledge/src/symbheap/equality_test.ml | 9 +++++++++
 2 files changed, 11 insertions(+)

diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml
index 657ab839a..c3baf8b4f 100644
--- a/sledge/src/llair/term.ml
+++ b/sledge/src/llair/term.ml
@@ -572,6 +572,8 @@ and simp_div x y =
       integer (Z.div i j)
   (* e / 1 ==> e *)
   | e, Integer {data} when Z.equal Z.one data -> e
+  (* e / -1 ==> -1×e *)
+  | e, (Integer {data} as c) when Z.equal Z.minus_one data -> simp_mul2 e c
   (* (∑ᵢ cᵢ × Xᵢ) / z ==> ∑ᵢ cᵢ/z × Xᵢ *)
   | Add args, Integer {data} ->
       sum_to_term (Sum.mul_const Q.(inv (of_z data)) args)
diff --git a/sledge/src/symbheap/equality_test.ml b/sledge/src/symbheap/equality_test.ml
index 046a1357a..93e52ce38 100644
--- a/sledge/src/symbheap/equality_test.ml
+++ b/sledge/src/symbheap/equality_test.ml
@@ -403,4 +403,13 @@ let%test_module _ =
           (((u8) %y_6) + 1) = %y_6
         ∧ %x_5 = ((u8) %x_5)
         ∧ ((u8) %y_6) = ((u8) (((u8) %y_6) + 1)) |}]
+
+    let r19 = of_eqs [(x, y + z); (x, !0); (y, !0)]
+
+    let%expect_test _ =
+      pp r19 ;
+      [%expect
+        {| {sat= true; rep= [[%x_5 ↦ 0]; [%y_6 ↦ 0]; [%z_7 ↦ 0]]} |}]
+
+    let%test _ = entails_eq r19 z !0
   end )