Skip to content

Commit

Permalink
Review changes
Browse files Browse the repository at this point in the history 
Add some boxes to improve the output of the printers of `Expr`.
  • Loading branch information
@Halbaroth
Halbaroth committed Nov 21, 2023
1 parent 6b69c87 commit 285b2d4
Show file tree
Hide file tree
Showing 3 changed files with 66 additions and 64 deletions.
106 changes: 53 additions & 53 deletions src/lib/structures/expr.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -325,24 +325,30 @@ module SmtPrinter = struct
let rec pp_formula ppf form xs bind =
match form, xs, bind with
| Sy.F_Unit _, [f1; f2], _ ->
Fmt.pf ppf "@[(and %a %a)@]" pp_silent f1 pp_silent f2
Fmt.pf ppf "@[<hv 2>(and %a@ %a@])" pp_silent f1 pp_silent f2

| Sy.F_Iff, [f1; f2], _ ->
Fmt.pf ppf "@[(= %a %a)@]" pp_silent f1 pp_silent f2
Fmt.pf ppf "@[<hv 2>(= %a@ %a@])" pp_silent f1 pp_silent f2

| Sy.F_Xor, [f1; f2], _ ->
Fmt.pf ppf "@[(xor %a %a)@]" pp_silent f1 pp_silent f2
Fmt.pf ppf "@[<hv 2>(xor %a@ %a@])" pp_silent f1 pp_silent f2

| Sy.F_Clause _, [f1; f2], _ ->
Fmt.pf ppf "@[(or %a %a)@]" pp_silent f1 pp_silent f2
Fmt.pf ppf "@[<hv 2>(or %a@ %a@])" pp_silent f1 pp_silent f2

| Sy.F_Lemma, [], B_lemma { main; name; binders; _ } ->
Fmt.pf ppf "(! (forall (%a) %a) :named %s)"
pp_binders binders pp_silent main name
| Sy.F_Lemma, [], B_lemma { user_trs; main; name; binders; _ } ->
if Options.get_verbose () then
Fmt.pf ppf "@[<hv 2>(! @[<hv 2>(forall@ (%a)@ %a@ %a@])@ :named %s@])"
pp_binders binders pp_silent main pp_triggers user_trs name
else
Fmt.string ppf name

| Sy.F_Skolem, [], B_skolem { main; name; binders; _ } ->
Fmt.pf ppf "(! (exists (%a) %a) :named %s)"
pp_binders binders pp_silent main name
| Sy.F_Skolem, [], B_skolem { user_trs; main; name; binders; _ } ->
if Options.get_verbose () then
Fmt.pf ppf "@[<hv 2>(! @[<hv 2>(exists (%a) %a %a@])@ :named %s@])"
pp_binders binders pp_silent main pp_triggers user_trs name
else
Fmt.string ppf name

| _ -> assert false

Expand All @@ -352,41 +358,37 @@ module SmtPrinter = struct
Fmt.pf ppf "(= %a %a)"
pp a (fun ppf -> List.iter (Fmt.pf ppf " %a" pp)) l

| Sy.L_neg_eq, [a; b] ->
Fmt.pf ppf "(not (= %a %a))" pp a pp b

| Sy.L_neg_eq, _ :: _ ->
Fmt.pf ppf "(distinct %a)" Fmt.(list ~sep:sp pp) xs
Fmt.pf ppf "@[<hv 2>(distinct %a@])" Fmt.(list ~sep:sp pp) xs

| Sy.L_built Sy.LE, [a;b] ->
Fmt.pf ppf "(<= %a %a)" pp a pp b
Fmt.pf ppf "@[<hv 2>(<= %a@ %a@])" pp a pp b

| Sy.L_built Sy.LT, [a;b] ->
Fmt.pf ppf "(< %a %a)" pp a pp b
Fmt.pf ppf "@[<hv 2>(< %a@ %a@])" pp a pp b

| Sy.L_neg_built Sy.LE, [a; b] ->
Fmt.pf ppf "(> %a %a)" pp a pp b
Fmt.pf ppf "@[<hv 2>(> %a@ %a@])" pp a pp b

| Sy.L_neg_built Sy.LT, [a; b] ->
Fmt.pf ppf "(>= %a %a)" pp a pp b
Fmt.pf ppf "@[<hv 2>(>= %a@ %a@])" pp a pp b

| Sy.L_neg_pred, [a] ->
Fmt.pf ppf "(not %a)" pp a
Fmt.pf ppf "@[<hv 2>(not@ %a@])" pp a

