[WIP] Removing exceptions from the Sat solver API #795

Stevendeo · 2023-09-06T10:09:28Z

This PR removes the Sat, Unsat and I_dont_know exceptions raised by the library. It now returns an ADT which is either Done, Sat, Unsat or I_dont_know.
Alt-ergo has the exact same behavior than before, but it is not a bit cleaner.

This PR also removes a raise Exit lost in the middle of the library.

bclement-ocp · 2023-09-06T10:13:14Z

src/lib/reasoners/satml_frontend.ml

+  (* Leaving this exception in case we actually raise Sat one day.
+     Remember to update `safe_call` by catching this exception if you do. *)


safe_call already catches this exception?

Oops, I removed the Sat exception, wrote this comment, put it back and forgot about it.

bclement-ocp · 2023-09-06T10:15:43Z

src/lib/reasoners/satml_frontend.ml

-                  | None -> raise Exit
+                  | None -> assert false


This code is within a try .. with Exit -> None, can you explain this change?

A mistake, I'll just revert the commit

bclement-ocp · 2023-09-06T10:16:23Z

src/lib/reasoners/sat_solver_sig.mli

  (** [unsat env f size] checks the unsatisfiability of [f] in
      [env]. Raises I_dont_know when the proof tree's height reaches
      [size]. Raises Sat if [f] is satisfiable in [env] *)


Needs to be updated

bclement-ocp · 2023-09-06T10:17:39Z

src/lib/frontend/frontend.ml

+             match
+               SAT.assume env
+                 {E.ff=f;
+                  origin_name = "";
+                  gdist = -1;
+                  hdist = -1;
+                  trigger_depth = max_int;
+                  nb_reductions = 0;
+                  age=0;
+                  lem=None;
+                  mf=false;
+                  gf=false;
+                  from_terms = [];
+                  theory_elim = true;
+                 } Ex.empty
+             with
+             | Done e -> e
+             | Sat t -> raise (SAT t)
+             | Unsat e -> raise (UNSAT e)


This should use process_sat_res?

bclement-ocp

I am a bit unsure about this change. While the goal to have a cleaner API interface is good, this means that we currently:

Raise an exception in the SAT solver,
Convert the exception to res in the SAT solver,
Immediately convert the res back into an exception in the frontend

This feels like artificial complexity to me, especially considering that this is all internal to the library (the interface for library users is process_decl, which already captures and deals with the underlying exceptions).

bclement-ocp · 2023-09-06T10:32:12Z

src/lib/reasoners/sat_solver_sig.mli

+  type res =
+    | Done of t
+    | Sat of t
+    | Unsat of Explanation.t
+    | I_dont_know of t


I'd suggest using

type outcome = Sat of t | Unsat of Explanation.t | I_dont_know of t type 'a res = ('a, outcome) Result.t

and use t res as return type for assume / assume_th_elt / pred_def, and outcome for unsat.

Your version adds an extra pointer in the Error case. Besides, the Error constructor of Result.t would be badly named. It is not an error, it is a standard response.

I don't think the extra pointer here matters, I was trying to optimise for readability —sure Error is badly named, but there is a fundamental difference here between Done and Sat / Unsat / I_dont_know (as exemplified by the fact that unsat can only return Sat / Unsat / I_dont_know, never Done).

But actually, as mentioned in another comment, that Sat of t | Unsat of Explanation.t | I_dont_know of t should be enough, bcause it makes sense for assume / assume_th_elt / pred_def to return I_dont_know.

Yes we could indeed replace Done by I_dont_know as they seem to play the same role (and I kind of did not like the Done name)

bclement-ocp · 2023-09-06T10:43:49Z

I am a bit unsure about this change. While the goal to have a cleaner API interface is good, this means that we currently:
* Raise an exception in the SAT solver,

* Convert the exception to `res` in the SAT solver,

* Immediately convert the `res` back into an exception in the frontend
This feels like artificial complexity to me, especially considering that this is all internal to the library (the interface for library users is process_decl, which already captures and deals with the underlying exceptions).

I think it would make more sense to change the interface of the Frontend module to have an abstract type t isomorphic to Sat of SAT.t | I_dont_know of SAT.t | Unsat of Explanation.t with an interface similar to the Sat_solver_sig. If the state is Sat or I_dont_know, adding things with assume etc. are passed over to the corresponding SAT function; if the state is already Unsat, silently accept everything. Then calling unsat (or a new function query) would return Sat | I_dont_know | Unsat as a public type.

