[sledge] Fix term ordering bug between monomials and vars

Summary:
Fix the crash in
```
(And_eq () (Var (id 10) (name v))
 (Mul (((Var (id 8) (name v)) 1) ((Var (id 9) (name v)) 1)))
 ((xs ()) (sat true) (rep ())))
```

The solver for interpreted functions relies on the solution
substitutions containing mappings from variables to interpreted
applications, and never in the reverse. When solving equations
involving polynomials, this constraint is specifically
established. But for equalities involving only monomials, it could
happen that e.g. `x` was chosen as the representative of `a × b`,
which violates this constraint.

Reviewed By: jvillard

Differential Revision: D20596422

fbshipit-source-id: 69b026f03

sledge/lib/equality_test.ml

@@ -15,7 +15,7 @@ let%test_module _ =
      *   Trace.init ~margin:160
      *     ~config:(Result.ok_exn (Trace.parse "+Equality"))
      *     ()
-     * 
+     *
      * [@@@warning "-32"] *)
 
     let printf pp = Format.printf "@\n%a@." pp
@@ -365,10 +365,10 @@ let%test_module _ =
       [%expect
         {|
       {sat= false;
-       rep= [[%x_5 ↦ (((u8) %y_6) + 3)];
-             [%y_6 ↦ (((u8) %y_6) + 2)];
-             [((u8) (%x_5 + -1)) ↦ (((u8) %y_6) + 5)];
-             [((u8) %y_6) ↦ ]]} |}]
+       rep= [[%x_5 ↦ (((u8) (%x_5 + -1)) + -2)];
+             [%y_6 ↦ (((u8) (%x_5 + -1)) + -3)];
+             [((u8) %y_6) ↦ (((u8) (%x_5 + -1)) + -5)];
+             [((u8) (%x_5 + -1)) ↦ ]]} |}]
 
     let%test _ = is_false r16
 
@@ -398,9 +398,9 @@ let%test_module _ =
                [((u8) %x_5) ↦ %x_5];
                [((u8) %y_6) ↦ ]]}
 
-          (((u8) %y_6) + 1) = %y_6
-        ∧ %x_5 = ((u8) %x_5)
-        ∧ ((u8) %y_6) = ((u8) (((u8) %y_6) + 1)) |}]
+          %x_5 = ((u8) %x_5)
+        ∧ ((u8) %y_6) = ((u8) (((u8) %y_6) + 1))
+        ∧ (((u8) %y_6) + 1) = %y_6 |}]
 
     let r19 = of_eqs [(x, y + z); (x, !0); (y, !0)]
 
@@ -413,7 +413,8 @@ let%test_module _ =
 
     let%expect_test _ =
       Equality.replay
-        {|(Solve_for_vars (() () ((Var (id 8) (name m)) (Var (id 9) (name n))))
-           ((xs ()) (sat true) (rep (((Var (id 9) (name n)) (Var (id 8) (name m)))))))|} ;
-      [%expect {||}]
+        {|(And_eq () (Var (id 10) (name v))
+           (Mul (((Var (id 8) (name v)) 1) ((Var (id 9) (name v)) 1)))
+           ((xs ()) (sat true) (rep ())))|} ;
+      [%expect {| |}]
   end )

sledge/lib/sh_test.ml

@@ -137,18 +137,18 @@ let%test_module _ =
       [%expect
         {|
         ∃ %x_6 .
-          (((u8) %y_7) + 1) = %y_7
-        ∧ %x_6 = ((u8) %x_6)
+          %x_6 = ((u8) %x_6)
         ∧ ((u8) %y_7) = ((u8) (((u8) %y_7) + 1))
+        ∧ (((u8) %y_7) + 1) = %y_7
         ∧ emp
 
-          (((u8) %y_7) + 1) = %y_7
-        ∧ ((u8) %y_7) = ((u8) (((u8) %y_7) + 1))
-        ∧ ((%y_7 + -1) = ((u8) %y_7))
+          ((u8) %y_7) = ((u8) (((u8) %y_7) + 1))
+        ∧ (((u8) %y_7) + 1) = %y_7
+        ∧ (((u8) %y_7) = (%y_7 + -1))
         ∧ emp
 
-          (((u8) %y_7) + 1) = %y_7
-        ∧ ((u8) %y_7) = ((u8) (((u8) %y_7) + 1))
+          ((u8) %y_7) = ((u8) (((u8) %y_7) + 1))
+        ∧ (((u8) %y_7) + 1) = %y_7
         ∧ emp |}]
 
     let%expect_test _ =

sledge/lib/solver_test.ml

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

sledge/lib/term.ml

@@ -58,14 +58,14 @@ and T : sig
   type qset = Qset.t [@@deriving compare, equal, hash, sexp]
 
   type t =
-    | Add of qset
-    | Mul of qset
     | Var of {id: int; name: string}
     | Ap1 of op1 * t
     | Ap2 of op2 * t * t
     | Ap3 of op3 * t * t * t
     | ApN of opN * t iarray
     | RecN of recN * t iarray  (** NOTE: cyclic *)
+    | Add of qset
+    | Mul of qset
     | Label of {parent: string; name: string}
     | Nondet of {msg: string}
     | Float of {data: string}
@@ -75,14 +75,14 @@ end = struct
   type qset = Qset.t [@@deriving compare, equal, hash, sexp]
 
   type t =
-    | Add of qset
-    | Mul of qset
     | Var of {id: int; name: string}
     | Ap1 of op1 * t
     | Ap2 of op2 * t * t
     | Ap3 of op3 * t * t * t
     | ApN of opN * t iarray
     | RecN of recN * t iarray  (** NOTE: cyclic *)
