From a18165c55309763ff64bd224f98d4f96ca03865b Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 12 Jan 2021 04:25:07 -0800 Subject: [PATCH] [sledge] Improve tracing Reviewed By: jvillard Differential Revision: D24630523 fbshipit-source-id: 1e42bd331 --- sledge/src/exec.ml | 4 ++- sledge/src/fol/context.ml | 29 ++++++++++++++++----- sledge/src/fol/trm.ml | 30 +++++++++++++++------- sledge/src/fol/var0.ml | 15 ++++++----- sledge/src/llair/exp.ml | 3 ++- sledge/src/llair/llair.ml | 2 +- sledge/src/sh.ml | 29 ++++++++++++--------- sledge/src/test/context_test.ml | 4 +-- sledge/src/test/fol_test.ml | 14 +++++----- sledge/src/test/sh_test.ml | 45 +++++++++++++++++---------------- sledge/src/test/solver_test.ml | 20 ++++----------- 11 files changed, 112 insertions(+), 83 deletions(-) diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml index da67e0f9a..4e33ff666 100644 --- a/sledge/src/exec.ml +++ b/sledge/src/exec.ml @@ -636,6 +636,8 @@ let strlen_spec reg ptr = open Option.Import +let pp ppf q = Sh.pp ppf (Option.value q ~default:(Sh.false_ Var.Set.empty)) + let check_preserve_us (q0 : Sh.t) (q1 : Sh.t) = let gain_us = Var.Set.diff q1.us q0.us in let lose_us = Var.Set.diff q0.us q1.us in @@ -679,7 +681,7 @@ let exec_spec_ (xs, pre) (gs, {foot; sub; ms; post}) = (Sh.star post (Sh.exists ms (Sh.rename sub frame)))) |> [%Trace.retn fun {pf} r -> - pf "%a" (Option.pp "%a" Sh.pp) r ; + pf "%a" pp r ; assert (Option.for_all ~f:(check_preserve_us (Sh.exists xs pre)) r)] (* execute a command with given spec from pre *) diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml index 008dc9e88..25c1c70a5 100644 --- a/sledge/src/fol/context.ml +++ b/sledge/src/fol/context.ml @@ -445,8 +445,8 @@ let pp_diff_cls = List.pp_diff ~cmp:Trm.compare "@ = " Trm.pp let ppx_classes x fs clss = List.pp "@ @<2>∧ " (fun fs (rep, cls) -> - Format.fprintf fs "@[%a@ = %a@]" (Trm.ppx x) rep (ppx_cls x) - (List.sort ~cmp:Trm.compare cls) ) + if not (List.is_empty cls) then + Format.fprintf fs "@[%a@ = %a@]" (Trm.ppx x) rep (ppx_cls x) cls ) fs (Iter.to_list (Trm.Map.to_iter clss)) @@ -455,9 +455,26 @@ let pp_classes fs r = ppx_classes (fun _ -> None) fs (classes r) let pp_diff_clss = Trm.Map.pp_diff ~eq:(List.equal Trm.equal) Trm.pp pp_cls pp_diff_cls -let pp fs r = ppx_classes (fun _ -> None) fs (classes r) +let pp fs r = + let clss = classes r in + if Trm.Map.is_empty clss then + Format.fprintf fs (if r.sat then "tt" else "ff") + else ppx_classes (fun _ -> None) fs clss let ppx var_strength fs clss noneqs = + let without_anon_vars = + List.filter ~f:(fun e -> + match Var.of_trm e with + | Some v -> Poly.(var_strength v <> Some `Anonymous) + | None -> true ) + in + let clss = + Trm.Map.fold clss Trm.Map.empty ~f:(fun ~key:rep ~data:cls m -> + let cls = without_anon_vars cls in + if not (List.is_empty cls) then + Trm.Map.add ~key:rep ~data:(List.sort ~cmp:Trm.compare cls) m + else m ) + in let first = Trm.Map.is_empty clss in if not first then Format.fprintf fs " " ; ppx_classes var_strength fs clss ; @@ -547,7 +564,7 @@ let rec canon r a = let canon_f r b = [%trace] - ~call:(fun {pf} -> pf "%a@ %a" Fml.pp b pp r) + ~call:(fun {pf} -> pf "%a@ %a" Fml.pp b pp_raw r) ~retn:(fun {pf} -> pf "%a" Fml.pp) @@ fun () -> Fml.map_trms ~f:(canon r) b @@ -773,7 +790,7 @@ let dnf f = Fml.fold_dnf ~meet1 ~join1 ~top ~bot f let rename r sub = - [%Trace.call fun {pf} -> pf "%a" pp r] + [%Trace.call fun {pf} -> pf "@[%a@]@ %a" Var.Subst.pp sub pp r] ; let rep = Subst.map_entries ~f:(Trm.map_vars ~f:(Var.Subst.apply sub)) r.rep @@ -1103,7 +1120,7 @@ let pp_vss fs vss = [fv u ⊆ ⋃ⱼ₌₁ⁱ vⱼ] *) let solve_for_vars vss r = [%Trace.call fun {pf} -> - pf "%a@ @[%a@]@ @[%a@]" pp_vss vss pp_classes r pp r ; + pf "%a@ @[%a@]" pp_vss vss pp r ; invariant r] ; let wrt = Var.Set.union_list vss in diff --git a/sledge/src/fol/trm.ml b/sledge/src/fol/trm.ml index 93cf75f29..f37fb603a 100644 --- a/sledge/src/fol/trm.ml +++ b/sledge/src/fol/trm.ml @@ -136,6 +136,24 @@ end = struct | Var {id= i; name= _}, Var {id= j; name= _} -> Int.equal i j | _ -> equal x y + (* nul-terminated string value represented by a concatenation *) + let string_of_concat xs = + let exception Not_a_string in + try + let len_1 = Array.length xs - 1 in + ( match xs.(len_1) with + | Sized {siz= Z o; seq= Z c} when Z.equal Z.one o && Z.equal Z.zero c + -> + () + | _ -> raise_notrace Not_a_string ) ; + Some + (String.init len_1 ~f:(fun i -> + match xs.(i) with + | Sized {siz= Z o; seq= Z c} when Z.equal Z.one o -> + Char.of_int_exn (Z.to_int c) + | _ -> raise_notrace Not_a_string )) + with _ -> None + let rec ppx strength fs trm = let rec pp fs trm = let pf fmt = pp_boxed fs fmt in @@ -149,15 +167,9 @@ end = struct | Extract {seq; off; len} -> pf "%a[%a,%a)" pp seq pp off pp len | Concat [||] -> pf "@<2>⟨⟩" | Concat xs -> ( - let exception Not_a_string in - try - pf "%S" - (String.init (Array.length xs) ~f:(fun i -> - match xs.(i) with - | Sized {siz= Z o; seq= Z c} when Z.equal Z.one o -> - Char.of_int_exn (Z.to_int c) - | _ -> raise_notrace Not_a_string )) - with _ -> pf "(%a)" (Array.pp "@,^" pp) xs ) + match string_of_concat xs with + | Some s -> pf "%S" s + | None -> pf "(%a)" (Array.pp "@,^" pp) xs ) | Apply (f, [||]) -> pf "%a" Funsym.pp f | Apply ( ( (Rem | BitAnd | BitOr | BitXor | BitShl | BitLshr | BitAshr) diff --git a/sledge/src/fol/var0.ml b/sledge/src/fol/var0.ml index 5e8240c0a..ec355703c 100644 --- a/sledge/src/fol/var0.ml +++ b/sledge/src/fol/var0.ml @@ -16,13 +16,14 @@ module Make (T : REPR) = struct let ppx strength ppf v = let id = id v in let name = name v in - if id = 0 then Trace.pp_styled `Bold "%%%s" ppf name - else - match strength v with - | None -> Format.fprintf ppf "%%%s_%d" name id - | Some `Universal -> Trace.pp_styled `Bold "%%%s_%d" ppf name id - | Some `Existential -> Trace.pp_styled `Cyan "%%%s_%d" ppf name id - | Some `Anonymous -> Trace.pp_styled `Cyan "_" ppf + let pp_id ppf id = if id <> 0 then Format.fprintf ppf "_%d" id in + match strength v with + | None -> + if id = 0 then Trace.pp_styled `Bold "%%%s" ppf name + else Format.fprintf ppf "%%%s%a" name pp_id id + | Some `Universal -> Trace.pp_styled `Bold "%%%s%a" ppf name pp_id id + | Some `Existential -> Trace.pp_styled `Cyan "%%%s%a" ppf name pp_id id + | Some `Anonymous -> Trace.pp_styled `Cyan "_" ppf let pp = ppx (fun _ -> None) diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index 81ef42b91..636c5cc1c 100644 --- a/sledge/src/llair/exp.ml +++ b/sledge/src/llair/exp.ml @@ -161,7 +161,8 @@ and pp_record fs elts = match String.init (IArray.length elts) ~f:(fun i -> match IArray.get elts i with - | Integer {data; _} -> Char.of_int_exn (Z.to_int data) + | Integer {data; typ= Integer {byts= 1; _}} -> + Char.of_int_exn (Z.to_int data) | _ -> raise_notrace (Invalid_argument "not a string") ) with | s -> Format.fprintf fs "@[%s@]" (String.escaped s) diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml index 1d61160c5..01bd54f21 100644 --- a/sledge/src/llair/llair.ml +++ b/sledge/src/llair/llair.ml @@ -284,7 +284,7 @@ let pp_inst fs inst = reg msg Loc.pp loc | Abort {loc} -> pf "@[<2>abort;@]\t%a" Loc.pp loc | Intrinsic {reg; name; args; loc} -> - pf "@[<2>%aintrinsic %a(%a);@]\t%a" + pf "@[<2>%aintrinsic@ %a(@,@[%a@]);@]\t%a" (Option.pp "%a := " Reg.pp) reg Intrinsic.pp name (IArray.pp ",@ " Exp.pp) args Loc.pp loc diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml index 764a6001c..15c8019ee 100644 --- a/sledge/src/sh.ml +++ b/sledge/src/sh.ml @@ -181,41 +181,46 @@ let pp_us ?(pre = ("" : _ fmt)) ?vs () fs us = [%Trace.fprintf fs "%( %)@[%a@] .@ " pre (Var.Set.pp_diff Var.pp) (vs, us)] -let rec pp_ ?var_strength vs parent_xs parent_ctx fs +let rec pp_ ?var_strength ?vs ancestor_xs parent_ctx fs {us; xs; ctx; pure; heap; djns} = Format.pp_open_hvbox fs 0 ; let x v = Option.bind ~f:(fun (_, m) -> Var.Map.find v m) var_strength in - pp_us ~vs () fs us ; + pp_us ~pre:"@<2>∀ " ?vs () fs us ; + let vs = Option.value vs ~default:Var.Set.empty in let xs_d_vs, xs_i_vs = Var.Set.diff_inter (Var.Set.filter xs ~f:(fun v -> Poly.(x v <> Some `Anonymous))) vs in if not (Var.Set.is_empty xs_i_vs) then ( - Format.fprintf fs "@<2>∃ @[%a@] ." (Var.Set.ppx x) xs_i_vs ; + Format.fprintf fs "@<3>∃↑ @[%a@] ." (Var.Set.ppx x) xs_i_vs ; if not (Var.Set.is_empty xs_d_vs) then Format.fprintf fs "@ " ) ; if not (Var.Set.is_empty xs_d_vs) then Format.fprintf fs "@<2>∃ @[%a@] .@ " (Var.Set.ppx x) xs_d_vs ; let first = if Option.is_some var_strength then Context.ppx_diff x fs parent_ctx pure ctx - else if Formula.equal Formula.tt pure then true else ( - Format.fprintf fs "@[ %a@]" Formula.pp pure ; + Format.fprintf fs "@[ %a@ @<2>∧ %a@]" Context.pp ctx Formula.pp + pure ; false ) in if List.is_empty heap then Format.fprintf fs ( if first then if List.is_empty djns then " emp" else "" else "@ @<5>∧ emp" ) - else pp_heap x ~pre:(if first then " " else "@ @<2>∧ ") ctx fs heap ; + else + pp_heap x + ~pre:(if first then " " else "@ @<2>∧ ") + (if Option.is_some var_strength then ctx else emp.ctx) + fs heap ; let first = first && List.is_empty heap in List.pp ~pre:(if first then " " else "@ * ") "@ * " (pp_djn ?var_strength (Var.Set.union vs (Var.Set.union us xs)) - (Var.Set.union parent_xs xs) + (Var.Set.union ancestor_xs xs) ctx) fs djns ; Format.pp_close_box fs () @@ -230,12 +235,12 @@ and pp_djn ?var_strength vs xs ctx fs = function var_strength_ xs var_strength_stem sjn in Format.fprintf fs "@[(%a)@]" - (pp_ ?var_strength vs (Var.Set.union xs sjn.xs) ctx) + (pp_ ?var_strength ~vs (Var.Set.union xs sjn.xs) ctx) sjn )) djn -let pp_diff_eq ?(us = Var.Set.empty) ?(xs = Var.Set.empty) ctx fs q = - pp_ ~var_strength:(var_strength ~xs q) us xs ctx fs q +let pp_diff_eq ?us ?(xs = Var.Set.empty) ctx fs q = + pp_ ~var_strength:(var_strength ~xs q) ?vs:us xs ctx fs q let pp fs q = pp_diff_eq Context.empty fs q @@ -243,7 +248,7 @@ let pp_djn fs d = pp_djn ?var_strength:None Var.Set.empty Var.Set.empty Context.empty fs d let pp_raw fs q = - pp_ ?var_strength:None Var.Set.empty Var.Set.empty Context.empty fs q + pp_ ?var_strength:None ?vs:None Var.Set.empty Context.empty fs q let fv_seg seg = fold_vars_seg ~f:Var.Set.add seg Var.Set.empty @@ -794,5 +799,5 @@ let simplify q = q |> [%Trace.retn fun {pf} q' -> - pf "@\n" ; + pf "%a" pp_raw q' ; invariant q'] diff --git a/sledge/src/test/context_test.ml b/sledge/src/test/context_test.ml index 109f44aeb..5160f8fa5 100644 --- a/sledge/src/test/context_test.ml +++ b/sledge/src/test/context_test.ml @@ -58,8 +58,8 @@ let%test_module _ = pp r3 ; [%expect {| - %t_1 = %u_2 = %v_3 = %w_4 = %x_5 = %z_7 = g(%y_6, %t_1) - = g(%y_6, %t_1) + %t_1 = g(%y_6, %t_1) = g(%y_6, %t_1) = %z_7 = %x_5 = %w_4 = %v_3 + = %u_2 {sat= true; rep= [[%t_1 ↦ ]; diff --git a/sledge/src/test/fol_test.ml b/sledge/src/test/fol_test.ml index 6b73ee786..e7604dc84 100644 --- a/sledge/src/test/fol_test.ml +++ b/sledge/src/test/fol_test.ml @@ -112,7 +112,7 @@ let%test_module _ = let%expect_test _ = pp r0 ; - [%expect {||}] + [%expect {| tt |}] let%test _ = difference r0 (f x) (f x) |> Poly.equal (Some (Z.of_int 0)) let%test _ = difference r0 !4 !3 |> Poly.equal (Some (Z.of_int 1)) @@ -138,7 +138,7 @@ let%test_module _ = pp_raw r2 ; [%expect {| - %x_5 = %y_6 = %z_7 = f(%x_5) + %x_5 = f(%x_5) = %z_7 = %y_6 {sat= true; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]; [f(%x_5) ↦ %x_5]]} |}] @@ -181,8 +181,8 @@ let%test_module _ = pp_raw r3 ; [%expect {| - %t_1 = %u_2 = %v_3 = %w_4 = %x_5 = %z_7 = g(%y_6, %t_1) - = g(%y_6, %t_1) + %t_1 = g(%y_6, %t_1) = g(%y_6, %t_1) = %z_7 = %x_5 = %w_4 = %v_3 + = %u_2 {sat= true; rep= [[%t_1 ↦ ]; @@ -228,7 +228,7 @@ let%test_module _ = pp_raw r6 ; [%expect {| - 1 = %x_5 = %y_6 + 1 = %y_6 = %x_5 {sat= true; rep= [[%x_5 ↦ 1]; [%y_6 ↦ 1]]} |}] @@ -241,7 +241,7 @@ let%test_module _ = pp_raw r7 ; [%expect {| - %v_3 = %x_5 ∧ %w_4 = %y_6 = %z_7 + %v_3 = %x_5 ∧ %w_4 = %z_7 = %y_6 {sat= true; rep= [[%v_3 ↦ ]; @@ -257,7 +257,7 @@ let%test_module _ = pp_raw r7' ; [%expect {| - %v_3 = %w_4 = %x_5 = %y_6 = %z_7 + %v_3 = %z_7 = %y_6 = %x_5 = %w_4 {sat= true; rep= [[%v_3 ↦ ]; diff --git a/sledge/src/test/sh_test.ml b/sledge/src/test/sh_test.ml index b2a5a6215..c6f7aa1bf 100644 --- a/sledge/src/test/sh_test.ml +++ b/sledge/src/test/sh_test.ml @@ -91,13 +91,11 @@ let%test_module _ = pp_djn (dnf q) ; [%expect {| - ( ( 0 = %x_6 ∧ emp) - ∨ ( ( ( 1 = _ = %y_7 ∧ emp) ∨ ( 2 = _ ∧ emp) )) - ) - - ( (∃ %x_6, %x_7 . (2 = %x_7) ∧ emp) - ∨ (∃ %x_6 . ((1 = %x_6) ∧ (1 = %y_7)) ∧ emp) - ∨ ( (0 = %x_6) ∧ emp) + ( ( 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) ) |}] let%expect_test _ = @@ -116,13 +114,13 @@ let%test_module _ = pp_djn (dnf q) ; [%expect {| - ( ( 0 = _ ∧ emp) - ∨ ( ( ( 1 = _ = %y_7 ∧ emp) ∨ ( 2 = _ ∧ emp) )) - ) - - ( (∃ %x_6, %x_8, %x_9 . (2 = %x_9) ∧ emp) - ∨ (∃ %x_6, %x_8 . ((1 = %y_7) ∧ (1 = %x_8)) ∧ emp) - ∨ (∃ %x_6 . (0 = %x_6) ∧ emp) + ( ( 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) + ∨ (∃ %x_6 . 0 = %x_6 ∧ (0 = %x_6) ∧ emp) ) |}] let%expect_test _ = @@ -141,9 +139,7 @@ let%test_module _ = pp (simplify q) ; [%expect {| - ( ( 0 = _ ∧ emp) - ∨ ( ( ( 1 = _ = %y_7 ∧ emp) ∨ ( 2 = _ ∧ emp) )) - ) + ( ( emp) ∨ ( ( ( 1 = %y_7 ∧ emp) ∨ ( emp) )) ) ( ( emp) ∨ ( 1 = %y_7 ∧ emp) ∨ ( emp) ) |}] @@ -157,7 +153,7 @@ let%test_module _ = {| ∃ %x_6 . %x_6 = f(%x_6) ∧ (-1 + %y_7) = f(%y_7) ∧ emp - ((1 + f(%y_7)) = %y_7) ∧ emp + (-1 + %y_7) = f(%y_7) ∧ ((1 + f(%y_7)) = %y_7) ∧ emp (-1 + %y_7) = f(%y_7) ∧ emp |}] @@ -180,13 +176,18 @@ let%test_module _ = [%expect {| ∃ %a_1, %c_3, %d_4, %e_5 . - (⟨16,%e_5⟩ = (⟨8,%a_1⟩^⟨8,%d_4⟩)) + (⟨8,%a_1⟩^⟨8,%d_4⟩) = %e_5 ∧ (⟨16,%e_5⟩ = (⟨8,%a_1⟩^⟨8,%d_4⟩)) ∧ emp - * ( ( (0 ≠ %x_6) ∧ emp) - ∨ (∃ %b_2 . (⟨8,%a_1⟩ = (⟨4,%c_3⟩^⟨4,%b_2⟩)) ∧ emp) + * ( ( tt ∧ (0 ≠ %x_6) ∧ emp) + ∨ (∃ %b_2 . + (⟨4,%c_3⟩^⟨4,%b_2⟩) = %a_1 + ∧ (⟨8,%a_1⟩ = (⟨4,%c_3⟩^⟨4,%b_2⟩)) + ∧ emp) ) - ( ( emp) ∨ ( (0 ≠ %x_6) ∧ emp) ) + tt ∧ tt + ∧ emp + * ( ( tt ∧ tt ∧ emp) ∨ ( tt ∧ (0 ≠ %x_6) ∧ emp) ) ( ( emp) ∨ ( (0 ≠ %x_6) ∧ emp) ) |}] end ) diff --git a/sledge/src/test/solver_test.ml b/sledge/src/test/solver_test.ml index 0d7098c46..41b7d31f7 100644 --- a/sledge/src/test/solver_test.ml +++ b/sledge/src/test/solver_test.ml @@ -143,7 +143,7 @@ let%test_module _ = {| ( infer_frame: %l_6 -[)-> ⟨8,%a_1⟩^⟨8,%a_2⟩ \- ∃ %a_3 . %l_6 -[)-> ⟨16,%a_3⟩ - ) infer_frame: %a_2 = _ ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}] + ) infer_frame: (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}] let%expect_test _ = check_frame @@ -158,8 +158,7 @@ let%test_module _ = %l_6 -[)-> ⟨8,%a_1⟩^⟨8,%a_2⟩ \- ∃ %a_3, %m_8 . %l_6 -[ %l_6, %m_8 )-> ⟨16,%a_3⟩ - ) infer_frame: - %a_2 = _ ∧ 16 = %m_8 ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}] + ) infer_frame: 16 = %m_8 ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}] let%expect_test _ = check_frame @@ -174,8 +173,7 @@ let%test_module _ = %l_6 -[)-> ⟨8,%a_1⟩^⟨8,%a_2⟩ \- ∃ %a_3, %m_8 . %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_3⟩ - ) infer_frame: - %a_2 = _ ∧ 16 = %m_8 ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}] + ) infer_frame: 16 = %m_8 ∧ (⟨8,%a_1⟩^⟨8,%a_2⟩) = %a_3 ∧ emp |}] let%expect_test _ = check_frame @@ -245,20 +243,12 @@ let%test_module _ = \- ∃ %a_1, %m_8 . %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩ ) infer_frame: - ( ( %a_3 = _ - ∧ 0 = %n_9 - ∧ 16 = %m_8 - ∧ (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1 - ∧ emp) + ( ( 0 = %n_9 ∧ 16 = %m_8 ∧ (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1 ∧ emp) ∨ ( %a_1 = %a_2 ∧ 2 = %n_9 ∧ 16 = %m_8 ∧ (16 + %l_6) -[ %l_6, 16 )-> ⟨0,%a_3⟩) - ∨ ( %a_3 = _ - ∧ 1 = %n_9 - ∧ 16 = %m_8 - ∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1 - ∧ emp) + ∨ ( 1 = %n_9 ∧ 16 = %m_8 ∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1 ∧ emp) ) |}] (* Incompleteness: equivalent to above but using ≤ instead of ∨ *)