Support `get-value` statement #1032

Halbaroth · 2024-01-26T12:52:08Z

This PR adds the support for the get-value statement for both SatML and FunSAT solvers.

I create a new functor to factorize the code between these solvers.
This PR doesn't change the code of FunSAT and I introduce only two changes in Satml_frontend but the introduction of the functor wrapper changes the indentation of all the file:

At the end of the function unsat, we perform a SAT.cancel_until env.satml 0 to be able to assert new statements in env later.
This is a requirement for get-value as we need to assert the model and new equation after unsat.
The boolean model of SatML (which is basically the trail) is lost after calling unsat now, so we save it in a mutable field of env to be able to retrieve it when we perform a get-assignment statement.

This isn't the best design and I think I will introduce a root_level à la MiniSAT in another PR.

Notice I assert the new model after each get-value and we could probably do it only once after the first get-value.

Before merging this PR, I plan to use get-value in order to test the model generation for the LIA theory.

bclement-ocp · 2024-01-26T13:55:24Z

Nice! I will not have time to look at this PR before the JFLA, however two quick remarks:

At the end of the function unsat, we perform a SAT.cancel_until env.satml 0 to be able to assert new statements in env later.

That is unfortunate we have to do this even if we never call (get-value); is there a chance we could call cancel_until at the moment (get-value) is called instead?

This isn't the best design and I think I will introduce a root_level à la MiniSAT in another PR.

We support incremental solving, and so we are already halfway there: the root level is at Vec.size env.increm_guards, and we could push a new level for the purpose of (get-value) shenanigans. There is code in #1000 that allows adding assertions at a level higher than 0, if I recall correctly.

Halbaroth · 2024-01-26T14:09:35Z

I will check later for the incremental issue but clearly we should fix this at some point ;)

Halbaroth · 2024-01-26T14:10:13Z

That is unfortunate we have to do this even if we never call (get-value); is there a chance we could call cancel_until at the moment (get-value) is called instead?

Seems doable :)

bclement-ocp

Please either remove entirely Sat_solver_util.Make or separate the definition of Satml_frontend.Make in Satml_frontend.Make_internal followed by Satml_frontend.Make(Th) = Sat_solver_util.Make(Make_internal(Th)); the indentation changes make it virtually impossible to review changes to that module.

Why are all the tests calling (get-value (true))? This doesn't seem to be a very demanding test of the feature! Please add specific tests for (get-value) rather than tacking on (get-value) to existing tests.

bclement-ocp · 2024-02-06T13:57:56Z

src/lib/util/lists.mli

+(** [iter_pair f (l1, l2)] iterates simultany on the pair of elements of the
+    lists [l1] and [l2].
+
+    @raise Invalid_arg if the lists haven't the same length. *)


Suggested change

@raise Invalid_arg if the lists haven't the same length. *)

@raise Invalid_arg if the lists don't have the same length. *)

bclement-ocp · 2024-02-06T14:00:34Z

src/lib/structures/symbols.mli

-(** Create a new symbol with the given name.
-
-    By default, names are created in the [User] name space.
-
-    Note that names are pre-mangled: the [hs] field of the resulting name may
-    not be exactly the name that was passed to this function (however, calling
-    `name` with the same string but two different name spaces is guaranteed to
-    return two [Name]s with distinct [hs] fields). *)


This documentation should either stay as is, or point the user towards Name.mk.

src/lib/util/lists.mli

bclement-ocp · 2024-02-06T14:06:58Z

src/lib/structures/symbols.ml


-type name_space = User | Internal | Fresh | Skolem | Abstract
+type name_space =
+    User | Internal | Fresh | Skolem | Abstract | GetValue [@@deriving eq]


If you are using deriving eq there is no reason to keep compare_name_space and not derive ord as well.

bclement-ocp · 2024-02-06T14:07:44Z

src/lib/structures/modelMap.mli

+(** [iter f mdl] iterates over all the graphes of the model [mdl]. *)
+


Suggested change

(** [iter f mdl] iterates over all the graphes of the model [mdl]. *)

(** [iter f mdl] iterates over all the graphs of the model [mdl]. *)

bclement-ocp · 2024-02-06T14:32:23Z

src/lib/reasoners/sat_solver_util.ml

+           hdist = -1;
+           gdist = 0;


You seem to have a better understanding of these fields than me — can you explain why hdist = -1 and gdist = 0 here but the opposite in internal_assume (and why gf is true here but false in internal_assume)? In frontend.ml we use -1 for hdist and gdist, and false for mf and gf.

I'm not totally sure why is necessary. I think we can merge the PR and I will document this point in another PR. I will open a remainder issue.

src/lib/reasoners/sat_solver_sig.mli

bclement-ocp · 2024-02-06T14:38:24Z

src/lib/reasoners/sat_solver_util.ml

+        match get_value_in_boolean_model env e with
+        | Some true -> Some Expr.vrai
+        | Some false -> Some Expr.faux
+        | None -> None
+      end


Note: if we add let of_bool b = if b then Expr.vrai else Expr.faux in Expr.Core, this would be List.map Expr.Core.of_bool @@ get_value_in_boolean_model env e.

bclement-ocp · 2024-02-06T14:40:46Z

src/lib/reasoners/sat_solver_sig.mli

+
+      @return [None] if the model generation is not enabled or the
+              environment is already unsatisfiable before calling this function.
+      @raise Unsat if the solver found a contradiction. *)


