Add support for the get-info SMT-LIB2 command (#837)

This patch adds support for the `get-info` command in the SMT-LIB format.

src/bin/common/solving_loop.ml

@@ -50,6 +50,9 @@ let empty_solver_ctx = {
   global = [];
 }
 
+let unsupported_opt () =
+  Printer.print_std "unsupported"
+
 let main () =
   let () = Dolmen_loop.Code.init [] in
 
@@ -399,8 +402,52 @@ let main () =
       | ":produce-unsat-assumptions"
       | ":print-success"
       | ":random-seed"), _
-      -> Printer.print_wrn "unsupported option %s" name
-    | _ -> Printer.print_wrn "unsupported option %s" name
+      ->
+      unsupported_opt ();
+      Printer.print_wrn "unsupported option '%s'" name
+    | _ ->
+      unsupported_opt ();
+      Printer.print_err "unknown option '%s'" name
+  in
+
+  let handle_get_info (st : State.t) (name: string) =
+    let print_std =
+      fun (type a) (pp :a Fmt.t) (a : a) ->
+        Printer.print_std "(%s %a)" name pp a
+    in
+    let pp_reason_unknown st =
+      let err () =
+        let msg = "Invalid (get-info :reason-unknown)" in
+        Printer.print_smtlib_err "%s" msg
+      in
+      match State.get partial_model_key st with
+      | None -> err ()
+      | Some sat ->
+        match SAT.get_unknown_reason sat with
+        | None -> err ()
+        | Some s ->
+          print_std
+            Format.pp_print_string
+            (Frontend.unknown_reason_to_string s)
+    in
+    match name with
+    | ":authors" ->
+      print_std (fun fmt -> Fmt.pf fmt "%S") "Alt-Ergo developers"
+    | ":error-behavior" ->
+      print_std Fmt.string "immediate-exit"
+    | ":name" ->
+      print_std (fun fmt -> Fmt.pf fmt "%S") "Alt-Ergo"
+    | ":reason-unknown" ->
+      pp_reason_unknown st
+    | ":version" ->
+      print_std Fmt.string Version._version
+    | ":all-statistics"
+    | ":assertion-stack-levels" ->
+      unsupported_opt ();
+      Printer.print_wrn "unsupported option '%s'" name
+    | _ ->
+      unsupported_opt ();
+      Printer.print_err "unknown option '%s'" name
   in
 
   let handle_stmt :
@@ -504,6 +551,10 @@ let main () =
             st
           end
 