This would get rid of process_decl entirely (although we could re-implement process_decl on top of that new API to avoid changing the current solving loop), and bring the public-facing API more in-line with what is expected of other solvers, which was the goal I understood at yesterday's meeting.

Edited to add: Actually, it would make sense to do this in the SAT solvers themselves rather than in the Frontend. The main point is that assume etc. should return the same type that they take as argument.

Stevendeo · 2023-09-06T10:59:44Z

I am a bit unsure about this change. While the goal to have a cleaner API interface is good, this means that we currently:
* Raise an exception in the SAT solver,

* Convert the exception to `res` in the SAT solver,

* Immediately convert the `res` back into an exception in the frontend
This feels like artificial complexity to me, especially considering that this is all internal to the library (the interface for library users is process_decl, which already captures and deals with the underlying exceptions).

IMO, the way the frontend handles the response of the sat solver should be independent from the sat solver functionning. The next step of this work would be indeed to remove the process_decl function and replacing it with specific functions, possibly without using exceptions at all.
I can add to this PR the simplification of frontend, or put it in another PR.

bclement-ocp · 2023-09-06T11:15:05Z

IMO, the way the frontend handles the response of the sat solver should be independent from the sat solver functionning. The next step of this work would be indeed to remove the process_decl function and replacing it with specific functions, possibly without using exceptions at all. I can add to this PR the simplification of frontend, or put it in another PR.

I agree; however, we also said yesterday that it made sense for the SAT solver to use exceptions.

I think the main question is: do we want to keep the Frontend module, or get rid of it?

If we keep the Frontend module, then it should be the interface for users (and I agree, it should expose specific functions instead of process_decl as a single entry point) — and so it should be the one that catches exceptions and provide a nice API. If we choose to do this, we can keep the exceptions in the Sat_solver_sig, as long as we don't use them in the Frontend that the users will interact with.
If we remove (or intend to — e.g. we could keep process_decl for the purpose of the internal solving loop for now) the Frontend module, and decide to make Sat_solver_sig the "official" interface, I think this PR should go a bit further than what it currently does and have Sat / Unsat / I_dont_know be the "public" type exposed by the solver, as mentioned in another message, so that the signatures are e.g. val assume : t -> Expr.gformula -> Explanation.t -> t (but t could be Unsat, in which case we do nothing).

I originally replied under the assumption we were going for the first option, but I think the second option may actually be closer to what @Halbaroth had in mind (and thinking about it more, it is probably the best option long-term, because it avoid one additional layer of wrapping).

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

I'm not sure to see the difference between the two versions. The Frontend does some preprocessing that is common to Fun_sat and Satml.
Also, it feels weird to be able to send Unsat to the Frontend, this not only will require the sat solver to check its input, but it is just not well typed.
I can go for the following, which is the most precise :

