Clean temporary

src/lib/dune

@@ -25,7 +25,16 @@
     alt_ergo_prelude
     fmt
   )
-  (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
@@ -44,12 +53,12 @@
     ; 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
     Options Timers Util Vec Version Steps Printer My_zip
-    Theories Compat
+    Theories Compat Fqueue
   )
 
  (js_of_ocaml

src/lib/frontend/cnf.ml

@@ -386,6 +386,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
@@ -467,5 +470,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)

src/lib/frontend/frontend.ml

@@ -335,6 +335,15 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
           let dep = mk_root_dep name f d.st_loc in
           SAT.pred_def env f name dep d.st_loc, consistent, dep
 
+      | Optimize (obj, to_max) ->
+        begin
+          match consistent with
+          | `Sat _ | `Unknown _ ->
+            SAT.optimize env ~to_max obj, consistent, dep
+          | `Unsat ->
+            env, consistent, dep
+        end
+
       | RwtDef _ -> assert false
 
       | Query(n, f, sort) ->

src/lib/frontend/models.ml

@@ -56,7 +56,7 @@ type t = {
   constants : ModelMap.t;
   functions : ModelMap.t;
   arrays : ModelMap.t;
-  objectives: (Expr.t * objective_value) Util.MI.t;
+  objectives: Objective.Model.t;
   terms_values : (Shostak.Combine.r * string) Expr.Map.t
 }
 
@@ -593,4 +593,4 @@ let output_concrete_model fmt m =
   (*     SmtlibCounterExample.output_arrays_counterexample fmt m.arrays; *)
 
   Printer.print_fmt fmt "@]@,)";
-  SmtlibCounterExample.output_objectives fmt m.objectives
+  (*   SmtlibCounterExample.output_objectives fmt m.objectives *)

src/lib/frontend/models.mli

@@ -41,7 +41,7 @@ type t = {
   constants : ModelMap.t;
   functions : ModelMap.t;
   arrays : ModelMap.t;
-  objectives: (Expr.t * objective_value) Util.MI.t;
+  objectives: Objective.Model.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. *)

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})

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

src/lib/frontend/typechecker.ml

@@ -1407,20 +1407,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
@@ -1689,9 +1675,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 ->
@@ -1949,12 +1932,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
@@ -2246,6 +2223,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, _, _)
@@ -2510,12 +2488,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*)

src/lib/reasoners/adt_rel.ml

@@ -713,7 +713,7 @@ let case_split env _uf ~for_model =
         []
     end
 
-let optimizing_split _env _uf _opt_split = None
+let optimizing_objective _env _uf _fun_ = None
 
 let query env uf (ra, _, ex, _) =
   if Options.get_disable_adts () then None

src/lib/reasoners/arrays_rel.ml

@@ -396,7 +396,7 @@ let case_split env _uf ~for_model:_ =
     Debug.case_split_none ();
     []
 
-let optimizing_split _env _uf _opt_split = None
+let optimizing_objective _env _uf _fun_ = None
 
 let count_splits env la =
   let nb =

src/lib/reasoners/bitv_rel.ml

@@ -72,7 +72,7 @@ let case_split _ _ ~for_model:_ = []
 let add env uf r t =
   let delayed, eqs = Rel_utils.Delayed.add env.delayed uf r t in
   { delayed }, eqs
-let optimizing_split _env _uf _opt_split = None
+let optimizing_objective _env _uf _fun_ = None
 let new_terms _ = Expr.Set.empty
 let instantiate ~do_syntactic_matching:_ _ env _ _ = env, []
 

src/lib/reasoners/ccx.ml

@@ -67,8 +67,8 @@ module type S = sig
     t * (r Sig_rel.literal * Explanation.t * Th_util.lit_origin) list
 
   val case_split : t -> for_model:bool -> Th_util.case_split list * t
-  val optimizing_split :
-    t -> Th_util.optimized_split -> Th_util.optimized_split option
+  val optimizing_objective :
+    t -> Objective.Function.t -> Th_util.optimized_split option
 
   val query :  t -> E.t -> Th_util.answer
   val new_terms : t -> Expr.Set.t
@@ -88,7 +88,7 @@ module type S = sig
 
   val extract_concrete_model :
     prop_model:Expr.Set.t ->
-    optimized_splits:Th_util.optimized_split Util.MI.t ->
+    optimized_objectives:Objective.Model.t ->
     t ->
     Models.t Lazy.t option
 
@@ -708,8 +708,8 @@ module Main : S = struct
       l, {env with uf}
     | _ -> cs, env
 
-  let optimizing_split env opt_split =
-    Rel.optimizing_split env.relation env.uf opt_split
+  let optimizing_objective env obj =
+    Rel.optimizing_objective env.relation env.uf obj
 
   let query env a =
     let ra, ex_ra = term_canonical_view env a Ex.empty in
@@ -752,6 +752,6 @@ module Main : S = struct
     in
     Uf.term_repr env.uf t
 
-  let extract_concrete_model ~prop_model ~optimized_splits env =
-    Uf.extract_concrete_model ~prop_model ~optimized_splits env.uf
+  let extract_concrete_model ~prop_model ~optimized_objectives env =
+    Uf.extract_concrete_model ~prop_model ~optimized_objectives env.uf
 end

src/lib/reasoners/ccx.mli

@@ -59,8 +59,8 @@ module type S = sig
     t * (r Sig_rel.literal * Explanation.t * Th_util.lit_origin) list
 
   val case_split : t -> for_model:bool -> Th_util.case_split list * t
-  val optimizing_split :
-    t -> Th_util.optimized_split -> Th_util.optimized_split option
+  val optimizing_objective :
+    t -> Objective.Function.t -> Th_util.optimized_split option
 
   val query :  t -> Expr.t -> Th_util.answer
   val new_terms : t -> Expr.Set.t
@@ -79,9 +79,10 @@ module type S = sig
 
   val extract_concrete_model :
     prop_model:Expr.Set.t ->
-    optimized_splits:Th_util.optimized_split Util.MI.t ->
+    optimized_objectives:Objective.Model.t ->
     t ->
     Models.t Lazy.t option
+
 end
 
 module Main : S

src/lib/reasoners/enum_rel.ml

@@ -330,7 +330,7 @@ let case_split env uf ~for_model =
     Debug.no_case_split ();
     []
 
-let optimizing_split _env _uf _opt_split = None
+let optimizing_objective _env _uf _fun_ = None
 
 let query env uf a_ex =
   try ignore(assume env uf [a_ex]); None

src/lib/reasoners/fun_sat.ml

@@ -1842,6 +1842,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
   let assume_th_elt env th_elt dep =
     {env with tbox = Th.assume_th_elt env.tbox th_elt dep}
 
+  let optimize _env ~to_max:_ _fun_ =
+    raise (Util.Not_implemented "optimization is not supported by FunSAT.")
+
   (** returns the latest model stored in the env if any *)
   let get_model env = !(env.last_saved_model)