feat: Option --optimize #916

Stevendeo · 2023-10-19T13:15:02Z

Adresses #897

bclement-ocp · 2023-10-19T14:06:51Z

src/bin/common/parse_command.ml

+          (* Optimization is so far only sound for CDCL & CDCL_Tableaux. We set
+             CDCL_Tableaux by default. *)
+          Fmt.pf
+            Format.err_formatter
+            ";Warning: --optimize is not compatible with %a: forcing it to %a@."
+            Util.pp_sat_solver s
+            Util.pp_sat_solver Util.CDCL_Tableaux;
+          set_sat_solver Util.CDCL_Tableaux;


I don't think overriding an explicitly requested solver is a good thing to do — we should rather fail using term_result if conflicting options are given.

bclement-ocp · 2023-10-19T14:10:24Z

src/bin/common/solving_loop.ml

+    | Dolmen.Std.Id.{name = Simple "minimize"; _}, [term] ->
+      handle_minimize_term term st
+    | Dolmen.Std.Id.{name = Simple "maximize"; _}, [term] ->
+      handle_maximize_term term st
+    | Dolmen.Std.Id.{name = Simple "get-objectives"; _}, args ->
+      handle_get_objectives args st
+    | Dolmen.Std.Id.{name = Simple (("minimize" | "maximize") as ext); _}, _ ->
+      recoverable_error
+        "Statement %s only expects 1 argument (%i given)"
+        ext
+        (List.length args);
+      st


These should be when O.get_optimize ()

In fact, instead of using O.get_optimize (), it would be better to:

Add a new boolean key optimize to the Dolmen state

Initialize the boolean key with O.get_optimize

Use when State.get st optimize_key here

Update the optimize_key on set-option :optimize but not call O.set_optimize

Reset the optimize_key to O.get_optimize when (reset) is encountered

This allows the set-option to be local to the Dolmen state, and is correct wrt the semantics of (reset) mandated by the SMT-LIB standard (which should reinitialize the state of the solver to what it was at the beginning of parsing the file, so should undo the set-option even though it currently doesn't — but we can move towards that slowly).

bclement-ocp · 2023-10-19T14:13:53Z

src/bin/common/solving_loop.ml

+  | _ when O.get_optimize () ->
+    warning
+      "Sat-solver %a is incompatible with optimization: ignoring command."
+      Util.pp_sat_solver
+      s


This is not correct — the sat solver is stlil set on the Dolmen state even though it is not updated through options. Either the check needs to be in handle_option and State.set sat_solver_key must not be called, or we must call both O.set_sat_solver and O.set_optimize false here.

(Yes, the way we manage options is currently a mess, sorry)

For further clarification — the SAT solver that is actually used by the binary is the one that is set on the Dolmen state. The options are only updated because of code in the SAT solvers that triggers different behavior depending on Options.get_cdcl_tableaux and related. We want to move away from code that depends on global Options values in the library as much as possible, but for now we have no choice but to update those options.

I understand. In an ideal world, options should only be used to initialize dolmen's state and never read again afterwards.

bclement-ocp

I think this is mostly good, but we should call DStd.Extensions.Smtlib2.(enable maxsmt) when initializing Dolmen as well, and either call DStd.Extensions.Smtlib2.(disable maxsmt) when disabling optimizations or have the proper guards in place in handle_custom_statement to error out on minimize/maximize/etc. if the option is not provided (2nd one is probably better so that we can instruct the user to set the optimize flag)

bclement-ocp · 2023-10-19T15:08:48Z

src/bin/common/solving_loop.ml

@@ -722,6 +809,7 @@ let main () =
        Parser.parse_logic ~preludes logic_file
      in
      let st = State.set Typer.additional_builtins D_cnf.builtins st in
+      let st = State.set optimize_key (O.get_optimize ()) st in


I think this should rather be in mk_state — in fact the previous line should be moved there as well.

For an obscure reason, moving the previous line to the mk_state makes alt-ergo fails on tests where it needs built-ins.

bclement-ocp · 2023-10-19T15:09:58Z

src/bin/common/solving_loop.ml

+      O.set_sat_solver sat;
+      State.set
+        sat_solver_key
+        (make_sat ())
+        st


This deserves a comment explaining that make_sat dispatches on O.get_sat_solver

bclement-ocp · 2023-10-23T08:04:00Z

src/bin/common/solving_loop.ml

+        "Sat-solver %a is incompatible with optimization: ignoring command."
+        Util.pp_sat_solver
+        sat;


You are not ignoring the command here since you call DStd.Extensions.Smtlib2.(enable maxsmt) above.

bclement-ocp · 2023-10-23T08:04:29Z

src/bin/common/solving_loop.ml

+        sat;
+      st
+    | Tableaux | Tableaux_CDCL | CDCL | CDCL_Tableaux ->
+      O.set_optimize optim;


O.set_optimize should not be called here for proper (reset) behavior.

Halbaroth · 2023-10-23T15:14:38Z

@Stevendeo Can I merge?

bclement-ocp · 2023-10-23T15:15:50Z

Sorry, forgot to do it

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)

Stevendeo marked this pull request as ready for review October 19, 2023 13:59

Stevendeo requested review from bclement-ocp, hra687261 and Halbaroth October 19, 2023 14:00

bclement-ocp requested changes Oct 19, 2023

View reviewed changes

Stevendeo requested a review from bclement-ocp October 19, 2023 14:58

bclement-ocp requested changes Oct 19, 2023

View reviewed changes

Halbaroth added frontend optimization This issue is related to optimization in models. labels Oct 20, 2023

Halbaroth added this to the 2.6.0 milestone Oct 20, 2023

Stevendeo requested a review from bclement-ocp October 23, 2023 07:48

bclement-ocp requested changes Oct 23, 2023

View reviewed changes

Stevendeo added 7 commits October 23, 2023 11:58

Adding --optimize option

58c1072

Adding placeholders for optimae

131796b

Get objectives

086fdf5

Poetry

bd40799

Failing on parse command instead of forcing options

ece6775

Relying on dolmen state options instead of options module

1d0e7a9

Activating extension and some poetry

4aead66

Stevendeo force-pushed the optimize-option branch from 8dca6ec to 4aead66 Compare October 23, 2023 09:58

Stevendeo added 2 commits October 23, 2023 12:21

Removign duplicate option

482eae0

Activating options where they should

96e463f

Stevendeo requested a review from bclement-ocp October 23, 2023 10:26

bclement-ocp approved these changes Oct 23, 2023

View reviewed changes

bclement-ocp merged commit a335ea0 into OCamlPro:next Oct 23, 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

feat: Option --optimize #916

feat: Option --optimize #916

Stevendeo commented Oct 19, 2023

bclement-ocp Oct 19, 2023

bclement-ocp Oct 19, 2023

bclement-ocp Oct 19, 2023

bclement-ocp Oct 19, 2023

bclement-ocp Oct 19, 2023

Stevendeo Oct 19, 2023

bclement-ocp left a comment

bclement-ocp Oct 19, 2023

Stevendeo Oct 23, 2023

bclement-ocp Oct 19, 2023

bclement-ocp Oct 23, 2023

bclement-ocp Oct 23, 2023

Halbaroth commented Oct 23, 2023

bclement-ocp commented Oct 23, 2023

feat: Option --optimize #916

feat: Option --optimize #916

Conversation

Stevendeo commented Oct 19, 2023

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Halbaroth commented Oct 23, 2023

bclement-ocp commented Oct 23, 2023