[sledge] Fix bug in Sh.simplify

Summary:
When a stem has an occurrence of an existential, say x, and x is
substituted out by different witnesses, say a and b, in two disjuncts,
then the connection to other occurrences of a and b are lost.

This diff fixes this problem by propagating the solved variables that
survive normalization down to subformulas, and not removing those
variables from subformulas.

Reviewed By: jvillard

Differential Revision: D25756583

fbshipit-source-id: dabda743f

sledge/src/sh.ml

@@ -767,7 +767,7 @@ let remove_absent_xs ks q =
     in
     {q with xs; djns}
 
-let rec simplify_ us rev_xss ancestor_subst q =
+let rec simplify_ us rev_xss survived ancestor_subst q =
   [%Trace.call fun {pf} ->
     pf "%a@ %a@ %a" pp_vss (List.rev rev_xss) Context.Subst.pp
       ancestor_subst pp_raw q]
@@ -795,14 +795,17 @@ let rec simplify_ us rev_xss ancestor_subst q =
       {(norm subst {q with djns= emp.djns; ctx= emp.ctx}) with ctx= q.ctx}
     in
     (* recursively simplify subformulas *)
+    let survived = Var.Set.union survived (fv (elim_exists stem.xs stem)) in
     let q =
       starN
         ( stem
         :: List.map q.djns ~f:(fun djn ->
-               orN (List.map ~f:(simplify_ us rev_xss subst) djn) ) )
+               orN (List.map ~f:(simplify_ us rev_xss survived subst) djn) )
+        )
     in
     if is_false q then false_ q.us
     else
+      let removed = Var.Set.diff removed survived in
       let removed =
         if Var.Set.is_empty removed then Var.Set.empty
         else (
@@ -836,7 +839,7 @@ let simplify q =
     let q = propagate_context Var.Set.empty Context.empty q in
     if is_false q then false_ q.us
     else
-      let q = simplify_ q.us [] Context.Subst.empty q in
+      let q = simplify_ q.us [] Var.Set.empty Context.Subst.empty q in
       q )
   |>
   [%Trace.retn fun {pf} q' ->

sledge/src/test/sh_test.ml

@@ -16,7 +16,10 @@ let%test_module _ =
 
     (* let () =
      *   Trace.init ~margin:160
-     *     ~config:(Result.get_ok (Trace.parse "+Sh+Context+Arithmetic"))
+     *     ~config:
+     *       (Result.get_ok
+     *          (Trace.parse
+     *             "+Sh.simplify+Sh.simplify_+Sh.norm+Sh.and_subst+Context.solve_and_elim+Context.partition_valid+Context.solve_for_vars+Context.apply_and_elim+Context.apply_subst+Context.elim"))
      *     () *)
 
     [@@@warning "-32"]
@@ -36,16 +39,20 @@ let%test_module _ =
     let c_, wrt = Var.fresh "c" ~wrt
     let d_, wrt = Var.fresh "d" ~wrt
     let e_, wrt = Var.fresh "e" ~wrt
+    let m_, wrt = Var.fresh "m" ~wrt
     let x_, wrt = Var.fresh "x" ~wrt
     let y_, wrt = Var.fresh "y" ~wrt
+    let z_, wrt = Var.fresh "z" ~wrt
     let _ = wrt
     let a = Term.var a_
     let b = Term.var b_
     let c = Term.var c_
     let d = Term.var d_
     let e = Term.var e_
+    let m = Term.var m_
     let x = Term.var x_
     let y = Term.var y_
+    let z = Term.var z_
 
     let eq_concat (siz, seq) ms =
       Formula.eq (Term.sized ~siz ~seq)
@@ -61,7 +68,7 @@ let%test_module _ =
            (seg {loc= x; bas= x; len= !16; siz= !8; cnt= a})
            (seg {loc= x + !8; bas= x; len= !16; siz= !8; cnt= b})) ;
       [%expect {|
-          %x_6 -[)-> ⟨8,%a_1⟩^⟨8,%b_2⟩ |}]
+          %x_7 -[)-> ⟨8,%a_1⟩^⟨8,%b_2⟩ |}]
 
     let%expect_test _ =
       let p = exists ~$[x_] (extend_us ~$[x_] emp) in
