From 09081e4b984206fa346ca0c5a89c183cc6a2849e Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 20 Nov 2023 11:57:03 +0100 Subject: [PATCH] Adding a SMT-LIB compliant printer for `Expr` We plan to use expression from `Expr` to store model values but we haven't appropriate printer for it in the SMT-LIB format. Indeed, the current SMT-LIB printer of `Expr` is wrong, both on formula and simple symbols as rational numbers or bitvector literals. This commit changes the SMT-LIB printer of `Expr` in order to always print SMT-LIB format. The new SMT-LIB printer have only two limitations: 1. it doesn't print the triggers of lemmas when the verbose flag is up because there is no appropriate syntax in the SMT-LIB standard. 2. it doesn't print the detail of the semantic trigger `In`. Notice that multi-trigger are now printed as DNF formulae. After discussion, we decide to keep the actual printer of `Symbols` as we need it for debugging messages. Instead I split it in several printers in module's implementation and I expose a new printer `pp_operator` for sake of code factorisation. Notice that printing names and literal constants should be sufficient to output models but for sake of completeness, this commit refactors completely the SMT-LIB printer of `Expr`. I also clean up the code of both `Symbols` and `Expr` printers in the following way: - I use everywhere `Fmt` and in particular `Fmt.list` and `Fmt.iter`. - I rename some functions but I keep the previous API. I just add a new function `pp_operator` to the signature of `Symbols`. - I remove some useless test with `Options.get_output_smtlib`. --- src/lib/frontend/models.ml | 11 +- src/lib/structures/expr.ml | 455 ++++++++++++++++----------------- src/lib/structures/symbols.ml | 300 +++++++++++++++------- src/lib/structures/symbols.mli | 10 +- 4 files changed, 439 insertions(+), 337 deletions(-) diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml index ffe5cb104f..d15884e697 100644 --- a/src/lib/frontend/models.ml +++ b/src/lib/frontend/models.ml @@ -312,10 +312,19 @@ module SmtlibCounterExample = struct | [Ty.Trecord _r, _arg] -> begin match xs_values with | [record_name,_] -> + (* HOTFIX: this fix is temporary. The current implementation of + model generation for records relies on string representants, + which means the printer for access symbols has to agree with + the name of the field in the type trecord. As the printer + [Symbols.print] will always output AE native format, this + doesn't agree when the output format is SMT-LIB. But the + printer of expression will output the right string if we don't + give the arguments of the field. *) + let access = Fmt.str "%a" Expr.print (Expr.mk_term f [] ty) in add_records_destr records (asprintf "%a" Expr.print record_name) - (Sy.to_string f) + access rep | [] | _ -> records end diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 74cecdd1ca..cdf6deecea 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -311,393 +311,374 @@ module F_Htbl : Hashtbl.S with type key = t = (** pretty printing *) -let print_binders = - let print_one fmt (sy, (ty, _)) = - Format.fprintf fmt "%a:%a" Sy.print sy Ty.print ty - in fun fmt b -> - match SMap.bindings b with - | [] -> - (* can happen when quantifying only on type variables *) - Format.fprintf fmt "(no term variables)" - | e::l -> - print_one fmt e; - List.iter (fun e -> Format.fprintf fmt ", %a" print_one e) l - -(* let print_list_sep sep pp fmt = - * Format.pp_print_list ~pp_sep:(fun fmt _ -> Format.fprintf fmt sep) pp fmt - * - * let print_list pp fmt = print_list_sep "," pp fmt *) - module SmtPrinter = struct + let pp_binder ppf (var, (ty, _)) = + let var = + match var with + | Sy.Var v -> v + | _ -> assert false + in + Fmt.pf ppf "(%a %a)" Var.print var Ty.pp_smtlib ty - let rec print_formula fmt form xs bind = - let open Format in + let pp_binders = Fmt.(iter_bindings ~sep:sp SMap.iter pp_binder) + + let rec pp_formula ppf form xs bind = match form, xs, bind with | Sy.F_Unit _, [f1; f2], _ -> - Format.fprintf fmt "@[(and %a %a)@]" print_silent f1 print_silent f2 + Fmt.pf ppf "@[(and %a %a)@]" pp_silent f1 pp_silent f2 | Sy.F_Iff, [f1; f2], _ -> - fprintf fmt "@[(= %a %a)@]" print_silent f1 print_silent f2 + Fmt.pf ppf "@[(= %a %a)@]" pp_silent f1 pp_silent f2 | Sy.F_Xor, [f1; f2], _ -> - fprintf fmt "@[(not (= %a %a))@]" print_silent f1 print_silent f2 + Fmt.pf ppf "@[(xor %a %a)@]" pp_silent f1 pp_silent f2 | Sy.F_Clause _, [f1; f2], _ -> - fprintf fmt "@[(or %a %a)@]" print_silent f1 print_silent f2 + Fmt.pf ppf "@[(or %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)" - name - print_binders binders - print_triggers user_trs - print_silent main - else - fprintf fmt "(lem %s)" name + | 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_Skolem, [], B_skolem { main; binders; _ } -> - fprintf fmt "( %a)" - print_binders binders print_silent main + | Sy.F_Skolem, [], B_skolem { main; name; binders; _ } -> + Fmt.pf ppf "(! (exists (%a) %a) :named %s)" + pp_binders binders pp_silent main name | _ -> assert false - and print_lit fmt lit xs = - let open Format in + and pp_lit ppf lit xs = match lit, xs with | Sy.L_eq, a::l -> - fprintf fmt "(= %a%a)" - print a (fun fmt -> List.iter (fprintf fmt " %a" print)) l + Fmt.pf ppf "(= %a %a)" + pp a (fun ppf -> List.iter (Fmt.pf ppf " %a" pp)) l + | Sy.L_neg_eq, [a; b] -> - fprintf fmt "(not (= %a %a))" print a print b + Fmt.pf ppf "(not (= %a %a))" pp a pp b - | Sy.L_neg_eq, a::l -> - fprintf fmt "(distinct %a%a)" - print a (fun fmt -> List.iter (fprintf fmt " %a" print)) l + | Sy.L_neg_eq, _ :: _ -> + Fmt.pf ppf "(distinct %a)" Fmt.(list ~sep:sp pp) xs | Sy.L_built Sy.LE, [a;b] -> - fprintf fmt "(<= %a %a)" print a print b + Fmt.pf ppf "(<= %a %a)" pp a pp b | Sy.L_built Sy.LT, [a;b] -> - fprintf fmt "(< %a %a)" print a print b + Fmt.pf ppf "(< %a %a)" pp a pp b | Sy.L_neg_built Sy.LE, [a; b] -> - fprintf fmt "(> %a %a)" print a print b + Fmt.pf ppf "(> %a %a)" pp a pp b | Sy.L_neg_built Sy.LT, [a; b] -> - fprintf fmt "(>= %a %a)" print a print b + Fmt.pf ppf "(>= %a %a)" pp a pp b | Sy.L_neg_pred, [a] -> - fprintf fmt "(not %a)" print a + Fmt.pf ppf "(not %a)" pp a | Sy.L_built (Sy.IsConstr hs), [e] -> - fprintf fmt "((_ is %a) %a)" Hstring.print hs print e + Fmt.pf ppf "((_ is %a) %a)" Hstring.print hs pp e | Sy.L_neg_built (Sy.IsConstr hs), [e] -> - fprintf fmt "(not ((_ is %a) %a))" Hstring.print hs print e + Fmt.pf ppf "(not ((_ 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 _)) , _ -> + | Sy.L_neg_built (Sy.IsConstr _)), _ -> assert false - and print_silent fmt t = - let open Format in + and pp_operator = Symbols.pp_operator ~format:`Smtlib + + and pp_silent ppf t = let { f ; xs ; ty; bind; _ } = t in match f, xs with - (* Formulas *) - | Sy.Form form, xs -> print_formula fmt form xs bind + | Sy.Form form, xs -> pp_formula ppf form xs bind + + | Sy.Lit lit, xs -> pp_lit ppf lit xs | Sy.Let, [] -> let x = match bind with B_let x -> x | _ -> assert false in - fprintf fmt - "(let%a %a =@ %a in@ %a)" - (fun fmt x -> if Options.get_verbose () then - fprintf fmt - " [sko = %a]" print x.let_sko) x - Sy.print x.let_v print x.let_e print_silent x.in_e + Fmt.pf ppf "(let ((%a %a)) %a)" + Symbols.print x.let_v + pp x.let_e + pp_silent x.in_e - (* Literals *) - | Sy.Lit lit, xs -> print_lit fmt lit xs + | Sy.(Op Record), _ -> + begin + match ty with + | Ty.Trecord { Ty.lbs = lbs; record_constr; _ } -> + assert (List.compare_lengths xs lbs = 0); + Fmt.pf ppf "(%a %a)" + Hstring.print record_constr + Fmt.(list ~sep:sp pp) xs - | Sy.Op Sy.Get, [e1; e2] -> - if Options.get_output_smtlib () then - fprintf fmt "(select %a %a)" print e1 print e2 - else - fprintf fmt "%a[%a]" print e1 print e2 - - | Sy.Op Sy.Set, [e1; e2; e3] -> - if Options.get_output_smtlib () then - fprintf fmt "(store %a %a %a)" - print e1 - print e2 - print e3 - else - fprintf fmt "%a[%a<-%a]" print e1 print e2 print e3 + | _ -> + (* Exclude by the typechecker. *) + assert false + end - | Sy.Op Sy.Concat, [e1; e2] -> - fprintf fmt "%a@@%a" print e1 print e2 + | Sy.Op op, [] -> Fmt.pf ppf "%a" pp_operator op - | Sy.Op Sy.Extract (i, j), [e] -> - fprintf fmt "%a^{%d,%d}" print e i j + | Sy.Op op, _ :: _ -> + Fmt.pf ppf "(%a %a)" pp_operator op Fmt.(list ~sep:sp pp) xs - | Sy.Op (Sy.Access field), [e] -> - if Options.get_output_smtlib () then - fprintf fmt "(%s %a)" (Hstring.view field) print e - else - fprintf fmt "%a.%s" print e (Hstring.view field) + | Sy.True, [] -> Fmt.pf ppf "true" - | Sy.Op (Sy.Record), _ -> - begin match ty with - | Ty.Trecord { Ty.lbs = lbs; _ } -> - assert (List.length xs = List.length lbs); - fprintf fmt "{"; - ignore (List.fold_left2 (fun first (field,_) e -> - fprintf fmt "%s%s = %a" (if first then "" else "; ") - (Hstring.view field) print e; - false - ) true lbs xs); - fprintf fmt "}"; - | _ -> assert false - end + | Sy.False, [] -> Fmt.pf ppf "false" - (* TODO: introduce PrefixOp in the future to simplify this ? *) - | Sy.Op op, [e1; e2] when op == Sy.Pow || op == Sy.Integer_round || - op == Sy.Max_real || op == Sy.Max_int || - op == Sy.Min_real || op == Sy.Min_int -> - fprintf fmt "%a(%a,%a)" Sy.print f print e1 print e2 + | Sy.Name (n, _, _), [] -> Symbols.pp_name ppf (Hstring.view n) - (* TODO: introduce PrefixOp in the future to simplify this ? *) - | Sy.Op (Sy.Constr hs), ((_::_) as l) -> - fprintf fmt - "%a(%a)" Hstring.print hs (Util.print_list ~sep:"," ~pp:print) l + | Sy.Name (n, _, _), _ :: _ -> + Fmt.pf ppf "(%a %a)" + Symbols.pp_name (Hstring.view n) + Fmt.(list ~sep:sp pp) xs - | Sy.Op _, [e1; e2] -> - fprintf fmt "(%a %a %a)" Sy.print f print e1 print e2 + | Sy.Var v, [] -> Var.print ppf v + + | Sy.Int i, [] -> + if Z.sign i = -1 then + Fmt.pf ppf "(- %a)" Z.pp_print (Z.abs i) + else + Fmt.pf ppf "%a" Z.pp_print i + + | Sy.Real q, [] -> + if Z.equal (Q.den q) Z.one then + Fmt.pf ppf "%a.0" Z.pp_print (Q.num q) + else if Q.sign q = -1 then + Fmt.pf ppf "(/ (- %a) %a)" + Z.pp_print (Z.abs (Q.num q)) + Z.pp_print (Q.den q) + else + Fmt.pf ppf "(/ %a %a)" Z.pp_print (Q.num q) Z.pp_print (Q.den q) - | Sy.Op Sy.Destruct (hs, grded), [e] -> - fprintf fmt "%a#%s%a" - print e (if grded then "" else "!") Hstring.print hs + | Sy.Bitv (n, s), [] -> + Fmt.pf ppf "#b%s" (Z.format (Fmt.str "%%0%db" n) s) + | Sy.MapsTo v, [t] -> + Fmt.pf ppf "(ae.mapsto %a %a)" Var.print v pp t - | Sy.In(lb, rb), [t] -> - fprintf fmt "(%a in %a, %a)" print t Sy.print_bound lb Sy.print_bound rb + | Sy.In (_lb, _rb), [_t] -> + (* WARNING: we don't print the content of this semantic trigger as + it requires to write a SMT-LIB compliant printer for bounds. *) + Fmt.pf ppf "ae.in" - | _, [] -> - fprintf fmt "%a" Sy.print f + | Sy.Void, [] -> + (* The void type doesn't exist in SMT-LIB standard. *) + Fmt.pf ppf "ae.void" - | _, _ -> - Format.fprintf fmt "(%a %a)" Sy.print f - (Util.print_list ~sep:"," ~pp:print) xs + | Sy.(True | False | Let | Void | Var _ | Int _ | Real _ | Bitv _ + | MapsTo _ | In _), _ -> + (* All the cases have been excluded by the parser. *) + assert false - and print_triggers fmt trs = - List.iter (fun { content = l; _ } -> - Format.fprintf fmt "| %a@," (Util.print_list ~sep:"," ~pp:print) l; - ) trs + and pp_trigger ppf { content; _ } = + Fmt.pf ppf "@[(and %a)@]" Fmt.(list ~sep:sp pp) content + + and pp_triggers ppf trs = + Fmt.pf ppf "@[(or %a)@]" Fmt.(list ~sep:sp pp_trigger) trs - and print_verbose fmt t = print_silent fmt t (* Not displaying types when int SMT format *) + and pp_verbose ppf t = pp_silent ppf t - and print fmt t = - if Options.get_debug () then print_verbose fmt t - else print_silent fmt t + and pp ppf t = + if Options.get_debug () then pp_verbose ppf t + else pp_silent ppf t end module AEPrinter = struct + let pp_binder ppf (var, (ty, _)) = + let var = + match var with + | Sy.Var v -> v + | _ -> assert false + in + Fmt.pf ppf "%a:%a" Var.print var Ty.pp_smtlib ty - (* Same as SmtPrinter.print_formula *) - let rec print_formula fmt form xs bind = + let pp_binders ppf binders = + if SMap.is_empty binders then + (* Can happen when quantifying only on type variables. *) + Fmt.pf ppf "(no term variables)" + else + Fmt.(iter_bindings ~sep:sp SMap.iter pp_binder) ppf binders + + let rec pp_formula fmt form xs bind = let open Format in match form, xs, bind with | Sy.F_Unit _, [f1; f2], _ -> - fprintf fmt "@[(%a /\\@ %a)@]" print_silent f1 print_silent f2 + fprintf fmt "@[(%a /\\@ %a)@]" pp_silent f1 pp_silent f2 | Sy.F_Iff, [f1; f2], _ -> - fprintf fmt "@[(%a <->@ %a)@]" print_silent f1 print_silent f2 + fprintf fmt "@[(%a <->@ %a)@]" pp_silent f1 pp_silent f2 | Sy.F_Xor, [f1; f2], _ -> - fprintf fmt "@[(%a xor@ %a)@]" print_silent f1 print_silent f2 + fprintf fmt "@[(%a xor@ %a)@]" pp_silent f1 pp_silent f2 | Sy.F_Clause _, [f1; f2], _ -> - fprintf fmt "@[(%a \\/@ %a)@]" print_silent f1 print_silent f2 + fprintf fmt "@[(%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)" name - print_binders binders - print_triggers user_trs - print_silent main + pp_binders binders + pp_triggers user_trs + pp_silent main else fprintf fmt "(lem %s)" name | Sy.F_Skolem, [], B_skolem { main; binders; _ } -> fprintf fmt "( %a)" - print_binders binders print_silent main + pp_binders binders pp_silent main | _ -> assert false - and print_lit fmt lit xs = - let open Format in + and pp_lit ppf lit xs = match lit, xs with - | Sy.L_eq, a::l -> - fprintf fmt "(%a%a)" - print a (fun fmt -> List.iter (fprintf fmt " = %a" print)) l + | Sy.L_eq, _ :: _ -> + Fmt.pf ppf "@[(%a)@]" + Fmt.(list ~sep:(fun ppf () -> Fmt.pf ppf " =@, ") pp) xs | Sy.L_neg_eq, [a; b] -> - fprintf fmt "(%a <> %a)" print a print b + Fmt.pf ppf "(%a <> %a)" pp a pp b - | Sy.L_neg_eq, a::l -> - fprintf fmt "distinct(%a%a)" - print a (fun fmt -> List.iter (fprintf fmt ", %a" print)) l + | Sy.L_neg_eq, _ :: _ -> + Fmt.pf ppf "@[distinct(%a)@]" Fmt.(list ~sep:comma pp) xs | Sy.L_built Sy.LE, [a;b] -> - fprintf fmt "(%a <= %a)" print a print b + Fmt.pf ppf "(%a <= %a)" pp a pp b | Sy.L_built Sy.LT, [a;b] -> - fprintf fmt "(%a < %a)" print a print b + Fmt.pf ppf "(%a < %a)" pp a pp b | Sy.L_neg_built Sy.LE, [a; b] -> - fprintf fmt "(%a > %a)" print a print b + Fmt.pf ppf "(%a > %a)" pp a pp b | Sy.L_neg_built Sy.LT, [a; b] -> - fprintf fmt "(%a >= %a)" print a print b + Fmt.pf ppf "(%a >= %a)" pp a pp b | Sy.L_neg_pred, [a] -> - fprintf fmt "(not %a)" print a + Fmt.pf ppf "(not %a)" pp a | Sy.L_built (Sy.IsConstr hs), [e] -> - fprintf fmt "(%a ? %a)" print e Hstring.print hs + Fmt.pf ppf "(%a ? %a)" pp e Hstring.print hs | Sy.L_neg_built (Sy.IsConstr hs), [e] -> - fprintf fmt "not (%a ? %a)" print e Hstring.print hs + Fmt.pf ppf "not (%a ? %a)" pp e Hstring.print hs | (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 _)) , _ -> + | Sy.L_neg_built (Sy.IsConstr _)), _ -> assert false - and print_silent fmt t = - let open Format in + and pp_operator = Sy.pp_operator ~format:`Ae + + and pp_silent ppf t = let { f ; xs ; ty; bind; _ } = t in match f, xs with - (* Formulas *) - | Sy.Form form, xs -> print_formula fmt form xs bind + | Sy.Form form, xs -> pp_formula ppf form xs bind + + | Sy.Lit lit, xs -> pp_lit ppf lit xs | Sy.Let, [] -> let x = match bind with B_let x -> x | _ -> assert false in - fprintf fmt + Fmt.pf ppf "(let%a %a =@ %a in@ %a)" - (fun fmt x -> if Options.get_verbose () then - fprintf fmt - " [sko = %a]" print x.let_sko) x - Sy.print x.let_v print x.let_e print_silent x.in_e + (fun ppf x -> if Options.get_verbose () then + Fmt.pf ppf + " [sko = %a]" pp x.let_sko) x + Symbols.print x.let_v pp x.let_e pp_silent x.in_e - (* Literals *) - | Sy.Lit lit, xs -> print_lit fmt lit xs + | Sy.(Op Get), [e1; e2] -> + Fmt.pf ppf "%a[%a]" pp e1 pp e2 - | Sy.Op Sy.Get, [e1; e2] -> - if Options.get_output_smtlib () then - fprintf fmt "(select %a %a)" print e1 print e2 - else - fprintf fmt "%a[%a]" print e1 print e2 - - | Sy.Op Sy.Set, [e1; e2; e3] -> - if Options.get_output_smtlib () then - fprintf fmt "(store %a %a %a)" - print e1 - print e2 - print e3 - else - fprintf fmt "%a[%a<-%a]" print e1 print e2 print e3 + | Sy.(Op Set), [e1; e2; e3] -> + Fmt.pf ppf "%a[%a<-%a]" pp e1 pp e2 pp e3 - | Sy.Op Sy.Concat, [e1; e2] -> - fprintf fmt "%a@@%a" print e1 print e2 + | Sy.(Op Concat), [e1; e2] -> + Fmt.pf ppf "%a@@%a" pp e1 pp e2 - | Sy.Op Sy.Extract (i, j), [e] -> - fprintf fmt "%a^{%d, %d}" print e i j + | Sy.(Op Extract (i, j)), [e] -> + Fmt.pf ppf "%a^{%d, %d}" pp e i j - | Sy.Op (Sy.Access field), [e] -> - if Options.get_output_smtlib () then - fprintf fmt "(%s %a)" (Hstring.view field) print e - else - fprintf fmt "%a.%s" print e (Hstring.view field) + | Sy.(Op (Access field)), [e] -> + Fmt.pf ppf "%a.%s" pp e (Hstring.view field) - | Sy.Op (Sy.Record), _ -> + | Sy.(Op Record), _ -> begin match ty with | Ty.Trecord { Ty.lbs = lbs; _ } -> - assert (List.length xs = List.length lbs); - fprintf fmt "{"; + assert (List.compare_lengths xs lbs = 0); + Fmt.pf ppf "{"; ignore (List.fold_left2 (fun first (field,_) e -> - fprintf fmt "%s%s = %a" (if first then "" else "; ") - (Hstring.view field) print e; + Fmt.pf ppf "%s%s = %a" (if first then "" else "; ") + (Hstring.view field) pp e; false ) true lbs xs); - fprintf fmt "}"; - | _ -> assert false + Fmt.pf ppf "}"; + | _ -> + (* Exclude by the typechecker. *) + assert false end - (* TODO: introduce PrefixOp in the future to simplify this ? *) - | Sy.Op op, [e1; e2] when op == Sy.Pow || op == Sy.Integer_round || - op == Sy.Max_real || op == Sy.Max_int || - op == Sy.Min_real || op == Sy.Min_int -> - fprintf fmt "%a(%a,%a)" Sy.print f print e1 print e2 + | 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 - (* TODO: introduce PrefixOp in the future to simplify this ? *) - | Sy.Op (Sy.Constr hs), ((_::_) as l) -> - fprintf fmt "%a(%a)" - Hstring.print hs (Util.print_list ~sep:"," ~pp:print) l + | Sy.(Op (Constr _ as op)), _::_ -> + Fmt.pf ppf "%a(%a)" pp_operator op Fmt.(list ~sep:comma pp) xs - | Sy.Op _, [e1; e2] -> - if Options.get_output_smtlib () then - fprintf fmt "(%a %a %a)" Sy.print f print e1 print e2 - else - fprintf fmt "(%a %a %a)" print e1 Sy.print f print e2 - - | Sy.Op Sy.Destruct (hs, grded), [e] -> - fprintf fmt "%a#%s%a" - print e (if grded then "" else "!") Hstring.print hs + | 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 - | Sy.In(lb, rb), [t] -> - fprintf fmt "(%a in %a, %a)" print t Sy.print_bound lb Sy.print_bound rb - + | Sy.In (lb, rb), [t] -> + Fmt.pf ppf "(%a in %a, %a)" pp t Sy.print_bound lb Sy.print_bound rb | _, [] -> - fprintf fmt "%a" Sy.print f + Fmt.pf ppf "%a" Sy.print f | _, _ -> - fprintf fmt "%a(%a)" Sy.print f (Util.print_list ~sep:"," ~pp:print) xs + 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 - and print_triggers fmt trs = - List.iter (fun { content = l; _ } -> - Format.fprintf fmt "| %a@," (Util.print_list ~sep:"," ~pp:print) l; - ) trs + and pp_triggers ppf trs = + Fmt.list ~sep:(fun ppf () -> Fmt.pf ppf "|@,") pp_trigger ppf trs - and print_verbose fmt t = - Format.fprintf fmt "(%a : %a)" print_silent t Ty.print t.ty + and print_verbose ppf t = + Fmt.pf ppf "(%a : %a)" pp_silent t Ty.print t.ty - and print fmt t = + and pp fmt t = if Options.get_debug () then print_verbose fmt t - else print_silent fmt t + else pp_silent fmt t end -let print fmt = +let print ppf = if Options.get_output_smtlib () - then SmtPrinter.print fmt - else AEPrinter.print fmt + then SmtPrinter.pp ppf + else AEPrinter.pp ppf -let print_triggers fmt = +let print_triggers ppf = if Options.get_output_smtlib () - then SmtPrinter.print_triggers fmt - else AEPrinter.print_triggers fmt + then SmtPrinter.pp_triggers ppf + else AEPrinter.pp_triggers ppf -let print_list_sep sep = Util.print_list ~sep ~pp:print +let print_list_sep sep = + if Options.get_output_smtlib () then + Fmt.list ~sep:(fun ppf () -> Fmt.pf ppf "%s" sep) SmtPrinter.pp + else + Fmt.list ~sep:(fun ppf () -> Fmt.pf ppf "%s" sep) AEPrinter.pp + +let print_list ppf = print_list_sep "," ppf -let print_list fmt = print_list_sep "," fmt +let pp_binders ppf = + if Options.get_output_smtlib () + then SmtPrinter.pp_binders ppf + else AEPrinter.pp_binders ppf (** different views of an expression *) @@ -1254,8 +1235,8 @@ let no_capture_issue s_t binders = Printer.print_wrn "captures between@,%aand%a!@,(captured = %a)" (SMap.print print) s_t - print_binders binders - print_binders capt_bind; + pp_binders binders + pp_binders capt_bind; false end diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index 2f443c8c54..45863cc149 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -278,28 +278,7 @@ let string_of_bound b = let print_bound fmt b = Format.fprintf fmt "%s" (string_of_bound b) -let string_of_lit lit = match lit with - | L_eq -> "=" - | L_neg_eq -> "<>" - | L_neg_pred -> "not " - | L_built LE -> "<=" - | L_built LT -> "<" - | L_neg_built LE -> ">" - | L_neg_built LT -> ">=" - | L_built (IsConstr h) -> - Format.sprintf "? %s" (Hstring.view h) - | L_neg_built (IsConstr h) -> - Format.sprintf "?not? %s" (Hstring.view h) - -let string_of_form f = match f with - | F_Unit _ -> "/\\" - | F_Clause _ -> "\\/" - | F_Lemma -> "Lemma" - | F_Skolem -> "Skolem" - | F_Iff -> "<->" - | F_Xor -> "xor" - -let name_to_string = +let pp_name ppf = let no_need_to_quote s = String.length s > 0 && (match s.[0] with | '0'..'9' -> false | _ -> true) && @@ -317,82 +296,209 @@ let name_to_string = true with Exit -> false in - fun s -> if no_need_to_quote s then s else Format.sprintf "|%s|" s - -let to_string ?(show_vars=true) x = match x with - | Name (n, _, _) -> name_to_string @@ Hstring.view n - | Var v when show_vars -> Format.sprintf "'%s'" (Var.to_string v) - | Var v -> Var.to_string v - | Int n -> Z.to_string n - | Real n -> Q.to_string n - | Bitv (n, s) -> Fmt.str "[|%s|]" (Z.format (Fmt.str "%%0%db" n) s) - | Op Plus -> "+" - | Op Minus -> "-" - | Op Mult -> "*" - | Op Div -> "/" - | Op Modulo -> "%" - | Op (Access s) -> - if Options.get_output_smtlib () then - (Hstring.view s) + fun s -> + if no_need_to_quote s then + Fmt.string ppf s else - "@Access_"^(Hstring.view s) - | Op (Constr s) -> (Hstring.view s) - | Op (Destruct (s,g)) -> - Format.sprintf "%s%s" (if g then "" else "!") (Hstring.view s) - - | Op Record -> "@Record" - | Op Get -> "get" - | Op Set -> "set" - | Op Float -> "float" - | Op Fixed -> "fixed" - | Op Abs_int -> "abs_int" - | Op Abs_real -> "abs_real" - | Op Sqrt_real -> "sqrt_real" - | Op Sqrt_real_default -> "sqrt_real_default" - | Op Sqrt_real_excess -> "sqrt_real_excess" - | Op Real_of_int -> "real_of_int" - | Op Real_is_int -> "real_is_int" - | Op Int_floor -> "int_floor" - | Op Int_ceil -> "int_ceil" - | Op Max_real -> "max_real" - | Op Max_int -> "max_int" - | Op Min_real -> "min_real" - | Op Min_int -> "min_int" - | Op Integer_log2 -> "integer_log2" - | Op Pow -> "**" - | Op Integer_round -> "integer_round" - | Op Not_theory_constant -> "not_theory_constant" - | Op Is_theory_constant -> "is_theory_constant" - | Op Linear_dependency -> "linear_dependency" - | Op Concat -> "@" - | Op Extract (i, j) -> Format.sprintf "^{%d; %d}" i j - | Op BVnot -> "bvnot" - | Op BVand -> "bvand" - | Op BVor -> "bvor" - | Op Int2BV n -> Format.sprintf "int2bv[%d]" n - | Op BV2Nat -> "bv2nat" - | Op Tite -> "ite" - | Op Reach -> assert false - | True -> "true" - | False -> "false" - | Void -> "void" - | In (lb, rb) -> - Format.sprintf "%s , %s" (string_of_bound lb) (string_of_bound rb) - - | MapsTo x -> Format.sprintf "%s |->" (Var.to_string x) - - | Lit lit -> string_of_lit lit - | Form form -> string_of_form form - | Let -> "let" - - | Op (Optimize {order; is_max=true}) -> Format.sprintf "maximize(-,%d)" order - | Op (Optimize {order; is_max=false}) -> Format.sprintf "minimize(-,%d)" order - -let to_string_clean s = to_string ~show_vars:false s -let to_string s = to_string ~show_vars:true s - -let print_clean fmt s = Format.fprintf fmt "%s" (to_string_clean s) -let print fmt s = Format.fprintf fmt "%s" (to_string s) + Fmt.pf ppf "|%s|" s + +module AEPrinter = struct + let pp_operator ppf op = + match op with + (* Core theory *) + | Tite -> Fmt.pf ppf "ite" + + (* Reals and Ints theories *) + | Plus -> Fmt.pf ppf "+" + | Minus -> Fmt.pf ppf "-" + | Mult -> Fmt.pf ppf "*" + | Div -> Fmt.pf ppf "/" + | Modulo -> Fmt.pf ppf "%%" + | Pow -> Fmt.pf ppf "**" + | Sqrt_real -> Fmt.pf ppf "sqrt_real" + | Sqrt_real_default -> Fmt.pf ppf "sqrt_real_default" + | Sqrt_real_excess -> Fmt.pf ppf "sqrt_real_excess" + | Int_floor -> Fmt.pf ppf "int_floor" + | Int_ceil -> Fmt.pf ppf "int_ceil" + | Max_real -> Fmt.pf ppf "max_real" + | Max_int -> Fmt.pf ppf "max_int" + | Min_real -> Fmt.pf ppf "min_real" + | Min_int -> Fmt.pf ppf "min_int" + | Integer_log2 -> Fmt.pf ppf "integer_log2" + | Integer_round -> Fmt.pf ppf "integer_round" + + (* Reals_Ints theory *) + | Abs_int -> Fmt.pf ppf "abs_int" + | Abs_real -> Fmt.pf ppf "abs_real" + | Real_of_int -> Fmt.pf ppf "real_of_int" + | Real_is_int -> Fmt.pf ppf "real_is_int" + + (* FixedSizedBitVectors theory *) + | Extract (i, j) -> Fmt.pf ppf "^{%d; %d}" i j + | Concat -> Fmt.pf ppf "@" + | BV2Nat -> Fmt.pf ppf "bv2nat" + | Int2BV n -> Fmt.pf ppf "int2bv[%d]" n + | BVnot -> Fmt.pf ppf "bvnot" + | BVand -> Fmt.pf ppf "bvand" + | BVor -> Fmt.pf ppf "bvor" + + (* ArraysEx theory *) + | Get -> Fmt.pf ppf "get" + | Set -> Fmt.pf ppf "set" + + (* DT theory *) + | Record -> Fmt.pf ppf "@Record" + | Access s -> Fmt.pf ppf "@Access_%a" Hstring.print s + | Constr s -> Hstring.print ppf s + | Destruct (s, g) -> + Fmt.pf ppf "%s%a" (if g then "" else "!") Hstring.print s + + (* Float theory *) + | Float -> Fmt.pf ppf "float" + | Fixed -> Fmt.pf ppf "fixed" + + | Not_theory_constant -> Fmt.pf ppf "not_theory_constant" + | Is_theory_constant -> Fmt.pf ppf "is_theory_constant" + | Linear_dependency -> Fmt.pf ppf "linear_dependency" + + | Optimize {order; is_max=true} -> + Fmt.pf ppf "maximize(-,%d)" order + | Optimize {order; is_max=false} -> + Fmt.pf ppf "minimize(-,%d)" order + | Reach -> assert false + + let pp_lit ppf lit = + match lit with + | L_eq -> Fmt.pf ppf "=" + | L_neg_eq -> Fmt.pf ppf "distinct" + | L_built LE -> Fmt.pf ppf "<=" + | L_built LT -> Fmt.pf ppf "<" + | L_neg_built LE -> Fmt.pf ppf ">" + | L_neg_built LT -> Fmt.pf ppf ">=" + | L_neg_pred -> Fmt.pf ppf "not " + | L_built (IsConstr h) -> + Fmt.pf ppf "? %a" Hstring.print h + | L_neg_built (IsConstr h) -> + Fmt.pf ppf "?not? %a" Hstring.print h + + let pp_form ppf f = + match f with + | F_Unit _ -> Fmt.pf ppf "/\\" + | F_Clause _ -> Fmt.pf ppf "\\/" + | F_Lemma -> Fmt.pf ppf "Lemma" + | F_Skolem -> Fmt.pf ppf "Skolem" + | F_Iff -> Fmt.pf ppf "<->" + | F_Xor -> Fmt.pf ppf "xor" + + let pp ?(show_vars = true) ppf sy = + match sy with + | Lit lit -> pp_lit ppf lit + | Form form -> pp_form ppf form + | Let -> Fmt.pf ppf "let" + | Op op -> pp_operator ppf op + + (* Core theory *) + | True -> Fmt.pf ppf "true" + | False -> Fmt.pf ppf "false" + | Void -> Fmt.pf ppf "void" + | Name (n, _, _) -> pp_name ppf (Hstring.view n) + | Var v when show_vars -> Fmt.pf ppf "'%s'" (Var.to_string v) + | Var v -> Fmt.string ppf (Var.to_string v) + + (* Reals and Ints theories *) + | Int i -> Z.pp_print ppf i + | Real q -> Q.pp_print ppf q + + (* FixedSizedBitVectors theory *) + | Bitv (n, s) -> + Fmt.pf ppf "[|%s|]" (Z.format (Fmt.str "%%0%db" n) s) + + (* Symbols used in semantic triggers *) + | In (lb, rb) -> + Fmt.pf ppf "%s, %s" (string_of_bound lb) (string_of_bound rb) + | MapsTo v -> Fmt.pf ppf "%a |->" Var.print v +end + +module SmtPrinter = struct + let pp_operator ppf op = + match op with + (* Core theory *) + |Tite -> Fmt.pf ppf "ite" + + (* Reals and Ints theories *) + | Plus -> Fmt.pf ppf "+" + | Minus -> Fmt.pf ppf "-" + | Mult -> Fmt.pf ppf "*" + | Div -> Fmt.pf ppf "/" + | Modulo -> Fmt.pf ppf "%%" + + (* Reals_Ints theory *) + | 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" + + (* FixedSizedBitVectors theory *) + | Extract (i, j) -> + Fmt.pf ppf "(_ extract %d %d)" i j + | Concat -> Fmt.pf ppf "concat" + | BV2Nat -> Fmt.pf ppf "bv2nat" + | BVnot -> Fmt.pf ppf "bvnot" + | BVand -> Fmt.pf ppf "bvand" + | BVor -> Fmt.pf ppf "bvor" + + (* ArraysEx theory *) + | Get -> Fmt.pf ppf "select" + | Set -> Fmt.pf ppf "store" + + (* DT theory *) + | Record -> () + | Access s | Constr s | Destruct (s, _) -> Hstring.print ppf s + + (* Float theory *) + | Float -> Fmt.pf ppf "ae.round" + + (* Not in the SMT-LIB standard *) + | Int2BV _ -> Fmt.pf ppf "(_ int2bv)" + | 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" + | Pow -> Fmt.pf ppf "ae.pow" + + | Optimize _ -> + (* TODO: this case will be removed in the PR #921. *) + assert false + + | Fixed | Reach -> + (* Unused symbols *) + assert false + +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 print_clean = AEPrinter.pp ~show_vars:false +let print = AEPrinter.pp ~show_vars:true + +let to_string_clean sy = + Fmt.str "%a" (AEPrinter.pp ~show_vars:false) sy + +let to_string sy = + Fmt.str "%a"(AEPrinter.pp ~show_vars:true) sy + module type Id = sig val fresh : ?base:string -> unit -> string diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli index 59078b83ff..a620669e5b 100644 --- a/src/lib/structures/symbols.mli +++ b/src/lib/structures/symbols.mli @@ -122,10 +122,16 @@ val compare_operators : operator -> operator -> int val hash : t -> int val to_string : t -> string -val print : Format.formatter -> t -> unit +val print : t Fmt.t +(* Printer used by debugging messages. *) val to_string_clean : t -> string -val print_clean : Format.formatter -> t -> unit +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 dummy : t*)