Clean up OptimAE

This PR refactors the way we manage optimization constraints in Alt-Ergo. - Optimization constraints aren't tag on subformulas anymore. Instead we use the MaxSMT syntaxes. - We don't support optimization in Alt-Ergo native format. As this feature haven't been published, we don't need to deprecated it. - We support `maximize`, `minimize` and `get-objectives`. There is no support for `assert-soft`. I think it's out of the scope of this PR. - The SAT solver API exposes two new functions: `optimize` and `get_objectives` which, respectively, register objective function and return the current objective model. - The objective values are expressions.
OCamlPro · Nov 28, 2023 · 28c6ba6 · 28c6ba6
1 parent acbbe6c
commit 28c6ba6
Show file tree

Hide file tree

Showing 76 changed files with 18,096 additions and 632 deletions.
diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml
@@ -628,32 +628,50 @@ let main () =
       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
+  let handle_optimize_stmt ~to_max loc id (term : DStd.Expr.Term.t) st =
+    let contents = `Optimize (term, to_max) in
+    let stmt = { Typer_Pipe.id; contents; loc; attrs = []; implicit = false } in
+    let cnf =
+      D_cnf.make (State.get State.logic_file st).loc
+        (State.get solver_ctx_key st).ctx stmt
+    in
+    State.set solver_ctx_key (
+      let solver_ctx = State.get solver_ctx_key st in
+      { solver_ctx with ctx = cnf }
+    ) st
   in
-  (* TODO: implement when optimae is merged *)
 
-  let handle_get_objectives (_args : DStd.Term.t list) st =
-    warning "Unsupported get-objectives.";
+  let handle_get_objectives (_args : DStd.Expr.Term.t list) st =
+    let () =
+      if Options.get_interpretation () then
+        match State.get partial_model_key st with
+        | Some Model ((module SAT), partial_model) ->
+          let objectives = SAT.get_objectives partial_model in
+          begin
+            match objectives with
+            | Some o ->
+              Objective.Model.pp (Options.Output.get_fmt_regular ()) o
+            | None ->
+              recoverable_error "No objective generated"
+          end
+        | None ->
+          recoverable_error
+            "Model generation is disabled (try --produce-models)"
+    in
     st
   in
-  (* TODO: implement when optimae is merged *)
 
-  let handle_custom_statement id args st =
-    match id, args with
+  let handle_custom_statement loc id args st =
+    let args = List.map Dolmen_type.Core.Smtlib2.sexpr_as_term args in
+    let logic_file = State.get State.logic_file st in
+    let st, terms = Typer.terms st ~input:(`Logic logic_file) ~loc args in
+    match id, terms.ret with
     | Dolmen.Std.Id.{name = Simple "minimize"; _}, [term] ->
-      handle_minimize_term term st
+      handle_optimize_stmt ~to_max:false loc id 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
+      handle_optimize_stmt ~to_max:true loc id term st
+    | Dolmen.Std.Id.{name = Simple "get-objectives"; _}, terms ->
+      handle_get_objectives terms st
     | Dolmen.Std.Id.{name = Simple (("minimize" | "maximize") as ext); _}, _ ->
       recoverable_error
         "Statement %s only expects 1 argument (%i given)"
@@ -891,8 +909,8 @@ let main () =
             st
         end
 
-      | {contents = `Other (custom, args); _} ->
-        handle_custom_statement custom args st
+      | {contents = `Other (custom, args); loc; _} ->
+        handle_custom_statement loc custom args st
 
       | _ ->
         (* TODO:

diff --git a/src/lib/dune b/src/lib/dune
@@ -26,7 +26,16 @@
     fmt
     stdcompat
   )
