feat: check-all-sat support #846

Halbaroth · 2023-09-29T09:59:42Z

This PR adds the support for the check-all-sat support. I think we can merge the PR without clean-up its implementation as the feature doesn't break the classical model generation. Please see #847 for a clean-up roadmap of this feature.

The PR includes two ways to use this new feature:

using the new CLI option --all-sat (or --all-models), AE produces all the possible propositional models after each check-sat.
For instance using the input file:

(set-logic ALL)
(declare-const x Bool)
(declare-const y Bool)
(declare-const z Bool)
(assert (or x y))
(assert (or (not y) z))
(check-sat)

and the command dune exec -- alt-ergo --all-sat --produce-models --sat-solver CDCL test.smt2, we got the output:

output of the command

                                
; File "test.smt2", line 7, characters 1-12: I don't know (0.4635) (7 steps) (goal g_1)
unknown

; Returned timeout reason = NoTimeout

(

(define-fun x () Bool true)

(define-fun y () Bool false)

(define-fun z () Bool false)

)
; File "test.smt2", line 7, characters 1-12: I don't know (0.4636) (13 steps) (goal g_1)
unknown

; Returned timeout reason = NoTimeout

(

(define-fun x () Bool false)

(define-fun y () Bool true)

(define-fun z () Bool true)

)
; File "test.smt2", line 7, characters 1-12: I don't know (0.4637) (17 steps) (goal g_1)
unknown

; Returned timeout reason = NoTimeout

(

(define-fun x () Bool true)

(define-fun y () Bool false)

(define-fun z () Bool true)

)
; File "test.smt2", line 7, characters 1-12: I don't know (0.4638) (23 steps) (goal g_1)
unknown

; Returned timeout reason = NoTimeout

(

(define-fun x () Bool true)

(define-fun y () Bool true)

(define-fun z () Bool true)

)
; File "test.smt2", line 7, characters 1-12: Valid (0.4638) (23 steps) (goal g_1)
unsat

A new keyword check-all-sat is available in the SMT-LIB input language only. For instance

(set-logic ALL)
(declare-const x Bool)
(declare-const y Bool)
(declare-const z Bool)
(assert (or x y))
(assert (or (not y) z))
(check-all-sat x y)

with the command dune exec -- alt-ergo --produce-models --sat-solver CDCL --frontend legacy test.smt2
outputs

output of the commad

; File "test.smt2", line 7, characters 1-20: I don't know (0.0003) (7 steps) (goal g_1)
unknown

; Returned timeout reason = NoTimeout

(

(define-fun x () Bool true)

(define-fun y () Bool false)

(define-fun z () Bool false)

)
; File "test.smt2", line 7, characters 1-20: I don't know (0.0005) (14 steps) (goal g_1)
unknown

; Returned timeout reason = NoTimeout

(

(define-fun x () Bool false)

(define-fun y () Bool true)

(define-fun z () Bool true)

)
; File "test.smt2", line 7, characters 1-20: I don't know (0.0005) (16 steps) (goal g_1)
unknown

; Returned timeout reason = NoTimeout

(

(define-fun x () Bool true)

(define-fun y () Bool true)

(define-fun z () Bool true)

)
; File "test.smt2", line 7, characters 1-20: Valid (0.0006) (16 steps) (goal g_1)
unsat

This feature is clearly more interesting as you can choose for which literals you want all the boolean models.

The PR includes also another option to print a boolean model while printing the first-order model. The feature is broken but I can restore it easily. I'm not sure if the option is really useful, at least while using the SMT-LIB input language, as there is a standard way to obtain this feature (in fact a more general feature), see #844. We should deprecate the option or reserve it for the native input language.

Some important remarks about the feature:

The feature doesn't work properly with the tableaux solver. The reason is simple and I actually ran into this issue while testing outputted models with the Tableaux solver. I have a solution that I will explain in details in an appropriate issue.
The solver outputs unsat at the end because it exhausted all the possible boolean models. This answer leaks the way AE works under the hood. I guess the best solution consists to print a comment telling we have exhausted all the boolean models. But fixing this issue will be easier after fixing Bubble decision of printing models upwards #833.

- add a data-structure for models, - save the strucutre in the SAT's env - print the models in the Frontend module

all_models: reset last saved model before exploring other branches all_models: re-set timelimit, which is inteded to be used per SAT branch/model in this case print_status: Unknown instead of Timeout if get_interpretation && why3 output continue models enumeration after a Timeout avoid infinite loop in case no progression is made in all-models enumeration do not support check-all-sat/all-models in Fun_SAT

Stevendeo · 2023-09-29T16:33:15Z

src/bin/js/worker_js.ml

@@ -145,7 +145,107 @@ let main worker_id content =
        begin match kind with
          | Ty.Check
          | Ty.Cut -> { state with local = []; }
-          | Ty.Thm | Ty.Sat -> { state with global = []; local = []; }
+          | Ty.Thm | Ty.Sat | Ty.AllSat _ ->


There seems to be twice the same code here. Why the duplication?

Stevendeo · 2023-09-29T16:33:32Z

src/bin/text/main_text.ml

@@ -40,6 +40,7 @@ let parse_cmdline () =
  try Parse_command.parse_cmdline_arguments ()
  with Parse_command.Exit_parse_command i -> exit i

+


Remove this line

Stevendeo · 2023-09-29T16:39:50Z

src/lib/frontend/frontend.ml

+      timeout_kind =
+    match d.st_decl with
+    | Assume _ | PredDef _ | RwtDef _ | Push _ | Pop _ | ThAssume _->
+      (* cannot raise Sat or Unknown in this case *)


Can't alt-ergo Timeout during one of these steps?

Stevendeo · 2023-09-29T16:40:34Z

src/lib/frontend/frontend.ml

+                     E.Set.add t acc
+                  )E.Set.empty l)
+
+        | Thm | Sat ->


| Thm | Sat when Options.get_all_models ()

Stevendeo · 2023-09-29T16:43:12Z

src/lib/frontend/frontend.ml

+               (for instance, in case of timeout and no model computed
+               so far). We should stop to avoid infinite loop *)
+            if timeout_kind != NoTimeout then raise Util.Timeout;
+            (* TODO: is it the appropriate status? *)


I don't know, is it?

Stevendeo · 2023-09-29T16:43:32Z

src/lib/frontend/frontend.ml

+        (* 2. default case + case where a simple interpretation is
+           requested *)
+        print_model t (Some timeout_kind);
+        (* TODO: is it the appropriate status? *)


I don't know, is it?

Stevendeo · 2023-09-29T16:44:22Z

src/lib/frontend/models.ml

@@ -490,7 +490,7 @@ let rec pp_value ppk ppf = function
 let pp_constant ppf (_sy, t) =
  Fmt.pf ppf "%a" SmtlibCounterExample.pp_abstract_value_of_type t

-let output_concrete_model fmt m =
+let output_concrete_model ~pp_prop_model:_ fmt m =


Can't you remove this argument?

Stevendeo · 2023-09-29T16:47:39Z

src/lib/structures/ty.mli

@@ -286,6 +286,9 @@ type goal_sort =
  (** The goal to be proved valid *)
  | Sat
  (** The goal to be proved satisfiable *)