| Sy.L_built (Sy.IsConstr hs), [e] ->
Fmt.pf ppf "((_ is %a) %a)" Hstring.print hs pp e
Fmt.pf ppf "@[<hv 2>((_ is %a)@ %a@])" Hstring.print hs pp e

| Sy.L_neg_built (Sy.IsConstr hs), [e] ->
Fmt.pf ppf "(not ((_ is %a) %a))" Hstring.print hs pp e
Fmt.pf ppf "(not @[<hv 2>((_ is %a)@ %a@]))"
Hstring.print hs pp e

| (Sy.L_built (Sy.LT | Sy.LE) | Sy.L_neg_built (Sy.LT | Sy.LE)
| Sy.L_neg_pred | Sy.L_eq | Sy.L_neg_eq
| Sy.L_built (Sy.IsConstr _)
| Sy.L_neg_built (Sy.IsConstr _)), _ ->
assert false

and pp_operator = Symbols.pp_operator ~format:`Smtlib

and pp_silent ppf t =
let { f ; xs ; ty; bind; _ } = t in
match f, xs with
Expand All @@ -396,7 +398,7 @@ module SmtPrinter = struct

| Sy.Let, [] ->
let x = match bind with B_let x -> x | _ -> assert false in
Fmt.pf ppf "(let ((%a %a)) %a)"
Fmt.pf ppf "@[<hv 2>(let@ ((%a %a))@ %a@])"
Symbols.print x.let_v
pp x.let_e
pp_silent x.in_e
Expand All @@ -406,19 +408,21 @@ module SmtPrinter = struct
match ty with
| Ty.Trecord { Ty.lbs = lbs; record_constr; _ } ->
assert (List.compare_lengths xs lbs = 0);
Fmt.pf ppf "(%a %a)"
Fmt.pf ppf "@[<hv 2>(%a@ %a@])"
Hstring.print record_constr
Fmt.(list ~sep:sp pp) xs

| _ ->
(* Exclude by the typechecker. *)
(* Excluded by the typechecker. *)
assert false
end

| Sy.Op op, [] -> Fmt.pf ppf "%a" pp_operator op
| Sy.Op op, [] -> Symbols.pp_smtlib_operator ppf op

| Sy.Op op, _ :: _ ->
Fmt.pf ppf "(%a %a)" pp_operator op Fmt.(list ~sep:sp pp) xs
Fmt.pf ppf "@[<hv 2>(%a@ %a@])"
Symbols.pp_smtlib_operator op
Fmt.(list ~sep:sp pp) xs

| Sy.True, [] -> Fmt.pf ppf "true"

Expand All @@ -427,7 +431,7 @@ module SmtPrinter = struct
| Sy.Name (n, _, _), [] -> Symbols.pp_name ppf (Hstring.view n)

| Sy.Name (n, _, _), _ :: _ ->
Fmt.pf ppf "(%a %a)"
Fmt.pf ppf "@[<hv 2>(%a@ %a@])"
Symbols.pp_name (Hstring.view n)
Fmt.(list ~sep:sp pp) xs

Expand Down Expand Up @@ -470,10 +474,10 @@ module SmtPrinter = struct
assert false

and pp_trigger ppf { content; _ } =
Fmt.pf ppf "@[<hv 2>(and %a)@]" Fmt.(list ~sep:sp pp) content
Fmt.pf ppf ":pattern @[<hv 2>(%a@])" Fmt.(list ~sep:sp pp) content

and pp_triggers ppf trs =
Fmt.pf ppf "@[<hv 2>(or %a)@]" Fmt.(list ~sep:sp pp_trigger) trs
Fmt.pf ppf "@[%a@]" Fmt.(list ~sep:sp pp_trigger) trs

(* Not displaying types when int SMT format *)
and pp_verbose ppf t = pp_silent ppf t
Expand All @@ -500,42 +504,40 @@ module AEPrinter = struct
else
Fmt.(iter_bindings ~sep:sp SMap.iter pp_binder) ppf binders

let rec pp_formula fmt form xs bind =
let open Format in
let rec pp_formula ppf form xs bind =
match form, xs, bind with
| Sy.F_Unit _, [f1; f2], _ ->
fprintf fmt "@[(%a /\\@ %a)@]" pp_silent f1 pp_silent f2
Fmt.pf ppf "@[(%a /\\@ %a@])" pp_silent f1 pp_silent f2

| Sy.F_Iff, [f1; f2], _ ->
fprintf fmt "@[(%a <->@ %a)@]" pp_silent f1 pp_silent f2
Fmt.pf ppf "@[(%a <->@ %a)@])" pp_silent f1 pp_silent f2

| Sy.F_Xor, [f1; f2], _ ->
fprintf fmt "@[(%a xor@ %a)@]" pp_silent f1 pp_silent f2
Fmt.pf ppf "@[(%a xor@ %a@])" pp_silent f1 pp_silent f2

| Sy.F_Clause _, [f1; f2], _ ->
fprintf fmt "@[(%a \\/@ %a)@]" pp_silent f1 pp_silent f2
Fmt.pf ppf "@[(%a \\/@ %a)@])" pp_silent f1 pp_silent f2

| Sy.F_Lemma, [], B_lemma { user_trs ; main ; name ; binders; _ } ->
if Options.get_verbose () then
fprintf fmt "(lemma: %s forall %a[%a].@ %a)"
Fmt.pf ppf "@[(lemma: %s@ forall %a[%a].@ %a@])"
name
pp_binders binders
pp_triggers user_trs
pp_silent main
else
fprintf fmt "(lem %s)" name
Fmt.pf ppf "(lem %s)" name

| Sy.F_Skolem, [], B_skolem { main; binders; _ } ->
fprintf fmt "(<sko exists %a.> %a)"
Fmt.pf ppf "(<sko exists %a.> %a)"
pp_binders binders pp_silent main

| _ -> assert false

and pp_lit ppf lit xs =
match lit, xs with
| Sy.L_eq, _ :: _ ->
Fmt.pf ppf "@[<hv 2>(%a)@]"
Fmt.(list ~sep:(fun ppf () -> Fmt.pf ppf " =@, ") pp) xs
Fmt.pf ppf "@[<hv 2>(%a)@]" Fmt.(list ~sep:(any " =@, ") pp) xs

| Sy.L_neg_eq, [a; b] ->
Fmt.pf ppf "(%a <> %a)" pp a pp b
Expand Down Expand Up @@ -570,8 +572,6 @@ module AEPrinter = struct
| Sy.L_neg_built (Sy.IsConstr _)), _ ->
assert false

and pp_operator = Sy.pp_operator ~format:`Ae

