[sledge] Fix: Fol.ses_map to account for simplification in Fol.to_ses

Summary:
The Ses constructors might simplify terms when called from
Fol.to_ses. Fix Fol.ses_map to account for this.

Reviewed By: jvillard

Differential Revision: D22571151

fbshipit-source-id: 1d573ac5f

sledge/src/fol.ml

@@ -1173,16 +1173,10 @@ let v_map_ses : (var -> var) -> Ses.Var.t -> Ses.Var.t =
   if v' == v then x else v_to_ses v'
 
 let ses_map : (Ses.Term.t -> Ses.Term.t) -> exp -> exp =
- fun f x ->
+ fun f x -> of_ses (f (to_ses x))
-  let e = to_ses x in
-  let e' = f e in
-  if e' == e then x else of_ses e'
 
 let f_ses_map : (Ses.Term.t -> Ses.Term.t) -> fml -> fml =
- fun f x ->
+ fun f x -> f_of_ses (f (f_to_ses x))
-  let e = f_to_ses x in
-  let e' = f e in
-  if e' == e then x else f_of_ses e'
 
 (*
  * Contexts

sledge/src/solver_test.ml

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