@@ -71,11 +78,11 @@ let%test_module _ =
       pp (star p q) ;
       [%expect
         {|
-          ∃ %x_6 .   emp
+          ∃ %x_7 .   emp
 
-            0 = %x_6 ∧ emp
+            0 = %x_7 ∧ emp
 
-            0 = %x_6 ∧ emp |}]
+            0 = %x_7 ∧ emp |}]
 
     let%expect_test _ =
       let q =
@@ -91,11 +98,11 @@ let%test_module _ =
       pp_djn (dnf q) ;
       [%expect
         {|
-          ( (  0 = %x_6 ∧ emp) ∨ (  ( (  1 = %y_7 ∧ emp) ∨ (  emp) )) )
-
-        ( (∃ %x_6, %x_7 .   2 = %x_7 ∧ (2 = %x_7) ∧ emp)
-        ∨ (∃ %x_6 .   1 = %y_7 = %x_6 ∧ ((1 = %x_6) ∧ (1 = %y_7)) ∧ emp)
-        ∨ (  0 = %x_6 ∧ (0 = %x_6) ∧ emp)
+          ( (  0 = %x_7 ∧ emp) ∨ (  ( (  1 = %y_8 ∧ emp) ∨ (  emp) )) )
+    
+        ( (∃ %x_7, %x_8 .   2 = %x_8 ∧ (2 = %x_8) ∧ emp)
+        ∨ (∃ %x_7 .   1 = %y_8 = %x_7 ∧ ((1 = %x_7) ∧ (1 = %y_8)) ∧ emp)
+        ∨ (  0 = %x_7 ∧ (0 = %x_7) ∧ emp)
         ) |}]
 
     let%expect_test _ =
@@ -114,13 +121,13 @@ let%test_module _ =
       pp_djn (dnf q) ;
       [%expect
         {|
-          ( (  emp) ∨ (  ( (  1 = %y_7 ∧ emp) ∨ (  emp) )) )
-
-        ( (∃ %x_6, %x_8, %x_9 .   2 = %x_9 ∧ (2 = %x_9) ∧ emp)
-        ∨ (∃ %x_6, %x_8 .
-             1 = %x_8 = %y_7 ∧ ((1 = %y_7) ∧ (1 = %x_8))
+          ( (  emp) ∨ (  ( (  1 = %y_8 ∧ emp) ∨ (  emp) )) )
+    
+        ( (∃ %x_7, %x_9, %x_10 .   2 = %x_10 ∧ (2 = %x_10) ∧ emp)
+        ∨ (∃ %x_7, %x_9 .
+             1 = %x_9 = %y_8 ∧ ((1 = %y_8) ∧ (1 = %x_9))
            ∧ emp)
-        ∨ (∃ %x_6 .   0 = %x_6 ∧ (0 = %x_6) ∧ emp)
+        ∨ (∃ %x_7 .   0 = %x_7 ∧ (0 = %x_7) ∧ emp)
         ) |}]
 
     let%expect_test _ =
@@ -139,9 +146,9 @@ let%test_module _ =
       pp (simplify q) ;
       [%expect
         {|
-        ( (  emp) ∨ (  ( (  1 = %y_7 ∧ emp) ∨ (  emp) )) )
-
-        ( (  emp) ∨ (  1 = %y_7 ∧ emp) ∨ (  emp) ) |}]
+        ( (  emp) ∨ (  ( (  1 = %y_8 ∧ emp) ∨ (  emp) )) )
+    
+        ( (  emp) ∨ (  1 = %y_8 ∧ emp) ∨ (  emp) ) |}]
 
     let%expect_test _ =
       let q = exists ~$[x_] (of_eqs [(f x, x); (f y, y - !1)]) in
@@ -151,11 +158,11 @@ let%test_module _ =
       pp q' ;
       [%expect
         {|
-        ∃ %x_6 .   %x_6 = f(%x_6) ∧ (-1 + %y_7) = f(%y_7) ∧ emp
-
-          (-1 + %y_7) = f(%y_7) ∧ ((1 + f(%y_7)) = %y_7) ∧ emp
-
-          (-1 + %y_7) = f(%y_7) ∧ emp |}]
+        ∃ %x_7 .   %x_7 = f(%x_7) ∧ (-1 + %y_8) = f(%y_8) ∧ emp
+    
+          (-1 + %y_8) = f(%y_8) ∧ ((1 + f(%y_8)) = %y_8) ∧ emp
+    
+          (-1 + %y_8) = f(%y_8) ∧ emp |}]
 
     let%expect_test _ =
       let q =