+  | AllSat of string list
+  (** Rather generate all models involving the given list of


Why 'Rather'?

bclement-ocp · 2023-10-02T10:26:55Z

Before reviewing the code in detail, I want to better understand what we are trying to achieve with that feature, so I will only make high-level remarks here.

It was my understanding that this feature was required for OptimAE. After looking at the code, it doesn't appear to be the case, as OptimAE uses a different mechanism to iterate over the propositional models for optimization (in fact, in the OptimAE branch, the all-models feature has been implemented after the rest of the optimization work). Given that OptimAE does not need this feature, and that it is actually fairly small and self-contained (all changes but those in frontend.ml seem to be trivial plumbing), we can evaluate the feature on its own merit without rushing to merge the implementation as-is.

As an aside, this feature was initially implemented for an unnamed intern project in 2011, dropped during the development of OptimAE (the removal was merged in #530) and then re-implemented later --- but if I had to wager, without that one-day hack in 2011, it would not have been implemented in OptimAE.

With that out of the way, I am not sure we want to merge this at all. I don't think there is much value in enumerating propositional models rather than actual models in general (in part because having a propositional model does not guarantee that a corresponding model of the input formula exists), and if we care about models, then model enumeration can be implemented outside the solver.

The typical way to implement model enumeration uses incremental solving: first get a model using (check-sat), get the value of the propositional term(s) you are interested in with (get-assignment) (see #844), assert that one of them should be false, then call (check-sat) again and repeat until you get unsat. Replace (check-sat) and (get-assignment) by the appropriate (incremental) API calls if not using SMT-LIB input.

I agree that providing this loop in a built-in way would be useful (in fact, the current implementation uses the exact loop I described above), but given that there is no rush for the feature I think it would be better to first clean up the interface to be able to do proper incremental solving (rather than giving a single list of commands and we're done, as we discussed) and to implement this feature on top of the incremental solving API once it exists (I think the relevant issue is #382 ).

Edit: as a side note, we should all this check-allsat rather than check-all-sat when using SMT-LIB to be compatible with MathSat5, see bottom of https://mathsat.fbk.eu/smt2examples.html

Halbaroth · 2023-10-04T15:02:27Z

I agree to postpone this feature until we have a sufficient support for incremental mode.

iguerNL and others added 6 commits September 29, 2023 11:51

Fun_sat: refactor the way models are handled/printed

7804408

- add a data-structure for models, - save the strucutre in the SAT's env - print the models in the Frontend module

Simplify get-model processing

3a07c8e

Move --all-models option in the MODEL section

bd79ad0

Some todo comments

3b6ddfd

Move show-prop-model in the MODEL section

aee063a

Halbaroth added enhancement models This issue is related to model generation. labels Sep 29, 2023

Halbaroth changed the title ~~Feat: check-all-sat support~~ feat: check-all-sat support Sep 29, 2023

Halbaroth mentioned this pull request Sep 29, 2023

clean-up: check-all-sat feature #847

Open

9 tasks

Run the linter

a6fe1b9

Halbaroth marked this pull request as ready for review September 29, 2023 10:29

Halbaroth requested a review from bclement-ocp September 29, 2023 10:29

Stevendeo reviewed Sep 29, 2023

View reviewed changes

Halbaroth added the backlog label Oct 4, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: check-all-sat support #846

feat: check-all-sat support #846

Halbaroth commented Sep 29, 2023 •

edited

Loading

Stevendeo Sep 29, 2023

Stevendeo Sep 29, 2023

Stevendeo Sep 29, 2023

Stevendeo Sep 29, 2023

Stevendeo Sep 29, 2023

Stevendeo Sep 29, 2023

Stevendeo Sep 29, 2023

Stevendeo Sep 29, 2023

bclement-ocp commented Oct 2, 2023 •

edited

Loading

Halbaroth commented Oct 4, 2023

		@@ -40,6 +40,7 @@ let parse_cmdline () =
		try Parse_command.parse_cmdline_arguments ()
		with Parse_command.Exit_parse_command i -> exit i

feat: check-all-sat support #846

Are you sure you want to change the base?

feat: check-all-sat support #846

Conversation

Halbaroth commented Sep 29, 2023 • 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 Oct 2, 2023 • edited Loading

Halbaroth commented Oct 4, 2023

Halbaroth commented Sep 29, 2023 •

edited

Loading

bclement-ocp commented Oct 2, 2023 •

edited

Loading