From 46c2b3200e936999086d0fc813955a2054458000 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 9 Oct 2023 15:06:02 +0200 Subject: [PATCH] Give up if we try to optimize a strict inequality --- src/lib/reasoners/intervalCalculus.ml | 21 +++--- src/lib/reasoners/satml_frontend.ml | 2 +- src/lib/reasoners/theory.ml | 72 +++++++++++++-------- tests/dune.inc | 23 +++++++ tests/models/arith/arith7.optimize.expected | 10 +++ tests/models/arith/arith7.optimize.smt2 | 15 +++++ 6 files changed, 106 insertions(+), 37 deletions(-) create mode 100644 tests/models/arith/arith7.optimize.expected create mode 100644 tests/models/arith/arith7.optimize.smt2 diff --git a/src/lib/reasoners/intervalCalculus.ml b/src/lib/reasoners/intervalCalculus.ml index 999dcf9f97..e5e71dd3f3 100644 --- a/src/lib/reasoners/intervalCalculus.ml +++ b/src/lib/reasoners/intervalCalculus.ml @@ -1383,9 +1383,6 @@ let fm (module Oracle : S with type p = P.t) uf are_eq rclass_of env eqs = let is_num r = let ty = X.type_info r in ty == Ty.Tint || ty == Ty.Treal -let is_num_term r = - let ty = E.type_info r in ty == Ty.Tint || ty == Ty.Treal - let add_disequality are_eq env eqs p expl = let ty = P.type_info p in match P.to_list p with @@ -2062,11 +2059,16 @@ let optimizing_split env uf opt_split = E.print e (if to_max then "maximum" else "minimum") Q.print optim; + let r2 = alien_of (P.create [] optim ty) in - let t2 = mk_const_term optim ty in Debug.case_split r1 r2; - let o = Some {Th_util.opt_ord = order; opt_val = Th_util.Value t2} in - let s = LR.mkv_eq r1 r2, true, Th_util.CS (o, Th_util.Th_arith, Q.one) in + let t2 = mk_const_term optim ty in + let o = + Some {Th_util.opt_ord = order; opt_val = Th_util.Value t2} + in + let s = + LR.mkv_eq r1 r2, true, Th_util.CS (o, Th_util.Th_arith, Q.one) + in Some { opt_split with value = Value s } | None -> @@ -2089,8 +2091,7 @@ let optimizing_split env uf opt_split = in Some { opt_split with value } - | Sim.Core.Max(mx,_sol) -> - let {Sim.Core.max_v; _} = Lazy.force mx in + | Sim.Core.Max (lazy Sim.Core.{ max_v; is_le = true }, _sol) -> let max_p = Q.add max_v.bvalue.v c in let optim = if to_max then max_p else Q.mult Q.m_one max_p in Printer.print_dbg "%a has a %s: %a@." @@ -2108,6 +2109,10 @@ let optimizing_split env uf opt_split = LR.mkv_eq r1 r2, true, Th_util.CS (o, Th_util.Th_arith, Q.one) in Some { opt_split with value = Value s; } + + | Sim.Core.Max (lazy Sim.Core.{ is_le = false; _ }, _) -> + (* There is no upper bound as we try to optimize a strict bound. *) + None end (*** part dedicated to FPA reasoning ************************************) diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index d0f830470f..f6b91f77c1 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -1063,7 +1063,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct | Value _ -> assert false | Unknown -> - assert false + seen_infinity := true; acc ) obj [] in begin match acc with diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml index 9ac426041a..fcef2f82a2 100644 --- a/src/lib/reasoners/theory.ml +++ b/src/lib/reasoners/theory.ml @@ -428,42 +428,58 @@ module Main_Default : S = struct | Th_util.Unknown -> acc (* not optimized yet *) | Value _ -> Util.MI.add ord {v with value = Unknown} acc | Pinfinity | Minfinity -> assert false (* may happen? *) - )objectives objectives + ) objectives objectives let look_for_sat ?(bad_last=None) ch env l ~for_model = - let rec aux ch bad_last dl env li = + let rec aux ~optimize ch bad_last dl env li = Options.exec_thread_yield (); match li, bad_last with | [], _ -> begin Options.tool_req 3 "TR-CCX-CS-Case-Split"; - match next_optimization ~for_model env with - | Some opt_split -> - begin - let opt_split = + if optimize then + match next_optimization ~for_model env with + | Some opt_split -> + begin match CC_X.optimizing_split env.gamma_finite opt_split with - | Some x -> x + | Some x -> + let to_opt = + register_optimized_split env.objectives x + in + let env = {env with objectives = to_opt} in + begin + match x.value with + | Value v -> + let splits = add_explanations_to_splits [v] in + aux ~optimize ch None dl env splits + | Pinfinity | Minfinity -> + if for_model then + aux ~optimize:false ch None dl env [] + else + { env with choices = List.rev dl }, ch + | Unknown -> assert false + end | None -> - (* At least one theory should be able to optimize the - split. *) - assert false - in - let to_opt = register_optimized_split env.objectives opt_split in - let env = {env with objectives = to_opt} in - begin - match opt_split.value with - | Value v -> - let splits = add_explanations_to_splits [v] in - aux ch None dl env splits - | Pinfinity | Minfinity -> if for_model then - aux ch None dl env [] + aux ~optimize:false ch None dl env [] else { env with choices = List.rev dl }, ch - | Unknown -> assert false end - end - | None -> + | None -> + begin + let l, base_env = + CC_X.case_split env.gamma_finite ~for_model + in + let env = {env with gamma_finite = base_env} in + match l with + | [] -> + { env with choices = List.rev dl }, ch + + | _ -> + let l = add_explanations_to_splits l in + aux ~optimize ch None dl env l + end + else begin let l, base_env = CC_X.case_split env.gamma_finite ~for_model @@ -475,7 +491,7 @@ module Main_Default : S = struct | _ -> let l = add_explanations_to_splits l in - aux ch None dl env l + aux ~optimize ch None dl env l end end | ((c, lit_orig, CNeg, ex_c) as a)::l, _ -> @@ -483,7 +499,7 @@ module Main_Default : S = struct CC_X.add_fact facts (LSem c,ex_c,lit_orig); let base_env, ch = CC_X.assume_literals env.gamma_finite ch facts in let env = { env with gamma_finite = base_env} in - aux ch bad_last (a::dl) env l + aux ~optimize ch bad_last (a::dl) env l (* This optimisation is not correct with the current explanation *) (* | [(c, lit_orig, CPos exp, ex_c)], Yes (dep,_) -> *) @@ -500,7 +516,7 @@ module Main_Default : S = struct let base_env, ch = CC_X.assume_literals env.gamma_finite ch facts in let env = { env with gamma_finite = base_env} in Options.tool_req 3 "TR-CCX-CS-Normal-Run"; - aux ch bad_last (a::dl) env l + aux ~optimize ch bad_last (a::dl) env l with Ex.Inconsistent (dep, classes) -> match Ex.remove_fresh exp dep with | None -> @@ -524,9 +540,9 @@ module Main_Default : S = struct let env = { env with objectives = partial_objectives_reset env.objectives is_opt } in - aux ch None dl env [neg_c, lit_orig, CNeg, dep] + aux ~optimize ch None dl env [neg_c, lit_orig, CNeg, dep] in - aux ch bad_last (List.rev env.choices) env l + aux ~optimize:true ch bad_last (List.rev env.choices) env l (* remove old choices involving fresh variables that are no longer in UF *) let filter_valid_choice uf (ra,_,_,_) = diff --git a/tests/dune.inc b/tests/dune.inc index 7b2fbdb31a..3dc1591fd0 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -192436,6 +192436,29 @@ ; Auto-generated part begin (subdir models/arith + (rule + (target arith7.optimize_optimize.output) + (deps (:input arith7.optimize.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend legacy + --dump-models + --dump-models-on stdout + %{input}))))))) + (rule + (deps arith7.optimize_optimize.output) + (alias runtest) + (package alt-ergo) + (action + (diff arith7.optimize.expected arith7.optimize_optimize.output))) (rule (target arith6.optimize_optimize.output) (deps (:input arith6.optimize.smt2)) diff --git a/tests/models/arith/arith7.optimize.expected b/tests/models/arith/arith7.optimize.expected new file mode 100644 index 0000000000..c8aef236fb --- /dev/null +++ b/tests/models/arith/arith7.optimize.expected @@ -0,0 +1,10 @@ + +unknown +( + (define-fun x () Real 0) +) + +unknown +( + (define-fun x () Real (- (/ 3 2))) +) diff --git a/tests/models/arith/arith7.optimize.smt2 b/tests/models/arith/arith7.optimize.smt2 new file mode 100644 index 0000000000..e61fb733a3 --- /dev/null +++ b/tests/models/arith/arith7.optimize.smt2 @@ -0,0 +1,15 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-const x Real) +(push 1) +(assert (< x 0.5)) +(maximize x) +(check-sat) +(get-model) +(pop 1) +(push 1) +(assert (< x (- 0.0 0.5))) +(maximize x) +(check-sat) +(get-model) +(pop 1)