assume returns [Unknown of t | Unsat of Explanation.t]
unsat returns [Unknown of t | Sat of t | `Unsat of Explanation.t]
all the other methods return an environment
process_decl is split
commands.ml is removed

Halbaroth · 2023-09-06T11:35:28Z

IMO, the way the frontend handles the response of the sat solver should be independent from the sat solver functionning. The next step of this work would be indeed to remove the process_decl function and replacing it with specific functions, possibly without using exceptions at all. I can add to this PR the simplification of frontend, or put it in another PR.

I agree; however, we also said yesterday that it made sense for the SAT solver to use exceptions.

I think the main question is: do we want to keep the Frontend module, or get rid of it?
* If we keep the `Frontend` module, then it should be the interface for users (and I agree, it should expose specific functions instead of `process_decl` as a single entry point) — and so it should be the one that catches exceptions and provide a nice API. If we choose to do this, we can keep the exceptions in the `Sat_solver_sig`, as long as we don't use them in the `Frontend` that the users will interact with.

* If we remove (or intend to — e.g. we could keep `process_decl` for the purpose of the internal solving loop for now) the `Frontend` module, and decide to make `Sat_solver_sig` the "official" interface, I think this PR should go a bit further than what it currently does and have `Sat / Unsat / I_dont_know` be the "public" type exposed by the solver, as mentioned in another message, so that the signatures are e.g. `val assume : t -> Expr.gformula -> Explanation.t -> t` (but `t` could be `Unsat`, in which case we do nothing).
I originally replied under the assumption we were going for the first option, but I think the second option may actually be closer to what @Halbaroth had in mind (and thinking about it more, it is probably the best option long-term, because it avoid one additional layer of wrapping).

I had the second option in mind. I agree the PR should remove the exceptions in the frontend but Util.Timeout. Removing Util.Timeout requires more works.

bclement-ocp · 2023-09-06T11:42:10Z

The preprocessing performed by the frontend is very light and could be instead provided as a (shared) helper module for both solvers.

Also, it feels weird to be able to send Unsat to the Frontend, this not only will require the sat solver to check its input, but it is just not well typed.

More precise types are not always desirable. As a user, if I have 5 formulas to add to my context, most of the time I don't really care if the context becomes inconsistent after I added 2 of them or 4 of them, I just care about the conjunction of all of them. If we expose the API you suggest, I have to do something like:

let extract = function
  | Unknown t -> t
  | Unsat expl -> raise (Unsat expl)
in
let t = extract @@ assume t fmla1 in
let t = extract @@ assume t fmla2 in
let t = extract @@ assume t fmla3 in
let t = extract @@ assume t fmla4 in
let t = extract @@ assume t fmla5 in
match unsat t with
| Sat _ | Unknown _ -> (* Do something appropriate *) ()
| Unsat expl -> raise (Unsat expl)

But if we hide from the user the fact that we can actually detect inconsistencies early (this will cause an "early" Unsat exception, before the user ever calls the unsat function), then I can write:

(* `assume` returns [ `I_dont_know of env | `Unsat of Explanation.t ] as an abstract type `t` *)
let t = assume t fmla1 in
let t = assume t fmla2 in
let t = assume t fmla3 in (* Maybe we detect an inconsistency between fmla1 and fmla3 here *)
let t = assume t fmla4 in
let t = assume t fmla5 in
unsat t (* Returns [ `Sat of env | `I_dont_know of env | `Unsat of Explanation.t ] *)

which is much more pleasant. And we can expose a function:

val is_inconsistent : t -> option Explanation.t

to be able to check whether an inconsistency was detected.

Stevendeo · 2023-09-06T12:00:47Z

The preprocessing performed by the frontend is very light and could be instead provided as a (shared) helper module for both solvers.

Also, it feels weird to be able to send Unsat to the Frontend, this not only will require the sat solver to check its input, but it is just not well typed.

More precise types are not always desirable. As a user, if I have 5 formulas to add to my context, most of the time I don't really care if the context becomes inconsistent after I added 2 of them or 4 of them, I just care about the conjunction of all of them. If we expose the API you suggest, I have to do something like:
let extract = function
  | Unknown t -> t
  | Unsat expl -> raise (Unsat expl)