and pp_silent ppf t =
let { f ; xs ; ty; bind; _ } = t in
match f, xs with
Expand All @@ -582,7 +582,7 @@ module AEPrinter = struct
| Sy.Let, [] ->
let x = match bind with B_let x -> x | _ -> assert false in
Fmt.pf ppf
"(let%a %a =@ %a in@ %a)"
"@[<hv 2>(let%a %a =@ %a in@ %a@])"
(fun ppf x -> if Options.get_verbose () then
Fmt.pf ppf
" [sko = %a]" pp x.let_sko) x
Expand Down Expand Up @@ -615,23 +615,23 @@ module AEPrinter = struct
) true lbs xs);
Fmt.pf ppf "}";
| _ ->
(* Exclude by the typechecker. *)
(* Excluded by the typechecker. *)
assert false
end

| Sy.(Op ((Pow | Integer_round | Max_real | Min_real | Max_int
| Min_int) as op)), [e1; e2] ->
Fmt.pf ppf "%a(%a, %a)" pp_operator op pp e1 pp e2
Fmt.pf ppf "%a(%a, %a)" Symbols.pp_ae_operator op pp e1 pp e2

| Sy.(Op (Constr _ as op)), _::_ ->
Fmt.pf ppf "%a(%a)" pp_operator op Fmt.(list ~sep:comma pp) xs
Fmt.pf ppf "%a(%a)" Symbols.pp_ae_operator op Fmt.(list ~sep:comma pp) xs

| Sy.(Op Destruct (hs, grded)), [e] ->
Fmt.pf ppf "%a#%s%a"
pp e (if grded then "" else "!") Hstring.print hs

| Sy.Op op, [e1; e2] ->
Fmt.pf ppf "(%a %a %a)" pp e1 pp_operator op pp e2
Fmt.pf ppf "(%a %a %a)" pp e1 Symbols.pp_ae_operator op pp e2

| Sy.In (lb, rb), [t] ->
Fmt.pf ppf "(%a in %a, %a)" pp t Sy.print_bound lb Sy.print_bound rb
Expand All @@ -643,10 +643,10 @@ module AEPrinter = struct
Fmt.pf ppf "%a(%a)" Sy.print f Fmt.(list ~sep:comma pp) xs

and pp_trigger ppf { content; _ } =
Fmt.list ~sep:Fmt.comma pp ppf content
Fmt.pf ppf "@[%a@]" Fmt.(list ~sep:comma pp) content

and pp_triggers ppf trs =
Fmt.list ~sep:(fun ppf () -> Fmt.pf ppf "|@,") pp_trigger ppf trs
Fmt.pf ppf "@[ %a@]" Fmt.(list ~sep:(any "@,| ") pp_trigger) trs

