diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml index d0bf054c9..570fe0465 100644 --- a/sledge/src/sh.ml +++ b/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' -> diff --git a/sledge/src/test/sh_test.ml b/sledge/src/test/sh_test.ml index c6f7aa1bf..3ed12cba8 100644 --- a/sledge/src/test/sh_test.ml +++ b/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 )