in
let t = extract @@ assume t fmla1 in
let t = extract @@ assume t fmla2 in
let t = extract @@ assume t fmla3 in
let t = extract @@ assume t fmla4 in
let t = extract @@ assume t fmla5 in
match unsat t with
| Sat _ | Unknown _ -> (* Do something appropriate *) ()
| Unsat expl -> raise (Unsat expl)
But if we hide from the user the fact that we can actually detect inconsistencies early (this will cause an "early" Unsat exception, before the user ever calls the unsat function), then I can write:
(* `assume` returns [ `I_dont_know of env | `Unsat of Explanation.t ] as an abstract type `t` *)
let t = assume t fmla1 in
let t = assume t fmla2 in
let t = assume t fmla3 in (* Maybe we detect an inconsistency between fmla1 and fmla3 here *)
let t = assume t fmla4 in
let t = assume t fmla5 in
unsat t (* Returns [ `Sat of env | `I_dont_know of env | `Unsat of Explanation.t ] *)
which is much more pleasant. And we can expose a function:
val is_inconsistent : t -> option Explanation.t
to be able to check whether an inconsistency was detected.

I understand your point. Note that you can already create a syntactic sugar for your example :

let extract_and x f = match x with
  | Unknown t -> f t
  | Unsat expl -> raise (Unsat expl)

let (let*) = extract_and
 
let* t = assume t fmla1 in
let* t = assume t fmla2 in
let* t = assume t fmla3 in
let* t = assume t fmla4 in
let* t = assume t fmla5 in
unsat t

bclement-ocp · 2023-09-06T13:11:07Z

I understand your point. Note that you can already create a syntactic sugar for your example :

let extract_and x f = match x with
  | Unknown t -> f t
  | Unsat expl -> raise (Unsat expl)

let (let*) = extract_and
 
let* t = assume t fmla1 in
let* t = assume t fmla2 in
let* t = assume t fmla3 in
let* t = assume t fmla4 in
let* t = assume t fmla5 in
unsat t

True, but then I am also either forced to use exceptions (as I did in my example and you do here, but is what we were trying to avoid), or to live in a monad.

Stevendeo · 2023-09-06T13:35:48Z

Exceptions have now disapeared from both modules; the only remaining exceptions are used for debugging. I almost "purified" the whole API, but there still are few options dependencies left.

bclement-ocp · 2023-09-06T14:12:28Z

I had in mind that these changes would be mostly in the SAT solver modules rather than the frontend, sorry if I was not clear. But I suppose doing this in the frontend could work as well — at first glance this looks mostly OK, although I have not checked the new logic in detail.

I'll let @Halbaroth make a proper review since he mentioned in #789 (comment) that this part of the frontend changes a lot in OptimAE and will know better if this risk causing issues.

Halbaroth · 2023-09-06T14:29:39Z

I will review it tomorrow :)

Stevendeo · 2023-10-11T10:06:16Z

As this PR will not be compatible with the optimae changes, I created another branch from scratch, based on optimae, that reworks the frontend to make it more user-friendly. Should I close this PR and open another one, or recycle this one?

Removing Sat/Unsat/I_dont_know exceptions from the Sat solvers API

86286c3

bclement-ocp reviewed Sep 6, 2023

View reviewed changes

Remove bad comment

7e16334

Stevendeo force-pushed the non-failing-api branch from b3bb728 to 7e16334 Compare September 6, 2023 10:35

Call process_sat_res everywhere

ff318de

Halbaroth added this to the 2.6.0 milestone Sep 6, 2023

The frontend now exports all the SAT functions

90a0480

Style fix

e088ccd

Halbaroth self-assigned this Sep 6, 2023

Stevendeo marked this pull request as draft October 10, 2023 08:46

Stevendeo changed the title ~~Removing exceptions from the Sat solver API~~ [WIP] Removing exceptions from the Sat solver API Oct 10, 2023

Stevendeo closed this Oct 31, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[WIP] Removing exceptions from the Sat solver API #795

[WIP] Removing exceptions from the Sat solver API #795

Stevendeo commented Sep 6, 2023

bclement-ocp Sep 6, 2023

Stevendeo Sep 6, 2023

bclement-ocp Sep 6, 2023

Stevendeo Sep 6, 2023

bclement-ocp Sep 6, 2023

bclement-ocp Sep 6, 2023

bclement-ocp left a comment

bclement-ocp Sep 6, 2023

Stevendeo Sep 6, 2023

bclement-ocp Sep 6, 2023

Stevendeo Sep 6, 2023

bclement-ocp commented Sep 6, 2023 •

edited

Loading

Stevendeo commented Sep 6, 2023

bclement-ocp commented Sep 6, 2023

Stevendeo commented Sep 6, 2023 •

edited

Loading

Halbaroth commented Sep 6, 2023

bclement-ocp commented Sep 6, 2023

Stevendeo commented Sep 6, 2023 •

edited

Loading

bclement-ocp commented Sep 6, 2023

Stevendeo commented Sep 6, 2023 •

edited

Loading

bclement-ocp commented Sep 6, 2023

Halbaroth commented Sep 6, 2023

Stevendeo commented Oct 11, 2023

		(* Leaving this exception in case we actually raise Sat one day.
		Remember to update `safe_call` by catching this exception if you do. *)

[WIP] Removing exceptions from the Sat solver API #795

[WIP] Removing exceptions from the Sat solver API #795

Conversation

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

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

bclement-ocp commented Sep 6, 2023 • edited Loading

Stevendeo commented Sep 6, 2023

bclement-ocp commented Sep 6, 2023

Stevendeo commented Sep 6, 2023 • edited Loading

Halbaroth commented Sep 6, 2023

bclement-ocp commented Sep 6, 2023

Stevendeo commented Sep 6, 2023 • edited Loading

bclement-ocp commented Sep 6, 2023

Stevendeo commented Sep 6, 2023 • edited Loading

bclement-ocp commented Sep 6, 2023

Halbaroth commented Sep 6, 2023

Stevendeo commented Oct 11, 2023

bclement-ocp commented Sep 6, 2023 •

edited

Loading

Stevendeo commented Sep 6, 2023 •

edited

Loading

Stevendeo commented Sep 6, 2023 •

edited

Loading

Stevendeo commented Sep 6, 2023 •

edited

Loading