feat: Option --optimize (#916)

Fixes #897

src/bin/common/parse_command.ml

@@ -876,7 +876,6 @@ let parse_output_opt =
       Arg.(value & opt interpretation INone &
            info ["interpretation"] ~docv ~docs:s_models ~doc)
     in
-
     let produce_models =
       let doc =
         "Enable model generation (equivalent to --interpretation last)."
@@ -997,23 +996,45 @@ let parse_output_opt =
     Term.(const not $ no_tableaux_cdcl_in_theories)
   in
 
+  let optim =
+    let doc =
+      "Enable model optimization (experimental)."
+    in
+    Arg.(value & flag & info ["optimize"] ~doc ~docs:s_models)
+  in
+
   let set_sat_options =
-    let set_sat_options sat_solver cdcl_tableaux_inst cdcl_tableaux_th =
-      set_sat_solver sat_solver;
+    let set_sat_options sat_solver cdcl_tableaux_inst cdcl_tableaux_th optim =
+      set_optimize optim;
       begin match sat_solver with
-        | CDCL_Tableaux ->
+        | Util.CDCL_Tableaux ->
+          set_sat_solver sat_solver;
           set_cdcl_tableaux_inst cdcl_tableaux_inst;
-          set_cdcl_tableaux_th cdcl_tableaux_th
+          set_cdcl_tableaux_th cdcl_tableaux_th;
+          Ok ()
+        | Util.CDCL ->
+          set_sat_solver sat_solver;
+          set_cdcl_tableaux_inst false;
+          set_cdcl_tableaux_th false;
+          Ok ()
+        | s when optim ->
+          Fmt.error
+            "--optimize is not compatible with Sat solver %a@."
+            Util.pp_sat_solver s;
         | _ ->
+          set_sat_solver sat_solver;
           set_cdcl_tableaux_inst false;
-          set_cdcl_tableaux_th false
-      end;
-      ()
+          set_cdcl_tableaux_th false;
+          Ok ()
+      end
     in
-    Term.(
-      const set_sat_options $ sat_solver $ cdcl_tableaux_inst
-      $ cdcl_tableaux_th
-    )
+    let term =
+      Term.(
+        const set_sat_options $ sat_solver $ cdcl_tableaux_inst
+        $ cdcl_tableaux_th $ optim
+      )
+    in
+    Term.term_result' term
   in
 
   let use_underscore =
@@ -1075,7 +1096,8 @@ let parse_output_opt =
   in
 
   Term.(ret (const mk_output_opt $
-             interpretation $ use_underscore $ unsat_core $
+             interpretation $
+             use_underscore $ unsat_core $
              output_format $ model_type $
              set_dump_models $ set_dump_models_on $
              set_sat_options $ set_frontend

src/bin/common/solving_loop.ml

@@ -29,9 +29,10 @@
 (**************************************************************************)
 
 open AltErgoLib
-open Options
 open D_loop
 
+module O = Options
+
 type solver_ctx = {
   ctx    : Commands.sat_tdecl list;
   local  : Commands.sat_tdecl list;
@@ -88,6 +89,12 @@ let unsupported_opt opt =
   in
   warning "unsupported option %s" opt
 
+let enable_maxsmt b =
+  if b then
+    DStd.Extensions.Smtlib2.(enable maxsmt)
+  else
+    DStd.Extensions.Smtlib2.(disable maxsmt)
+
 (* We currently use the full state of the solver as model. *)
 type model = Model : 'a sat_module * 'a -> model
 
@@ -102,7 +109,7 @@ let main () =
       (val
         (if Options.get_no_theory() then (module Theory.Main_Empty : Theory.S)
          else (module Theory.Main_Default : Theory.S)) : Theory.S ) in
-
+    O.get_sat_solver (),
     (module SatCont.Make(TH) : Sat_solver_sig.S)
   in
 
@@ -148,7 +155,7 @@ let main () =
   in
 
   let typed_loop all_context state td =
-    if get_type_only () then state else begin
+    if O.get_type_only () then state else begin
       match td.Typed.c with
       | Typed.TGoal (_, kind, name, _) ->
         let l =
@@ -243,7 +250,7 @@ let main () =
       Frontend.print_status Preprocess 0;
     let assertion_stack = Stack.create () in
     let typing_loop state p =
-      if get_parse_only () then state else begin
+      if O.get_parse_only () then state else begin
         try
           let l, env = I.type_parsed state.env assertion_stack p in
           List.fold_left (typed_loop all_used_context) { state with env; } l
@@ -263,7 +270,7 @@ let main () =
     let state = {
       env = I.empty_env;
       solver_ctx = empty_solver_ctx;
-      sat_solver = make_sat ();
+      sat_solver = snd @@ make_sat ();
     } in
     try
       let parsed_seq = parsed () in
@@ -278,20 +285,24 @@ let main () =
     State.create_key ~pipe:"" "solving_state"
   in
 
-  let sat_solver_key : (module Sat_solver_sig.S) State.key =
+  let sat_solver_key : (Util.sat_solver * (module Sat_solver_sig.S)) State.key =
     State.create_key ~pipe:"" "sat_solver"
   in
 
   let partial_model_key: model option State.key =
     State.create_key ~pipe:"" "sat_state"
   in
 
+  let optimize_key: bool State.key =
+    State.create_key ~pipe:"" "optimize"
+  in
+
   let debug_parsed_pipe st c =
     if State.get State.debug st then
       Format.eprintf "[logic][parsed][%a] @[<hov>%a@]@."
         Dolmen.Std.Loc.print_compact c.Dolmen.Std.Statement.loc
         Dolmen.Std.Statement.print c;
-    if get_parse_only () then
+    if O.get_parse_only () then
       st, `Done ()
     else
       st, `Continue c
@@ -301,7 +312,7 @@ let main () =
       Format.eprintf "[logic][typed][%a] @[<hov>%a@]@\n@."
         Dolmen.Std.Loc.print_compact stmt.Typer_Pipe.loc
         Typer_Pipe.print stmt;
-    if get_type_only () then
+    if O.get_type_only () then
       st, `Done ()
     else
       st, `Continue stmt
@@ -397,6 +408,7 @@ let main () =
     |> State.set sat_solver_key (make_sat ())
     |> State.set solver_ctx_key solver_ctx
     |> State.set partial_model_key partial_model
+    |> State.set optimize_key (O.get_optimize ())
     |> State.init ~debug ~report_style ~reports ~max_warn ~time_limit
       ~size_limit ~response_file
     |> Parser.init
@@ -410,6 +422,39 @@ let main () =
       Loc.report loc name ty DStd.Term.print value
   in
 
+  let set_sat_solver sat st =
+    let optim = State.get optimize_key st in
+    match sat with
+    | Util.Tableaux | Tableaux_CDCL when optim ->
+      warning
+        "Sat-solver %a is incompatible with optimization: ignoring command."
+        Util.pp_sat_solver
+        sat;
+      st
+    | Tableaux | Tableaux_CDCL | CDCL | CDCL_Tableaux ->
+      O.set_sat_solver sat;
+      (* `make_sat` returns the sat solver corresponding to the new sat_solver
+         option. *)
+      State.set
+        sat_solver_key
+        (make_sat ())
+        st
+  in
+
+  let set_optimize optim st =
+    let sat, _ = State.get sat_solver_key st in
+    match sat with
+    | Util.Tableaux | Tableaux_CDCL when optim ->
+      warning
+        "Sat-solver %a is incompatible with optimization: ignoring command."
+        Util.pp_sat_solver
+        sat;
+      st
+    | Tableaux | Tableaux_CDCL | CDCL | CDCL_Tableaux ->
+      enable_maxsmt optim;
+      State.set optimize_key optim st
+  in
+
   let handle_option st_loc name (value : DStd.Term.t) st =
     match name, value.term with
     (* Smtlib2 regular options *)
@@ -479,13 +524,12 @@ let main () =
                 Util.CDCL_Tableaux
               | _ -> raise Exit
             in
-            Options.set_sat_solver sat_solver;
             let is_cdcl_tableaux =
               match sat_solver with CDCL_Tableaux -> true | _ -> false
             in
             Options.set_cdcl_tableaux_inst is_cdcl_tableaux;
             Options.set_cdcl_tableaux_th is_cdcl_tableaux;
-            State.set sat_solver_key (make_sat ()) st
+            set_sat_solver sat_solver st
           with Exit ->
             recoverable_error
               "error setting ':sat-solver', invalid option value '%s'"
@@ -509,10 +553,57 @@ let main () =
         | None -> print_wrn_opt ~name st_loc "nonnegative integer" value
         | Some i -> Options.set_profiling true i
       end; st
+    | ":optimization", Symbol { name = Simple b; _} ->
+      begin
+        match bool_of_string_opt b with
+        | None -> print_wrn_opt ~name st_loc "bool" value; st
+        | Some b ->
+          set_optimize b st
+      end
     | _ ->
       unsupported_opt name; st
   in
 
+  let handle_minimize_term (_term : DStd.Term.t) st =
+    warning "Unsupported minimize.";
+    st
+  in
+  (* TODO: implement when optimae is merged *)
+
+  let handle_maximize_term (_term : DStd.Term.t) st =
+    warning "Unsupported maximize.";
+    st
+  in
+  (* TODO: implement when optimae is merged *)
+
+  let handle_get_objectives (_args : DStd.Term.t list) st =
+    warning "Unsupported get-objectives.";
+    st
+  in
+  (* TODO: implement when optimae is merged *)
+
+  let handle_custom_statement id args st =
+    match id, args with
+    | Dolmen.Std.Id.{name = Simple "minimize"; _}, [term] ->
+      handle_minimize_term term st
+    | Dolmen.Std.Id.{name = Simple "maximize"; _}, [term] ->
+      handle_maximize_term term st
+    | Dolmen.Std.Id.{name = Simple "get-objectives"; _}, args ->
+      handle_get_objectives args st
+    | Dolmen.Std.Id.{name = Simple (("minimize" | "maximize") as ext); _}, _ ->
+      recoverable_error
+        "Statement %s only expects 1 argument (%i given)"
+        ext
+        (List.length args);
+      st
+    | n, _ ->
+      recoverable_error
+        "Unknown statement %a."
+        Dolmen.Std.Id.print
+        n;
+      st
+  in
+
   let handle_get_info (st : State.t) (name: string) =
     let print_std =
       fun (type a) (pp :a Fmt.t) (a : a) ->
@@ -610,7 +701,10 @@ let main () =
           | _ -> assert false
         in
         let partial_model =
-          solve (State.get sat_solver_key st) all_context (cnf, name)
+          solve
+            (snd @@ State.get sat_solver_key st)
+            all_context
+            (cnf, name)
         in
         if is_thm
         then
@@ -668,6 +762,7 @@ let main () =
         st
         |> State.set partial_model_key None
         |> State.set solver_ctx_key empty_solver_ctx
+        |> State.set optimize_key (O.get_optimize ())
 
       | {contents = `Exit; _} -> raise Exit
 
@@ -683,6 +778,9 @@ let main () =
         handle_get_info st kind;
         st
 
+      | {contents = `Other (custom, args); _} ->
+        handle_custom_statement custom args st
+
       | _ ->
         (* TODO:
            - Separate statements that should be ignored from unsupported
@@ -700,6 +798,10 @@ let main () =
   in
   let d_fe filename =
     let logic_file, st = mk_state filename in
+    let () =
+      (* Activating maxsmt if the optimize option is ON. *)
+      enable_maxsmt (O.get_optimize ())
+    in
     try
       Options.with_timelimit_if (not (Options.get_timelimit_per_goal ()))
       @@ fun () ->
@@ -742,7 +844,7 @@ let main () =
       ignore (handle_exn st bt exn)
   in
 
-  let filename = get_file () in
-  match get_frontend () with
+  let filename = O.get_file () in
+  match O.get_frontend () with
   | "dolmen" -> d_fe filename
   | frontend -> ae_fe filename frontend

src/lib/reasoners/sat_solver.mli

@@ -28,7 +28,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-
 val get_current : unit -> (module Sat_solver_sig.SatContainer)
 (** returns the current activated SAT-solver depending on the value of
     `Options.sat_solver ()`. See command-line option `-sat-solver` for

src/lib/util/options.ml

@@ -338,6 +338,7 @@ let get_timelimit_per_goal () = !timelimit_per_goal
 (** Output options *)
 
 let interpretation = ref INone
+let optimize = ref false
 let dump_models = ref false
 let interpretation_use_underscore = ref false
 let output_format = ref Native
@@ -346,6 +347,7 @@ let infer_output_format = ref true
 let unsat_core = ref false
 
 let set_interpretation b = interpretation := b
+let set_optimize b = optimize := b
 let set_dump_models b = dump_models := b
 let set_interpretation_use_underscore b = interpretation_use_underscore := b
 let set_output_format b = output_format := b
@@ -380,6 +382,7 @@ let equal_mode_type a b =
   | Value, Value -> true
 
 let get_interpretation () = not @@ equal_mode !interpretation INone
+let get_optimize () = !optimize
 let get_dump_models () = !dump_models
 let get_first_interpretation () = equal_mode !interpretation IFirst
 let get_every_interpretation () = equal_mode !interpretation IEvery

src/lib/util/options.mli

@@ -215,6 +215,9 @@ val set_input_format : input_format option -> unit
 *)
 val set_interpretation : interpretation -> unit
 
+(** Set [optimize] accessible with {!val:get_optimize}. *)
+val set_optimize : bool -> unit
+
 (** [dump_models] accessible with {!val:get_dump_models}. *)
 val set_dump_models : bool -> unit
 
@@ -709,6 +712,9 @@ val get_timelimit_per_goal : unit -> bool
 val get_interpretation : unit -> bool
 (** Default to [false] *)
 
+(** [true] if optimization is activated. *)
+val get_optimize : unit -> bool
+
 (** [true] if the interpretation for each goal or check-sat is
     printed. *)
 val get_dump_models : unit -> bool