diff --git a/sledge/nonstdlib/multiset.ml b/sledge/nonstdlib/multiset.ml index 7dc9e7e40..48988dcbe 100644 --- a/sledge/nonstdlib/multiset.ml +++ b/sledge/nonstdlib/multiset.ml @@ -41,8 +41,8 @@ struct (Sexplib.Conv.pair_of_sexp elt_of_sexp Mul.t_of_sexp) sexp) - let pp sep pp_elt fs s = - List.pp sep pp_elt fs (Iter.to_list (M.to_iter s)) + let pp ?pre ?suf sep pp_elt fs s = + List.pp ?pre ?suf sep pp_elt fs (Iter.to_list (M.to_iter s)) let empty = M.empty let of_ x i = if Mul.equal Mul.zero i then empty else M.singleton x i diff --git a/sledge/nonstdlib/multiset_intf.ml b/sledge/nonstdlib/multiset_intf.ml index 2ae34de6c..1b758b9d8 100644 --- a/sledge/nonstdlib/multiset_intf.ml +++ b/sledge/nonstdlib/multiset_intf.ml @@ -28,7 +28,13 @@ module type S = sig val hash_fold_t : elt Hash.folder -> t Hash.folder val sexp_of_t : t -> Sexp.t val t_of_sexp : (Sexp.t -> elt) -> Sexp.t -> t - val pp : (unit, unit) fmt -> (elt * mul) pp -> t pp + + val pp : + ?pre:(unit, unit) fmt + -> ?suf:(unit, unit) fmt + -> (unit, unit) fmt + -> (elt * mul) pp + -> t pp (* constructors *) diff --git a/sledge/src/arithmetic.ml b/sledge/src/arithmetic.ml index 51f05f75f..52652712f 100644 --- a/sledge/src/arithmetic.ml +++ b/sledge/src/arithmetic.ml @@ -41,7 +41,9 @@ module Representation (Trm : INDETERMINATE) = struct (Prod.map_counts ~f:Int.neg den) in let num, den = num_den power_product in - Format.fprintf ppf "@[<2>(%a%a)@]" pp_num num pp_den den + if Prod.is_singleton num && Prod.is_empty den then + Format.fprintf ppf "@[<2>%a@]" pp_num num + else Format.fprintf ppf "@[<2>(%a%a)@]" pp_num num pp_den den (** [one] is the empty product Πᵢ₌₁⁰ xᵢ^pᵢ *) let one = Prod.empty @@ -86,10 +88,16 @@ module Representation (Trm : INDETERMINATE) = struct else let pp_coeff_mono ppf (m, c) = if Mono.equal_one m then Trace.pp_styled `Magenta "%a" ppf Q.pp c - else - Format.fprintf ppf "%a @<2>× %a" Q.pp c (Mono.ppx strength) m + else if Q.equal Q.one c then + Format.fprintf ppf "%a" (Mono.ppx strength) m + else Format.fprintf ppf "%a@<1>×%a" Q.pp c (Mono.ppx strength) m in - Format.fprintf ppf "@[<2>(%a)@]" (Sum.pp "@ + " pp_coeff_mono) poly + if Sum.is_singleton poly then + Format.fprintf ppf "@[<2>%a@]" (Sum.pp "@ + " pp_coeff_mono) poly + else + Format.fprintf ppf "@[<2>(%a)@]" + (Sum.pp "@ + " pp_coeff_mono) + poly let mono_invariant mono = let@ () = Invariant.invariant [%here] mono [%sexp_of: Mono.t] in diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml index 9502afefb..655d70fdc 100644 --- a/sledge/src/fol.ml +++ b/sledge/src/fol.ml @@ -314,6 +314,10 @@ let ppx_f strength fs fml = let pp_t = Trm.ppx strength in let rec pp fs fml = let pf fmt = pp_boxed fs fmt in + let pp_arith op x = + let a, c = Arith.split_const (Arith.trm x) in + pf "(%a@ @<2>%s %a)" Q.pp (Q.neg c) op (Arith.ppx strength) a + in let pp_join sep pos neg = pf "(%a%t%a)" (Fmls.pp ~sep pp) pos (fun ppf -> @@ -327,10 +331,10 @@ let ppx_f strength fs fml = | Not Tt -> pf "ff" | Eq (x, y) -> pf "(%a@ = %a)" pp_t x pp_t y | Not (Eq (x, y)) -> pf "(%a@ @<2>≠ %a)" pp_t x pp_t y - | Eq0 x -> pf "(0 = %a)" pp_t x - | Not (Eq0 x) -> pf "(0 @<2>≠ %a)" pp_t x - | Pos x -> pf "(0 < %a)" pp_t x - | Not (Pos x) -> pf "(0 @<2>≥ %a)" pp_t x + | Eq0 x -> pp_arith "=" x + | Not (Eq0 x) -> pp_arith "≠" x + | Pos x -> pp_arith "<" x + | Not (Pos x) -> pp_arith "≥" x | Not x -> pf "@<1>¬%a" pp x | And {pos; neg} -> pp_join "@ @<2>∧ " pos neg | Or {pos; neg} -> pp_join "@ @<2>∨ " pos neg diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml index f74423992..ec3fd34c4 100644 --- a/sledge/src/sh.ml +++ b/sledge/src/sh.ml @@ -210,6 +210,7 @@ let rec pp_ ?var_strength vs parent_xs parent_ctx fs 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 ; false ) diff --git a/sledge/src/test/fol_test.ml b/sledge/src/test/fol_test.ml index d3e8ecb98..dfafe2d09 100644 --- a/sledge/src/test/fol_test.ml +++ b/sledge/src/test/fol_test.ml @@ -189,8 +189,8 @@ let%test_module _ = pp_raw r3 ; [%expect {| - %z_7 = %u_2 = %v_3 = %w_4 = %x_5 = (1 × (%y_6 × %z_7)) - ∧ (1 × (%y_6^2 × %z_7)) = %t_1 + %z_7 = %u_2 = %v_3 = %w_4 = %x_5 = (%y_6 × %z_7) + ∧ (%y_6^2 × %z_7) = %t_1 {sat= true; rep= [[%t_1 ↦ (%y_6^2 × %z_7)]; @@ -216,9 +216,7 @@ let%test_module _ = pp_raw r4 ; [%expect {| - (-4 + 1 × (%z_7)) = %y_6 - ∧ (3 + 1 × (%z_7)) = %w_4 - ∧ (8 + 1 × (%z_7)) = %x_5 + (-4 + %z_7) = %y_6 ∧ (3 + %z_7) = %w_4 ∧ (8 + %z_7) = %x_5 {sat= true; rep= [[%w_4 ↦ (%z_7 + 3)]; @@ -324,7 +322,7 @@ let%test_module _ = pp_raw r8 ; [%expect {| - 14 = %y_6 ∧ (13 × (%z_7)) = %x_5 + 14 = %y_6 ∧ 13×%z_7 = %x_5 {sat= true; rep= [[%x_5 ↦ (13 × %z_7)]; [%y_6 ↦ 14]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}] @@ -363,11 +361,11 @@ let%test_module _ = {sat= true; rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} - (-8 + -1 × (%x_5) + 1 × (%z_7)) + (-8 + -1×%x_5 + %z_7) 8 - (8 + 1 × (%x_5) + -1 × (%z_7)) + (8 + %x_5 + -1×%z_7) -8 |}] @@ -380,13 +378,13 @@ let%test_module _ = let%expect_test _ = pp r11 ; - [%expect {| (-16 + 1 × (%z_7)) = %x_5 |}] + [%expect {| (-16 + %z_7) = %x_5 |}] let r12 = of_eqs [(!16, z - x); (x + !8 - z, z + !16 + !8 - z)] let%expect_test _ = pp r12 ; - [%expect {| (-16 + 1 × (%z_7)) = %x_5 |}] + [%expect {| (-16 + %z_7) = %x_5 |}] let r13 = of_eqs @@ -488,7 +486,7 @@ let%test_module _ = [-1 ↦ ]; [0 ↦ ]]} - %x_5 = %x_5^ ∧ (-1 + 1 × (%y_6)) = %y_6^ |}] + %x_5 = %x_5^ ∧ (-1 + %y_6) = %y_6^ |}] let r19 = of_eqs [(x, y + z); (x, !0); (y, !0)] diff --git a/sledge/src/test/sh_test.ml b/sledge/src/test/sh_test.ml index 11b8ea424..87966f656 100644 --- a/sledge/src/test/sh_test.ml +++ b/sledge/src/test/sh_test.ml @@ -154,11 +154,11 @@ let%test_module _ = pp q' ; [%expect {| - ∃ %x_6 . %x_6 = %x_6^ ∧ (-1 + 1 × (%y_7)) = %y_7^ ∧ emp + ∃ %x_6 . %x_6 = %x_6^ ∧ (-1 + %y_7) = %y_7^ ∧ emp - (tt ∧ ((-1 + 1 × (%y_7)) = %y_7^)) ∧ emp + (tt ∧ ((-1 + %y_7) = %y_7^)) ∧ emp - (-1 + 1 × (%y_7)) = %y_7^ ∧ emp |}] + (-1 + %y_7) = %y_7^ ∧ emp |}] let%expect_test _ = let q = @@ -185,7 +185,7 @@ let%test_module _ = ∨ (∃ %b_2 . (tt ∧ (⟨8,%a_1⟩ = (⟨4,%c_3⟩^⟨4,%b_2⟩))) ∧ emp) ) - tt ∧ emp * ( ( tt ∧ emp) ∨ ( (tt ∧ (0 ≠ %x_6)) ∧ emp) ) + ( ( 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 e4edc9da3..1b7473951 100644 --- a/sledge/src/test/solver_test.ml +++ b/sledge/src/test/solver_test.ml @@ -197,7 +197,7 @@ let%test_module _ = %a_2 = %a0_10 ∧ 16 = %m_8 = %n_9 ∧ (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1 - ∧ (16 + 1 × (%k_5)) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}] + ∧ (16 + %k_5) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}] let%expect_test _ = infer_frame @@ -219,7 +219,7 @@ let%test_module _ = %a_2 = %a0_10 ∧ 16 = %m_8 = %n_9 ∧ (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1 - ∧ (16 + 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 _ = [%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 + -8×%n_9),%a_3⟩ * ( ( 1 = %n_9 ∧ emp) ∨ ( 0 = %n_9 ∧ emp) ∨ ( 2 = %n_9 ∧ emp) @@ -254,7 +253,7 @@ let%test_module _ = ∨ ( %a_1 = %a_2 ∧ 2 = %n_9 ∧ 16 = %m_8 - ∧ (16 + 1 × (%l_6)) -[ %l_6, 16 )-> ⟨0,%a_3⟩) + ∧ (16 + %l_6) -[ %l_6, 16 )-> ⟨0,%a_3⟩) ∨ ( %a_3 = _ ∧ 0 = %n_9 ∧ 16 = %m_8 @@ -271,9 +270,8 @@ let%test_module _ = [%expect {| ( infer_frame: - (0 ≥ (-2 + 1 × (%n_9))) - ∧ %l_6 - -[ %l_6, 16 )-> ⟨(8 × (%n_9)),%a_2⟩^⟨(16 + -8 × (%n_9)),%a_3⟩ + (2 ≥ %n_9) + ∧ %l_6 -[ %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: |}]