Poetry

src/bin/common/solving_loop.ml

@@ -51,7 +51,7 @@ let empty_solver_ctx = {
 }
 
 let unsupported_opt s =
-  Printer.print_wrn "unsupported option %s" s
+  Printer.print_wrn "unsupported option %S" s
 
 let main () =
   let () = Dolmen_loop.Code.init [] in
@@ -415,44 +415,45 @@ let main () =
   in
 
   let pp_reason_unknown fmt st =
+    let err () =
+      let msg = "Invalid (get-info :reason-unknown)" in
+      Printer.print_err "%s" msg;
+      Format.fprintf fmt "(error %S)" msg
+    in
     match State.get partial_model_key st with
     | None ->
       (* This case should happen only when there is no check-sat before
          a get-info statement. *)
-      Printer.print_err "Invalid (get-info :reason-unknown)";
-      Format.fprintf fmt ""
+      err ()
     | Some sat ->
       match SAT.get_unknown_reason sat with
-      | None ->
-        Printer.print_err "Invalid (get-info :reason-unknown)";
-        Format.fprintf fmt ""
-      | Some s ->
-        Format.pp_print_string fmt s
+      | None -> err ()
+      | Some s -> Format.pp_print_string fmt s
   in
 
   let handle_get_info (st : State.t) (kind: string) =
     let print_std =
       fun (type a) (pp :(Format.formatter -> a -> unit)) (a : a) ->
-        Printer.print_std "(%s \"%a\")" kind pp a
+        Printer.print_std "(%s %a)" kind pp a
     in
     match kind with
     | ":authors" ->
-      print_std Format.pp_print_string "Alt-Ergo developers"
+      print_std (fun fmt -> Format.fprintf fmt "%S") "Alt-Ergo developers"
     | ":error-behavior" ->
       print_std Format.pp_print_string "immediate-exit"
     | ":name" ->
-      print_std Format.pp_print_string "alt-ergo"
+      print_std (fun fmt -> Format.fprintf fmt "%S") "alt-ergo"
     | ":reason-unknown" ->
       print_std pp_reason_unknown st
     | ":version" ->
       print_std Format.pp_print_string Version._version
     | ":all-statistics"
     | ":assertion-stack-levels" ->
       unsupported_opt kind;
-      print_std Format.pp_print_string "-- unsupported --"
+      print_std Format.pp_print_string "unsupported"
     | _ ->
-      Printer.print_wrn "unknown option %s" kind;
-      print_std Format.pp_print_string "-- unknown option --"
+      Printer.print_wrn "unknown option %S" kind;
+      print_std Format.pp_print_string "unsupported"
 
   in
 

src/lib/reasoners/fun_sat.ml

@@ -175,7 +175,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     guards : guards;
     add_inst: E.t -> bool;
     unit_facts_cache : (E.gformula * Ex.t) ME.t ref;
-    ur : Sat_solver_sig.unknown_reason option;
+    unknown_reason : Sat_solver_sig.unknown_reason option;
+    (** The reason why fun_sat raised I_dont_know f it does; None by default. *)
   }
 
   let latest_saved_env = ref None
@@ -203,7 +204,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
   exception IUnsat of Ex.t * SE.t list
 
   let i_dont_know ur env =
-    raise (I_dont_know {env with ur = Some ur})
+    raise (I_dont_know {env with unknown_reason = Some ur})
 
   (*BISECT-IGNORE-BEGIN*)
   module Debug = struct
@@ -1336,12 +1337,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       return_answer
         env
         (Options.get_last_interpretation ())
-        (fun e ->
-           i_dont_know
-             "I won't conclude 'SAT' because I am not sure, hence \
-              I conclude 'Unknown'."
-             e
-        )
+        (i_dont_know "incomplete")
     | IAuto | IGreedy ->
       let gre_inst =
         ME.fold
@@ -1368,12 +1364,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       if ok1 || ok2 || ok3 || ok4 then env
       else
         return_answer env (Options.get_last_interpretation ())
-          (fun e ->
-             i_dont_know
-               "I won't conclude 'SAT' because I am not sure, hence \
-                I conclude 'Unknown'."
-               e
-          )
+          (i_dont_know "incomplete")
 
   let normal_instantiation env try_greedy =
     try
@@ -1909,7 +1900,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       unit_facts_cache = ref ME.empty;
       guards = init_guards ();
       add_inst = (fun _ -> true);
-      ur = None;
+      unknown_reason = None;
     }
     in
     assume env gf_true Ex.empty
@@ -1949,7 +1940,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       env.tbox;
     terminated_normally := true
 
-  let get_unknown_reason env = env.ur
+  let get_unknown_reason env = env.unknown_reason
 
   let () =
     Steps.save_steps ();

src/lib/reasoners/sat_solver_sig.ml

@@ -80,7 +80,7 @@ module type S = sig
   (** [get_model t] produces the current model. *)
   val get_model : t -> unit
 
-  (** [get_unknown_reason t] returns the reason Alt-Ergo returned
+  (** [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

@@ -80,7 +80,7 @@ module type S = sig
   (** [get_model t] produces the current model. *)
   val get_model : t -> unit
 
-  (** [get_unknown_reason t] returns the reason Alt-Ergo returned
+  (** [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/satml_frontend.ml

@@ -60,7 +60,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     skolems : E.gformula ME.t; (* key <-> f *)
     add_inst : E.t -> bool;
     guards : guards;
-    ur : Sat_solver_sig.unknown_reason option;
+    unknown_reason : Sat_solver_sig.unknown_reason option;
+    (** The reason why satml raised I_dont_know f it does; None by default. *)
   }
 
   let empty_guards () = {
@@ -88,7 +89,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       skolems = ME.empty;
       guards = init_guards ();
       add_inst = (fun _ -> true);
-      ur = None;
+      unknown_reason = None;
     }
 
   let empty_with_inst add_inst =
@@ -1010,8 +1011,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
         in
         let () =
           if not updated then
-            let ur = "I don't have enough information to conclude" in
-            raise (I_dont_know {env with ur = Some ur})
+            let ur = "incomplete" in
+            raise (I_dont_know {env with unknown_reason = Some ur})
         in
         unsat_rec env ~first_call:false
 
@@ -1177,7 +1178,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
 
   let get_model _env = failwith "not yet supported"
 
-  let get_unknown_reason env = env.ur
+  let get_unknown_reason env = env.unknown_reason
 
   let () =
     Steps.save_steps ();