Fix model generation with SatML

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.
   ```
 
 ### Output

src/bin/common/parse_command.ml

@@ -923,58 +923,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

@@ -223,7 +223,7 @@ let main () =
     State.create_key ~pipe:"" "solving_state"
   in
 
-  let partial_model_key: SAT.t option State.key =
+  let partial_model_key: Models.t Lazy.t option State.key =
     State.create_key ~pipe:"" "sat_state"
   in
 
@@ -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"; _ } ->
@@ -461,20 +453,20 @@ let main () =
             List.rev (cnf :: hyps), is_thm
           | _ -> assert false
         in
-        let partial_model = solve all_context (cnf, name) in
+        let sat_env = solve all_context (cnf, name) in
         if is_thm
         then
           State.set solver_ctx_key (
             let solver_ctx = State.get solver_ctx_key st in
             { solver_ctx with global = []; local = [] }
           ) st
-          |> State.set partial_model_key partial_model
+          |> State.set partial_model_key (Option.bind sat_env SAT.get_model)
         else
           State.set solver_ctx_key (
             let solver_ctx = State.get solver_ctx_key st in
             { solver_ctx with local = [] }
           ) st
-          |> State.set partial_model_key partial_model
+          |> State.set partial_model_key (Option.bind sat_env SAT.get_model)
 
       | {contents = `Set_option
              { DStd.Term.term =
@@ -489,7 +481,10 @@ 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 (lazy model) ->
+            Models.output_concrete_model
+              (Options.Output.get_fmt_regular ()) model;
+            st
           | 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_regular ()) model
+    end
+
   let process_decl print_status used_context consistent_dep_stack
       ((env, consistent, dep) as acc) d =
     try
@@ -246,27 +270,33 @@ 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;*)
-      env, `Sat t, dep
+      print_model env (Some SAT.NoTimeout);
+      env , consistent, dep
     | SAT.Unsat dep' ->
       (* This case should mainly occur when a new assumption results in an unsat
          env, in which case we do not want to print status, since the correct
          status should be printed at the next query. *)
       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, `Unknown t, dep
+      env , `Unsat, dep
+    | SAT.I_dont_know {env; timeout} ->
+      (* TODO: always print Unknown for why3 ? *)
+      let status =
+        if timeout != NoTimeout then (Timeout (Some d))
+        else (Unknown (d, env))
+      in
+      print_status status (Steps.get_steps ());
+      print_model env (Some timeout);
+      (* TODO: Is it an appropriate behaviour? *)
+      (*       if timeout != NoTimeout then raise Util.Timeout; *)
+      env, `Unknown env, 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 =
@@ -477,28 +484,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 =
-  if ModelMap.(is_suspicious functions || is_suspicious constants
-               || is_suspicious arrays) then
+let output_concrete_model fmt m =
+  (* TODO: does we need to check also m.propositional ? *)
+  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 ->
@@ -508,9 +514,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, _) ->
@@ -520,12 +525,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