[sledge] Strengthen normalization of arithmetic equalities

Reviewed By: jvillard

Differential Revision: D24371083

fbshipit-source-id: b928f534d

sledge/src/fol.ml

@@ -103,6 +103,7 @@ and Trm : sig
   val _Record : trm array -> trm
   val _Ancestor : int -> trm
   val _Apply : Funsym.t -> trm array -> trm
+  val sub : trm -> trm -> trm
 end = struct
   type var = Var.t
 
@@ -223,6 +224,7 @@ end = struct
     | Compound -> Arith a )
     |> check invariant
 
+  let sub x y = _Arith Arith.(sub (trm x) (trm y))
   let _Splat x = Splat x |> check invariant
   let _Sized seq siz = Sized {seq; siz} |> check invariant
   let _Extract seq off len = Extract {seq; off; len} |> check invariant
@@ -274,8 +276,9 @@ module Fml = struct
     else if y == zero then _Eq0 x
     else
       match (x, y) with
-      | Z y, Z z -> bool (Z.equal y z)
-      | Q q, Q r -> bool (Q.equal q r)
+      (* x = y ==> 0 = x - y when x = y is an arithmetic equality *)
+      | (Z _ | Q _ | Arith _), _ | _, (Z _ | Q _ | Arith _) ->
+          _Eq0 (sub x y)
       | _ -> (
         match Sign.of_int (compare_trm x y) with
         | Neg -> _Eq x y
@@ -660,7 +663,7 @@ module Term = struct
   let rational q = `Trm (_Q q)
   let neg = ap1t @@ fun x -> _Arith Arith.(neg (trm x))
   let add = ap2t @@ fun x y -> _Arith Arith.(add (trm x) (trm y))
-  let sub = ap2t @@ fun x y -> _Arith Arith.(sub (trm x) (trm y))
+  let sub = ap2t Trm.sub
   let mulq q = ap1t @@ fun x -> _Arith Arith.(mulc q (trm x))
   let mul = ap2t @@ fun x y -> _Arith (Arith.mul x y)
   let div = ap2t @@ fun x y -> _Arith (Arith.div x y)

sledge/src/test/fol_test.ml

@@ -76,7 +76,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp_raw f2 ;
-      [%expect {| {sat= false; rep= [[%x_5 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}]
+      [%expect {| {sat= false; rep= [[-1 ↦ ]; [0 ↦ ]]} |}]
 
     let f3 = of_eqs [(x + !0, x + !1)]
 
@@ -84,7 +84,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp_raw f3 ;
-      [%expect {| {sat= false; rep= [[%x_5 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}]
+      [%expect {| {sat= false; rep= [[-1 ↦ ]; [0 ↦ ]]} |}]
 
     let f4 = of_eqs [(x, y); (x + !0, y + !1)]
 
@@ -512,13 +512,13 @@ let%test_module _ =
         (Formula.orN (Iter.to_list (Iter.map ~f:snd3 (Context.dnf f)))) ;
       [%expect
         {|
-        ((%x_5 = %y_6) ∧ ((%w_4 = 4) ∨ (%w_4 = 5))
-          ∧ ((0 = %x_5) ? (%z_7 = 2) : (%z_7 = 3)))
+        ((%x_5 = %y_6) ∧ ((5 = %w_4) ∨ (4 = %w_4))
+          ∧ ((0 = %x_5) ? (2 = %z_7) : (3 = %z_7)))
 
-        (((%w_4 = 4) ∧ (%x_5 = %y_6) ∧ (%z_7 = 2) ∧ (0 = %x_5))
-          ∨ ((%w_4 = 4) ∧ (%x_5 = %y_6) ∧ (%z_7 = 3) ∧ (0 ≠ %x_5))
-          ∨ ((%w_4 = 5) ∧ (%x_5 = %y_6) ∧ (%z_7 = 2) ∧ (0 = %x_5))
-          ∨ ((%w_4 = 5) ∧ (%x_5 = %y_6) ∧ (%z_7 = 3) ∧ (0 ≠ %x_5))) |}]
+        (((%x_5 = %y_6) ∧ (0 = %x_5) ∧ (5 = %w_4) ∧ (2 = %z_7))
+          ∨ ((%x_5 = %y_6) ∧ (0 = %x_5) ∧ (4 = %w_4) ∧ (2 = %z_7))
+          ∨ ((%x_5 = %y_6) ∧ (5 = %w_4) ∧ (3 = %z_7) ∧ (0 ≠ %x_5))
+          ∨ ((%x_5 = %y_6) ∧ (4 = %w_4) ∧ (3 = %z_7) ∧ (0 ≠ %x_5))) |}]
 
     let%test "unsigned boolean overflow" =
       Formula.equal Formula.tt

sledge/src/test/sh_test.ml

@@ -94,8 +94,8 @@ let%test_module _ =
           ∨ (  ( (  1 = _ = %y_7 ∧ emp) ∨ (  2 = _ ∧ emp) ))
           )
     
-        ( (∃ %x_6, %x_7 .   (%x_7 = 2) ∧ emp)
-        ∨ (∃ %x_6 .   ((%x_6 = 1) ∧ (%y_7 = 1)) ∧ emp)
+        ( (∃ %x_6, %x_7 .   (2 = %x_7) ∧ emp)
+        ∨ (∃ %x_6 .   ((1 = %x_6) ∧ (1 = %y_7)) ∧ emp)
         ∨ (  (0 = %x_6) ∧ emp)
         ) |}]
 
@@ -119,8 +119,8 @@ let%test_module _ =
           ∨ (  ( (  1 = _ = %y_7 ∧ emp) ∨ (  2 = _ ∧ emp) ))
           )
     
-        ( (∃ %x_6, %x_8, %x_9 .   (%x_9 = 2) ∧ emp)
-        ∨ (∃ %x_6, %x_8 .   ((%y_7 = 1) ∧ (%x_8 = 1)) ∧ emp)
+        ( (∃ %x_6, %x_8, %x_9 .   (2 = %x_9) ∧ emp)
+        ∨ (∃ %x_6, %x_8 .   ((1 = %y_7) ∧ (1 = %x_8)) ∧ emp)
         ∨ (∃ %x_6 .   (0 = %x_6) ∧ emp)
         ) |}]
 
@@ -156,7 +156,7 @@ let%test_module _ =
         {|
         ∃ %x_6 .   %x_6 = %x_6^ ∧ (-1 + %y_7) = %y_7^ ∧ emp
 
-          (tt ∧ ((-1 + %y_7) = %y_7^)) ∧ emp
+          (tt ∧ (-1 = (-1×%y_7 + %y_7^))) ∧ emp
 
           (-1 + %y_7) = %y_7^ ∧ emp |}]
 

sledge/src/test/solver_test.ml

@@ -238,26 +238,26 @@ let%test_module _ =
         {|
         ( infer_frame:
             %l_6 -[ %l_6, 16 )-> ⟨8×%n_9,%a_2⟩^⟨(16 + -8×%n_9),%a_3⟩
-          * ( (  1 = %n_9 ∧ emp)
-            ∨ (  0 = %n_9 ∧ emp)
+          * ( (  0 = %n_9 ∧ emp)
+            ∨ (  1 = %n_9 ∧ emp)
             ∨ (  2 = %n_9 ∧ emp)
             )
           \- ∃ %a_1, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩
         ) infer_frame:
             ( (  %a_3 = _
-               ∧ 1 = %n_9
+               ∧ 0 = %n_9
                ∧ 16 = %m_8
-               ∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1
+               ∧ (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1
                ∧ emp)
             ∨ (  %a_1 = %a_2
                ∧ 2 = %n_9
                ∧ 16 = %m_8
                ∧ (16 + %l_6) -[ %l_6, 16 )-> ⟨0,%a_3⟩)
             ∨ (  %a_3 = _
-               ∧ 0 = %n_9
+               ∧ 1 = %n_9
                ∧ 16 = %m_8
-               ∧ (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1
+               ∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1
                ∧ emp)
             ) |}]