@@ -178,7 +185,7 @@ let%test_module _ =
         ∃ %a_1, %c_3, %d_4, %e_5 .
           (⟨8,%a_1⟩^⟨8,%d_4⟩) = %e_5 ∧ (⟨16,%e_5⟩ = (⟨8,%a_1⟩^⟨8,%d_4⟩))
         ∧ emp
-        * ( (  tt ∧ (0 ≠ %x_6) ∧ emp)
+        * ( (  tt ∧ (0 ≠ %x_7) ∧ emp)
           ∨ (∃ %b_2 .
                (⟨4,%c_3⟩^⟨4,%b_2⟩) = %a_1
              ∧ (⟨8,%a_1⟩ = (⟨4,%c_3⟩^⟨4,%b_2⟩))
@@ -187,7 +194,43 @@ let%test_module _ =
 
           tt ∧ tt
         ∧ emp
-        * ( (  tt ∧ tt ∧ emp) ∨ (  tt ∧ (0 ≠ %x_6) ∧ emp) )
+        * ( (  tt ∧ tt ∧ emp) ∨ (  tt ∧ (0 ≠ %x_7) ∧ emp) )
+
+          ( (  emp) ∨ (  (0 ≠ %x_7) ∧ emp) ) |}]
+
+    let%expect_test _ =
+      let q =
+        exists
+          ~$[b_; m_]
+          (star
+             (seg {loc= x; bas= b; len= m; siz= !8; cnt= !0})
+             (or_ (of_eqs [(b, y); (m, c)]) (of_eqs [(b, z); (m, c)])))
+      in
+      pp_raw q ;
+      let q' = simplify q in
+      pp_raw q' ;
+      pp q' ;
+      [%expect
+        {|
+        ∃ %b_2, %m_6 .
+          tt ∧ tt
+        ∧ %x_7 -[ %b_2, %m_6 )-> ⟨8,0⟩
+        * ( (  %b_2 = %y_8 ∧ %c_3 = %m_6
+             ∧ ((%b_2 = %y_8) ∧ (%c_3 = %m_6))
+             ∧ emp)
+          ∨ (  %b_2 = %z_9 ∧ %c_3 = %m_6
+             ∧ ((%b_2 = %z_9) ∧ (%c_3 = %m_6))
+             ∧ emp)
+          )
+    
+        ∃ %b_2 .
+          tt ∧ tt
+        ∧ %x_7 -[ %b_2, %c_3 )-> ⟨8,0⟩
+        * ( (  %b_2 = %z_9 ∧ (%b_2 = %z_9) ∧ emp)
+          ∨ (  %b_2 = %y_8 ∧ (%b_2 = %y_8) ∧ emp)
+          )
 
-          ( (  emp) ∨ (  (0 ≠ %x_6) ∧ emp) ) |}]
+        ∃ %b_2 .
+          %x_7 -[ %b_2, %c_3 )-> ⟨8,0⟩
+        * ( (  %b_2 = %z_9 ∧ emp) ∨ (  %b_2 = %y_8 ∧ emp) ) |}]
   end )