Add timeout-as-unknown option

src/bin/common/parse_command.ml

@@ -368,7 +368,7 @@ let mk_limit_opt age_bound fm_cross_limit timelimit_interpretation
 let mk_output_opt
     interpretation use_underscore
     objectives_in_interpretation all_models show_prop_model
-    unsat_core output_format model_type () () ()
+    timeout_as_unknown unsat_core output_format model_type () () ()
   =
   set_infer_output_format (Option.is_none output_format);
   let output_format = match output_format with
@@ -384,6 +384,7 @@ let mk_output_opt
   set_objectives_in_interpretation objectives_in_interpretation;
   set_all_models all_models;
   set_show_prop_model show_prop_model;
+  set_timeout_as_unknown timeout_as_unknown;
   set_unsat_core unsat_core;
   set_output_format output_format;
   set_model_type model_type;
@@ -1034,7 +1035,7 @@ let parse_output_opt =
            ~docv ~docs:s_models ~doc)
   in
   let objectives_in_interpretation =
-    let doc = " inline pretty-printing of optimized expressions in the \
+    let doc = "Inline pretty-printing of optimized expressions in the \
                model instead of a dedicated section '(objectives \
                ...)'. Be aware that a part of the model may be shrunk \
                or not accurate if some expressions to optimize are \
@@ -1045,7 +1046,7 @@ let parse_output_opt =
             "obj-in-interpretation";"obj-in-model"] ~docv ~docs ~doc) in
 
   let all_models =
-    let doc = " enable all-models (or all-sat) feature, in which case, \
+    let doc = "Enable all-models (or all-sat) feature, in which case, \
                all possible boolean models will be explored. If \
                --interpretation is also set, an interpretation for \
                each boolean model will also be displayed. Note that \
@@ -1055,12 +1056,18 @@ let parse_output_opt =
            ["all-models"; "all-sat"] ~docv ~docs ~doc) in
 
   let show_prop_model =
-    let doc = " also show the propositional if a model is requested \
+    let doc = "Also show the propositional if a model is requested \
                (with --interpretation or with --all-models options)." in
     let docv = "VAL" in
     Arg.(value & flag & info
            ["show-prop-model"; "show-propositional-model"] ~docv ~docs ~doc) in
 
+  let timeout_as_unknown =
+    let doc = "Returns unknown status instead of timeout" in
+    let docv = "VAL" in
+    Arg.(value & flag & info
+           ["timeout-as-unknown"; "to-as-unknown"] ~docv ~docs ~doc) in
+
   let unsat_core =
     let doc = "Experimental support for computing and printing unsat-cores." in
     Arg.(value & flag & info ["u"; "unsat-core"] ~doc ~docs)
@@ -1107,7 +1114,7 @@ let parse_output_opt =
   Term.(ret (const mk_output_opt $
              interpretation $ use_underscore $
              objectives_in_interpretation $ all_models $ show_prop_model $
-             unsat_core $ output_format $ model_type $
+             timeout_as_unknown $unsat_core $ output_format $ model_type $
              set_dump_models $ set_sat_options $
              set_frontend))
 

src/lib/frontend/frontend.ml

@@ -279,7 +279,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
     | SAT.I_dont_know {env; timeout} ->
       (* TODO: always print Unknown for why3 ? *)
       let status =
-        if timeout != NoTimeout then (Timeout (Some d))
+        if timeout != NoTimeout && (not (get_timeout_as_unknwon ())) then
+          (Timeout (Some d))
         else (Unknown (d, env))
       in
       print_status status (Steps.get_steps ());
@@ -288,9 +289,11 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
         env dep d timeout
 
     | 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_status (
+        if get_timeout_as_unknwon () then
+          (Unknown (d, env))
+        else Timeout (Some d))
+        (Steps.get_steps ());
       (* dont call 'process_unknown' in this case. Timeout stops
          all-models listing *)
       print_model (SAT.get_model env) None;

src/lib/util/options.ml

@@ -352,6 +352,7 @@ let show_prop_model = ref false
 let output_format = ref Native
 let model_type = ref Value
 let infer_output_format = ref true
+let timeout_as_unknown = ref false
 let unsat_core = ref false
 
 let set_interpretation b = interpretation := b
@@ -363,6 +364,7 @@ let set_show_prop_model b = show_prop_model := b
 let set_output_format b = output_format := b
 let set_model_type t = model_type := t
 let set_infer_output_format b = infer_output_format := b
+let set_timeout_as_unknown b = timeout_as_unknown := b
 let set_unsat_core b = unsat_core := b
 
 let equal_mode a b =
@@ -405,6 +407,7 @@ let get_output_smtlib () = equal_output_format !output_format Smtlib2
 let get_model_type () = !model_type
 let get_model_type_constraints () = equal_mode_type !model_type Constraints
 let get_infer_output_format () = !infer_output_format
+let get_timeout_as_unknwon () = !timeout_as_unknown
 let get_unsat_core () = !unsat_core || !save_used_context || !debug_unsat_core
 
 (** Profiling options *)

src/lib/util/options.mli

@@ -300,6 +300,9 @@ val set_triggers_var : bool -> unit
 (** Set [type_smt2] accessible with {!val:get_type_smt2} *)
 val set_type_smt2 : bool -> unit
 
+(** Set [timeout_as_unknown] accessible with {!val:get_timeout_as_unknown} *)
+val set_timeout_as_unknown : bool -> unit
+
 (** Set [unsat_core] accessible with {!val:get_unsat_core} *)
 val set_unsat_core : bool -> unit
 
@@ -790,6 +793,11 @@ val get_model_type_constraints : unit -> bool
 val get_infer_output_format : unit -> bool
 (** Default to [true] *)
 
+(** [true] if Alt-Ergo returns [unknown] instead of [timeout] when the timelimit
+    is reached *)
+val get_timeout_as_unknwon : unit -> bool
+(** Default to [false] *)
+
 (** [true] if experimental support for unsat-cores is on. *)
 val get_unsat_core : unit -> bool
 (** Default to [false] *)