I believe that we raise Unsat if we find that the current model turns out to actually be infeasible, while the documentation seems to indicate that we raise Unsat if the problem is unfeasible.

I don't really understand why we want to raise Unsat here — we should just return None.

The documentation is a bit unclear. This function returns None if there is no model generated because we don't enable the model generation or the environment env was already unsatisfiable before calling get_value.

We raise Unsat if we found a contradiction while asserting the model in get_value.

We don't display the same message in Solving_loop:

let handle_get_value loc ~get_value l = let l = List.map (D_cnf.mk_expr ~loc ~toplevel:false ~decl_kind:Daxiom) l in match get_value l with | Some values -> Printer.print_std "(@[<v 0>%a@])@," Fmt.(iter ~sep:cut Lists.iter_pair ((pair ~sep:sp Expr.pp_smtlib Expr.pp_smtlib) |> parens)) (l, values) | None -> recoverable_error "No model produced, cannot execute get-value." | exception Sat_solver_sig.Unsat _ -> recoverable_error "The model is wrong, cannot execute get-value." in

So if you got None, it means you don't use the API correctly (or the SMT-LIB language), or there is something wrong in our model generation.
If you got Unsat, it means there is something wrong in the model.

If you got Unsat, it means there is something wrong in the model.

I think we should use a different exception here — the Unsat exception strongly implies that the problem is unsatisfiable, but since this comes from a specific model of the problem, there may be another model that is satisfiable. It is not a problem for Solving_loop, but if we ever use get_value in another context we take the risk of introducing unsoundness.

I will add a new exception here.

bclement-ocp · 2024-02-06T14:44:11Z

src/lib/reasoners/sat_solver_util.ml

+       If we don't find the model term for an expression of [l], we assert a
+       new equation to force the solver to produce a model term for this
+       expression. *)
+    let res =


This list only contains either Some v, None or None, Some name which indicates that a type isomorphic to Either.t should be used instead (e.g. type name_value = Value of value | Name of name).

bclement-ocp · 2024-02-09T09:59:58Z

src/lib/reasoners/satml_frontend.ml

          try
-            SAT.conflict_analyze_and_fix env.satml (Satml.C_theory expl);
+            do_case_split env Util.BeforeMatching;
+            env.last_saved_boolean_model <- Some (SAT.boolean_model env.satml);


Shouldn't this be done in may_update_last_saved_model?

bclement-ocp · 2024-02-09T10:00:19Z

src/lib/reasoners/satml_frontend.ml

