Add a SMT-LIB compliant printer for `Expr` #952

Halbaroth · 2023-11-20T11:02:12Z

We plan to use expression from Expr to store model values but we haven't appropriate printer for Symbols in the SMT-LIB format. This commit add an new printer pp_smtlib into Symbols which prints (as much as possible) symbols using the SMT-LIB standard.

This new printer should be sufficient for printing models as model values couldn't be nonconstant values or even applications of function. Still the printer pp_smtlib tries to be as complete as possible and outputs a correct answer for symbols of functions or literals.

I also clean up a bit the AE format printer.

bclement-ocp

There are extraneous indexing in some identifiers that should be removed.

I think in practice we only need to be able to print constant symbols and names (the rest needs to be matched at the expression level to print the correct structure), is that correct?

bclement-ocp · 2023-11-20T11:46:26Z

src/lib/structures/symbols.ml

+    | Op (Int2BV _) -> Fmt.pf ppf "(_ int2bv)"
+    | Op Not_theory_constant -> Fmt.pf ppf "(_ not_theory_constant)"
+    | Op Is_theory_constant -> Fmt.pf ppf "(_ is_theory_constant)"
+    | Op Linear_dependency -> Fmt.pf ppf "(_ linear_dependency)"
+    | Op Sqrt_real -> Fmt.pf ppf "(_ sqrt_real)"
+    | Op Sqrt_real_default -> Fmt.pf ppf "(_ sqrt_real_default)"
+    | Op Sqrt_real_excess -> Fmt.pf ppf "(_ sqrt_real_excess)"
+    | Op Int_floor -> Fmt.pf ppf "(_ int_floor)"
+    | Op Int_ceil -> Fmt.pf ppf "(_ int_ceil)"
+    | Op Max_real -> Fmt.pf ppf "(_ max_real)"
+    | Op Max_int -> Fmt.pf ppf "(_ max_int)"
+    | Op Min_real -> Fmt.pf ppf "(_ min_real)"
+    | Op Min_int -> Fmt.pf ppf "(_ min_int)"
+    | Op Integer_log2 -> Fmt.pf ppf "(_ integer_log2)"
+    | Op Pow -> Fmt.pf ppf "(_ pow)"
+    | Op Integer_round -> Fmt.pf ppf "(_ integer_round)"


These should not be indexed (there should be no _).

Well except for Int2BV which should be (_ int2bv n) for Int2BV n.

Besides, I remember @Stevendeo used a different name for one them, something as ae.round. We should be consistent with that right? We may prefix all of them with ae.

Integer_round is not ae.round. Integer_round does not exist in the SMT-LIB format. ae.round is Float.

Ah but yes for custom primitives we should prefix with ae that is a good idea! BTW, Int_floor is to_int from the Reals_Ints theory.

bclement-ocp · 2023-11-20T11:47:56Z

src/lib/structures/symbols.ml

+    | L_neg_built LT -> Fmt.pf ppf ">="
+    | L_neg_pred -> Fmt.pf ppf "not"
+    | L_built (IsConstr hs) -> Fmt.pf ppf "(_ is %a)" Hstring.print hs
+    | L_neg_built (IsConstr hs) -> Fmt.pf ppf "(not (_ is %a))" Hstring.print hs


This is not a valid smt-lib symbol?

The one on the line that I commented on :) (not (_ is %a))

Halbaroth · 2023-11-21T09:12:51Z

I completely change the commit:
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 formulas 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 has only two limitations:

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.
it doesn't print the detail of the semantic trigger In.

Notice that multi-triggers 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.

bclement-ocp

Mostly reasonable, but there are some small issues that should be fixed.

I completely change the commit:

Ideally, when this is the case, the PR should be closed and a new PR opened instead :)

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.

As I already mentioned on Zulip, this is ! with :pattern. See page 32 of the standard.

Notice that multi-triggers are now printed as DNF formulae.

This seems weird; triggers are not booleans. I'd suggest using the standard :pattern syntax.

