[sledge] Canonize e / -1 to -1×e

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

Reviewed By: jvillard

Differential Revision: D19950366

fbshipit-source-id: 0d6eb0428

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)

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 )