and print_verbose ppf t =
Fmt.pf ppf "(%a : %a)" pp_silent t Ty.print t.ty
Expand All @@ -669,9 +669,9 @@ let print_triggers ppf =

let print_list_sep sep =
if Options.get_output_smtlib () then
Fmt.list ~sep:(fun ppf () -> Fmt.pf ppf "%s" sep) SmtPrinter.pp
Fmt.list ~sep:Fmt.(const string sep) SmtPrinter.pp
else
Fmt.list ~sep:(fun ppf () -> Fmt.pf ppf "%s" sep) AEPrinter.pp
Fmt.list ~sep:Fmt.(const string sep) AEPrinter.pp

let print_list ppf = print_list_sep "," ppf

Expand Down
15 changes: 6 additions & 9 deletions src/lib/structures/symbols.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -436,11 +436,10 @@ module SmtPrinter = struct
| Abs_int | Abs_real -> Fmt.pf ppf "abs"
| Real_of_int -> Fmt.pf ppf "to_real"
| Real_is_int -> Fmt.pf ppf "is_int"
| Integer_round -> Fmt.pf ppf "to_int"
| Int_floor -> Fmt.pf ppf "to_int"

(* FixedSizedBitVectors theory *)
| Extract (i, j) ->
Fmt.pf ppf "(_ extract %d %d)" i j
| Extract (i, j) -> Fmt.pf ppf "(_ extract %d %d)" j i
| Concat -> Fmt.pf ppf "concat"
| BV2Nat -> Fmt.pf ppf "bv2nat"
| BVnot -> Fmt.pf ppf "bvnot"
Expand All @@ -459,20 +458,20 @@ module SmtPrinter = struct
| Float -> Fmt.pf ppf "ae.round"

(* Not in the SMT-LIB standard *)
| Int2BV _ -> Fmt.pf ppf "(_ int2bv)"
| Int2BV n -> Fmt.pf ppf "(_ int2bv %d)" n
| Not_theory_constant -> Fmt.pf ppf "ae.not_theory_constant"
| Is_theory_constant -> Fmt.pf ppf "ae.is_theory_constant"
| Linear_dependency -> Fmt.pf ppf "ae.linear_dependency"
| Sqrt_real -> Fmt.pf ppf "ae.sqrt_real"
| Sqrt_real_default -> Fmt.pf ppf "ae.sqrt_real_default"
| Sqrt_real_excess -> Fmt.pf ppf "ae.sqrt_real_excess"
| Int_floor -> Fmt.pf ppf "ae.int_floor"
| Int_ceil -> Fmt.pf ppf "ae.int_ceil"
| Max_real -> Fmt.pf ppf "ae.max_real"
| Max_int -> Fmt.pf ppf "ae.max_int"
| Min_real -> Fmt.pf ppf "ae.min_real"
| Min_int -> Fmt.pf ppf "ae.min_int"
| Integer_log2 -> Fmt.pf ppf "ae.integer_log2"
| Integer_round -> Fmt.pf ppf "ae.integer_round"
| Pow -> Fmt.pf ppf "ae.pow"

| Optimize _ ->
Expand All @@ -485,10 +484,8 @@ module SmtPrinter = struct

end

let[@inline always] pp_operator ~(format:[`Ae | `Smtlib]) ppf op =
match format with
| `Ae -> AEPrinter.pp_operator ppf op
| `Smtlib -> SmtPrinter.pp_operator ppf op
let pp_ae_operator = AEPrinter.pp_operator
let pp_smtlib_operator = SmtPrinter.pp_operator

let print_clean = AEPrinter.pp ~show_vars:false
let print = AEPrinter.pp ~show_vars:true
Expand Down
9 changes: 7 additions & 2 deletions src/lib/structures/symbols.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -130,8 +130,13 @@ val print_clean : t Fmt.t

val pp_name : string Fmt.t

val pp_operator : format:[`Ae | `Smtlib] -> operator Fmt.t
(* [pp_smtlib ppf sy] prints the symbol [sy] on the formatter [ppf]. *)
val pp_ae_operator : operator Fmt.t
(* [pp_ae_operator ppf op] prints the operator symbol [op] on the
formatter [ppf] using the Alt-Ergo native format. *)

val pp_smtlib_operator : operator Fmt.t
(* [pp_smtlib_operator ppf op] prints the operator symbol [op] on the
formatter [ppf] using the SMT-LIB format. *)

(*val dummy : t*)

Expand Down

0 comments on commit 285b2d4

Please sign in to comment.