+      | {contents = `Get_info kind; _ } ->
+        handle_get_info st kind;
+        st
+
       | _ ->
         (* TODO:
            - Separate statements that should be ignored from unsupported

src/lib/frontend/frontend.ml

@@ -32,6 +32,21 @@ open Commands
 open Format
 open Options
 
+let timeout_reason_to_string = function
+  | Sat_solver_sig.Assume -> "Assume"
+  | ProofSearch -> "ProofSearch"
+  | ModelGen -> "ModelGen"
+
+let unknown_reason_to_string = function
+  | Sat_solver_sig.Incomplete -> "Incomplete"
+  | Memout -> "Memout"
+  | Timeout t -> Format.sprintf "Timeout:%s" (timeout_reason_to_string t)
+
+let unknown_reason_opt_to_string =
+  function
+  | None -> "Decided"
+  | Some r -> unknown_reason_to_string r
+
 module E = Expr
 module Ex = Explanation
 module type S = sig
@@ -154,27 +169,20 @@ 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 =
+  let print_model env unknown_reason_opt =
     if Options.(get_interpretation () && get_dump_models ()) then begin
-      let s = timeout_reason_to_string timeout in
+      let s = unknown_reason_opt_to_string unknown_reason_opt 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
+           or to increase your timeouts. Returned unknown reason = %s@]" s
 
       | Some (lazy model) ->
         Printer.print_fmt
           (Options.Output.get_fmt_diagnostic ())
-          "@[<v 0>; Returned timeout reason = %s@]" s;
+          "@[<v 0>; Returned unknown reason = %s@]" s;
         Models.output_concrete_model (Options.Output.get_fmt_models ()) model
     end
 
@@ -270,7 +278,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 ());
-      print_model env (Some SAT.NoTimeout);
+      print_model env None;
       env, `Sat t, dep
     | SAT.Unsat dep' ->
       (* This case should mainly occur when a new assumption results in an unsat
@@ -280,14 +288,16 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
       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 {env = t; timeout} ->
+    | SAT.I_dont_know t ->
       (* TODO: always print Unknown for why3 ? *)
+      let ur = SAT.get_unknown_reason t in
       let status =
-        if timeout != NoTimeout then (Timeout (Some d))
-        else (Unknown (d, t))
+        match ur with
+        | Some (Sat_solver_sig.Timeout _) -> Timeout (Some d)
+        | _ -> Unknown (d, t)
       in
       print_status status (Steps.get_steps ());
-      print_model t (Some timeout);
+      print_model t ur;
       (* TODO: Is it an appropriate behaviour? *)
       (*       if timeout != NoTimeout then raise Util.Timeout; *)
       env, `Unknown t, dep

src/lib/frontend/frontend.mli

@@ -63,3 +63,5 @@ module type S = sig
 end
 
 module Make (SAT: Sat_solver_sig.S) : S with type sat_env = SAT.t
+
+val unknown_reason_to_string : Sat_solver_sig.unknown_reason -> string

src/lib/reasoners/fun_sat.ml

@@ -176,6 +176,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     add_inst: E.t -> bool;
     unit_facts_cache : (E.gformula * Ex.t) ME.t ref;
     last_saved_model : Models.t Lazy.t option ref;
+    unknown_reason : Sat_solver_sig.unknown_reason option;
   }
 
   let reset_refs () =
@@ -192,25 +193,13 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     { env with
       unit_facts_cache = ref refs.unit_facts}, guard
 
-  (* Specify the pass in which Alt-Ergo runs out of time. This information
-     is used to decide if the last produced model is relevant. *)
-  type timeout_reason =
-    | NoTimeout
-    | Assume
-    (* Timeout while assuming a ground formula. *)
-
-    | ProofSearch
-    (* Timeout while doing instantiation or backtracking phases
-       during the proof search. *)
-
-    | ModelGen
-    (* Timeout while generating a new model. *)
-
   exception Sat of t
   exception Unsat of Explanation.t
-  exception I_dont_know of { env : t; timeout : timeout_reason }
+  exception I_dont_know of t
   exception IUnsat of Ex.t * SE.t list
 
+  let i_dont_know env ur =
+    raise (I_dont_know {env with unknown_reason = Some ur})
 
   (*BISECT-IGNORE-BEGIN*)
   module Debug = struct
@@ -1144,14 +1133,14 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
         raise (IUnsat (expl, classes))
     end
 
-  let update_model_and_return_unknown env compute_model ~timeout =
+  let update_model_and_return_unknown env compute_model ~unknown_reason =
     try
       let env = may_update_last_saved_model env compute_model in
       Options.Time.unset_timeout ();
-      raise (I_dont_know {env; timeout })
+      i_dont_know env unknown_reason
     with Util.Timeout when !(env.model_gen_phase) ->
       (* In this case, timeout reason becomes 'ModelGen' *)
-      raise (I_dont_know {env; timeout = ModelGen })
+      i_dont_know env (Timeout ModelGen)
 
   let model_gen_on_timeout env =
     let i = Options.get_interpretation () in
@@ -1160,7 +1149,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
        !(env.model_gen_phase) ||  (* we timeouted in model-gen-phase *)
        Stdlib.(=) ti 0. (* no time allocated for extra model search *)
     then
-      raise (I_dont_know {env; timeout = ProofSearch})
+      i_dont_know env (Timeout ProofSearch)
     else
       begin
         (* Beware: models generated on timeout of ProofSearch phase may
@@ -1170,7 +1159,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
         Options.Time.unset_timeout ();
         Options.Time.set_timeout ti;
         update_model_and_return_unknown
-          env i ~timeout:ProofSearch (* may becomes ModelGen *)
+          env i ~unknown_reason:(Timeout ProofSearch) (* may becomes ModelGen *)
       end
 
   let reduce_hypotheses tcp_cache tmp_cache env acc (hyp, gf, dep) =
@@ -1286,7 +1275,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
          this returns a wrong model. *)
       update_model_and_return_unknown
         env (Options.get_last_interpretation ())
-        ~timeout:NoTimeout (* may becomes ModelGen *)
+        ~unknown_reason:Incomplete (* may becomes ModelGen *)
     | IAuto | IGreedy ->
       let gre_inst =
         ME.fold
@@ -1314,7 +1303,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       else
         update_model_and_return_unknown
           env (Options.get_last_interpretation ())
-          ~timeout:NoTimeout (* may becomes ModelGen *)
+          ~unknown_reason:Incomplete (* may becomes ModelGen *)
 
   let normal_instantiation env try_greedy =
     Debug.print_nb_related env;
@@ -1763,8 +1752,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     | Util.Timeout ->
       (* don't attempt to compute a model if timeout before
          calling unsat function *)
-      raise (I_dont_know {env; timeout = Assume})
-
+      i_dont_know env (Timeout Assume)
 
   let pred_def env f name dep _loc =
     Debug.pred_def f;
@@ -1842,6 +1830,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       guards = init_guards ();
       add_inst = (fun _ -> true);
       last_saved_model = ref None;
+      unknown_reason = None;
     }
     in
     assume env gf_true Ex.empty
@@ -1856,6 +1845,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
   (** returns the latest model stored in the env if any *)
   let get_model env = !(env.last_saved_model)
 
+  let get_unknown_reason env = env.unknown_reason
+
   let reinit_ctx () =
     (* all_models_sat_env := None; *)
     (* latest_saved_env := None;

src/lib/reasoners/sat_solver_sig.ml

@@ -31,18 +31,22 @@
 (* We put an ml file for the module type, to avoid issues when
    building the lib *)
 
+type timeout_reason =
+  | Assume
+  | ProofSearch
+  | ModelGen
+
+type unknown_reason =
+  | Incomplete
+  | Memout
+  | Timeout of timeout_reason
+
 module type S = sig
   type t
 
-  type timeout_reason =
-    | NoTimeout
-    | Assume
-    | ProofSearch
-    | ModelGen
-
   exception Sat of t
   exception Unsat of Explanation.t
-  exception I_dont_know of { env : t; timeout : timeout_reason }
+  exception I_dont_know of t
 
   (* the empty sat-solver context *)
   val empty : unit -> t
@@ -82,6 +86,9 @@ module type S = sig
   (** [get_model t] produces the current model. *)
   val get_model: t -> Models.t Lazy.t option
 
+  (** [get_unknown_reason t] returns the reason Alt-Ergo raised
+      [I_dont_know] if it did. If it did not, returns None. *)
+  val get_unknown_reason : t -> unknown_reason option
 end
 
 

src/lib/reasoners/sat_solver_sig.mli

@@ -28,18 +28,22 @@
 (*                                                                        *)
 (**************************************************************************)
 
+type timeout_reason =
+  | Assume
+  | ProofSearch
+  | ModelGen
+
+type unknown_reason =
+  | Incomplete
+  | Memout
+  | Timeout of timeout_reason
+
 module type S = sig
   type t
 
-  type timeout_reason =
-    | NoTimeout
-    | Assume
-    | ProofSearch
-    | ModelGen
-
   exception Sat of t
   exception Unsat of Explanation.t
-  exception I_dont_know of { env : t; timeout : timeout_reason }
+  exception I_dont_know of t
 
   (** the empty sat-solver context *)
   val empty : unit -> t
@@ -83,6 +87,9 @@ module type S = sig
   (** [get_model t] produces the current model. *)
   val get_model: t -> Models.t Lazy.t option
 
+  (** [get_unknown_reason t] returns the reason Alt-Ergo raised
+      [I_dont_know] if it did. If it did not, returns None. *)
+  val get_unknown_reason : t -> unknown_reason option
 end