diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index aa3d2c89a0..6097a4bcdc 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -588,6 +588,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct try env.cdcl := CDCL.forget_decision !(env.cdcl) f lvl with + (* TODO: remove this dangerous match. *) | _ -> Printer.print_err "@[cdcl_backjump error:@,%s@]" @@ -770,8 +771,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct try let ff, _, _, _ = ME.find nf env.gamma in aux gf ff with Not_found -> gf - - let do_bcp env tcp tcp_cache tmp_cache delta acc = let tcp = tcp && not (Options.get_no_tcp ()) in List.fold_left @@ -1689,8 +1688,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct check_no_decision_in_env env; Debug.is_it_unsat gf; try - let env = assume env env.pending_assumes in - let env = { env with pending_assumes = [] } in + (* let env = assume env env.pending_assumes in + let env = { env with pending_assumes = [] } in *) let guards_to_assume = ME.fold (fun _g gf_guard_with_ex acc -> gf_guard_with_ex :: acc @@ -1767,7 +1766,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct (* in case of all-models and/or call to solver with old unbacktracked decisions *) check_no_decision_in_env env; - if Options.get_process_when_assuming() then + if true then + (* TODO: fix regressions when we disable this option. *) +(* if Options.get_process_when_assuming() then *) try if Options.get_tableaux_cdcl () then cdcl_assume false env [add_guard env fg,dep]; diff --git a/src/lib/reasoners/intervalCalculus.ml b/src/lib/reasoners/intervalCalculus.ml index 9e2aed732c..465cc08d10 100644 --- a/src/lib/reasoners/intervalCalculus.ml +++ b/src/lib/reasoners/intervalCalculus.ml @@ -1656,6 +1656,27 @@ let update_used_by_pow env r1 p2 orig eqs = ) s eqs with Exit | Not_found -> eqs +let exists_in_simplex sim x = + Sim.Core.(MX.mem x sim.basic) || Sim.Core.(MX.mem x sim.non_basic) + +(* used radius in cube-test implementation *) +let radius = X.term_embed @@ Expr.mk_term (Sy.name "!radius") [] Ty.Tint +let cube_obj = Sim.Core.P.from_list [radius, Q.one] + +let bnd_to_simplex_bound ((bnd, explanation) : I.bnd) : Sim.Core.bound option = + match bnd with + | None -> None + | Some (bnd, offset) -> + let bvalue = + if Q.equal offset Q.one + then Sim.Core.R2.lower bnd + else if Q.equal offset Q.m_one + then Sim.Core.R2.upper bnd + else if Q.equal offset Q.zero + then Sim.Core.R2.of_r bnd + else assert false (* alt-ergo style *) + in Some {bvalue; explanation} + (* extract non trivial constraints on integer expressions from maps of intervals *) let int_constraints_from_map_intervals = @@ -1671,14 +1692,6 @@ let int_constraints_from_map_intervals = in MX.fold (fun x (i,_) acc -> aux (poly_of x) x i uf acc) env.monomes acc - -let exists_in_simplex sim x = - Sim.Core.(MX.mem x sim.basic) || Sim.Core.(MX.mem x sim.non_basic) - -(* used radius in cube-test implementation *) -let radius = X.term_embed @@ Expr.mk_term (Sy.name "!radius") [] Ty.Tint -let cube_obj = Sim.Core.P.from_list [radius, Q.one] - let fm_simplex_cube_integers_encoding env uf has_eqs = let simplex = match env.cube_sim with @@ -1686,19 +1699,17 @@ let fm_simplex_cube_integers_encoding env uf has_eqs = cube (* reuse existing simplex *) | _ -> (* existing simplex, if any, not normalized wrt eqs ? reset it *) - Sim.Core.empty ~is_int:true ~check_invs:true ~debug:0 + Sim.Core.empty ~is_int:true ~check_invs:true in let simplex, _ = (* assert that radius >= 0 *) - Sim.Assert.var - simplex radius (Some (Q.zero, Q.zero)) Ex.empty None Ex.empty in + Sim.Assert.var simplex radius + in List.fold_left (fun simplex (p, uints) -> let (mn, ex_mn), (mx, ex_mx) = match uints, List.rev uints with - | [], [] -> - (None, Ex.empty), (None, Ex.empty) - | ((mn, ex_mn), _) ::_, (_, (mx, ex_mx)) :: _ -> - (mn, ex_mn), (mx, ex_mx) + | [], [] -> (None, Ex.empty), (None, Ex.empty) + | (min, _) ::_, (_, max) :: _ -> min, max | [], _ | _, [] -> assert false in if mn == None && mx == None then simplex @@ -1707,7 +1718,7 @@ let fm_simplex_cube_integers_encoding env uf has_eqs = assert (Q.sign c = 0); let l = List.rev_map (fun (c, x) -> x, c) (List.rev l) in let cst0 = - List.fold_left (fun z (_, c) -> Q.add z (Q.abs c))Q.zero l + List.fold_left (fun z (_, c) -> Q.add z (Q.abs c)) Q.zero l in let cst = Q.div cst0 (Q.from_int 2) in let p_radius = P.create [cst, radius] Q.zero Ty.Tint in @@ -1722,16 +1733,16 @@ let fm_simplex_cube_integers_encoding env uf has_eqs = let lpge = P.to_list pge |> fst |> List.map (fun (a, b) -> b, a) in let lple = P.to_list ple |> fst |> List.map (fun (a, b) -> b, a) in let simplex = (* assert lower bound *) - if mn == None then simplex - else + match mn with + | None -> simplex + | Some _ -> + let min = bnd_to_simplex_bound (mn, ex_mn) in fst @@ if exists_in_simplex simplex xpge then - Sim.Assert.var - simplex xpge mn ex_mn None Ex.empty + Sim.Assert.var simplex xpge ?min else Sim.Assert.poly - simplex (Sim.Core.P.from_list lpge) xpge - mn ex_mn None Ex.empty + simplex (Sim.Core.P.from_list lpge) xpge ?min in let rev_mx = match mx with @@ -1739,17 +1750,17 @@ let fm_simplex_cube_integers_encoding env uf has_eqs = | Some (a, b) -> Some (Q.mult Q.m_one a, Q.mult Q.m_one b) in let simplex = - if rev_mx == None then simplex - else - fst @@ - (* assert upper bound -> inverted as a lower bound *) - if exists_in_simplex simplex xple then - Sim.Assert.var - simplex xple rev_mx ex_mx None Ex.empty - else - Sim.Assert.poly - simplex (Sim.Core.P.from_list lple) xple - rev_mx ex_mx None Ex.empty + match rev_mx with + | None -> simplex + | Some _ -> + let max = bnd_to_simplex_bound (mx, ex_mx) in + fst @@ + (* assert upper bound -> inverted as a lower bound *) + if exists_in_simplex simplex xple then + Sim.Assert.var simplex xple ?max + else + Sim.Assert.poly + simplex (Sim.Core.P.from_list lple) xple ?max in simplex ) simplex (int_constraints_from_map_intervals env uf) @@ -1777,7 +1788,7 @@ let solve_cube_integers env are_eq sim = | Sim.Core.Max(mx,_sol) -> (* implied bounds or eqs *) let {Sim.Core.max_v; _} = Lazy.force mx in let obj = match mx_res with None -> assert false | Some (p, _) -> p in - Debug.optimum obj max_v; + Debug.optimum obj (max_v.bvalue.v); let deds, ex = (* deductions + explanation *) List.fold_left (fun (l, ex) (x0, q) -> @@ -1788,37 +1799,44 @@ let solve_cube_integers env are_eq sim = let rv = alien_of (P.create [] Q.zero Ty.Tint) in let x = X.subst radius rv x0 in (* remove radius from x *) (* necessiraly equals low min or max bound *) - let (l_i, w) as value = x_info.value in + let (l_i, w) = + (x_info.value.v, x_info.value.offset) + in assert (Q.sign w = 0); (* no strict ineqs on Ints *) (* why is this deduction correct: - we assumed constraints l_i <= ctx_i - radius is maximized by setting ctx_i's slake variables - that appear in 'obj' to their min 'l_i' + that appear in 'obj' to their min 'l_i' - 'obj' evaluates to a constant, and the coefficients of - the constraints ctx_i in it are negative (because we hit - max for objective with lower bounds). + the constraints ctx_i in it are negative (because we hit + max for objective with lower bounds). - if we rather transform the constraints to 0 <= (- l_i) + ctx_i - then, we multiply them by the abs (positive) value of - their coefficients in obj (without changin ineq's direction) + their coefficients in obj (without changin ineq's direction) 0 <= (- q) ((- l_i) + ctx_i) - finally, the SUM (- q) ((- l_i) + ctx_i) is actually equal to - obj. + obj. - Now, we can use, FM/FM-Simplex bounds deduction mecanism: - -> 0 <= (- q) ((- l_i) + ctx_i) <= max_v - -> ctx_i <= l_i + floor (max_v / (-q)) + -> 0 <= (- q) ((- l_i) + ctx_i) <= max_v + -> ctx_i <= l_i + floor (max_v / (-q)) Hence, an upper bound for ctx_i *) assert (Q.sign q < 0); - assert (Sim.Core.equals_optimum value x_info.mini); - let ded = Q.add l_i @@ Q.floor @@ Q.div max_v @@ Q.abs q in - (x, ded) :: l, Ex.union ex x_info.min_ex + assert (Sim.Core.equals_optimum x_info.value x_info.mini); + let ded = Q.add l_i @@ Q.floor @@ Q.div max_v.bvalue.v @@ Q.abs q in + let ex = + match x_info.mini with + | Some { explanation; _ } -> Ex.union ex explanation + | None -> ex + in + (x, ded) :: l, ex )([], Ex.empty) (Sim.Core.P.bindings obj) in List.fold_left (fun env (x, max_bnd) -> @@ -2174,34 +2192,6 @@ let case_split_union_of_intervals = (*****) -let bnd_to_simplex_bound ((bnd, explanation) : I.bnd) : Sim.Core.bound option = - match bnd with - | None -> None - | Some (bnd, offset) -> - let bvalue = - if Q.equal offset Q.one - then Sim.Core.R2.lower bnd - else if Q.equal offset Q.m_one - then Sim.Core.R2.upper bnd - else if Q.equal offset Q.zero - then Sim.Core.R2.of_r bnd - else assert false (* alt-ergo style *) - in Some {bvalue; explanation} - -let int_constraints_from_map_intervals = - let aux p xp i uf acc = - if Uf.is_normalized uf xp && I.is_point i == None - && P.type_info p == Ty.Tint - then (p, I.bounds_of i) :: acc - else acc - in - fun env uf -> - let acc = - MP.fold (fun p i acc -> aux p (alien_of p) i uf acc) env.polynomes [] - in - MX.fold (fun x (i,_) acc -> aux (poly_of x) x i uf acc) env.monomes acc - - let fm_simplex_unbounded_integers_encoding env uf = let simplex = Sim.Core.empty ~is_int:true ~check_invs:true in let int_ctx = int_constraints_from_map_intervals env uf in @@ -2342,11 +2332,6 @@ let optimizing_split env uf opt = let p = poly_of repr in match P.is_const p with | Some optim -> - Format.eprintf - "%a has a %s: %a@." - 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; @@ -2365,9 +2350,6 @@ let optimizing_split env uf opt = | Sim.Core.Sat _ -> assert false (* because we maximized *) | Sim.Core.Unsat _ -> assert false (* we know sim is SAT *) | Sim.Core.Unbounded _ -> - Format.eprintf - "%a is unbounded. Let other methods assign a value for it@." - E.print e; let value = if to_max then Th_util.Pinfinity else Th_util.Minfinity in Sig_rel.Optimized_split { opt with value } @@ -2378,12 +2360,6 @@ let optimizing_split env uf opt = if to_max then max_p else Q.mult Q.m_one max_p in - Format.eprintf - "%a has a %s: %a@." - E.print e - (if to_max then "maximum" else "minimum") - Q.print optim; - let r2 = alien_of (P.create [] optim ty) in Debug.case_split r1 r2; let t2 = mk_const_term optim ty in diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index b1c3fd1ef6..2e3826157c 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -1064,22 +1064,11 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct E.mk_or and_ ((if is_max then gt else lt) e tv) false 0 )((if is_max then gt else lt) e tv) l in - Format.eprintf - "Obj %a has an optimum. Should continue beyond SAT to try to \ - find a better opt than v = %a@." - Expr.print e Expr.print tv; - Format.eprintf "neg is %a@." E.print neg; let l = [mk_gf neg] in - Format.eprintf - "TODO: can we add the clause without 'cancel_until 0' ?"; + (* TODO: can we add the clause without 'cancel_until 0' ? *) SAT.cancel_until env.satml 0; let env, updated = assume_aux ~dec_lvl:0 env l in - if not updated then begin - Format.eprintf - "env not updated after injection of neg! termination \ - issue.@.@."; - assert false - end; + assert (updated); let is_gui = Options.get_is_gui() in Options.Time.unset_timeout ~is_gui; Options.Time.set_timeout ~is_gui (Options.get_timelimit ()); diff --git a/src/lib/reasoners/satml_frontend_hybrid.ml b/src/lib/reasoners/satml_frontend_hybrid.ml index 1b9da2e61c..a11240c2a4 100644 --- a/src/lib/reasoners/satml_frontend_hybrid.ml +++ b/src/lib/reasoners/satml_frontend_hybrid.ml @@ -58,9 +58,10 @@ module Make (Th : Theory.S) = struct SE.add (formula_of_atom env a) acc) (SAT.reason_of_deduction p) SE.empty in lazy (Ex.make_deps r) in - Some (l_ex,Atom.level p) + Some (l_ex, Atom.level p) else None - | None -> assert false + | None -> + Util.failwith "No proxy formula for the formula %a" E.print f let forget_decision env f lvl = let l_ok, _ = diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli index 6aaa984f15..cfa5d98513 100644 --- a/src/lib/util/options.mli +++ b/src/lib/util/options.mli @@ -455,7 +455,8 @@ val set_tighten_vars : bool -> unit (** Set [use_fpa] accessible with {!val:get_use_fpa} *) val set_use_fpa : bool -> unit -(** Set [process_when_assuming] accessible with {!val:get_process_when_assuming} *) +(** Set [process_when_assuming] accessible with + {!val:get_process_when_assuming} *) val set_process_when_assuming : bool -> unit (** Set [session_file] accessible with {!val:get_session_file} *) @@ -1026,8 +1027,8 @@ val get_use_fpa : unit -> bool (** Default to [false] *) (** [true] if SAT engine processes assumed formulas before unsat is - called (ie. adding them to SAT's env, translation to CNF, bcp, - propagation to theories, ... *) + called (ie. adding them to SAT's env, translation to CNF, bcp, + propagation to theories, ... *) val get_process_when_assuming : unit -> bool (** Default to [false] *)