(As an aside: commit messages should be written using imperative style — "Add a SMT-LIB compliant printer for Expr" rather than "Adding a SMT-LIB compliant printer for Expr" etc. — and generally describe things from a point of view of the change set, i.e. "Use Fmt everywhere" rather than "I use Fmt everywhere". This helps focus the attention on the changes rather than the author.)

bclement-ocp · 2023-11-21T09:27:54Z

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


Ideally, there would be a GitHub issue referenced here.

Sure, actually it will be fix by the new representation of model values because we will use Expr.t here instead of string.

It's done #958.

The comment should mention a link to #958 — the point of having an issue is so that we can track what we have to do, and the point of having the link in the comment is so that we know which issue to update if the problem ends up fixed by an unrelated refactor.

bclement-ocp · 2023-11-21T09:51:51Z

src/lib/structures/expr.ml

-    | 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


Suggested change

Fmt.pf ppf "(%a %a)" pp_operator op Fmt.(list ~sep:sp pp) xs

Fmt.pf ppf "@[(%a@ %a@])" pp_operator op Fmt.(list ~sep:sp pp) xs

I guess you meant "@[(%a@ %a)@]" to be consistent with other printers?

Actually I meant what I wrote because I don't like closing boxes after the parentheses (it leads to more unreadable )))))))))) but that would work as well as long as we don't print everything as a unit.

bclement-ocp · 2023-11-21T09:52:01Z

src/lib/structures/expr.ml

-      fprintf fmt
-        "%a(%a)" Hstring.print hs (Util.print_list ~sep:"," ~pp:print) l
+    | Sy.Name (n, _, _), _ :: _ ->
+      Fmt.pf ppf "(%a %a)"


Suggested change

Fmt.pf ppf "(%a %a)"

Fmt.pf ppf "@[(%a@ %a)@]"

bclement-ocp · 2023-11-21T09:56:03Z

src/lib/structures/expr.ml

-        Format.fprintf fmt "| %a@,"  (Util.print_list ~sep:"," ~pp:print) l;
-      ) trs
+  and pp_trigger ppf { content; _ } =
+    Fmt.pf ppf "@[<hv 2>(and %a)@]" Fmt.(list ~sep:sp pp) content


Suggested change

Fmt.pf ppf "@[<hv 2>(and %a)@]" Fmt.(list ~sep:sp pp) content

Fmt.pf ppf "@[<hv 2>(%a)@]" Fmt.(list ~sep:sp pp) content

bclement-ocp · 2023-11-21T09:56:39Z

src/lib/structures/expr.ml

+    Fmt.pf ppf "@[<hv 2>(and %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


Suggested change

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

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

After a quick check in the SMT-LIB references, it seems patterns of multi-triggers are separated by :pattern.

Ah yes, I messed up the structure — this should be Fmt.pf ppf "@[<hv 2>:pattern@ (%a)@]" Fmt.(list ~sep:sp pp_trigger) trs

src/lib/structures/symbols.ml

bclement-ocp · 2023-11-21T10:08:33Z

src/lib/structures/symbols.ml

+
+    (* FixedSizedBitVectors theory *)
+    | Extract (i, j) ->
+      Fmt.pf ppf "(_ extract %d %d)" i j


I believe that Alt-Ergo uses opposite conventions for extract arguments compared to SMT-LIB and that i and j must be flipped here (see for instance Expr.Core.BV.extract)

bclement-ocp · 2023-11-21T10:09:18Z

src/lib/structures/symbols.ml

+    | Float -> Fmt.pf ppf "ae.round"
+
+    (* Not in the SMT-LIB standard *)
+    | Int2BV _ -> Fmt.pf ppf "(_ int2bv)"


As I already mentioned:

Suggested change

| Int2BV _ -> Fmt.pf ppf "(_ int2bv)"

| Int2BV n -> Fmt.pf ppf "(_ int2bv %d)" n

