From a16677e7a4d26620510c1e959fc67157831e25bf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Wed, 28 Aug 2024 16:31:33 +0200 Subject: [PATCH 1/3] fix(opt): Only perform optimization when building a model The optimization module is supposed to help us build an optimized model, so it doesn't make much sense to start optimizing before we start actually looking for a model. Previously, we were kind of forced into it because it would be incorrect to perform case splits before optimizing. Now that optimization is integrated directly into the SAT solver, it is fully independent from case splits, and this restriction does not apply any longer. This fixes issues where we would try to optimize eagerly in a small solution space and would end up enumerating the solution space before performing examining some decisions that would prune it for us, which is exactly what happened in #1222. Separate optimization (`do_optimize`) from case splitting (`do_case_split`) at the `Theory` level, and perform optimization in `compute_concrete_model`, i.e. at the time we switch to model generation (note: this limits the impact of optimization on unsat problems). Also change the order of decisions to consider optimized splits last for consistency, although that should not have much impact in practice. --- src/lib/reasoners/satml.ml | 76 ++++++++++++++++++++++-------------- src/lib/reasoners/theory.ml | 37 +++++++++--------- src/lib/reasoners/theory.mli | 2 + 3 files changed, 66 insertions(+), 49 deletions(-) diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml index 59248fffa..ddc480132 100644 --- a/src/lib/reasoners/satml.ml +++ b/src/lib/reasoners/satml.ml @@ -1796,37 +1796,36 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct make_decision env atom and pick_branch_lit env = - match env.next_optimized_split with - | Some (fn, value, atom) -> - env.next_optimized_split <- None; - let v = atom.var in - if v.level >= 0 then ( - assert (v.pa.is_true || v.na.is_true); - if atom.is_true then - env.tenv <- Th.add_objective env.tenv fn value; - pick_branch_lit env - ) else ( - make_decision env atom; - if atom.is_true then - env.tenv <- Th.add_objective env.tenv fn value - ) - | None -> - match env.next_decisions with - | atom :: tl -> - env.next_decisions <- tl; + match env.next_decisions with + | atom :: tl -> + env.next_decisions <- tl; + pick_branch_aux env atom + | [] -> + match env.next_split with + | Some atom -> + env.next_split <- None; pick_branch_aux env atom - | [] -> - match env.next_split with - | Some atom -> - env.next_split <- None; - pick_branch_aux env atom - | None -> - match Vheap.pop_min env.order with - | v -> pick_branch_aux env v.na - | exception Not_found -> - if Options.get_cdcl_tableaux_inst () then - assert (Matoms.is_empty env.lazy_cnf); - raise_notrace Sat + | None -> + match Vheap.pop_min env.order with + | v -> pick_branch_aux env v.na + | exception Not_found -> + if Options.get_cdcl_tableaux_inst () then + assert (Matoms.is_empty env.lazy_cnf); + match env.next_optimized_split with + | Some (fn, value, atom) -> + env.next_optimized_split <- None; + let v = atom.var in + if v.level >= 0 then ( + assert (v.pa.is_true || v.na.is_true); + if atom.is_true then + env.tenv <- Th.add_objective env.tenv fn value; + pick_branch_lit env + ) else ( + make_decision env atom; + if atom.is_true then + env.tenv <- Th.add_objective env.tenv fn value + ) + | None -> raise Sat let pick_branch_lit env = if env.next_dec_guard < Vec.size env.increm_guards then @@ -1941,6 +1940,23 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct conflict_analyze_and_fix env (C_theory ex); compute_concrete_model ~declared_ids env + let compute_concrete_model ~declared_ids env = + assert (is_sat env); + + (* Make sure all objectives are optimized before starting model + generation. This can cause us to backtrack some of the splits + done at the theory level, which is fine, because we don't care + about these at the SAT level. *) + let rec loop env = + let acts = theory_slice env in + env.tenv <- Th.do_optimize ~acts env.tenv; + if not (is_sat env) then + try solve env; assert false + with Sat -> loop env + else + compute_concrete_model ~declared_ids env + in loop env + exception Trivial let partition atoms init = diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml index 31973c37d..7d571646b 100644 --- a/src/lib/reasoners/theory.ml +++ b/src/lib/reasoners/theory.ml @@ -57,6 +57,8 @@ module type S = sig 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_optimize : + acts:Shostak.Literal.t Th_util.acts -> t -> t val do_case_split : ?acts:Shostak.Literal.t Th_util.acts -> t -> Util.case_split_policy -> t * Expr.Set.t @@ -670,33 +672,29 @@ module Main_Default : S = struct else [], t - let do_optimize acts objectives t = + let do_optimize ~acts t = + let objectives = t.objectives in match Objective.Model.next_unknown objectives with | Some obj -> let add_objective = acts.Th_util.acts_add_objective in optimize_obj ~for_model:false add_objective obj t; + t + | None -> t + + let do_sat_splits acts t = + let splits, t = sat_splits t in + match splits with + | [] -> do_case_split_aux t ~for_model:false + | (lview, _, _) :: _ -> + let lit = Shostak.(Literal.make @@ LSem (L.make lview)) in + acts.Th_util.acts_add_split lit; t, SE.empty - | None -> - let splits, t = sat_splits t in - match splits with - | [] -> - do_case_split_aux t ~for_model:false - | (lview, _, _) :: _ -> - let lit = Shostak.(Literal.make @@ LSem (L.make lview)) in - acts.Th_util.acts_add_split lit; - t, SE.empty - - let do_case_split_or_optimize ?acts t = - match acts with - | Some acts -> - do_optimize acts t.objectives t - | None -> - do_case_split_aux t ~for_model:false - let do_case_split ?acts t origin = if Options.get_case_split_policy () == origin then - do_case_split_or_optimize ?acts t + match acts with + | Some acts -> do_sat_splits acts t + | None -> do_case_split_aux t ~for_model:false else t, SE.empty @@ -965,6 +963,7 @@ module Main_Empty : S = struct let get_real_env _ = CC_X.empty let get_case_split_env _ = CC_X.empty + let do_optimize ~acts:_ env = env let do_case_split ?acts:_ env _ = env, E.Set.empty let add_term env _ ~add_in_cs:_ = env let compute_concrete_model ~acts:_ _env = () diff --git a/src/lib/reasoners/theory.mli b/src/lib/reasoners/theory.mli index 8a2387e53..b86e1f256 100644 --- a/src/lib/reasoners/theory.mli +++ b/src/lib/reasoners/theory.mli @@ -48,6 +48,8 @@ module type S = sig 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_optimize : + acts:Shostak.Literal.t Th_util.acts -> t -> t val do_case_split : ?acts:Shostak.Literal.t Th_util.acts -> t -> Util.case_split_policy -> t * Expr.Set.t From 4275551b1253c1342312ae811d446a77d73fcee0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Wed, 28 Aug 2024 16:48:00 +0200 Subject: [PATCH 2/3] do_optimize only performs side effects --- src/lib/reasoners/satml.ml | 2 +- src/lib/reasoners/theory.ml | 9 ++++----- src/lib/reasoners/theory.mli | 2 +- 3 files changed, 6 insertions(+), 7 deletions(-) diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml index ddc480132..f97f4107f 100644 --- a/src/lib/reasoners/satml.ml +++ b/src/lib/reasoners/satml.ml @@ -1949,7 +1949,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct about these at the SAT level. *) let rec loop env = let acts = theory_slice env in - env.tenv <- Th.do_optimize ~acts env.tenv; + Th.do_optimize ~acts env.tenv; if not (is_sat env) then try solve env; assert false with Sat -> loop env diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml index 7d571646b..a0de55cde 100644 --- a/src/lib/reasoners/theory.ml +++ b/src/lib/reasoners/theory.ml @@ -58,7 +58,7 @@ module type S = sig val get_real_env : t -> Ccx.Main.t val get_case_split_env : t -> Ccx.Main.t val do_optimize : - acts:Shostak.Literal.t Th_util.acts -> t -> t + acts:Shostak.Literal.t Th_util.acts -> t -> unit val do_case_split : ?acts:Shostak.Literal.t Th_util.acts -> t -> Util.case_split_policy -> t * Expr.Set.t @@ -677,9 +677,8 @@ module Main_Default : S = struct match Objective.Model.next_unknown objectives with | Some obj -> let add_objective = acts.Th_util.acts_add_objective in - optimize_obj ~for_model:false add_objective obj t; - t - | None -> t + optimize_obj ~for_model:false add_objective obj t + | None -> () let do_sat_splits acts t = let splits, t = sat_splits t in @@ -963,7 +962,7 @@ module Main_Empty : S = struct let get_real_env _ = CC_X.empty let get_case_split_env _ = CC_X.empty - let do_optimize ~acts:_ env = env + let do_optimize ~acts:_ _ = () let do_case_split ?acts:_ env _ = env, E.Set.empty let add_term env _ ~add_in_cs:_ = env let compute_concrete_model ~acts:_ _env = () diff --git a/src/lib/reasoners/theory.mli b/src/lib/reasoners/theory.mli index b86e1f256..f8c4e115d 100644 --- a/src/lib/reasoners/theory.mli +++ b/src/lib/reasoners/theory.mli @@ -49,7 +49,7 @@ module type S = sig val get_real_env : t -> Ccx.Main.t val get_case_split_env : t -> Ccx.Main.t val do_optimize : - acts:Shostak.Literal.t Th_util.acts -> t -> t + acts:Shostak.Literal.t Th_util.acts -> t -> unit val do_case_split : ?acts:Shostak.Literal.t Th_util.acts -> t -> Util.case_split_policy -> t * Expr.Set.t From 379dcc191a5b8d91ee86c2ca64450f24f1136f70 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Thu, 29 Aug 2024 12:34:03 +0200 Subject: [PATCH 3/3] Revert pick_branch_lit changes --- src/lib/reasoners/satml.ml | 59 +++++++++++++++++++------------------- 1 file changed, 30 insertions(+), 29 deletions(-) diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml index f97f4107f..cd061c17c 100644 --- a/src/lib/reasoners/satml.ml +++ b/src/lib/reasoners/satml.ml @@ -1796,36 +1796,37 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct make_decision env atom and pick_branch_lit env = - match env.next_decisions with - | atom :: tl -> - env.next_decisions <- tl; - pick_branch_aux env atom - | [] -> - match env.next_split with - | Some atom -> - env.next_split <- None; + match env.next_optimized_split with + | Some (fn, value, atom) -> + env.next_optimized_split <- None; + let v = atom.var in + if v.level >= 0 then ( + assert (v.pa.is_true || v.na.is_true); + if atom.is_true then + env.tenv <- Th.add_objective env.tenv fn value; + pick_branch_lit env + ) else ( + make_decision env atom; + if atom.is_true then + env.tenv <- Th.add_objective env.tenv fn value + ) + | None -> + match env.next_decisions with + | atom :: tl -> + env.next_decisions <- tl; pick_branch_aux env atom - | None -> - match Vheap.pop_min env.order with - | v -> pick_branch_aux env v.na - | exception Not_found -> - if Options.get_cdcl_tableaux_inst () then - assert (Matoms.is_empty env.lazy_cnf); - match env.next_optimized_split with - | Some (fn, value, atom) -> - env.next_optimized_split <- None; - let v = atom.var in - if v.level >= 0 then ( - assert (v.pa.is_true || v.na.is_true); - if atom.is_true then - env.tenv <- Th.add_objective env.tenv fn value; - pick_branch_lit env - ) else ( - make_decision env atom; - if atom.is_true then - env.tenv <- Th.add_objective env.tenv fn value - ) - | None -> raise Sat + | [] -> + match env.next_split with + | Some atom -> + env.next_split <- None; + pick_branch_aux env atom + | None -> + match Vheap.pop_min env.order with + | v -> pick_branch_aux env v.na + | exception Not_found -> + if Options.get_cdcl_tableaux_inst () then + assert (Matoms.is_empty env.lazy_cnf); + raise_notrace Sat let pick_branch_lit env = if env.next_dec_guard < Vec.size env.increm_guards then