Model generation support for SatML (#829)

* Theory: harden 'compute_concrete_model' function

* Push the test 'get_case_split_policy() == origin' into Theory.do_case_split

* CS: functions return all the env instead of just 'gamma_finite'.

* Fun_sat: refactor the way models are handled/printed

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

* satML: add missing case-split strategies

* satML: implement models generation.

* Make model tests negative

Some tests about models failed in the OptimAE PR.
This commit allows to tag tests in `tests/` with `fail` tag
which means the test is supposed to fail.

* Reindent

* Update documentation about `output_concrete_model`

I also remove the mention about the different kind of formats used
to print models. Indeed, we use only the SMT-LIB format and
the Why3 format is slightly different but probably outdated.

* Document the timeout_reason ADT

* poetry

* Restore the comment about `reinit_cpt`

* Fix spelling

* Remainder to the issue 834

* Simplify get-model processing

* Remove SAT solver choices while model generating

As SatML supports model generation, we don't need to select
the appropriate SAT solver while parsing the command line or
the SMT-LIB statement `(set-option :produce-models true)`.

* Fix model output

We should print constraints in models only if the appropriate flag is
used in the command line.

* All the model tests are positive

* Remove deprecated cram tests

Some cram tests are not valid anymore as we don't need to select the SAT
solver Tableaux while generating models.

* Test models with all the SAT solvers

* Restoring dump-models option

The dump-models option have been broken by the refactoring in OptimAE.
I restore this feature.

* Use the right post-solve SAT environment for models

Return the appropriate environment in the Frontend module to
retrieve the model with `(get-model)` as we did in the PR #789.

* Print dump models on the channel models

This commit restore the feature of the PR #838 as the
location of code moved after the refactoring of model generation in
OptimAE.

* Prevent printing internal names in models

Symbol names prefixed with a dot or @ shouldn't never be printed
in models as they cannot be declared by the user.

This behaviour is SMT-LIB compliant.

* Promote tests

* Revert "Simplify get-model processing"

This reverts commit 9507d63.

* Review changes

* Test only models with FunSAT

Prevent to test models with other solvers as we cannot
guarantee they will produce exactly the same model.
We have to modify gentest to manage several expected files while
testing models.

---------

Co-authored-by: iguer <[email protected]>

docs/sphinx_docs/Usage/index.md

@@ -51,8 +51,8 @@ Model generation is disabled by default. There are two recommended ways to enabl
   on demand using the statement `(get-model)`.
 
   Alternatively, you can enable model generation using the statement
-  `(set-option :produce-models true)`. This currently requires using the options
-  `--sat-solver tableaux` and `--frontend dolmen`.
+  `(set-option :produce-models true)`. This currently requires using the option
+  `--frontend dolmen`.
 
 #### Examples
 
@@ -142,7 +142,7 @@ Model generation is disabled by default. There are two recommended ways to enabl
    (get-model)
 
   ```
-  and the command `alt-ergo --frontend dolmen --sat-solver tableaux INPUT.smt2` produces
+  and the command `alt-ergo --frontend dolmen INPUT.smt2` produces
   the output model
   ```
   unknown
@@ -154,10 +154,8 @@ Model generation is disabled by default. There are two recommended ways to enabl
   ```
 
   ```{admonition} Note
-  You need to select the Dolmen frontend and the SAT solver Tableaux as the
-  model generation is not supported yet by the other SAT solvers. The options
-  `--dump-models` and `--produce-models` select the right frontend and SAT solver
-  for you.
+  You need to select the Dolmen frontend. The options `--dump-models` and
+  `--produce-models` select the right frontend for you.
   ```
 
   - As a more didactic example, let us imagine while checking the loop invariant

src/bin/common/parse_command.ml

@@ -943,58 +943,38 @@ let parse_output_opt =
     frontend
   in
 
-  (* Use the --sat-solver to determine the sat solver.
-
-     If an interpretation is provided, the solver is forced to be Tableaux,
-     because generation of models requires OptimAE for the other solvers.
-
-     See https://github.com/OCamlPro/alt-ergo/pull/553 *)
+  (* Use the --sat-solver to determine the sat solver. *)
   let sat_solver =
-    let sat_solver_arg =
-      let sat_solver : _ Arg.conv =
-        let parse = function
-          | "CDCL" | "satML" ->
-            Ok Util.CDCL
-          | "CDCL-Tableaux" | "satML-Tableaux"
-          | "CDCL-tableaux" | "satML-tableaux" ->
-            Ok Util.CDCL_Tableaux
-          | "tableaux" | "Tableaux"
-          | "tableaux-like" | "Tableaux-like" ->
-            Ok Util.Tableaux
-          | "tableaux-cdcl" | "Tableaux-CDCL"
-          | "tableaux-CDCL" | "Tableaux-cdcl" ->
-            Ok Util.Tableaux_CDCL
-          | sat_solver ->
-            Error ("Args parsing error: unkown SAT solver " ^ sat_solver)
+    let sat_solver : _ Arg.conv =
+      let parse = function
+        | "CDCL" | "satML" ->
+          Ok Util.CDCL
+        | "CDCL-Tableaux" | "satML-Tableaux"
+        | "CDCL-tableaux" | "satML-tableaux" ->
+          Ok Util.CDCL_Tableaux
+        | "tableaux" | "Tableaux"
+        | "tableaux-like" | "Tableaux-like" ->
+          Ok Util.Tableaux
+        | "tableaux-cdcl" | "Tableaux-CDCL"
+        | "tableaux-CDCL" | "Tableaux-cdcl" ->
+          Ok Util.Tableaux_CDCL
+        | sat_solver ->
+          Error ("Args parsing error: unkown SAT solver " ^ sat_solver)
 
-        in
-        Arg.(conv' (parse, Util.pp_sat_solver))
       in
-      let default, sum_up = "CDCL-Tableaux", "satML" in
-      let doc = Format.sprintf
-          "Choose the SAT solver to use. Default value is %s (i.e. %s\
-           solver). Possible options are %s."
-          default sum_up
-          (Arg.doc_alts ["CDCL"; "satML"; "CDCL-Tableaux";
-                         "satML-Tableaux"; "Tableaux-CDCL"])
-      in
-      let docv = "SAT" in
-      Arg.(value & opt (some ~none:default sat_solver) None &
-           info ["sat-solver"] ~docv ~docs:s_sat ~doc)
+      Arg.(conv' (parse, Util.pp_sat_solver))
     in
-
-    let mk_sat_solver sat_solver interpretation =
-      match interpretation, sat_solver with
-      | INone, None -> Ok Util.CDCL_Tableaux
-      | INone, Some sat_solver -> Ok sat_solver
-      | _, (None | Some Util.Tableaux) -> Ok Tableaux
-      | _, Some sat_solver ->
-        Fmt.error
-          "solver '%a' does not suppot model generation"
-          Util.pp_sat_solver sat_solver
+    let default, sum_up = "CDCL-Tableaux", "satML" in
+    let doc = Format.sprintf
+        "Choose the SAT solver to use. Default value is %s (i.e. %s\
+         solver). Possible options are %s."
+        default sum_up
+        (Arg.doc_alts ["CDCL"; "satML"; "CDCL-Tableaux";
+                       "satML-Tableaux"; "Tableaux-CDCL"])
     in
-    Term.term_result' @@
-    Term.(const mk_sat_solver $ sat_solver_arg $ interpretation)
+    let docv = "SAT" in
+    Arg.(value & opt sat_solver Util.CDCL_Tableaux &
+         info ["sat-solver"] ~docv ~docs:s_sat ~doc)
   in
 
   let cdcl_tableaux_inst =

src/bin/common/solving_loop.ml

@@ -358,15 +358,7 @@ let main () =
       Options.Output.create_channel name
       |> Options.Output.set_diagnostic
     | ":produce-models", Symbol { name = Simple "true"; _ } ->
-      (* TODO: The generation of models is supported only with the SAT
-         solver Tableaux. Remove this line after merging the OptimAE
-         PR. See https://github.com/OCamlPro/alt-ergo/pull/553 *)
-      if Stdlib.(Options.get_sat_solver () = Tableaux) then
-        Options.set_interpretation ILast
-      else
-        Printer.print_smtlib_err
-          "Model generation requires the Tableaux solver \
-           (try --produce-models)";
+      Options.set_interpretation ILast
     | ":produce-models", Symbol { name = Simple "false"; _ } ->
       Options.set_interpretation INone
     | ":produce-unsat-cores", Symbol { name = Simple "true"; _ } ->
@@ -489,7 +481,17 @@ let main () =
       | {contents = `Get_model; _ } ->
         if Options.get_interpretation () then
           match State.get partial_model_key st with
