Support of get-info SMT2 command #837

Stevendeo · 2023-09-25T13:05:54Z

Adds support for the (get-info) command, based on https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf#page=58

src/lib/reasoners/sat_solver_sig.ml

src/lib/reasoners/satml_frontend.ml

src/lib/reasoners/fun_sat.ml

bclement-ocp

Except when an error occurs (in which case the error message should be descriptive), SMT-LIB results should generally be short atoms rather than strings, to facilitate parsing by automated tools. We can use the standard incomplete response most of the time, or be more precise when appropriate e.g. (unsupported :feature array-models) if we really want to.

As an aside: %S automatically escapes quotes and is often better for printing strings than \"%s\" or \"%a\".

bclement-ocp · 2023-09-25T13:59:29Z

src/bin/common/solving_loop.ml

+    | ":authors" ->
+      print_std Format.pp_print_string "Alt-Ergo developers"
+    | ":error-behavior" ->
+      print_std Format.pp_print_string "immediate-exit"


This must be an S-expr atom, not a string (the expected output is (:error-behavior immediate-exit), not (:error-behavior "immediate-exit")).

Actually, a string is a valid s-expression in the SMT-LIB, see p. 25 in the standard. But we have to use double-quoted string actually. So we can simply output "immediate-exit".

On further consideration, we have to print as we said.

A string is a valid s-expression, but if we want to be compatible with the standard, we must reply with either immediate-exit or continued-execution as atoms to a (get-info :error-behavior) query (see section 4.1.8).

bclement-ocp · 2023-09-25T13:59:36Z

src/bin/common/solving_loop.ml

+    | ":all-statistics"
+    | ":assertion-stack-levels" ->
+      unsupported_opt kind;
+      print_std Format.pp_print_string "-- unsupported --"
+    | _ ->
+      Printer.print_wrn "unknown option %s" kind;
+      print_std Format.pp_print_string "-- unknown option --"
+


This should just output unsupported (see section 4.2.8).

bclement-ocp · 2023-09-25T14:01:56Z

src/bin/common/solving_loop.ml

+      Printer.print_err "Invalid (get-info :reason-unknown)";
+      Format.fprintf fmt ""


The SMT-LIB way of indicating errors is to return an sexpr of the form (error "Blah") (this is required to not confuse automated tools; response to all commands must go to the same output).

src/bin/common/solving_loop.ml

bclement-ocp

There are still some formats that are not properly printed I belive. Maybe add tests to check the output format of get-info?

bclement-ocp · 2023-09-26T13:54:39Z

src/bin/common/solving_loop.ml

+let unsupported_opt s =
+  Printer.print_smtlib_err "unsupported option %S" s
+


This should be unsupported, not (error) (see e.g. 4.1.7)

Sorry, it's my mistake.

bclement-ocp · 2023-09-26T13:55:58Z

src/bin/common/solving_loop.ml

+      unsupported_opt kind;
+      print_std Fmt.string "unsupported"


This will now reply twice to the standard output, there needs to be a single reply. The reply needs to be unsupported (as a single atom -- not (:all-statistics unsupported)). Calling unsupported_opt here and below should be enough.

bclement-ocp · 2023-09-26T13:57:31Z

src/lib/reasoners/fun_sat.ml

@@ -1387,7 +1394,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
    with | Util.Not_implemented s ->
      Printer.print_err "Feature %s is not implemented. \
                         I can't conclude." s;
-      raise (I_dont_know env)
+      i_dont_know
+        "I stopped while trying to produce a model."


This is now printed as an SMT-LIB atom and can't be a free-form string, should be incomplete here.

bclement-ocp · 2023-09-26T13:58:15Z

src/lib/reasoners/sat_solver_sig.mli

+(** A reason for which the solver returned unknown. *)
+type unknown_reason = string


Nit: It would be cleaner for this to be an ADT, but we can keep a string for now (although I think the string is always "incomplete" currently)

Nit: It would be cleaner for this to be an ADT, but we can keep a string for now (although I think the string is always "incomplete" currently)

I added this comment in sat_solver_sig.ml

After merging #829, the ADT will be something like

type unknown_reason = | Incomplete | Memout | Timeout of timeout_reason

We can add the ADT right now but we will have to modify it just after merging the other PR.

We merged #829 so we can create the ADT now.

This ADT is strange, it makes the possibility of building a value Timeout NoTimeout. I'm changing this a bit.

bclement-ocp

Thank you for adding tests! I believe the expected outputs are not correct, can you fix them?

bclement-ocp · 2023-09-26T15:08:12Z

tests/everything/testfile-smt-instr-get-info.dolmen.expected

+(:all-statistics unsupported)
+(:assertion-stack-levels unsupported)


These lines need to be:

Suggested change

(:all-statistics unsupported)

(:assertion-stack-levels unsupported)

unsupported

unsupported

bclement-ocp · 2023-09-26T15:08:35Z

tests/everything/testfile-smt-instr-get-info.dolmen.expected

+(:name "Alt-Ergo")
+(error "Invalid (get-info :reason-unknown)")
+(:version dev)
+(error "unknown option ':foo'")


This line also needs to be:

Suggested change

(error "unknown option ':foo'")

unsupported

Stevendeo · 2023-09-28T11:15:22Z

Okay I fixed the output, but I added warning/error messages to give more insights on the unsupported/invalid requests

bclement-ocp

