Bubble printing model #932

Halbaroth · 2023-11-14T08:55:22Z

This PR solves the issue #833. The most of the refactoring have been done in OptimAE but still AE prints model in the library. Now, it will make this decision in the binary only.

Notice that AE printed model after getting timeout. I didn't keep this behaviour but I can restore it if you prefer. In my opinion, if we get a model after a timeout, the model is probably wrong and shouldn't be outputted.

This commit bubbles the decision of printing models in the binary. Now, the library do not print models at all.

We have to update the JS worker to dump models as we don't print models in the library anymore.

Halbaroth · 2023-11-14T08:59:32Z

Oups, I realize that I don't print timeout reason anymore as it's done during printing model ...

In some situations, we need to retrieve the reason of a timeout in the binary but we have no environment of the SAT solver in these locations. I add an argument to the timeout exception to save its reason.

This reverts commit dbfed1b.

Halbaroth · 2023-11-14T10:08:30Z

In fact, we don't need to print the timeout reason in the binary when we catch the exception Util.Timeout. Indeed, in this case it could mean only one thing: Alt-Ergo received the alarm signal and the reason is Signal. Thus I revert my last commit. If we raise another timeout in the SAT solver, we convert it to Unknown env in Frontend and the reason will be print in solving_loop.

Stevendeo · 2023-11-14T10:32:16Z

src/lib/reasoners/sat_solver_sig.ml

@@ -35,12 +35,22 @@ type timeout_reason =
  | Assume
  | ProofSearch
  | ModelGen
+[@@deriving show]

 type unknown_reason =
  | Incomplete
  | Memout
  | Timeout of timeout_reason


Why not [@@deriving show] ?

Not sure to understand your remark :D

bclement-ocp

Not a very big fan of duplicating the print_model function, could we keep it in the frontend and call it from both binary & worker?

bclement-ocp · 2023-11-14T12:15:58Z

src/bin/common/solving_loop.ml

+  let print_model ppf (Model ((module SAT), env)) =
+    let ur = SAT.get_unknown_reason env in
+    Printer.print_fmt (Options.Output.get_fmt_diagnostic ())
+      "@[<v 0>; Returned unknown reason = %a@]"


There shouldn't be ; comments on the diagnostic channel.

src/bin/common/solving_loop.ml

bclement-ocp · 2023-11-14T12:17:45Z

src/bin/common/solving_loop.ml

+          let _ = match State.get partial_model_key st with
+            | Some model ->
+              print_model (Options.Output.get_fmt_regular ()) model
+            | None ->
+              (* TODO: add the location of the statement. *)
+              recoverable_error "No model produced."
+          in
+          st


Not convinced we should print the unknown reason when we have a model, it will just be noise. If the user wants to see the unkonwn reason, they can call (get-info :unknown-reason), we shouldn't force it down their throat.

(For --dump-models I am not entirely convinced either but it kind of makes sense b/c the user has no control & it helps distinguish the intermediate models from the final models with --interpretation every, but for (get-model) there is a mechanism in place to display that information with (get-info :unknown-reason) already)

bclement-ocp · 2023-11-14T12:20:23Z

src/bin/common/solving_loop.ml

+      Printer.print_fmt (Options.Output.get_fmt_diagnostic ())
+        "@[<v 0>It seems that no model has been computed so \
+         far. You may need to change your model generation strategy \
+         or to increase your timeouts."


Why change the error message?

I didn't change it but I print the timeout reason just before. Now, if we don't print always the unknown reason while outputting the model, it makes sense to keep print it if we fail to produce a model here.

src/bin/js/worker_js.ml

We use `print_model` twice (in the usual binary and the JS worker), thus we can factorize it by moving it in `Frontend`.

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 frontend label Nov 14, 2023

Halbaroth added this to the 2.6.0 milestone Nov 14, 2023

Halbaroth linked an issue Nov 14, 2023 that may be closed by this pull request

Bubble decision of printing models upwards #833

Closed

Halbaroth force-pushed the bubble-printing-model branch from e0096a2 to c8e4fa1 Compare November 14, 2023 08:56

Halbaroth added 2 commits November 14, 2023 09:57

Bubbling the model printing in the binary

f934b75

This commit bubbles the decision of printing models in the binary. Now, the library do not print models at all.

Update the JS worker

c8e4fa1

We have to update the JS worker to dump models as we don't print models in the library anymore.

Halbaroth marked this pull request as draft November 14, 2023 08:58

Halbaroth added 2 commits November 14, 2023 11:02

Save a timeout reason in the exception Util.Timeout

dbfed1b

In some situations, we need to retrieve the reason of a timeout in the binary but we have no environment of the SAT solver in these locations. I add an argument to the timeout exception to save its reason.

Revert "Save a timeout reason in the exception Util.Timeout"

29c3841

This reverts commit dbfed1b.

Halbaroth marked this pull request as ready for review November 14, 2023 10:08

Halbaroth requested review from bclement-ocp, Stevendeo and hra687261 and removed request for bclement-ocp November 14, 2023 10:10

Stevendeo approved these changes Nov 14, 2023

View reviewed changes

bclement-ocp requested changes Nov 14, 2023

View reviewed changes

Halbaroth force-pushed the bubble-printing-model branch from aeb6f24 to 9cc2fd6 Compare November 14, 2023 13:04

Halbaroth requested a review from bclement-ocp November 14, 2023 13:05

Review changes

9cc2fd6

bclement-ocp requested changes Nov 14, 2023

View reviewed changes

src/bin/js/worker_js.ml Outdated Show resolved Hide resolved

Factorizing print_model

1b77978

We use `print_model` twice (in the usual binary and the JS worker), thus we can factorize it by moving it in `Frontend`.

bclement-ocp approved these changes Nov 17, 2023

View reviewed changes

Halbaroth merged commit 2a9a770 into OCamlPro:next Nov 17, 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

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Bubble printing model #932

Bubble printing model #932

Halbaroth commented Nov 14, 2023

Halbaroth commented Nov 14, 2023

Halbaroth commented Nov 14, 2023 •

edited

Loading

Stevendeo Nov 14, 2023 •

edited

Loading

Halbaroth Nov 14, 2023

bclement-ocp left a comment

bclement-ocp Nov 14, 2023

bclement-ocp Nov 14, 2023

bclement-ocp Nov 14, 2023

Halbaroth Nov 14, 2023

Bubble printing model #932

Bubble printing model #932

Conversation

Halbaroth commented Nov 14, 2023

Halbaroth commented Nov 14, 2023

Halbaroth commented Nov 14, 2023 • edited Loading

Stevendeo Nov 14, 2023 • edited Loading

Choose a reason for hiding this comment

Halbaroth Nov 14, 2023

Choose a reason for hiding this comment

bclement-ocp left a comment

Choose a reason for hiding this comment

bclement-ocp Nov 14, 2023

Choose a reason for hiding this comment

bclement-ocp Nov 14, 2023

Choose a reason for hiding this comment

bclement-ocp Nov 14, 2023

Choose a reason for hiding this comment

Halbaroth Nov 14, 2023

Choose a reason for hiding this comment

Halbaroth commented Nov 14, 2023 •

edited

Loading

Stevendeo Nov 14, 2023 •

edited

Loading