-          | Some partial_model -> SAT.get_model partial_model; st
+          | Some partial_model ->
+            begin
+              match SAT.get_model partial_model with
+              | Some (lazy model) ->
+                Models.output_concrete_model
+                  (Options.Output.get_fmt_regular ()) model;
+                st
+              | _ ->
+                (* TODO: is it reachable? *)
+                st
+            end
           | None ->
             (* TODO: add the location of the statement. *)
             Printer.print_smtlib_err "No model produced.";

src/lib/frontend/frontend.ml

@@ -154,6 +154,30 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
     if Options.get_unsat_core () then Ex.singleton (Ex.RootDep {name;f;loc})
     else Ex.empty
 
+  let timeout_reason_to_string = function
+    | None -> "(?)"
+    | Some SAT.NoTimeout -> "NoTimeout"
+    | Some SAT.Assume -> "Assume"
+    | Some SAT.ProofSearch -> "ProofSearch"
+    | Some SAT.ModelGen -> "ModelGen"
+
+  let print_model env timeout =
+    if Options.(get_interpretation () && get_dump_models ()) then begin
+      let s = timeout_reason_to_string timeout in
+      match SAT.get_model env with
+      | None ->
+        Printer.print_fmt (Options.Output.get_fmt_diagnostic ())
+          "@[<v 0>It seems that no model has been computed so \
+           far. You may need to change your model generation strategy \
+           or to increase your timeouts. Returned timeout reason = %s@]" s
+
+      | Some (lazy model) ->
+        Printer.print_fmt
+          (Options.Output.get_fmt_diagnostic ())
+          "@[<v 0>; Returned timeout reason = %s@]" s;
+        Models.output_concrete_model (Options.Output.get_fmt_models ()) model
+    end
+
   let process_decl print_status used_context consistent_dep_stack
       ((env, consistent, dep) as acc) d =
     try
