feat: get-assignment statement #848

Stevendeo · 2023-09-29T11:08:11Z

This PR adds the (get-assignment) statement handling (issue #844)

Produce assertion option handler
Registering & accessing to named expressions in kernel
Evaluation of boolean named expression
SMT Output

bclement-ocp · 2023-09-29T11:29:39Z

Please mark WIP PRs as draft so that others don't get notifications until it is ready (I just did it for this one). Thanks!

Stevendeo · 2023-10-02T09:19:32Z

I did not see where to set the PR as a draft

bclement-ocp · 2023-10-02T09:22:15Z

There is a drop-down on the "Create pull request" button:

For existing PRs there is a link below "Reviewers" (this is less effective WRT notifications because people are automatically subscribed once the PR becomes non-draft, but still indicates that the PR is still being worked on in the UI) :

To mark as non-draft once the PR is ready the button is at the bottom of the page:

bclement-ocp

We should figure out if we actually need model production for get-assignment. If we do, then (set-option :produce-assignments true) needs to activate model production, if we don't then we remove the check.

bclement-ocp · 2023-11-02T11:27:37Z

src/bin/common/solving_loop.ml

@@ -297,6 +343,14 @@ let main () =
    State.create_key ~pipe:"" "optimize"
  in

+  let get_assignment: bool State.key =


This should be called produce_assignments rather than get_assignment, no?

bclement-ocp · 2023-11-02T11:28:42Z

src/bin/common/solving_loop.ml

+        | DStd.Expr.Var _ | Cst _ -> terms_to_check
+        | App (t, _, tl) -> (t :: tl) :: terms_to_check
+        | Binder (b, t) ->
+          (t :: terms_of_dolmen_binder b) :: terms_to_check


Is this going to do the right thing wrt capture of bound variables (e.g. what happens if I do (let ((x 2)) (+ (! x :named name))))?

I did not think about the semantics of named terms in bindings. Do you think we should not record the named formulas in bindings for now?

If we don't have an easy way of checking capture avoidance then yes, that would be better (this is already what we do for quantifiers if I am not mistaken).

bclement-ocp · 2023-11-02T11:30:57Z

src/bin/common/solving_loop.ml

+                st
+              | _ ->
+                recoverable_error
+                  "Model generation disactivated, cannot execute \


disabled, not deactivated. We may want to mention (set-option :produce-model true) here.

Although do we actually need this case? It looks like we don't care about the result of SAT.get_model and I think it should work without?

The command should only be available in SAT mode, is that the good way to check it?

As the name indicates, the partial_model_key should only contain a value if we are in SAT mode, there is no need to also check SAT.get_model (even though AFAIK the call to SAT.get_model cannot fail currently).

bclement-ocp · 2023-11-02T11:36:57Z

src/bin/common/solving_loop.ml

+
+  let handle_get_assignment ~get_value st =
+    let assignments =
+      Util.MS.fold


Nit: you can probably leverage Fmt.iter_bindings here.

I preferred to build the list and print it afterwards to make the code more readable

bclement-ocp

We should have a test without (set-option :produce-models true), otherwise looks good (modulo the integer / boolean typo).

bclement-ocp · 2023-11-02T16:29:58Z

src/bin/common/solving_loop.ml

+      begin
+        match bool_of_string_opt b with
+        | None ->
+          print_wrn_opt ~name:":verbosity" st_loc "integer" value;


Suggested change

print_wrn_opt ~name:":verbosity" st_loc "integer" value;

print_wrn_opt ~name:":verbosity" st_loc "boolean" value;

bclement-ocp · 2023-11-02T16:34:52Z

src/bin/common/solving_loop.ml

+
+  let print_terms_assignments =
+    Fmt.list
+      ~sep:(fun fmt _ -> Fmt.pf fmt "@,")


Nit: Missed it earlier but (fun ppf _ -> Fmt.pf ppf "@,") is Fmt.cut.

bclement-ocp · 2023-11-06T10:18:20Z

Thanks for the new tests. Can you add one without (set-option :produce-models true) (but with (set-option :produce-assignments true) as requested previously? Thanks

bclement-ocp · 2023-11-08T13:03:51Z

src/bin/common/solving_loop.ml

+          if Options.get_interpretation () then begin
+            match State.get partial_model_key st with
+            | Some Model ((module SAT), partial_model) ->
+              if State.get produce_assignment st then
+                handle_get_assignment
+                  ~get_value:(SAT.get_value partial_model)
+                  st
+              else
+                recoverable_error
+                  "Produce assignments disabled; \
+                   add (set-option :produce-assignments true)";
+              st
+            | None ->
+              (* TODO: add the location of the statement. *)
              recoverable_error
-                "Produce assignments disabled; \
-                 add (set-option :produce-assignments true)";
-            st
-          | None ->
-            (* TODO: add the location of the statement. *)
-            recoverable_error
-              "No model produced, cannot execute get-assignment.";
-            st
+                "No model produced, cannot execute get-assignment.";
+              st
+          end
+          else
+            begin
+              (* TODO: add the location of the statement. *)
+              recoverable_error
+                "(get-assignment) requires model generation, \
+                 but it is disabled (try --produce-models)";
+              st
+            end


I thought we determined earlier that produce-assignments should work without produce-models, why are we disabling it instead?

I'm not sure why you requested an extra test for get-assignment if not for testing this specific case. Did you mean you wanted a non-error test with no models calculated but a get-assignment response anyway? Because there already was a test without (set-option :produce-models true).
The standard states that, when in sat mode, "the solver will have identified a model A of the current logic". I think that's what confused me (the said model can be abstract, which is specified later on the standard).

Yes, I wanted a successful test :) Indeed the sat does not require to have built the model explicitly.

Because there already was a test without (set-option :produce-models true).

Sorry, I must have missed it, but I still don't see it — can you point me to that test? The tests I see are bool1, bool2, bool3 that have both produce-models and produce-assignments; get-assignment1 that has neither, get-assignment2 that has produce-models but not produce-assignments and only the new get-assignment3 that has produce-assignment but not produce-models.

We should have a test without (set-option :produce-models true), otherwise looks good (modulo the integer / boolean typo).

tests/smtlib2/testfile-get-assignment1.err.dolmen.smt2 indeed has neither

Ah! Sorry I was not clear, I meant without produce-models but with produce-assignments as clarified in my later message :)

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)