+    | Add of qset
+    | Mul of qset
     | Label of {parent: string; name: string}
     | Nondet of {msg: string}
     | Float of {data: string}

sledge/lib/term.mli

@@ -73,8 +73,6 @@ and T : sig
   type qset = Qset.t [@@deriving compare, equal, hash, sexp]
 
   and t = private
-    | Add of qset  (** Sum of terms with rational coefficients *)
-    | Mul of qset  (** Product of terms with rational exponents *)
     | Var of {id: int; name: string}
         (** Local variable / virtual register *)
     | Ap1 of op1 * t  (** Unary application *)
@@ -85,6 +83,8 @@ and T : sig
         (** Recursive n-ary application, may recursively refer to itself
             (transitively) from its args. NOTE: represented by cyclic
             values. *)
+    | Add of qset  (** Sum of terms with rational coefficients *)
+    | Mul of qset  (** Product of terms with rational exponents *)
     | Label of {parent: string; name: string}
         (** Address of named code block within parent function *)
     | Nondet of {msg: string}

sledge/lib/term_test.ml

@@ -75,7 +75,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp ((!2 * z * z) + (!3 * z) + !4) ;
-      [%expect {| (2 × (%z_2^2) + 3 × %z_2 + 4) |}]
+      [%expect {| (3 × %z_2 + 2 × (%z_2^2) + 4) |}]
 
     let%expect_test _ =
       pp
@@ -88,9 +88,9 @@ let%test_module _ =
         + (!9 * z * z * z) ) ;
       [%expect
         {|
-         (6 × (%y_1 × %z_2) + 8 × (%y_1 × %z_2^2) + 5 × (%y_1^2)
-           + 7 × (%y_1^2 × %z_2) + 4 × (%z_2^2) + 9 × (%z_2^3) + 3 × %y_1
-           + 2 × %z_2 + 1) |}]
+         (3 × %y_1 + 2 × %z_2 + 6 × (%y_1 × %z_2) + 8 × (%y_1 × %z_2^2)
+           + 5 × (%y_1^2) + 7 × (%y_1^2 × %z_2) + 4 × (%z_2^2) + 9 × (%z_2^3)
+           + 1) |}]
 
     let%expect_test _ =
       pp (!0 * z * y) ;
@@ -142,7 +142,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp (((!3 * y) + !2) * (!4 + (!5 * z))) ;
-      [%expect {| (15 × (%y_1 × %z_2) + 12 × %y_1 + 10 × %z_2 + 8) |}]
+      [%expect {| (12 × %y_1 + 10 × %z_2 + 15 × (%y_1 × %z_2) + 8) |}]
 
     let%expect_test _ =
       pp (((!2 * z) - !3 + ((!(-2) * z) + !3)) * (!4 + (!5 * z))) ;
@@ -170,19 +170,19 @@ let%test_module _ =
 
     let%expect_test _ =
       pp (!3 * y = z = true_) ;
-      [%expect {| ((3 × %y_1) = %z_2) |}]
+      [%expect {| (%z_2 = (3 × %y_1)) |}]
 
     let%expect_test _ =
       pp (true_ = (!3 * y = z)) ;
-      [%expect {| ((3 × %y_1) = %z_2) |}]
+      [%expect {| (%z_2 = (3 × %y_1)) |}]
 
     let%expect_test _ =
       pp (!3 * y = z = false_) ;
-      [%expect {| ((3 × %y_1) ≠ %z_2) |}]
+      [%expect {| (%z_2 ≠ (3 × %y_1)) |}]
 
     let%expect_test _ =
       pp (false_ = (!3 * y = z)) ;
-      [%expect {| ((3 × %y_1) ≠ %z_2) |}]
+      [%expect {| (%z_2 ≠ (3 × %y_1)) |}]
 
     let%expect_test _ =
       pp (y - (!(-3) * y) + !4) ;
@@ -194,11 +194,11 @@ let%test_module _ =
 
     let%expect_test _ =
       pp (y = (!(-3) * y) + !4) ;
-      [%expect {| ((-3 × %y_1 + 4) = %y_1) |}]
+      [%expect {| (%y_1 = (-3 × %y_1 + 4)) |}]
 
     let%expect_test _ =
       pp ((!(-3) * y) + !4 = y) ;
-      [%expect {| ((-3 × %y_1 + 4) = %y_1) |}]
+      [%expect {| (%y_1 = (-3 × %y_1 + 4)) |}]
 
     let%expect_test _ =
       pp (sub true_ (z = !4)) ;
@@ -206,7 +206,7 @@ let%test_module _ =
 
     let%expect_test _ =
       pp (add true_ (z = !4) = (z = !4)) ;
-      [%expect {| (((%z_2 = 4) + -1) = (%z_2 = 4)) |}]
+      [%expect {| ((%z_2 = 4) = ((%z_2 = 4) + -1)) |}]
 
     let%expect_test _ =
       pp ((!13 * z) + !42 = (!3 * y) + (!13 * z)) ;
@@ -255,7 +255,7 @@ let%test_module _ =
       pp (z1_2 * z1_2) ;
       [%expect
         {|
-        ((%z_2^2) + 2 × %z_2 + 1)
+        (2 × %z_2 + (%z_2^2) + 1)
 
-        (6 × (%z_2^2) + 4 × (%z_2^3) + (%z_2^4) + 4 × %z_2 + 1) |}]
+        (4 × %z_2 + 6 × (%z_2^2) + 4 × (%z_2^3) + (%z_2^4) + 1) |}]
   end )