@@ -246,7 +270,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
       (* This case should mainly occur when a query has a non-unsat result,
          so we want to print the status in this case. *)
       print_status (Sat (d,t)) (Steps.get_steps ());
-      (*if get_model () then SAT.print_model ~header:true (get_fmt_mdl ()) t;*)
+      print_model env (Some SAT.NoTimeout);
       env, `Sat t, dep
     | SAT.Unsat dep' ->
       (* This case should mainly occur when a new assumption results in an unsat
@@ -255,18 +279,24 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
       let dep = Ex.union dep dep' in
       if get_debug_unsat_core () then check_produced_unsat_core dep;
       (* print_status (Inconsistent d) (Steps.get_steps ()); *)
-      env, `Unsat, dep
-    | SAT.I_dont_know t ->
-      (* In this case, it's not clear whether we want to print the status.
-         Instead, it'd be better to accumulate in `consistent` a 3-case adt
-         and not a simple bool. *)
-      print_status (Unknown (d, t)) (Steps.get_steps ());
-      (*if get_model () then SAT.print_model ~header:true (get_fmt_mdl ()) t;*)
+      env , `Unsat, dep
+    | SAT.I_dont_know {env = t; timeout} ->
+      (* TODO: always print Unknown for why3 ? *)
+      let status =
+        if timeout != NoTimeout then (Timeout (Some d))
+        else (Unknown (d, t))
+      in
+      print_status status (Steps.get_steps ());
+      print_model t (Some timeout);
+      (* TODO: Is it an appropriate behaviour? *)
+      (*       if timeout != NoTimeout then raise Util.Timeout; *)
       env, `Unknown t, dep
+
     | Util.Timeout as e ->
       (* In this case, we obviously want to print the status,
          since we exit right after  *)
       print_status (Timeout (Some d)) (Steps.get_steps ());
+      print_model env None;
       raise e
 
   let print_status status steps =

src/lib/frontend/models.ml

@@ -45,6 +45,13 @@ module MX = Shostak.MXH
 
 let constraints = ref MS.empty
 
+type t = {
+  propositional : Expr.Set.t;
+  constants : ModelMap.t;
+  functions : ModelMap.t;
+  arrays : ModelMap.t;
+}
+
 module Pp_smtlib_term = struct
 
   let to_string_type t =
@@ -483,29 +490,27 @@ 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 props ~functions ~constants ~arrays =
+let output_concrete_model fmt m =
   SmtlibCounterExample.reset_counter ();
-  if ModelMap.(is_suspicious functions || is_suspicious constants
-               || is_suspicious arrays) then
+  if ModelMap.(is_suspicious m.functions || is_suspicious m.constants
+               || is_suspicious m.arrays) then
     Format.fprintf fmt "; This model is a best-effort. It includes symbols
         for which model generation is known to be incomplete. @.";
 
   Format.fprintf fmt "@[<v 2>(";
