diff --git a/src/lib/dune b/src/lib/dune index cdad791516..5c6688912b 100644 --- a/src/lib/dune +++ b/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 diff --git a/src/lib/frontend/cnf.ml b/src/lib/frontend/cnf.ml index e01baba4a9..fbbe94da49 100644 --- a/src/lib/frontend/cnf.ml +++ b/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) diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index b6f6331a48..8cb47f929d 100644 --- a/src/lib/frontend/frontend.ml +++ b/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) -> diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml index ffe5cb104f..dad471c80f 100644 --- a/src/lib/frontend/models.ml +++ b/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 *) diff --git a/src/lib/frontend/models.mli b/src/lib/frontend/models.mli index 9ba841e256..cbfd4ba1d2 100644 --- a/src/lib/frontend/models.mli +++ b/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. *) diff --git a/src/lib/frontend/parsed_interface.ml b/src/lib/frontend/parsed_interface.ml index 8a0fdc6d81..57e00ede67 100644 --- 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 index b01bd2f132..440b5f12f5 100644 --- 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 index 17aee6e487..a65591b669 100644 --- a/src/lib/frontend/typechecker.ml +++ b/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*) diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index 636f39399b..f6e98904ba 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/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 diff --git a/src/lib/reasoners/arrays_rel.ml b/src/lib/reasoners/arrays_rel.ml index f785cfa0aa..496709cf61 100644 --- a/src/lib/reasoners/arrays_rel.ml +++ b/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 = diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml index 34834aa21c..81856f6ecd 100644 --- a/src/lib/reasoners/bitv_rel.ml +++ b/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, [] diff --git a/src/lib/reasoners/ccx.ml b/src/lib/reasoners/ccx.ml index 0357cc8ce0..ba3f72b3ad 100644 --- a/src/lib/reasoners/ccx.ml +++ b/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 diff --git a/src/lib/reasoners/ccx.mli b/src/lib/reasoners/ccx.mli index 06d7ad1091..38f36ed8f7 100644 --- a/src/lib/reasoners/ccx.mli +++ b/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 diff --git a/src/lib/reasoners/enum_rel.ml b/src/lib/reasoners/enum_rel.ml index 405c220c7d..4c52378b61 100644 --- a/src/lib/reasoners/enum_rel.ml +++ b/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 diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index c9fa2acddc..c5ac95430a 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/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) diff --git a/src/lib/reasoners/intervalCalculus.ml b/src/lib/reasoners/intervalCalculus.ml index 74357d9c4c..68143ae89b 100644 --- a/src/lib/reasoners/intervalCalculus.ml +++ b/src/lib/reasoners/intervalCalculus.ml @@ -2045,17 +2045,32 @@ let case_split env uf ~for_model = end | _ -> res -let optimizing_split env uf opt_split = +(* Helper function used in [optimizing_objective]. *) +let middle_value env ~to_max ty p bound = + let interval = + match MP0.find_opt p env.polynomes, bound with + | Some i, Some bound -> + begin + try + if to_max then + Intervals.new_borne_sup Ex.empty bound ~is_le:false i + else + Intervals.new_borne_inf Ex.empty bound ~is_le:false i + with Intervals.NotConsistent _ -> assert false + end + | Some i, None -> i + | None, _ -> Intervals.point Q.zero ty Ex.empty + in + let q = Option.get (Intervals.pick ~to_max interval) in + alien_of (P.create [] q ty) + +let optimizing_objective env uf Objective.Function.{ e; to_max; _ } = (* soundness: if there are expressions to optmize, this should be done without waiting for ~for_model flag to be true *) - let {Th_util.r = r; is_max = to_max; e; value; _ } = opt_split in - assert (match value with - | Unknown -> true - | _ -> false - ); + let uf, _ = Uf.add uf e in let repr, _ = Uf.find uf e in let ty = E.type_info e in - let r1 = r in (* instead of repr, which may be a constant *) + let r1, _ = X.make e in (* instead of repr, which may be a constant *) let p = poly_of repr in match P.is_const p with | Some optim -> @@ -2067,11 +2082,11 @@ let optimizing_split env uf opt_split = let r2 = alien_of (P.create [] optim ty) in Debug.case_split r1 r2; let t2 = mk_const_term optim ty in - let value = Th_util.Value t2 in + let value = Objective.Value.Value t2 in let case_split = - Some (LR.mkv_eq r1 r2, true, Th_util.CS (Th_util.Th_arith, Q.one)) + LR.mkv_eq r1 r2, true, Th_util.CS (Th_util.Th_arith, Q.one) in - Some { opt_split with value; case_split } + Some Th_util.{ value; case_split } | None -> begin @@ -2097,9 +2112,16 @@ let optimizing_split env uf opt_split = | Sim.Core.Unbounded _ -> let value = - if to_max then Th_util.Pinfinity else Th_util.Minfinity + if to_max then + Objective.Value.Pinfinity + else + Objective.Value.Minfinity in - Some { opt_split with value } + let case_split = + LR.mkv_eq r1 (middle_value env ~to_max ty p None), true, Th_util.CS + (Th_util.Th_arith, Q.one) + in + Some Th_util.{ value; case_split } | Sim.Core.Max (lazy Sim.Core.{ max_v; is_le }, _sol) -> let max_p = Q.add max_v.bvalue.v c in @@ -2118,16 +2140,16 @@ let optimizing_split env uf opt_split = let t2 = mk_const_term optim ty in let value = if is_le then - Th_util.Value t2 + Objective.Value.Value t2 else begin - if to_max then Th_util.Limit (Below, t2) - else Th_util.Limit (Above, t2) + if to_max then Objective.Value.Limit (Below, t2) + else Objective.Value.Limit (Above, t2) end in - let case_split = + let r2 = if is_le then - Some (LR.mkv_eq r1 r2, true, Th_util.CS (Th_util.Th_arith, Q.one)) + r2 else (* As some bounds are strict, the value [r2] doesn't satisfy the constraints of the problem. We don't produce a case-split @@ -2136,9 +2158,12 @@ let optimizing_split env uf opt_split = we propagate the new value [value] for this objective. Indeed, we want to be able to print it while using the statement [get-objective]. *) - None + middle_value env ~to_max ty p None + in + let case_split = + LR.mkv_eq r1 r2, true, Th_util.CS (Th_util.Th_arith, Q.one) in - Some { opt_split with value; case_split } + Some { value; case_split } end (*** part dedicated to FPA reasoning ************************************) diff --git a/src/lib/reasoners/intervals.ml b/src/lib/reasoners/intervals.ml index 0a8a799751..8037d85cd0 100644 --- a/src/lib/reasoners/intervals.ml +++ b/src/lib/reasoners/intervals.ml @@ -1163,11 +1163,41 @@ let match_interval_lower {Sy.sort; is_open; kind; is_lower} i imatch = let c = Q.compare v vl in if c < 0 || c = 0 && is_open then raise Exit; imatch - let match_interval lb ub i accu = try Some (match_interval_upper ub i (match_interval_lower lb i accu)) with Exit -> None +(* Assumes: the input set of intervals is normalized. *) +let pick ~to_max { ints; is_int; _ } = + let ints = if to_max then List.rev ints else ints in + match ints with + | [] -> None + | (Minfty, Pinfty) :: _ -> Some Q.zero + | (_, Large (q, _)) :: _ when to_max -> Some q + | (_, Strict(q, _)) :: _ when to_max && is_int -> + (* By normalization, an integer interval of the form |p, q) has to + contain at least one integer and thus [q-1] is element of this + interval. *) + Some Q.(q - ~$1) + + | (Large (q, _), _) :: _ when not to_max -> Some q + | (Strict (q, _), _) :: _ when not to_max && is_int -> + (* By normalization, an integer interval of the form (q, p| has to + contain at least one integer and thus [q-1] is element of this + interval. *) + Some Q.(q + ~$1) + + | (Minfty, (Strict (q, _) | Large (q, _))) :: _ -> Some Q.(q - ~$1) + | ((Strict (q, _) | Large (q, _)), Pinfty) :: _ -> Some Q.(q + ~$1) + | ((Strict (q1, _) | Large (q1, _)), (Strict (q2, _) | Large (q2, _))) :: _ -> + begin + assert (not is_int); + Some Q.((q1 + q2) / ~$2) + end + | (_, Minfty) :: _ | (Pinfty, _) :: _ -> + (* As the set of intervals is normalized, it cannot contain + empty intervals. *) + assert false (*****************) diff --git a/src/lib/reasoners/intervals.mli b/src/lib/reasoners/intervals.mli index 51895826b3..032c908112 100644 --- a/src/lib/reasoners/intervals.mli +++ b/src/lib/reasoners/intervals.mli @@ -140,6 +140,10 @@ val add_explanation : t -> Explanation.t -> t val equal : t -> t -> bool +val pick : to_max:bool -> t -> Numbers.Q.t option +(** [pick ~to_max t] returns an elements of the set of intervals [t]. If + [to_max] is [true], we pick the largest element of [t], if it exists. + We look for the smallest element if [to_max] is [false]. *) type interval_matching = ((Numbers.Q.t * bool) option * (Numbers.Q.t * bool) option * Ty.t) diff --git a/src/lib/reasoners/ite_rel.ml b/src/lib/reasoners/ite_rel.ml index 5b255ef819..fcf3118f7d 100644 --- a/src/lib/reasoners/ite_rel.ml +++ b/src/lib/reasoners/ite_rel.ml @@ -223,7 +223,7 @@ let assume env uf la = let case_split _env _uf ~for_model:_ = [] -let optimizing_split _env _uf _opt_split = None +let optimizing_objective _env _uf _fun_ = None let query _ _ _ = None diff --git a/src/lib/reasoners/records_rel.ml b/src/lib/reasoners/records_rel.ml index 4ad392199a..a472e99f0a 100644 --- a/src/lib/reasoners/records_rel.ml +++ b/src/lib/reasoners/records_rel.ml @@ -35,7 +35,7 @@ let assume _ _ _ = (), { Sig_rel.assume = []; remove = []} let query _ _ _ = None let case_split _env _uf ~for_model:_ = [] -let optimizing_split _env _uf _opt_split = None +let optimizing_objective _env _uf _fun_ = None let add env _ _ _ = env, [] let new_terms _ = Expr.Set.empty let instantiate ~do_syntactic_matching:_ _ env _ _ = env, [] diff --git a/src/lib/reasoners/relation.ml b/src/lib/reasoners/relation.ml index db73866ef1..a489be03c3 100644 --- a/src/lib/reasoners/relation.ml +++ b/src/lib/reasoners/relation.ml @@ -152,14 +152,14 @@ let rec optimizing_dispatcher s l = | None -> optimizing_dispatcher s l end -let optimizing_split env uf opt_split = +let optimizing_objective env uf fun_ = Options.exec_thread_yield (); - optimizing_dispatcher opt_split [ - Rel1.optimizing_split env.r1 uf; - Rel2.optimizing_split env.r2 uf; - Rel3.optimizing_split env.r3 uf; - Rel4.optimizing_split env.r4 uf; - Rel5.optimizing_split env.r5 uf + optimizing_dispatcher fun_ [ + Rel1.optimizing_objective env.r1 uf; + Rel2.optimizing_objective env.r2 uf; + Rel3.optimizing_objective env.r3 uf; + Rel4.optimizing_objective env.r4 uf; + Rel5.optimizing_objective env.r5 uf ] let add env uf r t = diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml index f53c0ab225..b121031add 100644 --- a/src/lib/reasoners/sat_solver_sig.ml +++ b/src/lib/reasoners/sat_solver_sig.ml @@ -73,6 +73,10 @@ module type S = sig (* [pred_def env f] assume a new predicate definition [f] in [env]. *) val pred_def : t -> Expr.t -> string -> Explanation.t -> Loc.t -> t + (* TODO: update this documentation. *) + (** [optimize env obj ~is_max ~order] *) + val optimize : t -> to_max:bool -> Expr.t -> t + (* [unsat env f size] checks the unsatisfiability of [f] in [env]. Raises I_dont_know when the proof tree's height reaches [size]. Raises Sat if [f] is satisfiable in [env] *) diff --git a/src/lib/reasoners/sat_solver_sig.mli b/src/lib/reasoners/sat_solver_sig.mli index 53282e144b..e5228a3806 100644 --- a/src/lib/reasoners/sat_solver_sig.mli +++ b/src/lib/reasoners/sat_solver_sig.mli @@ -72,6 +72,10 @@ module type S = sig (** [pred_def env f] assume a new predicate definition [f] in [env]. *) val pred_def : t -> Expr.t -> string -> Explanation.t -> Loc.t -> t + (* TODO: update this documentation. *) + (** [optimize env obj ~is_max ~order] *) + val optimize : t -> to_max:bool -> Expr.t -> t + (** [unsat env f size] checks the unsatisfiability of [f] in [env]. Raises I_dont_know when the proof tree's height reaches [size]. Raises Sat if [f] is satisfiable in [env] *) diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml index 6cdb5e6fb6..8bccab325a 100644 --- a/src/lib/reasoners/satml.ml +++ b/src/lib/reasoners/satml.ml @@ -103,6 +103,8 @@ module type SAT_ML = sig val push : t -> Satml_types.Atom.atom -> unit val pop : t -> unit + val optimize : t -> to_max:bool -> Expr.t -> unit + end module MFF = FF.Map @@ -1857,4 +1859,8 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct end; enqueue env g.neg 0 None + let optimize env ~to_max obj = + (* TODO: Should we add the objective function to unit_tenv? *) + env.tenv <- Th.optimize env.tenv ~to_max obj + end diff --git a/src/lib/reasoners/satml.mli b/src/lib/reasoners/satml.mli index 9eaf97f760..0aa5902f32 100644 --- a/src/lib/reasoners/satml.mli +++ b/src/lib/reasoners/satml.mli @@ -97,6 +97,7 @@ module type SAT_ML = sig val push : t -> Satml_types.Atom.atom -> unit val pop : t -> unit + val optimize : t -> to_max:bool -> Expr.t -> unit end module Make (Th : Theory.S) : SAT_ML with type th = Th.t diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index a9a4e42903..eeab8f8515 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -28,6 +28,8 @@ (* *) (**************************************************************************) +module X = Shostak.Combine + module Make (Th : Theory.S) : Sat_solver_sig.S = struct module SAT = Satml.Make(Th) module Inst = Instances.Make(Th) @@ -66,7 +68,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct (** The reason why satml raised [I_dont_know] if it does; [None] by default. *) - objectives : Th_util.optimized_split Util.MI.t option ref + objectives : bool ref; } let empty_guards () = { @@ -97,7 +99,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct last_saved_model = ref None; model_gen_phase = ref false; unknown_reason = None; - objectives = ref None + objectives = ref false; } let empty_with_inst add_inst = @@ -1089,23 +1091,20 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct end let analyze_unknown_for_objectives env unknown_exn unsat_rec_prem : unit = - let obj = Th.get_objectives (SAT.current_tbox env.satml) in - if Util.MI.is_empty obj then raise unknown_exn; - env.objectives := Some obj; + let objs = Th.get_objectives (SAT.current_tbox env.satml) in + if Objective.Model.is_empty objs then raise unknown_exn; + env.objectives := true; let acc = try - Util.MI.fold - (fun _ {Th_util.e; value; r=_; is_max; _} acc -> - match value with - | Pinfinity | Minfinity -> - raise (Give_up acc) - | Value v -> - (e, v, is_max, true) :: acc - | Limit (_, v) -> - raise (Give_up ((e, v, is_max, false) :: acc)) - | Unknown -> - assert false - ) obj [] + Objective.Model.fold (fun { e; to_max; _ } value acc -> + match (value : Objective.Value.t) with + | Pinfinity | Minfinity -> + raise (Give_up acc) + | Value v -> + (e, v, to_max, true) :: acc + | Limit (_, v) -> + raise (Give_up ((e, v, to_max, false) :: acc)) + ) objs [] with Give_up acc -> acc in begin match acc with @@ -1218,7 +1217,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct try analyze_unknown_for_objectives env e unsat_rec_prem with | IUnsat (env, _) -> - assert (!(env.objectives) != None); (* objectives is a ref, it's necessiraly updated as a side-effect to best value *) raise (I_dont_know env) @@ -1226,7 +1224,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct | Util.Timeout as e -> raise e | IUnsat (env, _) as e -> - if !(env.objectives) == None then raise e; + if not !(env.objectives) then raise e; (* TODO: put the correct objectives *) raise (I_dont_know env) @@ -1380,6 +1378,10 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct SAT.assume_th_elt env.satml th_elt dep; env + let optimize env ~to_max obj = + SAT.optimize env.satml ~to_max obj; + env + let get_model env = !(env.last_saved_model) let get_unknown_reason env = env.unknown_reason diff --git a/src/lib/reasoners/sig_rel.mli b/src/lib/reasoners/sig_rel.mli index 0ee6032479..6827119342 100644 --- a/src/lib/reasoners/sig_rel.mli +++ b/src/lib/reasoners/sig_rel.mli @@ -62,10 +62,9 @@ module type RELATION = sig t -> Uf.t -> for_model:bool -> Th_util.case_split list (** case_split env returns a list of equalities *) - val optimizing_split : - t -> Uf.t -> Th_util.optimized_split -> Th_util.optimized_split option - (** [optimizing_split env uf opt_split] try to optimize the expression - contained in [opt_split]. *) + val optimizing_objective : + t -> Uf.t -> Objective.Function.t -> Th_util.optimized_split option + (** [optimizing_split env uf fun_] try to optimize objective [fun_]. *) val add : t -> Uf.t -> Shostak.Combine.r -> Expr.t -> t * (Shostak.Combine.r Xliteral.view * Explanation.t) list diff --git a/src/lib/reasoners/th_util.ml b/src/lib/reasoners/th_util.ml index fd86d5a77a..925fc6e138 100644 --- a/src/lib/reasoners/th_util.ml +++ b/src/lib/reasoners/th_util.ml @@ -38,17 +38,6 @@ type theory = | Th_UF [@@deriving show] -type limit_kind = - | Above - | Below - -type 'a optimized_split_value = - | Minfinity - | Pinfinity - | Value of 'a - | Limit of limit_kind * 'a - | Unknown - type lit_origin = | Subst | CS of theory * Numbers.Q.t @@ -59,13 +48,6 @@ type lit_origin = type case_split = Shostak.Combine.r Xliteral.view * bool * lit_origin type optimized_split = { - r : Shostak.Combine.r; - e : Expr.t; - value : Expr.t optimized_split_value; - case_split : case_split option; - is_max : bool; - (** For linear arithmetic: is_max <-> (opt = maximize). *) - - order : int - (** Ordering assigned by the user for this variable. *) + value : Objective.Value.t; + case_split : case_split; } diff --git a/src/lib/reasoners/th_util.mli b/src/lib/reasoners/th_util.mli index 44863888ac..eb121fd070 100644 --- a/src/lib/reasoners/th_util.mli +++ b/src/lib/reasoners/th_util.mli @@ -38,23 +38,6 @@ type theory = | Th_UF [@@deriving show] -type limit_kind = - | Above - | Below - (** Type used to discriminate between limits from above or below. *) - -type 'a optimized_split_value = - | Minfinity - | Pinfinity - | Value of 'a - | Limit of limit_kind * 'a - (** This case occurs when we try to optimize a strict bound. For instance, - we have a constraint of the form [x < 2], there is no maximum for [x] but - [2] is an upper bound. So [2] is a limit from below of the possible model - values. *) - - | Unknown - (** Indicates where asserted literals come from. Note that literals are deduplicated before being propagated to the @@ -98,10 +81,10 @@ type lit_origin = type case_split = Shostak.Combine.r Xliteral.view * bool * lit_origin type optimized_split = { - r : Shostak.Combine.r; - e : Expr.t; - value : Expr.t optimized_split_value; - case_split : case_split option; - is_max : bool; - order : int + value : Objective.Value.t; + case_split : case_split; + (** The underlying case-split. Notice that this case-split doesn't always + propagate to CC(X) an equality of the form [r = v] where [v] should be + the above value [v]. Indeed, the value [value] isn't always a proper model + value. *) } diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml index e75af7423b..520db88960 100644 --- a/src/lib/reasoners/theory.ml +++ b/src/lib/reasoners/theory.ml @@ -52,16 +52,19 @@ module type S = sig (E.t * Explanation.t * int * int) list -> t -> t * Expr.Set.t * int + val optimize : t -> to_max:bool -> Expr.t -> t + (** [optimize env obj] *) + (* TODO: update this documentation. *) + val query : E.t -> t -> Th_util.answer val cl_extract : t -> Expr.Set.t list val extract_ground_terms : t -> Expr.Set.t val get_real_env : t -> Ccx.Main.t val get_case_split_env : t -> Ccx.Main.t val do_case_split : t -> Util.case_split_policy -> t * Expr.Set.t + val add_term : t -> Expr.t -> add_in_cs:bool -> t - val compute_concrete_model : - t -> - Models.t Lazy.t option + val compute_concrete_model : t -> Models.t Lazy.t option val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t val theories_instances : @@ -72,7 +75,7 @@ module type S = sig val get_assumed : t -> E.Set.t val reinit_cpt : unit -> unit - val get_objectives : t -> Th_util.optimized_split Util.MI.t + val get_objectives : t -> Objective.Model.t end module Main_Default : S = struct @@ -348,7 +351,9 @@ module Main_Default : S = struct gamma : CC_X.t; gamma_finite : CC_X.t; choices : choice list; - objectives : Th_util.optimized_split Util.MI.t; + objectives : Objective.Function.t Fqueue.t; + objective_n : int; + objectives_values : Objective.Model.t; } let add_explanations_to_split (c, is_cs, size) = @@ -360,21 +365,12 @@ module Main_Default : S = struct (* A new explanation in order to track the choice *) (c, size, CPos exp, ex_c_exp, None) - let register_optimized_split objectives u = - try - let x = Util.MI.find u.Th_util.order objectives in - assert (E.equal x.Th_util.e u.Th_util.e); - (* and its Value ... *) - Util.MI.add u.Th_util.order u objectives - with Not_found -> - assert false - exception Found of Th_util.optimized_split (* TODO: this function could be optimized if "objectives" structure is coded differently *) - let next_optimization ~for_model env = - try + (* let next_optimization ~for_model env = + try Util.MI.iter (fun _ x -> match x.Th_util.value with | Value _ -> @@ -398,16 +394,17 @@ module Main_Default : S = struct ) env.objectives; None - with - | Found x -> Some x - - (* TODO: this function could be optimized if "objectives" structure - is coded differently *) - let partial_objectives_reset objectives order = - match order with - | None -> objectives - | Some opt_ord -> - Util.MI.fold + with + | Found x -> Some x *) + + (* TODO: We cannot retrieve the order of an objecive with the current + structure used for objective model. *) + let partial_objectives_reset env _order = + (* Objective.Map.filter (fun { }) + match order with + | None -> objectives + | Some opt_ord -> + Util.MI.fold (fun ord v acc -> if ord < opt_ord then (*don't change older optims that are still valid splits*) @@ -417,9 +414,10 @@ module Main_Default : S = struct | Th_util.Unknown -> acc (* not optimized yet *) | Value _ | Limit _ -> Util.MI.add ord {v with value = Unknown} acc - | Pinfinity | Minfinity -> - assert false (* may happen? *) - ) objectives objectives + | Pinfinity | Minfinity -> + assert false (* may happen? *) + ) objectives objectives *) + { env with objectives_values = Objective.Model.empty } let look_for_sat ~for_model env sem_facts new_choices = let rec generate_choices env sem_facts acc_choices = @@ -440,39 +438,15 @@ module Main_Default : S = struct in aux env sem_facts acc_choices new_choices - and optimizing_split env sem_facts acc_choices opt_split = + and optimizing_objective env sem_facts acc_choices obj = let opt_split = - Option.get (CC_X.optimizing_split env.gamma_finite opt_split) + Option.get (CC_X.optimizing_objective env.gamma_finite obj) in - let objectives = - register_optimized_split env.objectives opt_split + let objectives_values = + Objective.Model.add obj opt_split.value env.objectives_values in - let env = { env with objectives } in + let env = { env with objectives_values } in match opt_split.value with - | Unknown -> - (* In the current implementation of optimization, the function - [CC_X.optimizing_split] cannot fail to optimize the split - [opt_split]. First of all, the legacy parser only accepts - optimization clauses on expressions of type [Real] or [Int]. - - For the [Real] or [Int] expressions, we have two cases: - - If the objective function is a linear functions of variables, the - decision procedure implemented in Ocplib-simplex cannot fail to - optimize the split. For instance, if we try to maximize the - expression: - 5 * x + 2 * y + 3 where x and y are real variables, - the procedure will success to produce the upper bound of [x] and - [y] modulo the other constraints on it. - - - If the objective function isn't linear, the nonlinear part of the - expression have seen as uninterpreted term of the arithemic theory. - Let's imagine we try to maximize the expression: - 5 * x * x + 2 * y + 3, - The objective function given to Ocplib-simplex looks like: - 5 * U + 2 * y + 3 where U = x * x - and the procedure will optimize the problem in terms of U and y. *) - assert false - | Pinfinity | Minfinity | Limit _ -> (* We stop optimizing the split [opt_split] in this case, but we continue to produce a model if the flag [for_model] is up. *) @@ -483,11 +457,8 @@ module Main_Default : S = struct | Value _ -> begin - match opt_split.case_split with - | Some cs -> - let new_choice = add_explanations_to_split cs in - propagate_choices env sem_facts acc_choices [new_choice] - | None -> assert false + let new_choice = add_explanations_to_split opt_split.case_split in + propagate_choices env sem_facts acc_choices [new_choice] end (* Propagates the choice made by case-splitting to the environment @@ -552,8 +523,7 @@ module Main_Default : S = struct Printer.print_dbg "bottom (case-split):%a" Expr.print_tagged_classes classes; - let objectives = partial_objectives_reset env.objectives order in - let env = { env with objectives } in + let env = partial_objectives_reset env order in propagate_choices env sem_facts acc_choices [neg_c, lit_orig, CNeg, dep, order] @@ -561,15 +531,22 @@ module Main_Default : S = struct Options.tool_req 3 "TR-CCX-CS-Case-Split"; match new_choices with | [] -> - begin match next_optimization ~for_model env with - | Some opt_split -> - optimizing_split env sem_facts acc_choices opt_split - | None -> generate_choices env sem_facts acc_choices + let obj, objectives = Fqueue.dequeue env.objectives in + begin match obj with + | Some obj -> + let env = { env with objectives } in + optimizing_objective env sem_facts acc_choices obj + | None -> + generate_choices env sem_facts acc_choices end | _ -> propagate_choices env sem_facts acc_choices new_choices in - aux env sem_facts (List.rev env.choices) new_choices + let o = env.objectives in + let env, choices = + aux env sem_facts (List.rev env.choices) new_choices + in + { env with objectives = o }, choices (* remove old choices involving fresh variables that are no longer in UF *) let filter_valid_choice uf (ra, _, _, _, _) = @@ -618,13 +595,8 @@ module Main_Default : S = struct false ) candidates_to_keep - - let reset_objectives objectives = - Util.MI.map (fun x -> Th_util.({ x with value = Unknown }) ) objectives - let reset_case_split_env t = { t with - objectives = reset_objectives t.objectives; cs_pending_facts = []; (* be sure it's always correct when this function is called *) gamma_finite = t.gamma; (* we'll take gamma directly *) @@ -637,7 +609,7 @@ module Main_Default : S = struct (fun _ {Th_util.value; _} -> match value with | Pinfinity | Minfinity | Limit _ -> false - | Value _ | Unknown -> true + | Value _ -> true ) objectives (* This function attempts to produce a first-order model by case-splitting. @@ -673,14 +645,14 @@ module Main_Default : S = struct safely ignore the explanation which is not useful. *) let uf = CC_X.get_union_find t.gamma in let filt_choices = filter_choices uf t.choices in - let filt_choices = - if Util.MI.is_empty t.objectives || + (* let filt_choices = + if Util.MI.is_empty t.objectives || has_no_limit t.objectives (* otherwise, we may be unsound because infty optims are not propagated *) - then filt_choices - else [] - in + then filt_choices + else [] + in *) Debug.split_sat_contradicts_cs filt_choices; let t = reset_case_split_env t in look_for_sat ~for_model @@ -756,10 +728,10 @@ module Main_Default : S = struct else t, SE.empty - let update_objectives objectives assumed gamma = - let uf = CC_X.get_union_find gamma in - let reset_cs_env = ref false in - let res = + (* let update_objectives objectives assumed gamma = + let uf = CC_X.get_union_find gamma in + let reset_cs_env = ref false in + let res = List.fold_left (fun objectives (a, _, _) -> match E.term_view a with @@ -800,9 +772,9 @@ module Main_Default : S = struct (* | Not_a_term {is_lit = true} -> objectives | Not_a_term {is_lit = false} -> assert false *) ) objectives assumed - in - res, !reset_cs_env - + in + res, !reset_cs_env + *) (* facts are sorted in decreasing order with respect to (dlvl, plvl) *) let assume ordered in_facts t = let facts = CC_X.empty_facts () in @@ -830,14 +802,14 @@ module Main_Default : S = struct let gamma, _ = CC_X.assume_literals t.gamma [] facts in (* update to optimize with the new gamma *) - let objectives, reset_cs_env = - update_objectives t.objectives assumed gamma in + (* let objectives, reset_cs_env = + update_objectives t.objectives assumed gamma in *) let new_terms = CC_X.new_terms gamma in let t = {t with gamma = gamma; terms = Expr.Set.union t.terms new_terms; - objectives } + } in - let t = if reset_cs_env then reset_case_split_env t else t in + (* let t = if reset_cs_env then reset_case_split_env t else t in *) t, new_terms, cpt let get_debug_theories_instances th_instances ilvl dlvl = @@ -957,7 +929,9 @@ module Main_Default : S = struct assumed = []; cs_pending_facts = []; terms = Expr.Set.empty; - objectives = Util.MI.empty; + objectives = Fqueue.empty; + objective_n = 0; + objectives_values = Objective.Model.empty; } in let a = E.mk_distinct ~iff:false [E.vrai; E.faux] in @@ -996,11 +970,11 @@ module Main_Default : S = struct let get_case_split_env t = t.gamma_finite let compute_concrete_model env = - let { gamma_finite; assumed_set; objectives; _ }, _ = + let { gamma_finite; assumed_set; objectives_values; _ }, _ = do_case_split_aux env ~for_model:true in CC_X.extract_concrete_model ~prop_model:assumed_set - ~optimized_splits:objectives + ~optimized_objectives:objectives_values gamma_finite let assume_th_elt t th_elt dep = @@ -1008,10 +982,16 @@ module Main_Default : S = struct let get_assumed env = env.assumed_set + let optimize env ~to_max fun_ = + let obj = Objective.Function.mk ~to_max ~order:env.objective_n fun_ in + let objectives = Fqueue.enqueue obj env.objectives in + let env = reset_case_split_env env in + { env with objectives; objective_n = env.objective_n + 1 } + let reinit_cpt () = Debug.reinit_cpt () - let get_objectives env = env.objectives + let get_objectives env = env.objectives_values end module Main_Empty : S = struct @@ -1045,8 +1025,8 @@ module Main_Empty : S = struct let assume_th_elt e _ _ = e let theories_instances ~do_syntactic_matching:_ _ e _ _ _ = e, [] let get_assumed env = env.assumed_set - + let optimize env ~to_max:_ _fun_ = env let reinit_cpt () = () - let get_objectives _env = Util.MI.empty + let get_objectives _env = Objective.Model.empty end diff --git a/src/lib/reasoners/theory.mli b/src/lib/reasoners/theory.mli index 7fd2563a44..7f642d2000 100644 --- a/src/lib/reasoners/theory.mli +++ b/src/lib/reasoners/theory.mli @@ -41,17 +41,19 @@ module type S = sig (Expr.t * Explanation.t * int * int) list -> t -> t * Expr.Set.t * int + val optimize : t -> to_max:bool -> Expr.t -> t + (** [optimize env obj] *) + val query : Expr.t -> t -> Th_util.answer val cl_extract : t -> Expr.Set.t list val extract_ground_terms : t -> Expr.Set.t val get_real_env : t -> Ccx.Main.t val get_case_split_env : t -> Ccx.Main.t val do_case_split : t -> Util.case_split_policy -> t * Expr.Set.t + val add_term : t -> Expr.t -> add_in_cs:bool -> t - val compute_concrete_model : - t -> - Models.t Lazy.t option + val compute_concrete_model : t -> Models.t Lazy.t option val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t val theories_instances : @@ -64,7 +66,7 @@ module type S = sig val reinit_cpt : unit -> unit (** Reinitializes the internal counter. *) - val get_objectives : t -> Th_util.optimized_split Util.MI.t + val get_objectives : t -> Objective.Model.t end module Main_Default : S diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml index e1f03e2636..4cd6a33bab 100644 --- a/src/lib/reasoners/uf.ml +++ b/src/lib/reasoners/uf.ml @@ -1033,10 +1033,6 @@ let model_repr_of_term t env mrepr unbounded = let e = X.choose_adequate_model t rep cls in e, ME.add t e mrepr -let is_optimization_op = function - | Sy.Op Sy.Optimize _ -> true - | _ -> false - let save_cache () = LX.save_cache () @@ -1051,7 +1047,6 @@ let compute_concrete_model_of_val && not (Shostak.Records.is_mine_symb f ty)) || E.is_internal_name t || E.is_internal_skolem t || E.equal t E.vrai || E.equal t E.faux - || is_optimization_op f || Sy.is_internal f then acc @@ -1109,18 +1104,21 @@ module MED = Map.Make let terms env = ME.fold MED.add env.make MED.empty -let compute_concrete_model ?(optimized_splits=Util.MI.empty) env = +let compute_concrete_model ?(optimized_objectives=Objective.Model.empty) env = let bounded, pinfty, minfty = - Util.MI.fold - (fun _ord v ((bounded, pinfty, minfty) as acc) -> - let {Th_util.value; r; _} = v in - match value with - | Value _ | Limit _ -> - SetX.add v.Th_util.r bounded, pinfty, minfty - | Pinfinity -> bounded, SetX.add r pinfty, minfty - | Minfinity -> bounded, pinfty, SetX.add r minfty - | Unknown -> acc - ) optimized_splits (SetX.empty, SetX.empty, SetX.empty) + Objective.Model.fold (fun { e; _ } value (bounded, pinfty, minfty) -> + match (value : Objective.Value.t) with + | Value e | Limit (_, e) -> + (* TODO: we should use a different branch for the limit cases. *) + let r, _ = Shostak.Combine.make e in + SetX.add r bounded, pinfty, minfty + | Pinfinity -> + let r, _ = Shostak.Combine.make e in + bounded, SetX.add r pinfty, minfty + | Minfinity -> + let r, _ = Shostak.Combine.make e in + bounded, pinfty, SetX.add r minfty + ) optimized_objectives (SetX.empty, SetX.empty, SetX.empty) in let is_bounded = pinfty == SetX.empty && minfty == SetX.empty in (* Here, we fold on each term that appears in the 'make' map, @@ -1146,43 +1144,35 @@ let compute_concrete_model ?(optimized_splits=Util.MI.empty) env = ) (terms env) (ModelMap.empty, ModelMap.empty, ModelMap.empty, ME.empty) -let compute_objectives ~optimized_splits env mrepr = - let seen_infinity = ref false in - Util.MI.map - (fun {Th_util.e; value; r=_; _} -> - e, - (if !seen_infinity then Models.Obj_unk - else - match value with - | Pinfinity -> seen_infinity := true; Obj_pinfty - | Minfinity -> seen_infinity := true; Obj_minfty - | Value _ | Limit _ -> - let (_r_x, r_s), _mrepr = model_repr_of_term e env mrepr None in - Obj_val r_s - | Unknown -> - (* in this case, we should have !seen_infinity == true. - Which is handled in the if branch. Moreover, we - continue optimization now even if infinity is - encountered. *) - assert false - ) - ) optimized_splits - -let extract_concrete_model ~prop_model ~optimized_splits env = - let optimized_splits = - if Options.get_objectives_in_interpretation () then - optimized_splits - else - Util.MI.empty - in +(* let compute_objectives ~optimized_objectives env mrepr = + let seen_infinity = ref false in + Objective.Map.mapi + (fun { e; _ } value -> + if !seen_infinity then Models.Obj_unk + else + match (value : Objective.Value.t) with + | Pinfinity -> seen_infinity := true; Obj_pinfty + | Minfinity -> seen_infinity := true; Obj_minfty + | Value _ | Limit _ -> + let (_r_x, r_s), _mrepr = model_repr_of_term e env mrepr None in + Obj_val r_s + ) optimized_objectives +*) +let extract_concrete_model ~prop_model ~optimized_objectives env = + (* let optimized_objectives = + if Options.get_objectives_in_interpretation () then + optimized_objectives + else + Objective.Map.empty + in *) if Options.get_interpretation () then Some (lazy ( let functions, constants, arrays, mrepr = - compute_concrete_model env ~optimized_splits + compute_concrete_model env (* ~optimized_objectives *) in - let objectives = compute_objectives ~optimized_splits env mrepr in + (* let objectives = compute_objectives ~optimized_objectives env mrepr in *) { Models.propositional = prop_model; - functions; constants; arrays; objectives; + functions; constants; arrays; objectives = Objective.Model.empty; terms_values = mrepr } )) else diff --git a/src/lib/reasoners/uf.mli b/src/lib/reasoners/uf.mli index bbc2a540a8..196bfa063b 100644 --- a/src/lib/reasoners/uf.mli +++ b/src/lib/reasoners/uf.mli @@ -74,7 +74,7 @@ val assign_next : t -> (r Xliteral.view * bool * Th_util.lit_origin) list * t (** Compute a counterexample using the Uf environment *) 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 diff --git a/src/lib/structures/commands.ml b/src/lib/structures/commands.ml index d1960411d5..c539128bac 100644 --- a/src/lib/structures/commands.ml +++ b/src/lib/structures/commands.ml @@ -34,6 +34,7 @@ type sat_decl_aux = | Assume of string * Expr.t * bool | PredDef of Expr.t * string (*name of the predicate*) | RwtDef of (Expr.t Typed.rwt_rule) list + | Optimize of Expr.t * bool | Query of string * Expr.t * Ty.goal_sort | ThAssume of Expr.th_elt | Push of int @@ -62,6 +63,9 @@ let print_aux fmt = function Format.fprintf fmt "th assume %a" Expr.print_th_elt t | Push n -> Format.fprintf fmt "Push %d" n | Pop n -> Format.fprintf fmt "Pop %d" n + | Optimize (obj, is_max) -> + let s = if is_max then "maximize" else "minimize" in + Format.fprintf fmt "%s %a" s Expr.print obj let print fmt decl = print_aux fmt decl.st_decl diff --git a/src/lib/structures/commands.mli b/src/lib/structures/commands.mli index f3d5345df6..320da889ca 100644 --- a/src/lib/structures/commands.mli +++ b/src/lib/structures/commands.mli @@ -34,6 +34,7 @@ type sat_decl_aux = | Assume of string * Expr.t * bool | PredDef of Expr.t * string (*name of the predicate*) | RwtDef of (Expr.t Typed.rwt_rule) list + | Optimize of Expr.t * bool | Query of string * Expr.t * Ty.goal_sort | ThAssume of Expr.th_elt | Push of int diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 74cecdd1ca..6c2f61a318 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -2698,9 +2698,6 @@ module Purification = struct | _ -> failwith "unexpected expression in purify_form" end - | Sy.Op Sy.Optimize _ -> - purify_literal e - | Sy.Void | Sy.Int _ | Sy.Real _ | Sy.Bitv _ | Sy.Op _ | Sy.MapsTo _ -> failwith "unexpected expression in purify_form: not a formula" diff --git a/src/lib/structures/objective.ml b/src/lib/structures/objective.ml new file mode 100644 index 0000000000..df122c9d62 --- /dev/null +++ b/src/lib/structures/objective.ml @@ -0,0 +1,69 @@ +(**************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2013-2023 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of OCamlPro *) +(* Non-Commercial Purpose License, version 1. *) +(* *) +(* As an exception, Alt-Ergo Club members at the Gold level can *) +(* use this file under the terms of the Apache Software License *) +(* version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* The Alt-Ergo theorem prover *) +(* *) +(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) +(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) +(* *) +(* CNRS - INRIA - Universite Paris Sud *) +(* *) +(* Until 2013, some parts of this code were released under *) +(* the Apache Software License version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* More details can be found in the directory licenses/ *) +(* *) +(**************************************************************************) + +module Function = struct + type t = { + e : Expr.t; + to_max : bool; + order : int; + } + + let mk ~to_max ~order e = { e; order; to_max } + + let compare { order = o1; _ } { order = o2; _ } = o1 - o2 + + let pp ppf { e; order; _ } = Fmt.pf ppf "%a order: %i" Expr.print e order +end + +module Value = struct + type limit_kind = + | Above + | Below + + type t = + | Minfinity + | Pinfinity + | Value of Expr.t + | Limit of limit_kind * Expr.t + + let pp _ppf _val = assert false +end + +module Model = struct + module M = Map.Make (Function) + + type t = Value.t M.t + + let empty = M.empty + let is_empty = M.is_empty + let fold = M.fold + let add = M.add + let pp _ppf _mdl = assert false +end diff --git a/src/lib/structures/objective.mli b/src/lib/structures/objective.mli new file mode 100644 index 0000000000..5d966c6c89 --- /dev/null +++ b/src/lib/structures/objective.mli @@ -0,0 +1,70 @@ +(**************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2013-2023 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of OCamlPro *) +(* Non-Commercial Purpose License, version 1. *) +(* *) +(* As an exception, Alt-Ergo Club members at the Gold level can *) +(* use this file under the terms of the Apache Software License *) +(* version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* The Alt-Ergo theorem prover *) +(* *) +(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) +(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) +(* *) +(* CNRS - INRIA - Universite Paris Sud *) +(* *) +(* Until 2013, some parts of this code were released under *) +(* the Apache Software License version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* More details can be found in the directory licenses/ *) +(* *) +(**************************************************************************) + +module Function : sig + type t = private { + e : Expr.t; + to_max : bool; + order : int; + } + (** Type of an objective function. *) + + val mk : to_max:bool -> order:int -> Expr.t -> t + val pp : t Fmt.t +end + +module Value : sig + type limit_kind = + | Above + | Below + (** Type used to discriminate between limits from above or below. *) + + type t = + | Minfinity + | Pinfinity + | Value of Expr.t + | Limit of limit_kind * Expr.t + (** This case occurs when we try to optimize a strict bound. For instance, + we have a constraint of the form [x < 2], there is no maximum for [x] but + [2] is an upper bound. So [2] is a limit from below of the possible model + values. *) + + val pp : t Fmt.t +end + +module Model : sig + type t + + val empty : t + val is_empty : t -> bool + val fold : (Function.t -> Value.t -> 'a -> 'a) -> t -> 'a -> 'a + val add : Function.t -> Value.t -> t -> t + val pp : t Fmt.t +end diff --git a/src/lib/structures/parsed.ml b/src/lib/structures/parsed.ml index 7b9b8ec630..01a8077598 100644 --- a/src/lib/structures/parsed.ml +++ b/src/lib/structures/parsed.ml @@ -167,7 +167,6 @@ and pp_desc = | PPmatch of lexpr * (pattern * lexpr) list | PPisConstr of lexpr * string | PPproject of bool * lexpr * string - | PPoptimize of { expr : lexpr; order : string; is_max : bool } let rec pp_lexpr fmt {pp_desc; _} = let open Format in @@ -233,10 +232,6 @@ let rec pp_lexpr fmt {pp_desc; _} = | PPmatch (_le, _plel) -> fprintf fmt "match" | PPisConstr (le, s) -> fprintf fmt "isConstr: %a %s" pp_lexpr le s | PPproject (b, le, s) -> fprintf fmt "project: %b %a %s" b pp_lexpr le s - | PPoptimize {expr; order; is_max=true} -> - fprintf fmt "maximize(%a, %s)" pp_lexpr expr order - | PPoptimize {expr; order; is_max=false} -> - fprintf fmt "minimize(%a, %s)" pp_lexpr expr order and pp_lexpr_list fmt tl = Format.fprintf fmt "@[%a@]" @@ -283,5 +278,6 @@ type decl = | Pop of Loc.t * int | Reset of Loc.t | Exit of Loc.t + | Optimize of Loc.t * lexpr * bool type file = decl list diff --git a/src/lib/structures/parsed.mli b/src/lib/structures/parsed.mli index 9ecf29d1d8..33c348ac22 100644 --- a/src/lib/structures/parsed.mli +++ b/src/lib/structures/parsed.mli @@ -100,7 +100,6 @@ and pp_desc = | PPmatch of lexpr * (pattern * lexpr) list | PPisConstr of lexpr * string | PPproject of bool * lexpr * string - | PPoptimize of { expr : lexpr; order : string; is_max : bool } val pp_lexpr : Format.formatter -> lexpr -> unit val pp_lexpr_list : Format.formatter -> lexpr list -> unit @@ -140,5 +139,6 @@ type decl = | Pop of Loc.t * int | Reset of Loc.t | Exit of Loc.t + | Optimize of Loc.t * lexpr * bool type file = decl list diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index 2289d9ab4e..b8a9cbb029 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -55,7 +55,6 @@ type operator = | Int_floor | Int_ceil | Integer_log2 | Max_real | Max_int | Min_real | Min_int | Not_theory_constant | Is_theory_constant | Linear_dependency - | Optimize of {order : int; is_max : bool} type lit = (* literals *) @@ -160,10 +159,6 @@ let compare_operators op1 op2 = let r = Int.compare i1 i2 in if r = 0 then Int.compare j1 j2 else r | Int2BV n1, Int2BV n2 -> Int.compare n1 n2 - | Optimize {order=o1; is_max=b1}, Optimize {order=o2; is_max=b2} -> - let c = o1 - o2 in - if c <> 0 then c - else Stdlib.compare b1 b2 | _ , (Plus | Minus | Mult | Div | Modulo | Real_is_int | Concat | Extract _ | Get | Set | Fixed | Float | Reach | Access _ | Record | Sqrt_real | Abs_int | Abs_real @@ -172,7 +167,7 @@ let compare_operators op1 op2 = | Integer_log2 | Pow | Integer_round | BVnot | BVand | BVor | Int2BV _ | BV2Nat | Not_theory_constant | Is_theory_constant | Linear_dependency - | Constr _ | Destruct _ | Tite | Optimize _) -> assert false + | Constr _ | Destruct _ | Tite) -> assert false ) let compare_builtin b1 b2 = @@ -385,9 +380,6 @@ let to_string ?(show_vars=true) x = match x with | Form form -> string_of_form form | Let -> "let" - | Op (Optimize {order; is_max=true}) -> Format.sprintf "maximize(-,%d)" order - | Op (Optimize {order; is_max=false}) -> Format.sprintf "minimize(-,%d)" order - let to_string_clean s = to_string ~show_vars:false s let to_string s = to_string ~show_vars:true s diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli index 59078b83ff..b0eb98c384 100644 --- a/src/lib/structures/symbols.mli +++ b/src/lib/structures/symbols.mli @@ -55,7 +55,6 @@ type operator = | Int_floor | Int_ceil | Integer_log2 | Max_real | Max_int | Min_real | Min_int | Not_theory_constant | Is_theory_constant | Linear_dependency - | Optimize of {order : int; is_max : bool} type lit = (* literals *) diff --git a/src/lib/structures/typed.ml b/src/lib/structures/typed.ml index 5ea144cfed..01bc4cad15 100644 --- a/src/lib/structures/typed.ml +++ b/src/lib/structures/typed.ml @@ -175,6 +175,7 @@ and 'a tdecl = | TPop of Loc.t * int | TReset of Loc.t | TExit of Loc.t + | TOptimize of Loc.t * 'a atterm * bool (*****) @@ -363,5 +364,8 @@ let rec print_tdecl fmt = function | TTypeDecl _ -> Format.fprintf fmt "type decl" | TReset _ -> Format.fprintf fmt "reset" | TExit _ -> Format.fprintf fmt "exit" + | TOptimize (_loc, obj, is_max) -> + let s = if is_max then "maximize" else "minimize" in + Format.fprintf fmt "%s %a" s print_term obj and print_atdecl fmt a = print_tdecl fmt a.c diff --git a/src/lib/structures/typed.mli b/src/lib/structures/typed.mli index f12058d919..cfea91a510 100644 --- a/src/lib/structures/typed.mli +++ b/src/lib/structures/typed.mli @@ -285,6 +285,11 @@ and 'a tdecl = | TExit of Loc.t (** Exits the solver. *) + | TOptimize of Loc.t * 'a atterm * bool + (** Optimization declaration. + [TOptimize (loc, obj, is_max] declares an objective function [obj]. The + flag [is_max] determines if we try to maximize of minimize [obj]. *) + (** Typed declarations. *) (* TODO: wrap this in a record to factorize away the location and name of the declaration ? *) diff --git a/src/lib/util/fqueue.ml b/src/lib/util/fqueue.ml new file mode 100644 index 0000000000..baf9b307a3 --- /dev/null +++ b/src/lib/util/fqueue.ml @@ -0,0 +1,55 @@ +(**************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2013-2023 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of OCamlPro *) +(* Non-Commercial Purpose License, version 1. *) +(* *) +(* As an exception, Alt-Ergo Club members at the Gold level can *) +(* use this file under the terms of the Apache Software License *) +(* version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* The Alt-Ergo theorem prover *) +(* *) +(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) +(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) +(* *) +(* CNRS - INRIA - Universite Paris Sud *) +(* *) +(* Until 2013, some parts of this code were released under *) +(* the Apache Software License version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* More details can be found in the directory licenses/ *) +(* *) +(**************************************************************************) + +type 'a t = 'a list * ('a list) + +let empty : 'a t = ([], []) + +let enqueue elt (push, pop) = (elt :: push, pop) + +let rec dequeue (push, pop) = + match push, pop with + | [], [] -> None, ([], []) + | _, elt :: pop -> Some elt, (push, pop) + | push, _ -> dequeue ([], List.rev push) + +let rec peek (push, pop) = + match push, pop with + | [], [] -> None + | _, elt :: _ -> Some elt + | push, _ -> peek ([], List.rev push) + +let of_seq seq = ([], List.of_seq seq) + +let to_seq (push, pop) = + List.(rev_append push pop |> to_seq) + +let pp pp_elt ppf queue = + Fmt.seq pp_elt ppf (to_seq queue) diff --git a/src/lib/util/fqueue.mli b/src/lib/util/fqueue.mli new file mode 100644 index 0000000000..589ddb7cae --- /dev/null +++ b/src/lib/util/fqueue.mli @@ -0,0 +1,52 @@ +(**************************************************************************) +(* *) +(* Alt-Ergo: The SMT Solver For Software Verification *) +(* Copyright (C) 2013-2023 --- OCamlPro SAS *) +(* *) +(* This file is distributed under the terms of OCamlPro *) +(* Non-Commercial Purpose License, version 1. *) +(* *) +(* As an exception, Alt-Ergo Club members at the Gold level can *) +(* use this file under the terms of the Apache Software License *) +(* version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* The Alt-Ergo theorem prover *) +(* *) +(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) +(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) +(* *) +(* CNRS - INRIA - Universite Paris Sud *) +(* *) +(* Until 2013, some parts of this code were released under *) +(* the Apache Software License version 2.0. *) +(* *) +(* --------------------------------------------------------------- *) +(* *) +(* More details can be found in the directory licenses/ *) +(* *) +(**************************************************************************) + +type 'a t +(** Type of the functional queue. *) + +val empty : 'a t +(** The empty queue. *) + +val enqueue : 'a -> 'a t -> 'a t +(** [push e queue] pushes an element on the back of queue. *) + +val dequeue : 'a t -> 'a option * 'a t +(** [pop queue] returns and removes the element on the top + of [queue] or [None] if the queue is empty. *) + +val peek : 'a t -> 'a option +(** [top queue] returns the element on the top of [queue] or + [None] if the queue is empty. *) + +val pp : 'a Fmt.t -> 'a t Fmt.t +(** [pp pp_elt ppf queue] prints the queue [queue] on the formatter + [ppf] using the printer [pp_elt] for its elements. *) + +val of_seq : 'a Seq.t -> 'a t diff --git a/src/lib/util/numbers.ml b/src/lib/util/numbers.ml index c878b32461..0c37eec3c5 100644 --- a/src/lib/util/numbers.ml +++ b/src/lib/util/numbers.ml @@ -234,7 +234,13 @@ module Q = struct if not (is_zero s) then Some (div q s) else accurate_root_excess q 2 - let root_default = accurate_root_default let root_excess = accurate_root_excess + + let (~$$) = Q.(~$$) + let (~$) = Q.(~$) + let ( + ) = Q.(+) + let ( - ) = Q.(-) + let ( * ) = Q.( * ) + let ( / ) = Q.( / ) end diff --git a/src/lib/util/numbers.mli b/src/lib/util/numbers.mli index fac3e45b6e..e06de7a29b 100644 --- a/src/lib/util/numbers.mli +++ b/src/lib/util/numbers.mli @@ -154,4 +154,11 @@ module Q : sig val root_excess : t -> int -> t option val sqrt_default : t -> t option val sqrt_excess : t -> t option + + val (~$$) : Z.t -> t + val (~$) : int -> t + val ( + ) : t -> t -> t + val ( - ) : t -> t -> t + val ( * ) : t -> t -> t + val ( / ) : t -> t -> t end diff --git a/src/parsers/native_lexer.mll b/src/parsers/native_lexer.mll index 1090e63299..98fe57b157 100644 --- a/src/parsers/native_lexer.mll +++ b/src/parsers/native_lexer.mll @@ -100,8 +100,8 @@ let decimal_number s = let r = ref n_zero in for i=0 to String.length s - 1 do - r := Numbers.Q.(add (mult n_ten !r) - (from_int (Char.code s.[i] - Char.code '0'))) + let c = Char.(code s.[i] - code '0') in + r := Numbers.Q.(add (mult n_ten !r) (from_int c)) done; !r diff --git a/src/parsers/native_parser.mly b/src/parsers/native_parser.mly index dd96f92163..1c5ceda187 100644 --- a/src/parsers/native_parser.mly +++ b/src/parsers/native_parser.mly @@ -379,12 +379,6 @@ lexpr: | MATCH e = lexpr WITH cases = list1_match_cases END { mk_match ($startpos, $endpos) e (List.rev cases) } -| MAXIMIZE LEFTPAR simple_expr COMMA INTEGER RIGHTPAR - { mk_maximize ($startpos, $endpos) $3 $5 } - -| MINIMIZE LEFTPAR simple_expr COMMA INTEGER RIGHTPAR - { mk_minimize ($startpos, $endpos) $3 $5 } - list1_match_cases: | p = simple_pattern RIGHTARROW e = lexpr { [p, e]} | BAR p = simple_pattern RIGHTARROW e = lexpr { [p, e]} diff --git a/src/parsers/psmt2_to_alt_ergo.ml b/src/parsers/psmt2_to_alt_ergo.ml index 9c8ae8f1dc..094e12d1e4 100644 --- a/src/parsers/psmt2_to_alt_ergo.ml +++ b/src/parsers/psmt2_to_alt_ergo.ml @@ -404,17 +404,12 @@ module Translate = struct mk_goal loc gname e let translate_optimize = - let cpt = ref 0 in fun ~is_maximize pos term -> - Printer.print_wrn - "optimize commands only work if the file contains check-sat@."; - assert (name_of_assert term == None); - incr cpt; - let e = translate_term [] term in - let func = if is_maximize then mk_maximize else mk_minimize in - let e = func pos e (string_of_int !cpt) in - let name = Format.sprintf "unamed__assert__%d" !cpt in - mk_generic_axiom pos name e + Printer.print_wrn + "optimize commands only work if the file contains check-sat@."; + assert (name_of_assert term == None); + let e = translate_term [] term in + mk_optimize pos e is_maximize let translate_command acc command = match command.c with diff --git a/tests/dune.inc b/tests/dune.inc index 0eac6e7ac0..7aceeac9b1 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -193025,6 +193025,7 @@ --enable-assertions --output=smtlib2 --frontend legacy + --optimize --dump-models --dump-models-on stdout %{input}))))))) @@ -193048,6 +193049,7 @@ --enable-assertions --output=smtlib2 --frontend legacy + --optimize --dump-models --dump-models-on stdout %{input}))))))) @@ -193071,6 +193073,7 @@ --enable-assertions --output=smtlib2 --frontend legacy + --optimize --dump-models --dump-models-on stdout %{input}))))))) @@ -193094,6 +193097,7 @@ --enable-assertions --output=smtlib2 --frontend legacy + --optimize --dump-models --dump-models-on stdout %{input}))))))) @@ -193117,6 +193121,7 @@ --enable-assertions --output=smtlib2 --frontend legacy + --optimize --dump-models --dump-models-on stdout %{input}))))))) @@ -193140,6 +193145,7 @@ --enable-assertions --output=smtlib2 --frontend legacy + --optimize --dump-models --dump-models-on stdout %{input}))))))) @@ -193163,6 +193169,7 @@ --enable-assertions --output=smtlib2 --frontend legacy + --optimize --dump-models --dump-models-on stdout %{input}))))))) @@ -193208,6 +193215,7 @@ --enable-assertions --output=smtlib2 --frontend legacy + --optimize --dump-models --dump-models-on stdout %{input}))))))) @@ -193231,6 +193239,7 @@ --enable-assertions --output=smtlib2 --frontend legacy + --optimize --dump-models --dump-models-on stdout %{input}))))))) diff --git a/tools/gentest.ml b/tools/gentest.ml index 97ac7fbe8b..24c2ac2c44 100644 --- a/tools/gentest.ml +++ b/tools/gentest.ml @@ -407,6 +407,7 @@ let () = ; ("runtest", "optimize", [ "--output=smtlib2" ; "--frontend legacy" + ; "--optimize" ; "--dump-models" ; "--dump-models-on stdout"])] in