[sledge] Fix: Fol.of_ses to normalize Ses polynomials

Summary:
In Ses, the constant term of a polynomial is represented as a
redundant multiplication by 1. Fix Fol.of_ses to recognize and
normalize this.

Reviewed By: jvillard

Differential Revision: D22571131

fbshipit-source-id: 3e1a12e5f

sledge/src/fol.ml

@@ -1113,7 +1113,14 @@ and of_ses : Ses.Term.t -> exp =
     match Ses.Term.Qset.pop_min_elt sum with
     | None -> zero
     | Some (e, q, sum) ->
-        let mul e q = mulq q (of_ses e) in
+        let mul e q =
+          if Q.equal Q.one q then of_ses e
+          else
+            match of_ses e with
+            | `Trm (Z z) -> rational (Q.mul q (Q.of_z z))
+            | `Trm (Q r) -> rational (Q.mul q r)
+            | t -> mulq q t
+        in
         Ses.Term.Qset.fold sum ~init:(mul e q) ~f:(fun e q s ->
             add (mul e q) s ) )
   | Mul prod -> (

sledge/src/sh_test.ml

@@ -147,13 +147,11 @@ let%test_module _ =
       pp q' ;
       [%expect
         {|
-        ∃ %x_6 .   %x_6 = %x_6^ ∧ ((-1 × 1) + (1 × %y_7)) = %y_7^ ∧ emp
+        ∃ %x_6 .   %x_6 = %x_6^ ∧ (-1 + %y_7) = %y_7^ ∧ emp
     
-          ((-1 × 1) + (1 × %y_7)) = %y_7^
-        ∧ (%y_7^ = ((-1 × 1) + (1 × %y_7)))
-        ∧ emp
+          (-1 + %y_7) = %y_7^ ∧ (%y_7^ = (-1 + %y_7)) ∧ emp
 
-          ((-1 × 1) + (1 × %y_7)) = %y_7^ ∧ emp |}]
+          (-1 + %y_7) = %y_7^ ∧ emp |}]
 
     let%expect_test _ =
       let q =

sledge/src/solver_test.ml

@@ -196,7 +196,7 @@ let%test_module _ =
             %a_2 = %a0_10
           ∧ 16 = %m_8 = %n_9
           ∧ (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
-          ∧ ((16 × 1) + (1 × %k_5)) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
+          ∧ (16 + %k_5) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
 
     let%expect_test _ =
       infer_frame
@@ -218,7 +218,7 @@ let%test_module _ =
             %a_2 = %a0_10
           ∧ 16 = %m_8 = %n_9
           ∧ (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
-          ∧ ((16 × 1) + (1 × %k_5)) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
+          ∧ (16 + %k_5) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
 
     let seg_split_symbolically =
       Sh.star
@@ -237,8 +237,7 @@ let%test_module _ =
         {|
         ( infer_frame:
             %l_6
-              -[ %l_6, 16 )->
-              ⟨(8 × %n_9),%a_2⟩^⟨((16 × 1) + (-8 × %n_9)),%a_3⟩
+              -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩^⟨(16 + (-8 × %n_9)),%a_3⟩
           * ( (  2 = %n_9 ∧ emp)
             ∨ (  0 = %n_9 ∧ emp)
             ∨ (  1 = %n_9 ∧ emp)
@@ -249,7 +248,7 @@ let%test_module _ =
             ( (  %a_1 = %a_2
                ∧ 2 = %n_9
                ∧ 16 = %m_8
-               ∧ ((16 × 1) + (1 × %l_6)) -[ %l_6, 16 )-> ⟨0,%a_3⟩)
+               ∧ (16 + %l_6) -[ %l_6, 16 )-> ⟨0,%a_3⟩)
             ∨ (  %a_3 = _
                ∧ 1 = %n_9
                ∧ 16 = %m_8
@@ -273,8 +272,7 @@ let%test_module _ =
         ( infer_frame:
             (%n_9 ≤ 2)
           ∧ %l_6
-              -[ %l_6, 16 )->
-              ⟨(8 × %n_9),%a_2⟩^⟨((16 × 1) + (-8 × %n_9)),%a_3⟩
+              -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩^⟨(16 + (-8 × %n_9)),%a_3⟩
           \- ∃ %a_1, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩
         ) infer_frame: |}]