+            Timers.exec_timer_pause Timers.M_Sat Timers.F_assume;
+            raise exn
+
+      (* HOTFIX: we can assert new formula in [env.satml] only at the level of


Needs a reference to a GH issue.

Also see previous comment:

That is unfortunate we have to do this even if we never call (get-value); is there a chance we could call cancel_until at the moment (get-value) is called instead?

I fix it by adding a new function SAT.reset_decisions in the SAT API. Now we can reset all the decisions after doing a check-sat and saved the boolean model just before.

bclement-ocp · 2024-02-09T10:01:55Z

Please either remove entirely Sat_solver_util.Make or separate the definition of Satml_frontend.Make in Satml_frontend.Make_internal followed by Satml_frontend.Make(Th) = Sat_solver_util.Make(Make_internal(Th)); the indentation changes make it virtually impossible to review changes to that module.

Ignore this; turns out that the "Ignore white space" feature of GitHub works for this (I thought I had tried it, but must have messed up something).

Halbaroth · 2024-02-09T14:02:35Z

Please either remove entirely Sat_solver_util.Make or separate the definition of Satml_frontend.Make in Satml_frontend.Make_internal followed by Satml_frontend.Make(Th) = Sat_solver_util.Make(Make_internal(Th)); the indentation changes make it virtually impossible to review changes to that module.

Ignore this; turns out that the "Ignore white space" feature of GitHub works for this (I thought I had tried it, but must have messed up something).

I removed the functor.

Halbaroth · 2024-03-18T16:01:22Z

Why are all the tests calling (get-value (true))? This doesn't seem to be a very demanding test of the feature! Please add specific tests for (get-value) rather than tacking on (get-value) to existing tests.

The purpose of these statements wasn't to test the new get-value feature but to check models using this feature. I added a new option --verify-models that does the same thing. I will remove these extra lines and update gentest to use the new option.

Halbaroth · 2024-03-18T16:19:55Z

Finally, I added a new SMT option :verify-models. This option doesn't output a message in case of success.

Halbaroth · 2024-03-19T13:12:56Z

src/lib/reasoners/satml_frontend.ml

+    List.map (fun Atom.{ lit; _ } ->
+        match Shostak.Literal.view lit with
+        | Literal.LTerm e -> e
+        | LSem _ -> assert false


I am not sure this line is correct.

It is not — there can be semantic decisions in the boolean model (I think if you run with --enable-sat-cs on a problem with arrays it will crash).

This should probably be:

List.filter_map (fun Atom.{ lit; _ } -> match Shostak.Literal.view lit with | Literal.LTerm e -> Some e | LSem _ -> None

bclement-ocp

This looks fairly good, just a few questions.

The hdist / gdist / gf thing seems to be FunSat-related, is it? You say "this is needed" so I presume things break with other values?

I am wondering if we should pass --verify-models in the tests (like we do --enable-assertions) rather than explicitly use set-option everywhere. This would mean that --verity-models does not imply --produce-models, which I think is OK; "verify any model that is produced" seems to be a more generally useful option than "produce models and also verify them".

I also think it would be useful to have a test for (get-value) + incremental solving, for instance

(define-const x Int)
(push)
(assert (= x 42))
(check-sat)
(get-value x) ; Should be 42
(pop)
(assert (= x 0))
(get-value x) ; Should be 0

bclement-ocp · 2024-03-20T10:45:12Z

src/lib/structures/symbols.ml

@@ -168,7 +172,7 @@ let is_ac x = match x with

 let is_internal sy =
  match sy with
-  | Name { ns = User; _ } -> false
+  | Name { ns = (User | GetValue); _ } -> false


Why are GetValue names not internal? According to the documentation of is_internal they should be internal since they should not be printed; am I misunderstanding something?

bclement-ocp · 2024-03-20T10:52:25Z

src/lib/reasoners/satml_frontend.ml

+    List.map (fun Atom.{ lit; _ } ->
+        match Shostak.Literal.view lit with
+        | Literal.LTerm e -> e
+        | LSem _ -> assert false


It is not — there can be semantic decisions in the boolean model (I think if you run with --enable-sat-cs on a problem with arrays it will crash).

This should probably be:

List.filter_map (fun Atom.{ lit; _ } -> match Shostak.Literal.view lit with | Literal.LTerm e -> Some e | LSem _ -> None

bclement-ocp · 2024-03-20T10:56:40Z

src/lib/reasoners/sat_solver_util.ml

+
+(* Assert the last computed model in the environment [env].
+
+   @raise Unsat if the solver found a contradiction, which means the model


Should this be Wrong_model rather?

bclement-ocp · 2024-03-20T10:58:39Z

src/lib/reasoners/sat_solver_util.ml

+     See issue: https://github.com/OCamlPro/alt-ergo/issues/1063 *)
+  let bmdl = SAT.get_boolean_model env in
+  SAT.reset_decisions env;
+  assert_model (module SAT) env mdl;


This can still raise Unsat I think, which it should not — the current model may be wrong, but there could be another correct model.

bclement-ocp · 2024-03-20T11:02:03Z

src/lib/reasoners/sat_solver_util.ml

+             | None ->
+               (* The model generation has to produce a value for each
+                  declared names. If some declared names are missing in the
+                  model, it's a bug. *)


If it's a plausible bug (I think it is) it would be better to use a an actual exception rather than an assertion failure.

I agree. We shouldn't abort if the user wants to continue after this failure.

I added a new exception No_model and caught it in solving_loop with an appropriate recoverable error message.

Halbaroth · 2024-03-20T12:37:35Z

I am wondering if we should pass --verify-models in the tests (like we do --enable-assertions) rather than explicitly use set-option everywhere. This would mean that --verity-models does not imply --produce-models, which I think is OK; "verify any model that is produced" seems to be a more generally useful option than "produce models and also verify them".

Good idea. Indeed, I didn't use this option because it turns on model generation. I will apply your suggestion.
EDIT: actually, there is another reason for which I couldn't use a CLI option for all the tests. The get-value feature doesn't work with optimization. I can add (set-option :verify-models false) in the tests using the optimization. It works because the SMT options override CLI options (which is a bit counterintuitive for an user).

Halbaroth · 2024-03-20T13:39:03Z

I am not sure this file is correct:

(declare-const x Int)
(push 1)
(assert (= x 42))
(check-sat)
(get-value (x)) ; Should be 42
(pop 1)
(assert (= x 0))
(get-value (x)) ; Should be 0

Z3 produces the value 42 for the first get-value but outputs an error for the second one as we have to insert a check-sat before it. I got the same behavior with cvc5.
Still, the file triggers two bugs:

The SAT solver tableaux doesn't produce an error for the second get-value. Instead, we got 42 twice.
The SAT solver SatML raises an assertion for the first get-value because my hotfix isn't compatible with the incremental mode.

I suggest to add this test:

(set-option :produce-models true)
(set-logic ALL)
(declare-const x Int)
(push 1)
(assert (= x 42))
(check-sat)
(get-value (x)) ; Should be 42
(pop 1)
(assert (= x 0))
(check-sat)
(get-value (x)) ; Should be 0

bclement-ocp · 2024-03-20T13:49:01Z

actually, there is another reason for which I couldn't use a CLI option for all the tests. The get-value feature doesn't work with optimization. I can add (set-option :verify-models false) in the tests using the optimization. It works because the SMT options override CLI options (which is a bit counterintuitive for an user).

Oh no! Is this because we use the boolean model?

Maybe another option is to remove the --verify-model flags for .optimize. in the test runner?

I am not sure this file is correct:

Indeed, I forgot to add the second (check-sat).

The SAT solver tableaux doesn't produce an error for the second get-value. Instead, we got 42 twice.

I think this might be #1024

my hotfix isn't compatible with the incremental mode.

Oh dang. I almost made a remark on that point but then convinced myself it actually was. Maybe some of the fixes we made with @Stevendeo in #1000 are relevant?

(Alternatively I will repeat my suggestion to create a fresh new solver to assert the model in, which I think would avoid these issues at the cost of keeping the list of assertions around)

Halbaroth · 2024-03-20T13:52:00Z

Oh no! Is this because we use the boolean model?

I think it's because of #1023

Halbaroth · 2024-03-20T13:54:58Z

I will stall this PR. There are too much things to fix about the incremental mode. I prefer working on ADT now and fix the incremental mode later.

bclement-ocp · 2024-03-20T13:56:40Z

Yeah I think that's fair — things will probably be easier if we finish #1000 first :(

We keep the last consistent SAT environment with the Dolmen key `partial_model` in `Solving_loop`. This solution isn't sufficient to implement correctly `get-value`. Indeed, we need to ensure `get-model` statements located after some `get-value` statements will still print the same model. To obtain this behaviour, now we keep the last model and the last unknown reason after a `check-sat` in a separate key. Support `get-value` in Solving_loop Add support for the SMT-LIB statement `get-value` in `Solving_loop`. With the current implementation of the solver, it's not easy to keep a consistent environment of the SAT solver without reassuming all the formulas as we do in `Solving_loop`. Instead, we save the last consistent environment obtained after a `check-sat` statement in the Dolmen state and we have to keep the last model and unknown reason with different keys. Indeed, after using `get-value`, the `get-model` statement has to output the same model. Create a new type name in `Symbols` Refactoring `get-value` support This commit adds a better support of `get-value` and `get-assignment`. These features are implemented using a new wrapper functor on the top of the SAT solvers of Alt-Ergo. - Values for bool expressions are computed by the SAT solver; - Before launching the solver to compute some model terms, we check if there aren't already available in the boolean or first-order models; - Thanks to the wrapper functor, the feature works well with the legacy solver FunSAT; We also test our generated models by non-regression tests using the `get-value`. Add option `--verify-models` This option will be useful to check our models with the new `get-value` command. Adding `--verify-models` turns on the model generation (as we did with the `--produce-models` option). If our best-effort model checker doesn't find a contradiction, we don't print anything. fix documentation Add the location for get-value À la C Use first-class module instead of functor Add Expr.Core.of_bool Reinit GetValue cpt spelling Documentation of the module Graph Derive comparison function of name_space Restore the documentation of `name` Remove the joke :( Remove the joke :( New exception for wrong model We raise a new exception `Wrong_model` in `get_value` in order to clarify the API. Rebase artefacts Removing get-value statements to check models Add a new SMT option for the CLI option `--verify-models` Use `Stdcompat.Either` for OCaml 4.08 Reset decisions only for get-value statements We need to reset the decision level of SatML after calling the `unsat` function as the decision level of this solver isn't necessary zero. This hotfix is only necessary for SatML. Add a new function `reset_decisions` in the SAT API. Saved the boolean model before resetting decisions The call `SAT.reset_decisions` may erase part of the boolean models in `get_value`. For sake of efficiency, we save the boolean model before resetting decisions. Add tests Add a link to issue 1063 Address partially review

Halbaroth added enhancement frontend models This issue is related to model generation. labels Jan 26, 2024

Halbaroth marked this pull request as ready for review January 26, 2024 12:57

Halbaroth requested a review from bclement-ocp January 26, 2024 12:57

bclement-ocp requested changes Feb 6, 2024

View reviewed changes

bclement-ocp reviewed Feb 9, 2024

View reviewed changes

Halbaroth force-pushed the support-get-value-bis branch 4 times, most recently from e55167d to fb2552c Compare March 18, 2024 15:56

Halbaroth mentioned this pull request Mar 19, 2024

Decision level of SatML after calling unsat #1063

Open

Halbaroth requested a review from bclement-ocp March 19, 2024 13:11

Halbaroth commented Mar 19, 2024

View reviewed changes

bclement-ocp reviewed Mar 20, 2024

View reviewed changes

Halbaroth force-pushed the support-get-value-bis branch from c68f034 to 8b2ecf0 Compare March 20, 2024 13:59

bclement-ocp mentioned this pull request Mar 21, 2024

Incremental version of the solver #1000

Open

Halbaroth force-pushed the support-get-value-bis branch from 8b2ecf0 to ecb7e95 Compare April 2, 2024 07:21

Halbaroth force-pushed the support-get-value-bis branch from ecb7e95 to 5f625a1 Compare April 15, 2024 21:54

Halbaroth mentioned this pull request May 2, 2024

Handling abstract values in (get-value) statements Gbury/dolmen#202

Closed

Halbaroth force-pushed the support-get-value-bis branch from 5f625a1 to 1253be1 Compare May 17, 2024 10:49

Halbaroth mentioned this pull request Jun 17, 2024

Simple ADT test with different behavior with or without push #1008

Open

Halbaroth force-pushed the support-get-value-bis branch from 1253be1 to 79e5c26 Compare July 8, 2024 11:16

Halbaroth force-pushed the support-get-value-bis branch from 79e5c26 to 41be324 Compare August 16, 2024 14:42

Halbaroth force-pushed the support-get-value-bis branch from 0383115 to 34949ec Compare November 12, 2024 17:10

Halbaroth added 3 commits November 12, 2024 18:12

remove dune.inc

bfaf336

Disable verify models if we use optimize values

34949ec

	@raise Invalid_arg if the lists haven't the same length. *)
	@raise Invalid_arg if the lists don't have the same length. *)

		(** [iter f mdl] iterates over all the graphes of the model [mdl]. *)


		(* Assert the last computed model in the environment [env].

		@raise Unsat if the solver found a contradiction, which means the model

Support get-value statement #1032

Are you sure you want to change the base?

Support get-value statement #1032

Conversation

Halbaroth commented Jan 26, 2024 • edited Loading

bclement-ocp commented Jan 26, 2024

Halbaroth commented Jan 26, 2024

Halbaroth commented Jan 26, 2024

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

Halbaroth Feb 9, 2024 • 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

bclement-ocp commented Feb 9, 2024

Halbaroth commented Feb 9, 2024

Halbaroth commented Mar 18, 2024

Halbaroth commented Mar 18, 2024

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Halbaroth commented Mar 20, 2024 • edited Loading

Halbaroth commented Mar 20, 2024 • edited Loading

bclement-ocp commented Mar 20, 2024

Halbaroth commented Mar 20, 2024

Halbaroth commented Mar 20, 2024

bclement-ocp commented Mar 20, 2024

Support `get-value` statement #1032

Support `get-value` statement #1032

Halbaroth commented Jan 26, 2024 •

edited

Loading

Halbaroth Feb 9, 2024 •

edited

Loading

Halbaroth commented Mar 20, 2024 •

edited

Loading

Halbaroth commented Mar 20, 2024 •

edited

Loading