Thanks! You can also use the "Re-request a review" button once the changes are made.

I think this looks good now, I think the TODO comment should be removed before merging since you added the ADT.

It's not very important, but I am surprised about the blank lines in the output (although the output machinery is very convoluted so maybe I shouldn't be surprised). Do you understand where they are coming from?

bclement-ocp · 2023-09-28T11:42:57Z

src/lib/reasoners/sat_solver_sig.ml

+(* TODO: use an ADT and add Timeout when library starts acting like a
+   library. *)


I think this comment can go away?

@Stevendeo I can merge as soon as the comment has been removed ;)

Stevendeo · 2023-10-02T12:42:29Z

It's not very important, but I am surprised about the blank lines in the output (although the output machinery is very convoluted so maybe I shouldn't be surprised). Do you understand where they are coming from?

I did not investigate it but I thought about it as well... Maybe one day we'll find it

bclement-ocp

👍

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 frontend enhancement labels Sep 25, 2023

Stevendeo force-pushed the get-info branch from 854dd1f to 489c5d7 Compare September 25, 2023 13:46

Halbaroth reviewed Sep 25, 2023

View reviewed changes

src/lib/reasoners/sat_solver_sig.ml Outdated Show resolved Hide resolved

src/lib/reasoners/satml_frontend.ml Outdated Show resolved Hide resolved

src/lib/reasoners/fun_sat.ml Outdated Show resolved Hide resolved

Halbaroth mentioned this pull request Sep 22, 2023

Printing unknown reason #834

Closed

bclement-ocp requested changes Sep 25, 2023

View reviewed changes

Halbaroth reviewed Sep 26, 2023

View reviewed changes

src/bin/common/solving_loop.ml Outdated Show resolved Hide resolved

src/bin/common/solving_loop.ml Outdated Show resolved Hide resolved

src/bin/common/solving_loop.ml Outdated Show resolved Hide resolved

Halbaroth approved these changes Sep 26, 2023

View reviewed changes

Halbaroth requested a review from bclement-ocp September 26, 2023 13:51

bclement-ocp requested changes Sep 26, 2023

View reviewed changes

bclement-ocp mentioned this pull request Sep 26, 2023

Model generation support for SatML #829

Merged

bclement-ocp requested changes Sep 27, 2023

View reviewed changes

Support of get-info SMT2 command

fea288b

Stevendeo force-pushed the get-info branch from 7da5509 to fea288b Compare September 28, 2023 09:42

Stevendeo added 2 commits September 28, 2023 11:44

Update tests

52532f4

Format

2c2b300

bclement-ocp approved these changes Sep 28, 2023

View reviewed changes

Removing comment

96e04df

Stevendeo requested a review from bclement-ocp October 2, 2023 12:40

bclement-ocp merged commit 9e5b4aa into OCamlPro:next Oct 2, 2023
14 checks passed

bclement-ocp reviewed Oct 2, 2023

View reviewed changes

bclement-ocp mentioned this pull request Sep 24, 2024

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

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Support of get-info SMT2 command #837

Support of get-info SMT2 command #837

Stevendeo commented Sep 25, 2023

bclement-ocp left a comment

bclement-ocp Sep 25, 2023

Halbaroth Sep 25, 2023 •

edited

Loading

Halbaroth Sep 25, 2023

bclement-ocp Sep 25, 2023

bclement-ocp Sep 25, 2023

bclement-ocp Sep 25, 2023 •

edited

Loading

bclement-ocp left a comment

bclement-ocp Sep 26, 2023

Halbaroth Sep 26, 2023

bclement-ocp Sep 26, 2023

bclement-ocp Sep 26, 2023

bclement-ocp Sep 26, 2023

Stevendeo Sep 26, 2023

Halbaroth Sep 26, 2023 •

edited

Loading

Halbaroth Sep 27, 2023

Stevendeo Sep 28, 2023

bclement-ocp left a comment

bclement-ocp Sep 26, 2023

bclement-ocp Sep 26, 2023

Stevendeo commented Sep 28, 2023 •

edited

Loading

bclement-ocp left a comment

bclement-ocp Sep 28, 2023

Halbaroth Sep 29, 2023

Stevendeo commented Oct 2, 2023

bclement-ocp left a comment

		Printer.print_err "Invalid (get-info :reason-unknown)";
		Format.fprintf fmt ""

		let unsupported_opt s =
		Printer.print_smtlib_err "unsupported option %S" s

		(** A reason for which the solver returned unknown. *)
		type unknown_reason = string

		(:all-statistics unsupported)
		(:assertion-stack-levels unsupported)

		(* TODO: use an ADT and add Timeout when library starts acting like a
		library. *)

Support of get-info SMT2 command #837

Support of get-info SMT2 command #837

Conversation

Stevendeo commented Sep 25, 2023

bclement-ocp left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Halbaroth Sep 25, 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

bclement-ocp Sep 25, 2023 • edited Loading

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

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 Sep 26, 2023 • edited Loading

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

Stevendeo commented Sep 28, 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

Stevendeo commented Oct 2, 2023

bclement-ocp left a comment

Choose a reason for hiding this comment

Halbaroth Sep 25, 2023 •

edited

Loading

bclement-ocp Sep 25, 2023 •

edited

Loading

Halbaroth Sep 26, 2023 •

edited

Loading

Stevendeo commented Sep 28, 2023 •

edited

Loading