-  (preprocess (pps ppx_blob ppx_deriving.show ppx_deriving.enum ppx_deriving.fold))
+  (preprocess
+    (pps
+      ppx_blob
+      ppx_deriving.ord
+      ppx_deriving.show
+      ppx_deriving.enum
+      ppx_deriving.fold
+    )
+  )
+
   (preprocessor_deps (glob_files ../preludes/*.ae))
 
   ; .mli only modules *also* need to be in this field
@@ -46,7 +55,7 @@
     ; structures
     Commands Errors Explanation Fpa_rounding
     Parsed Profiling Satml_types Symbols
-    Expr Var Ty Typed Xliteral ModelMap
+    Expr Var Ty Typed Xliteral ModelMap Objective
     ; util
     Emap Gc_debug Hconsing Hstring Iheap Lists Loc
     MyUnix Numbers

diff --git a/src/lib/frontend/cnf.ml b/src/lib/frontend/cnf.ml
@@ -394,6 +394,9 @@ let mk_assume acc f name loc =
   let ff = make_form name f loc ~decl_kind:E.Daxiom in
   Commands.{st_decl=Assume(name, ff, true) ; st_loc=loc} :: acc
 
+let mk_optimize acc obj is_max loc =
+  let obj = make_term Sy.Map.empty "" obj in
+  Commands.{st_decl=Optimize (obj, is_max); st_loc=loc } :: acc
 
 (* extract defining term of the function or predicate. From the
    transformation of the parsed AST above, the typed AST is either of the
@@ -475,5 +478,6 @@ let make acc (d : (_ Typed.tdecl, _) Typed.annoted) =
        Solving_loop. *)
     Printer.print_wrn "Ignoring instruction %a" Typed.print_atdecl d;
     acc
+  | TOptimize (loc, obj, is_max) -> mk_optimize acc obj is_max loc
 
 let make_list l = List.fold_left make [] (List.rev l)
diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
@@ -1863,6 +1863,14 @@ let make_form name_base f loc ~decl_kind =
 let make dloc_file acc stmt =
   let rec aux acc (stmt: _ Typer_Pipe.stmt) =
     match stmt with
+    (* Optimize terms *)
+    | { contents = `Optimize (t, to_max); loc; _ } ->
+      let st_loc = dl_to_ael dloc_file loc in
+      let e =
+        mk_expr ~loc:st_loc ~toplevel:true ~decl_kind:Dobjective t
+      in
+      let st_decl = C.Optimize (e, to_max) in
+      C. { st_decl; st_loc } :: acc
 
     (* Push and Pop commands *)
     | { contents = `Pop n; loc; _ } ->

diff --git a/src/lib/frontend/d_cnf.mli b/src/lib/frontend/d_cnf.mli
@@ -55,6 +55,7 @@ val make :
   D_loop.DStd.Loc.file ->
   Commands.sat_tdecl list ->
   [< D_loop.Typer_Pipe.typechecked
+  | `Optimize of Dolmen.Std.Expr.term * bool
   | `Goal  of Dolmen.Std.Expr.term
   | `Check of Dolmen.Std.Expr.term list
          > `Hyp ] D_loop.Typer_Pipe.stmt ->

diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml
@@ -158,6 +158,8 @@ module type S = sig
 
   val th_assume : E.th_elt process
 
+  val optimize : (Expr.t * bool) process
+
   val process_decl:
     ?hook_on_status: (sat_env status -> int -> unit) ->
     env ->
@@ -396,6 +398,13 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
         env.expl <- expl
       | `Unsat -> ()
 
+ let internal_optimize ?(loc = Loc.dummy) (f, to_max) env =
+    ignore loc;
+    match env.res with
+    | `Sat | `Unknown ->
+      SAT.optimize env.sat_env ~to_max f
+    | `Unsat -> ()
+
   let check_step_limit f env =
     match SAT.get_unknown_reason env.sat_env with
     | Some (Step_limit _) -> ()
@@ -409,7 +418,6 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
       env.expl <- Ex.union expl env.expl
     | SAT.I_dont_know ->
       env.res <- `Unknown
-  (* The SAT.Timeout exception is not catched. *)
 
   (* Wraps the function f to check if the step limit is reached (in which case,
      don't do anything), and then calls the function & catches the
@@ -429,6 +437,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
 
   let th_assume = wrap_f internal_th_assume
 
+  let optimize = handle_sat_exn internal_optimize
+
   let process_decl ?(hook_on_status=(fun _ -> ignore)) env d =
     try
       match d.st_decl with
@@ -459,6 +469,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
         end
       | ThAssume th_elt ->
         check_step_limit (internal_th_assume ~loc:d.st_loc th_elt) env
+      | Optimize (f, to_max) -> internal_optimize ~loc:d.st_loc (f, to_max) env
     with
     | SAT.Sat ->
       (* This case should mainly occur when a query has a non-unsat result,
@@ -506,6 +517,6 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
          Returned unknown reason = %a@]"
         Sat_solver_sig.pp_ae_unknown_reason_opt ur;
 
-    | Some (lazy model) ->
+    | Some model ->
       Models.output_concrete_model ppf model
 end
diff --git a/src/lib/frontend/frontend.mli b/src/lib/frontend/frontend.mli
@@ -82,6 +82,8 @@ module type S = sig
 
   val th_assume : Expr.th_elt process
 
+  val optimize : (Expr.t * bool) process
+
   val process_decl:
     ?hook_on_status:(sat_env status -> int -> unit) ->
     env ->

diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml
@@ -45,18 +45,11 @@ module MX = Shostak.MXH
 
 let constraints = ref MS.empty
 
-type objective_value =
-  | Obj_pinfty
-  | Obj_minfty
-  | Obj_val of string
-  | Obj_unk
-
 type t = {
   propositional : Expr.Set.t;
   constants : ModelMap.t;
   functions : ModelMap.t;
   arrays : ModelMap.t;
-  objectives: (Expr.t * objective_value) Util.MI.t;
   terms_values : (Shostak.Combine.r * string) Expr.Map.t
 }
 
@@ -449,28 +442,6 @@ module SmtlibCounterExample = struct
       ) fprofs;
     !records
 
-  let output_objectives fmt objectives =
-    (* TODO: we can decide to print objectives to stderr if
-       Options.get_objectives_in_interpretation() is enabled *)
-    if not (Options.get_objectives_in_interpretation()) &&
-       not (Util.MI.is_empty objectives)
-    then begin
-      Format.fprintf fmt "@[<v 3>(objectives";
-      Util.MI.iter
-        (fun _i (e, x) ->
-           Format.fprintf fmt "@ (%a %a)"
-             E.print e
-             (fun fmt () ->
-                match x with
-                | Obj_pinfty -> Format.fprintf fmt "+oo"
-                | Obj_minfty -> Format.fprintf fmt "-oo"
-                | Obj_val s -> Format.fprintf fmt "%s" s
-                | Obj_unk -> Format.fprintf fmt "(interval -oo +oo)"
-             ) ()
-        )objectives;
-      Printer.print_fmt fmt "@]@ )"
-    end
-
 end
 (* of module SmtlibCounterExample *)
 
@@ -604,4 +575,3 @@ let output_concrete_model fmt m =
   (*     SmtlibCounterExample.output_arrays_counterexample fmt m.arrays; *)
 
   Printer.print_fmt fmt "@]@,)";
-  SmtlibCounterExample.output_objectives fmt m.objectives
diff --git a/src/lib/frontend/models.mli b/src/lib/frontend/models.mli
@@ -30,18 +30,11 @@
 
 (** {1 Models module} *)
 
-type objective_value =
-  | Obj_pinfty
-  | Obj_minfty
-  | Obj_val of string
-  | Obj_unk
-
 type t = {
   propositional : Expr.Set.t;
   constants : ModelMap.t;
   functions : ModelMap.t;
   arrays : ModelMap.t;
-  objectives: (Expr.t * objective_value) Util.MI.t;
   terms_values : (Shostak.Combine.r * string) Expr.Map.t
   (** A map from terms to their values in the model (as a
       representative of type X.r and as a string. *)

diff --git a/src/lib/frontend/parsed_interface.ml b/src/lib/frontend/parsed_interface.ml
@@ -120,6 +120,11 @@ let mk_push loc n =
 let mk_pop loc n =
   Pop (loc, n)
 
+(** Declaration of optimization of objective functions. *)
+
+let mk_optimize loc expr is_max =
+  Optimize (loc, expr, is_max)
+
 (** Making pure and logic types *)
 
 let int_type = PPTint
@@ -334,9 +339,3 @@ let mk_algebraic_test loc expr cstr =
 
 let mk_algebraic_project loc ~guarded expr cstr =
   mk_localized loc (PPproject (guarded, expr, cstr))
-
-let mk_maximize loc expr order =
-  mk_localized loc (PPoptimize {order; expr; is_max = true})
-
-let mk_minimize loc expr order =
-  mk_localized loc (PPoptimize {order; expr; is_max = false})
diff --git a/src/lib/frontend/parsed_interface.mli b/src/lib/frontend/parsed_interface.mli
@@ -100,6 +100,10 @@ val mk_push : Loc.t -> int -> decl
 
 val mk_pop : Loc.t -> int -> decl
 
+(** Declaration of optimization of objective functions. *)
+
+val mk_optimize : Loc.t -> lexpr -> bool -> decl
+
 (** Making pure and logic types *)
 
 val int_type : ppure_type
@@ -255,7 +259,3 @@ val mk_match : Loc.t -> lexpr -> (pattern * lexpr) list -> lexpr
 val mk_algebraic_test : Loc.t -> lexpr -> string -> lexpr
 
 val mk_algebraic_project : Loc.t -> guarded:bool -> lexpr -> string -> lexpr
-
-val mk_maximize: Loc.t -> lexpr -> string -> lexpr
-
-val mk_minimize: Loc.t -> lexpr -> string -> lexpr
diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml
@@ -1408,20 +1408,6 @@ and type_form ?(in_theory=false) env f =
       check_pattern_matching missing dead f.pp_loc;
       TFmatch (e, filtered_pats)
 
-    | PPoptimize {expr; order; is_max} ->
-      Options.tool_req 1 "TR-Typing-Optmize$_F$";
-      let e = type_term env expr in
-      let order =
-        try int_of_string order
-        with _ -> Errors.typing_error (ShouldBeIntLiteral order) f.pp_loc
-      in
-      let term = TTapp(Symbols.Op (Symbols.Optimize {order; is_max}), [e]) in
-      let t1 = {
-        c = {tt_desc=term; tt_ty=Ty.Tbool};
-        annot=new_id (); }
-      in
-      TFatom { c = TApred (t1, false); annot=new_id () }
-
     | _ ->
       let te1 = type_term env f in
       let ty = te1.c.tt_ty in
@@ -1690,9 +1676,6 @@ let rec no_alpha_renaming_b ((up, m) as s) f =
   | PPproject (_, e, _) ->
     no_alpha_renaming_b s e
 
-  | PPoptimize {expr; order=_; is_max=_} ->
-    no_alpha_renaming_b s expr
-
 let rec alpha_renaming_b ((up, m) as s) f =
   match f.pp_desc with
   | PPvar x ->
@@ -1950,12 +1933,6 @@ let rec alpha_renaming_b ((up, m) as s) f =
     if f1 == ff1 then f
     else {f with pp_desc = PPisConstr(ff1, a)}
 
-  | PPoptimize {expr; order; is_max} ->
-    let e' = alpha_renaming_b s expr in
-    if expr == e' then f
-    else {f with pp_desc = PPoptimize {expr=e'; order; is_max}}
-
-
 let alpha_renaming_b s f =
   try no_alpha_renaming_b s f; f
   with Exit -> alpha_renaming_b s f
@@ -2247,6 +2224,7 @@ let type_one_th_decl env e =
     let f = type_form ~in_theory:true env f in
     {c = TAxiom (loc,name,ax_kd,f); annot = new_id ()}
 
+  | Optimize (loc, _, _)
   | Theory (loc, _, _, _)
   | Logic (loc, _, _, _)
   | Rewriting(loc, _, _)
@@ -2511,12 +2489,18 @@ let rec type_decl (acc, env) d assertion_stack =
     else
       axioms_of_rules loc name lf acc env
 
-  | Goal(_loc, n, f) ->
+  | Goal (_loc, n, f) ->
     Options.tool_req 1 "TR-Typing-GoalDecl$_F$";
     (*let f = move_up f in*)
     let f = alpha_renaming_env env f in
     type_and_intro_goal acc env Thm n f, env
 
+  | Optimize (loc, expr, is_max) ->
+    Options.tool_req 1 "TR-Typing-Optimize$_F$";
+    let expr = type_term env expr in
+    let td = { c = TOptimize (loc, expr, is_max); annot = new_id () } in
+    (td, env) :: acc, env
+
   | Check_sat(_loc, n, f) ->
     Options.tool_req 1 "TR-Typing-CheckSatDecl$_F$";
     (*let f = move_up f in*)