-  if Options.get_model_type_constraints () then
-    begin
-      Why3CounterExample.output_constraints fmt props;
-      Format.fprintf fmt "@ ; values"
-    end;
+  if Options.get_model_type_constraints () then begin
+    Why3CounterExample.output_constraints fmt m.propositional
+  end;
 
   let values = Hashtbl.create 17 in
   (* Add the constants *)
   ModelMap.iter (fun (f, xs_ty, _) st ->
       assert (Lists.is_empty xs_ty);
-
       ModelMap.V.iter (fun (keys, (value_r, value_s)) ->
           assert (Lists.is_empty keys);
-          Hashtbl.add values f (value (value_r, value_s)))
-        st) constants;
+          Hashtbl.add values f (value (value_r, value_s))
+        ) st
+    ) m.constants;
 
   (* Add the arrays values, when applicable *)
   ModelMap.iter (fun (f, xs_ty, ty) st ->
@@ -515,9 +520,8 @@ let output_concrete_model fmt props ~functions ~constants ~arrays =
       in
       Hashtbl.replace values f @@
       ModelMap.V.fold (fun (keys, rs) acc ->
-          Store (acc, value (snd (List.hd keys)), value rs))
-        st root)
-    arrays;
+          Store (acc, value (snd (List.hd keys)), value rs)) st root
+    ) m.arrays;
 
   let pp_value =
     pp_value (fun ppf (sy, _) ->
@@ -527,12 +531,16 @@ let output_concrete_model fmt props ~functions ~constants ~arrays =
   let pp_x ppf xs = pp_value ppf (value xs) in
 
   (* Functions *)
-  let records = SmtlibCounterExample.output_functions_counterexample
-      pp_x fmt  MS.empty functions
+  let records =
+    SmtlibCounterExample.output_functions_counterexample
+      pp_x fmt MS.empty m.functions
   in
 
   (* Constants *)
   SmtlibCounterExample.output_constants_counterexample
-    pp_x fmt records constants;
+    pp_x fmt records m.constants;
+
+  (* Arrays *)
+  (*     SmtlibCounterExample.output_arrays_counterexample fmt m.arrays; *)
 
   Printer.print_fmt fmt "@]@,)";

src/lib/frontend/models.mli

@@ -30,16 +30,13 @@
 
 (** {1 Models module} *)
 
-(** Print the given counterexample on the given formatter with the
-    corresponding format set with Options.get_output_format.
-    - functions: the functions of the model;
-    - constants: the variables of the model;
-    - arrays: (experimental) the arrays of the model.
-*)
-val output_concrete_model :
-  Format.formatter ->
-  Expr.Set.t ->
-  functions:ModelMap.t ->
-  constants:ModelMap.t ->
-  arrays:ModelMap.t ->
-  unit
+type t = {
+  propositional : Expr.Set.t;
+  constants : ModelMap.t;
+  functions : ModelMap.t;
+  arrays : ModelMap.t;
+}
+
+val output_concrete_model : t Fmt.t
+(** [output_concrete_model ppf mdl] prints the model [mdl] on
+    the formatter [ppf]. *)

src/lib/reasoners/ccx.ml

@@ -85,11 +85,11 @@ module type S = sig
     Matching_types.info Expr.Map.t * Expr.t list Expr.Map.t Symbols.Map.t ->
     t -> (Expr.t -> Expr.t -> bool) -> t * Sig_rel.instances
 
-  val output_concrete_model :
-    Format.formatter ->
+  val extract_concrete_model :
     prop_model:Expr.Set.t ->
     t ->
-    unit
+    Models.t Lazy.t option
+
 end
 
 module Main : S = struct
@@ -738,7 +738,6 @@ module Main : S = struct
     in
     Uf.term_repr env.uf t
 
-  let output_concrete_model fmt ~prop_model env =
-    Uf.output_concrete_model fmt ~prop_model env.uf
-
+  let extract_concrete_model ~prop_model env =
+    Uf.extract_concrete_model ~prop_model env.uf
 end

src/lib/reasoners/ccx.mli

@@ -76,11 +76,10 @@ module type S = sig
     Matching_types.info Expr.Map.t * Expr.t list Expr.Map.t Symbols.Map.t ->
     t -> (Expr.t -> Expr.t -> bool) -> t * Sig_rel.instances
 
-  val output_concrete_model :
-    Format.formatter ->
+  val extract_concrete_model :
     prop_model:Expr.Set.t ->
     t ->
-    unit
+    Models.t Lazy.t option
 end
 
 module Main : S