bclement-ocp · 2023-11-21T10:09:53Z

src/lib/structures/symbols.ml

+    | 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"


As I already mentioned:

Suggested change

| Int_floor -> Fmt.pf ppf "ae.int_floor"

| Int_floor -> Fmt.pf ppf "to_int"

Uhm, so Integer_round and Int_floor are both to_int?

Integer_round is not to_int, I don't think I said that? Integer_round uses the fpa rounding mode for rounding to integers (it has type rounding_mode -> real -> int).

(If PR prints Integer_round as to_int, I missed that during review but it is wrong)

I misread, fixed.

bclement-ocp · 2023-11-21T10:11:58Z

src/lib/structures/symbols.ml

+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


I am not sure the polymorphic variants are very useful here, pp_operator ~format:`Ae and pp_operator ~format:`Smtlib are harder to type than separate names such as pp_ae_operator and pp_smt_operator which also wouldn't require additional parentheses when used with Fmt.pf.

Or really we could just expose the SmtPrinter and AEPrinter modules directly I think.

For me both solutions are equivalent.

bclement-ocp

Looks good now — please just include a backlink to #958 in the corresponding comment

bclement-ocp · 2023-11-21T14:28:48Z

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


The comment should mention a link to #958 — the point of having an issue is so that we can track what we have to do, and the point of having the link in the comment is so that we know which issue to update if the problem ends up fixed by an unrelated refactor.

bclement-ocp · 2023-11-21T14:32:57Z

src/lib/structures/expr.ml


  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