bclement-ocp marked this pull request as draft September 29, 2023 11:29

Stevendeo added 2 commits October 31, 2023 11:20

Produce assignments option

ec769f9

Placeholder for get_assignments

a6221a4

Stevendeo force-pushed the get-assignment branch 2 times, most recently from c150f37 to 026b45a Compare October 31, 2023 15:06

Gathering the named formulae

b465653

Stevendeo force-pushed the get-assignment branch from 026b45a to b465653 Compare October 31, 2023 15:13

Stevendeo added 4 commits October 31, 2023 17:44

Pulling threads up to the SAT solver

c9317ef

Update tests

fe5c2cb

Proprification

9b461ef

Adding basic get_value

0cfbec6

Stevendeo force-pushed the get-assignment branch from 935b1fa to 0cfbec6 Compare November 2, 2023 10:53

Stevendeo marked this pull request as ready for review November 2, 2023 11:00

Stevendeo requested review from bclement-ocp, hra687261 and Halbaroth and removed request for bclement-ocp and hra687261 November 2, 2023 11:01

Stevendeo changed the title ~~[WIP] Get assignment statement~~ feat: get-assignment statement Nov 2, 2023

bclement-ocp requested changes Nov 2, 2023

View reviewed changes

Stevendeo added 4 commits November 2, 2023 13:01

Update tests

f5cc809

Poetry

5c6f05f

Removing useless check

083693f

Removing spurious term selection in binder

541b4d6

Stevendeo requested a review from bclement-ocp November 2, 2023 12:47

Halbaroth added this to the 2.6.0 milestone Nov 2, 2023

Halbaroth added enhancement frontend labels Nov 2, 2023

bclement-ocp reviewed Nov 2, 2023

View reviewed changes

Stevendeo added 2 commits November 3, 2023 11:05

Poetry

86f8f33

Adding tests

9cbf833

Stevendeo requested a review from bclement-ocp November 6, 2023 10:09

Stevendeo force-pushed the get-assignment branch from d8c47c7 to 7d3b6bd Compare November 8, 2023 09:00

Adding tests & handling case where model gen is disabled

15f0560

Stevendeo force-pushed the get-assignment branch from 7d3b6bd to 15f0560 Compare November 8, 2023 09:20

bclement-ocp reviewed Nov 8, 2023

View reviewed changes

Update test

9c79109

bclement-ocp approved these changes Nov 8, 2023

View reviewed changes

Halbaroth approved these changes Nov 9, 2023

View reviewed changes

Halbaroth merged commit 7445b47 into OCamlPro:next Nov 9, 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: get-assignment statement #848

feat: get-assignment statement #848

Stevendeo commented Sep 29, 2023 •

edited

Loading

bclement-ocp commented Sep 29, 2023

Stevendeo commented Oct 2, 2023

bclement-ocp commented Oct 2, 2023 •

edited

Loading

bclement-ocp left a comment

bclement-ocp Nov 2, 2023

bclement-ocp Nov 2, 2023

Stevendeo Nov 2, 2023

bclement-ocp Nov 2, 2023

bclement-ocp Nov 2, 2023

bclement-ocp Nov 2, 2023

Stevendeo Nov 2, 2023

bclement-ocp Nov 2, 2023

bclement-ocp Nov 2, 2023

Stevendeo Nov 2, 2023

bclement-ocp left a comment

bclement-ocp Nov 2, 2023

bclement-ocp Nov 2, 2023

bclement-ocp commented Nov 6, 2023

bclement-ocp Nov 8, 2023

Stevendeo Nov 8, 2023

bclement-ocp Nov 8, 2023

Stevendeo Nov 8, 2023

bclement-ocp Nov 8, 2023

	print_wrn_opt ~name:":verbosity" st_loc "integer" value;
	print_wrn_opt ~name:":verbosity" st_loc "boolean" value;

feat: get-assignment statement #848

feat: get-assignment statement #848

Conversation

Stevendeo commented Sep 29, 2023 • edited Loading

bclement-ocp commented Sep 29, 2023

Stevendeo commented Oct 2, 2023

bclement-ocp commented Oct 2, 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

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

bclement-ocp commented Nov 6, 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

Stevendeo commented Sep 29, 2023 •

edited

Loading

bclement-ocp commented Oct 2, 2023 •

edited

Loading