Set option support (#608)

* Add a handler for set-option

* Add support for output channels options

* Add support for set-option

* Add support for set-option (bis)

* Add a bit of documentation

* Fix a bug and the documentation

* Naive support for produce-models, produce-unsat-cores, verbosity and reproducible-resource-limit

* Poetry

* Simplify the handler

* Poetry

* Add a link to the OptimAE PR

* Rename at_exit to close_all

* Rename some functions in Options

* Change the API of the buffers in Output module

* Readd the old options for formatter outputs

* Rollback modifications on create_channel and improve its documentation

* Hide the deprecated options in the CLI API

* Add a finalizer in the worker_js to flush properly the output buffers

* Flush formatter before reading buffer in the js worker

src/bin/common/parse_command.ml

@@ -125,31 +125,6 @@ let model_type_printer fmt format =
 let model_type_conv =
   Arg.conv ~docv:"MTYP" (model_type_parser, model_type_printer)
 
-type formatter = Stdout | Stderr | Other of string
-
-let value_of_fmt = function
-  | Stdout -> Format.std_formatter
-  | Stderr -> Format.err_formatter
-  | Other s ->
-    let oc = open_out s in
-    at_exit (fun () -> close_out oc);
-    Format.formatter_of_out_channel oc
-
-let formatter_parser = function
-  | "stdout" -> Ok Stdout
-  | "stderr" -> Ok Stderr
-  | s -> Ok (Other s)
-
-let formatter_to_string = function
-  | Stdout -> "stdout"
-  | Stderr -> "stderr"
-  | Other s -> s
-
-let formatter_printer fmt formatter =
-  Format.fprintf fmt "%s" (formatter_to_string formatter)
-
-let formatter_conv = Arg.conv ~docv:"FMT" (formatter_parser, formatter_printer)
-
 module Rule = struct
   type t = RParsing | RTyping | RSat | RCC | RArith | RNone
 
@@ -413,6 +388,9 @@ let mk_limit_opt age_bound fm_cross_limit timelimit_interpretation
 let mk_models_opt b =
   if b then begin
     set_interpretation ILast;
+    (* 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 *)
     set_sat_solver Tableaux
   end;
   `Ok ()
@@ -603,11 +581,10 @@ let mk_opts file () () debug_flags ddebug_flags dddebug_flags rule () halt_opt
     `Ok true
   end
 
-let mk_fmt_opt std_fmt err_fmt mdl_fmt
-  =
-  set_std_fmt (value_of_fmt std_fmt);
-  set_err_fmt (value_of_fmt err_fmt);
-  set_fmt_mdl (value_of_fmt mdl_fmt);
+let mk_output_channel_opt std_output err_output mdl_output =
+  Options.Output.(create_channel std_output |> set_std);
+  Options.Output.(create_channel err_output |> set_err);
+  Options.Output.(create_channel mdl_output |> set_mdl);
   `Ok()
 
 (* Custom sections *)
@@ -1228,35 +1205,65 @@ let parse_theory_opt =
        )
 
 let parse_fmt_opt =
-
   let docs = s_fmt in
+  let docv = "CHANNEL" in
 
-  let std_formatter =
-    let doc = Format.sprintf
-        "Set the standard formatter used by default to output the results,
-    models and unsat cores. Possible values are %s."
-        (Arg.doc_alts ["stdout"; "stderr"; "<filename>"]) in
-    Arg.(value & opt formatter_conv Stdout & info ["std-formatter"] ~docs ~doc)
+  let merge_formatters default preferred deprecated =
+    match preferred, deprecated with
+    | Some fmt, _ -> fmt
+    | None, Some fmt -> fmt
+    | None, None -> default
   in
 
-  let err_formatter =
-    let doc = Format.sprintf
-        "Set the error formatter used by default to output error, debug and
+  let std_output =
+    let doc =
+      Format.sprintf
+        "Set the standard output used by default to print the results,
+          models and unsat cores. Possible values are %s."
+        (Arg.doc_alts ["stdout"; "stderr"; "<filename>"])
+    in
+    let deprecated = "this option is depreciated. Please use --std-output." in
+    let std_output =
+      Arg.(value & opt (some' string) None & info ["std-output"] ~docs
+             ~doc ~docv)
+    in
+    let std_formatter =
+      Arg.(value & opt (some' string) None  & info ["std-formatter"]
+             ~deprecated ~docs ~docv)
+    in
+    Term.(const (merge_formatters "stdout") $ std_output $ std_formatter)
+  in
+
+  let err_output =
+    let doc =
+      Format.sprintf
+        "Set the error output used by default to print error, debug and
          warning informations. Possible values are %s."
-        (Arg.doc_alts ["stdout"; "stderr"; "<filename>"]) in
-    Arg.(value & opt formatter_conv Stderr & info ["err-formatter"] ~docs ~doc)
+        (Arg.doc_alts ["stdout"; "stderr"; "<filename>"])
+    in
+    let deprecated = "this option is depreciated. Please use --err-output." in
+    let err_output =
+      Arg.(value & opt (some' string) None & info ["err-output"] ~docs
+             ~doc ~docv)
+    in
+    let err_formatter =
+      Arg.(value & opt (some' string) None & info ["err-formatter"]
+             ~deprecated ~docs ~docv)
+    in
+    Term.(const (merge_formatters "stderr") $ err_output $ err_formatter)
   in
 
   let model_output =
-    let doc = Format.sprintf
+    let doc =
+      Format.sprintf
         "Set the output used for the model generation. Possible values are %s."
-        (Arg.doc_alts ["stdout"; "stderr"; "<filename>"]) in
-    Arg.(value & opt formatter_conv Stdout & info ["model-output"] ~docs ~doc)
+        (Arg.doc_alts ["stdout"; "stderr"; "<filename>"])
+    in
+    Arg.(value & opt string "stdout" & info ["model-output"] ~docv ~docs ~doc)
   in
 
-  Term.(ret (const mk_fmt_opt $
-             std_formatter $ err_formatter $ model_output
-            ))
+  Term.(ret (const mk_output_channel_opt $ std_output $ err_output
+             $ model_output))
 
 let main =
 
@@ -1336,6 +1343,7 @@ let main =
   Cmd.v info term
 
 let parse_cmdline_arguments () =
+  at_exit Options.Output.close_all;
   let r = Cmd.eval_value main in
   match r with
   | Ok `Ok true -> ()

src/bin/common/signals_profiling.ml

@@ -29,7 +29,6 @@
 (**************************************************************************)
 
 open AltErgoLib
-open Options
 
 let timers = Timers.empty ()
 
@@ -39,7 +38,8 @@ let init_sigterm_6 () =
   (* what to do with Ctrl+C ? *)
   Sys.set_signal Sys.sigint(*-6*)
     (Sys.Signal_handle (fun _ ->
-         if Options.get_profiling() then Profiling.switch (get_fmt_err ())
+         if Options.get_profiling() then
+           Profiling.switch (Options.Output.get_fmt_err ())
          else begin
            Printer.print_wrn "User wants me to stop.";
            Printer.print_std "unknown";
@@ -58,7 +58,7 @@ let init_sigterm_11_9 () =
            (Sys.Signal_handle
               (fun _ ->
                  Profiling.print true (Steps.get_steps ())
-                   timers (get_fmt_err ());
+                   timers (Options.Output.get_fmt_err ());
                  exit 1
               )
            )
@@ -71,7 +71,8 @@ let init_sigterm_21 () =
     Sys.set_signal Sys.sigprof (*-21*)
       (Sys.Signal_handle
          (fun _ ->
-            Profiling.print false (Steps.get_steps ()) timers (get_fmt_err ());
+            Profiling.print false (Steps.get_steps ()) timers
+              (Options.Output.get_fmt_err ());
          )
       )
 

src/bin/common/solving_loop.ml

@@ -81,7 +81,7 @@ let main () =
         Profiling.print true
           (Steps.get_steps ())
           (Signals_profiling.get_timers ())
-          (get_fmt_err ())
+          (Options.Output.get_fmt_err ())
     with Util.Timeout ->
       if not (Options.get_timelimit_per_goal()) then exit 142
   in
@@ -285,6 +285,73 @@ let main () =
     |> Typer_Pipe.init ~type_check
   in
 
+  let print_wrn_opt ~name loc ty value =
+    Printer.print_wrn "%a The option %s expects a %s, got %a"
+      Loc.report loc name ty DStd.Term.print value
+  in
+
+  let handle_option st_loc name (value : DStd.Term.t) =
+    match name, value.term with
+    | ":regular-output-channel", Symbol { name = Simple name; _ } ->
+      Options.Output.create_channel name
+      |> Options.Output.set_regular
+    | ":diagnostic-output-channel", Symbol { name = Simple name; _ } ->
+      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_wrn "%a The generation of models is not supported \
+                              for the current SAT solver. Please choose the \
+                              SAT solver Tableaux."
+          Loc.report st_loc
+    | ":produce-models", Symbol { name = Simple "false"; _ } ->
+      Options.set_interpretation INone
+    | ":produce-unsat-cores", Symbol { name = Simple "true"; _ } ->
+      (* The generation of unsat core is supported only with the SAT
+         solver Tableaux. *)
+      if Stdlib.(Options.get_sat_solver () = Tableaux) then
+        Options.set_unsat_core true
+      else Printer.print_wrn "%a The generation of unsat cores is not \
+                              supported for the current SAT solver. Please \
+                              choose the SAT solver Tableaux."
+          Loc.report st_loc
+    | ":produce-unsat-cores", Symbol { name = Simple "false"; _ } ->
+      Options.set_unsat_core false
+    | (":produce-models" | ":produce-unsat-cores" as name), _ ->
+      print_wrn_opt ~name st_loc "boolean" value
+    | ":verbosity", Symbol { name = Simple level; _ } ->
+      begin
+        match int_of_string_opt level with
+        | Some i when i > 0 -> Options.set_verbose true
+        | Some 0 -> Options.set_verbose false
+        | None | Some _ ->
+          print_wrn_opt ~name:":verbosity" st_loc "integer" value
+      end
+    | ":reproducible-resource-limit", Symbol { name = Simple level; _ } ->
+      begin
+        match int_of_string_opt level with
+        | Some i when i > 0 -> Options.set_timelimit_per_goal true
+        | Some 0 -> Options.set_timelimit_per_goal false
+        | None | Some _ ->
+          print_wrn_opt ~name:":reproducible-resource-limit" st_loc
+            "nonnegative integer" value
+      end
+    | (":global-declarations"
+      | ":interactive-mode"
+      | ":produce-assertions"
+      | ":produce-assignments"
+      | ":produce-proofs"
+      | ":produce-unsat-assumptions"
+      | ":print-success"
+      | ":random-seed"), _
+      -> Printer.print_wrn "unsupported option %s" name
+    | _ -> Printer.print_wrn "unsupported option %s" name
+  in
+
   let handle_stmt :
     FE.used_context -> State.t ->
     Typer_Pipe.typechecked Typer_Pipe.stmt -> State.t =
@@ -388,6 +455,17 @@ let main () =
             let solver_ctx = State.get solver_ctx_key st in
             { solver_ctx with local = [] }
           ) st
+
+      | {contents = `Set_option
+             { term =
+                 App ({ term = Symbol { name = Simple name; _ }; _ }, [value]);
+               _
+             }; loc = l; _ } ->
+        let dloc_file = (State.get State.logic_file st).loc in
+        let loc = DStd.Loc.(lexing_positions (loc dloc_file l)) in
+        handle_option loc name value;
+        st
+
       | _ ->
         (* TODO:
            - Separate statements that should be ignored from unsupported

src/bin/gui/main_gui.ml

@@ -499,7 +499,7 @@ let update_status image label buttonclean env s steps =
     else
       Printer.print_std "@{<C.F_Green>Valid@} (%2.4f) (%d)" time steps;
     if get_unsat_core () then begin
-      Printer.print_fmt (Options.get_fmt_usc ()) "unsat-core:@ %a"
+      Printer.print_fmt (Options.Output.get_fmt_usc ()) "unsat-core:@ %a"
         (Explanation.print_unsat_core ~tab:true) dep;
       show_used_lemmas env dep
     end;

src/bin/js/worker_js.ml

@@ -42,8 +42,9 @@ type 'a state = {
 }
 
 (* If the buffer is not empty split the string in strings at each newline *)
-let check_buffer_content b =
-  let buf_cont = Buffer.contents b in
+let check_buffer_content (buf, output) =
+  Format.pp_print_flush (Options.Output.to_formatter output) ();
+  let buf_cont = Buffer.contents buf in
   if String.equal buf_cont "" then
     None
   else
@@ -55,22 +56,30 @@ let check_context_content c =
   | [] -> None
   | _ -> Some c
 
+let create_buffer () =
+  let buf = Buffer.create 10 in
+  let output =
+    Format.formatter_of_buffer buf
+    |> Options.Output.of_formatter
+  in
+  buf, output
+
 let main worker_id content =
   try
     (* Create buffer for each formatter
        The content of this buffers are then retrieved and send as results *)
-    let buf_std = Buffer.create 10 in
-    Options.set_fmt_std (Format.formatter_of_buffer buf_std);
-    let buf_err = Buffer.create 10 in
-    Options.set_fmt_err (Format.formatter_of_buffer buf_err);
-    let buf_wrn = Buffer.create 10 in
-    Options.set_fmt_wrn (Format.formatter_of_buffer buf_wrn);
-    let buf_dbg = Buffer.create 10 in
-    Options.set_fmt_dbg (Format.formatter_of_buffer buf_dbg);
-    let buf_mdl = Buffer.create 10 in
-    Options.set_fmt_mdl (Format.formatter_of_buffer buf_mdl);
-    let buf_usc = Buffer.create 10 in
-    Options.set_fmt_usc (Format.formatter_of_buffer buf_usc);
+    let buf_std = create_buffer () in
+    Options.Output.set_std (snd buf_std);
+    let buf_err = create_buffer () in
+    Options.Output.set_err (snd buf_err);
+    let buf_wrn = create_buffer () in
+    Options.Output.set_wrn (snd buf_wrn);
+    let buf_dbg = create_buffer () in
+    Options.Output.set_dbg (snd buf_dbg);
+    let buf_mdl = create_buffer () in
+    Options.Output.set_mdl (snd buf_mdl);
+    let buf_usc = create_buffer () in
+    Options.Output.set_usc (snd buf_usc);
 
     (* Status updated regarding if AE succed or failed
        (error or steplimit reached) *)
@@ -273,6 +282,7 @@ let main worker_id content =
     and the corresponding set of options
     Return a couple of list for status (one per goal) and errors *)
 let () =
+  at_exit Options.Output.close_all;
   Worker.set_onmessage (fun (json_file,json_options) ->
       Lwt_js_events.async (fun () ->
           let filename,worker_id,filecontent =

src/lib/frontend/d_cnf.ml

@@ -1154,7 +1154,6 @@ and make_trigger ?(loc = Loc.dummy) ~name_base ~decl_kind
   in
   E.clean_trigger ~in_theory name trigger
 
-
 (** Preprocesses the body of a goal by:
     - removing the top-level universal quantifiers and considering their
       quantified variables as uninsterpreted symbols.

src/lib/frontend/frontend.ml

@@ -291,7 +291,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
          not (get_debug_unsat_core()) &&
          not (get_save_used_context())
       then
-        Printer.print_fmt (Options.get_fmt_usc ())
+        Printer.print_fmt (Options.Output.get_fmt_usc ())
           "unsat-core:@,%a@."
           (Ex.print_unsat_core ~tab:true) dep;
       check_status_consistency status;