Nit: this is now Fmt.(list ~sep:sp (box pp_trigger)) trs

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 formulas 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-triggers 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`.

Add some boxes to improve the output of the printers of `Expr`.

CHANGES: ### Command-line interface - Enable FPA theory by default (OCamlPro/alt-ergo#1177) - Remove deprecated output channels (OCamlPro/alt-ergo#782) - Deprecate the --use-underscore since it produces models that are not SMT-LIB compliant (OCamlPro/alt-ergo#805) - Add --dump-models-on to dump models on a specific output channel (OCamlPro/alt-ergo#838) - Use consistent return codes (OCamlPro/alt-ergo#842) - Add --continue-on-error flag to set the SMT-LIB error behavior (OCamlPro/alt-ergo#853) - Make dolmen the default value for the --frontend option (OCamlPro/alt-ergo#857) - Restore functionality to broken `--profiling` option (OCamlPro/alt-ergo#947) - Add bare-bones support for interactive input in SMT-LIB format (OCamlPro/alt-ergo#949) - Less confusing behavior on timeout (OCamlPro/alt-ergo#982, OCamlPro/alt-ergo#984) - Add `--strict` option for SMT-LIB compliant mode (OCamlPro/alt-ergo#916, OCamlPro/alt-ergo#1133) - Deprecate `sum`, `typing` and `warnings` debug flags (OCamlPro/alt-ergo#1204) ### SMT-LIB support - Add support for the many new SMT-LIB commands (OCamlPro/alt-ergo#837, OCamlPro/alt-ergo#848, OCamlPro/alt-ergo#852, OCamlPro/alt-ergo#863, OCamlPro/alt-ergo#911, OCamlPro/alt-ergo#942, OCamlPro/alt-ergo#945, OCamlPro/alt-ergo#961, OCamlPro/alt-ergo#975, OCamlPro/alt-ergo#1069) - Expose the FPA rounding builtin in the SMT-LIB format (OCamlPro/alt-ergo#876, OCamlPro/alt-ergo#1135) - Allow changing the SAT solver using (set-option) (OCamlPro/alt-ergo#880) - Add support for the `:named` attribute (OCamlPro/alt-ergo#957) - Add support for quoted identifiers (OCamlPro/alt-ergo#909, OCamlPro/alt-ergo#972) - Add support for naming lemmas in SMT-LIB syntax (OCamlPro/alt-ergo#1141, OCamlPro/alt-ergo#1143) ### Model generation - Use post-solve SAT environment in model generation, fixing issues where incorrect models were generated (OCamlPro/alt-ergo#789) - Restore support for records in models (OCamlPro/alt-ergo#793) - Use abstract values instead of dummy values in models where the actual value does not matter (OCamlPro/alt-ergo#804, OCamlPro/alt-ergo#835) - Use fresh names for all abstract values to prevent accidental captures (OCamlPro/alt-ergo#811) - Add support for model generation with the default CDCL solver (OCamlPro/alt-ergo#829) - Support model generation for the BV theory (OCamlPro/alt-ergo#841, OCamlPro/alt-ergo#968) - Add support for optimization (MaxSMT / OptiSMT) with lexicographic Int and Real objectives (OCamlPro/alt-ergo#861, OCamlPro/alt-ergo#921) - Add a SMT-LIB printer for expressions (OCamlPro/alt-ergo#952, OCamlPro/alt-ergo#981, OCamlPro/alt-ergo#1082, OCamlPro/alt-ergo#931, OCamlPro/alt-ergo#932) - Ensure models have a value for all constants in the problem (OCamlPro/alt-ergo#1019) - Fix a rare soundness issue with integer constraints when model generation is enabled (OCamlPro/alt-ergo#1025) - Support model generation for the ADT theory (OCamlPro/alt-ergo#1093, OCamlPro/alt-ergo#1153) ### Theory reasoning - Add word-level propagators for the BV theory (OCamlPro/alt-ergo#944, OCamlPro/alt-ergo#1004, OCamlPro/alt-ergo#1007, OCamlPro/alt-ergo#1010, OCamlPro/alt-ergo#1011, OCamlPro/alt-ergo#1012, OCamlPro/alt-ergo#1040, OCamlPro/alt-ergo#1044, OCamlPro/alt-ergo#1054, OCamlPro/alt-ergo#1055, OCamlPro/alt-ergo#1056, OCamlPro/alt-ergo#1057, OCamlPro/alt-ergo#1065, OCamlPro/alt-ergo#1073, OCamlPro/alt-ergo#1144, OCamlPro/alt-ergo#1152) - Add interval domains and arithmetic propagators for the BV theory (OCamlPro/alt-ergo#1058, OCamlPro/alt-ergo#1083, OCamlPro/alt-ergo#1084, OCamlPro/alt-ergo#1085) - Native support for bv2nat of bit-vector normal forms (OCamlPro/alt-ergo#1154) - Fix incompleteness issues in the BV solver (OCamlPro/alt-ergo#978, OCamlPro/alt-ergo#979) - Abstract more arguments of AC symbols to avoid infinite loops when they contain other AC symbols (OCamlPro/alt-ergo#990) - Do not make irrelevant decisions in CDCL solver, improving performance slightly (OCamlPro/alt-ergo#1041) - Rewrite the ADT theory to use domains and integrate the enum theory into the ADT theory (OCamlPro/alt-ergo#1078, OCamlPro/alt-ergo#1086, OCamlPro/alt-ergo#1087, OCamlPro/alt-ergo#1091, OCamlPro/alt-ergo#1094, OCamlPro/alt-ergo#1138) - Rewrite the Intervals module entirely (OCamlPro/alt-ergo#1108) - Add maximize/minimize terms for matching (OCamlPro/alt-ergo#1166) - Internalize `sign_extend` and `repeat` (OCamlPro/alt-ergo#1192) - Run cross-propagators to completion (OCamlPro/alt-ergo#1221) - Support binary distinct on arbitrary bit-widths (OCamlPro/alt-ergo#1222) - Only perform optimization when building a model (OCamlPro/alt-ergo#1224) - Make sure domains do not overflow the default domain (OCamlPro/alt-ergo#1225) - Do not build unnormalized values in `zero_extend` (OCamlPro/alt-ergo#1226) ### Internal/library changes - Rewrite the Vec module (OCamlPro/alt-ergo#607) - Move printer definitions closer to type definitions (OCamlPro/alt-ergo#808) - Mark proxy names as reserved (OCamlPro/alt-ergo#836) - Use a Zarith-based representation for numbers and bit-vectors (OCamlPro/alt-ergo#850, OCamlPro/alt-ergo#943) - Add native support for (bvnot) in the BV solver (OCamlPro/alt-ergo#856) - Add constant propagators for partially interpreted functions (OCamlPro/alt-ergo#869) - Remove `Util.failwith` in favor of `Fmt.failwith` (OCamlPro/alt-ergo#872) - Add more `Expr` smart constructors (OCamlPro/alt-ergo#877, OCamlPro/alt-ergo#878) - Do not use existential variables for integer division (OCamlPro/alt-ergo#881) - Preserve `Subst` literals to prevent accidental incompleteness (OCamlPro/alt-ergo#886) - Properly start timers (OCamlPro/alt-ergo#924) - Compute a concrete representation of a model instead of performing (OCamlPro/alt-ergo#925) - Allow direct access to the SAT API in the Alt-Ergo library computations during printing (OCamlPro/alt-ergo#927) - Better handling for step limit (OCamlPro/alt-ergo#936) - Add a generic option manager to deal with the dolmen state (OCamlPro/alt-ergo#951) - Expose an imperative SAT API in the Alt-Ergo library (OCamlPro/alt-ergo#962) - Keep track of the SMT-LIB mode (OCamlPro/alt-ergo#971) - Add ability to decide on semantic literals (OCamlPro/alt-ergo#1027, OCamlPro/alt-ergo#1118) - Preserve trigger order when parsing quantifiers with multiple trigger (OCamlPro/alt-ergo#1046). - Store domains inside the union-find module (OCamlPro/alt-ergo#1119) - Remove some polymorphic hashtables (OCamlPro/alt-ergo#1219) ### Build and integration - Drop support for OCaml <4.08.1 (OCamlPro/alt-ergo#803) - Use dune-site for the inequalities plugins. External pluginsm ust now be registered through the dune-site plugin mechanism in the `(alt-ergo plugins)` site to be picked up by Alt-Ergo (OCamlPro/alt-ergo#1049). - Add a release workflow (OCamlPro/alt-ergo#827) - Add a Windows workflow (OCamlPro/alt-ergo#1203) - Mark the dune.inc file as linguist-generated to avoid huge diffs (OCamlPro/alt-ergo#830) - Use GitHub Actions badges in the README (OCamlPro/alt-ergo#882) - Use `dune build @check` to build the project (OCamlPro/alt-ergo#887) - Enable warnings as errors on the CI (OCamlPro/alt-ergo#888) - Uniformization of internal identifiers generation (OCamlPro/alt-ergo#905, OCamlPro/alt-ergo#918) - Use an efficient `String.starts_with` implementation (OCamlPro/alt-ergo#912) - Fix the Makefile (OCamlPro/alt-ergo#914) - Add `Logs` dependency (OCamlPro/alt-ergo#1206) - Use `dynamic_include` to include the generated file `dune.inc` (OCamlPro/alt-ergo#1199) - Support Windows (OCamlPro/alt-ergo#1184,OCamlPro/alt-ergo#1189,OCamlPro/alt-ergo#1195,OCamlPro/alt-ergo#1199,OCamlPro/alt-ergo#1200) - Wrap the library `Alt_ergo_prelude` (OCamlPro/alt-ergo#1223) ### Testing - Use --enable-assertions in tests (OCamlPro/alt-ergo#809) - Add a test for push/pop (OCamlPro/alt-ergo#843) - Use the CDCL solver when testing model generation (OCamlPro/alt-ergo#938) - Do not test .smt2 files with the legacy frontend (OCamlPro/alt-ergo#939) - Restore automatic creation of .expected files (OCamlPro/alt-ergo#941) ### Documentation - Add a new example for model generation (OCamlPro/alt-ergo#826) - Add a Pygments lexer for the Alt-Ergo native language (OCamlPro/alt-ergo#862) - Update the current authors (OCamlPro/alt-ergo#865) - Documentation of the `Enum` theory (OCamlPro/alt-ergo#871) - Document `Th_util.lit_origin` (OCamlPro/alt-ergo#915) - Document the CDCL-Tableaux solver (OCamlPro/alt-ergo#995) - Document Windows support (OCamlPro/alt-ergo#1216) - Remove instructions to install Alt-Ergo on Debian (OCamlPro/alt-ergo#1217) - Document optimization feature (OCamlPro/alt-ergo#1231)

Halbaroth added the models This issue is related to model generation. label Nov 20, 2023

bclement-ocp requested changes Nov 20, 2023

View reviewed changes

Halbaroth force-pushed the symbol-smtlib-printer branch 2 times, most recently from 554dd10 to 09081e4 Compare November 21, 2023 09:00

Halbaroth requested a review from bclement-ocp November 21, 2023 09:11

Halbaroth changed the title ~~Adding a SMT-LIB compliant printer for Symbols~~ Adding a SMT-LIB compliant printer for Expr Nov 21, 2023

Halbaroth force-pushed the symbol-smtlib-printer branch from 09081e4 to 6b69c87 Compare November 21, 2023 09:15

bclement-ocp requested changes Nov 21, 2023

View reviewed changes

Halbaroth changed the title ~~Adding a SMT-LIB compliant printer for Expr~~ Add a SMT-LIB compliant printer for Expr Nov 21, 2023

Halbaroth mentioned this pull request Nov 21, 2023

Proprer fix for check_records #958

Closed

Halbaroth requested a review from bclement-ocp November 21, 2023 14:12

bclement-ocp requested changes Nov 21, 2023

View reviewed changes

Halbaroth force-pushed the symbol-smtlib-printer branch from 84ddff8 to e3cf52c Compare November 22, 2023 08:06

Halbaroth added 3 commits November 22, 2023 09:06

Review changes

7531455

Add some boxes to improve the output of the printers of `Expr`.

Add a link to issue 958

e3cf52c

bclement-ocp approved these changes Nov 22, 2023

View reviewed changes

Halbaroth merged commit ea7b486 into OCamlPro:next Nov 22, 2023
14 checks passed

bclement-ocp mentioned this pull request Sep 24, 2024

[new release] alt-ergo (4 packages) (2.6.0) ocaml/opam-repository#26609

Merged

	Fmt.pf ppf "(%a %a)" pp_operator op Fmt.(list ~sep:sp pp) xs
	Fmt.pf ppf "@[(%a@ %a@])" pp_operator op Fmt.(list ~sep:sp pp) xs

	Fmt.pf ppf "@[<hv 2>(and %a)@]" Fmt.(list ~sep:sp pp) content
	Fmt.pf ppf "@[<hv 2>(%a)@]" Fmt.(list ~sep:sp pp) content

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

	\| Int2BV _ -> Fmt.pf ppf "(_ int2bv)"
	\| Int2BV n -> Fmt.pf ppf "(_ int2bv %d)" n

	\| Int_floor -> Fmt.pf ppf "ae.int_floor"
	\| Int_floor -> Fmt.pf ppf "to_int"

Add a SMT-LIB compliant printer for Expr #952

Add a SMT-LIB compliant printer for Expr #952

Conversation

Halbaroth commented Nov 20, 2023

bclement-ocp left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Halbaroth Nov 20, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Halbaroth commented Nov 21, 2023 • edited Loading

bclement-ocp left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Halbaroth Nov 21, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bclement-ocp left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Add a SMT-LIB compliant printer for `Expr` #952

Add a SMT-LIB compliant printer for `Expr` #952

Halbaroth Nov 20, 2023 •

edited

Loading

Halbaroth commented Nov 21, 2023 •

edited

Loading

Halbaroth Nov 21, 2023 •

edited

Loading