Skip to content

Commit

Permalink
Refactoring optimization in satml_frontend
Browse files Browse the repository at this point in the history
  • Loading branch information
@Halbaroth
Halbaroth committed Feb 11, 2025
1 parent cdee651 commit 5fb13ae
Show file tree
Hide file tree
Showing 2 changed files with 162 additions and 160 deletions.
320 changes: 161 additions & 159 deletions src/lib/reasoners/satml_frontend.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,15 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
mutable last_saved_model : Models.t Lazy.t option;
mutable last_saved_objectives : Objective.Model.t option;
mutable last_saved_bmodel : Shostak.Literal.t atom list option;
(** The boolean model saved in this field is intented for use by
[get_value]. This field can be updated in two situations:
- Just before returning [I_dont_know] in the [unsat_rec] function, it
is updated with the current boolean model of [env.satml].
- After encountering a contradiction in [optimize_models], it is
updated with the lastest consistent boolean model produced by
SatML. This model must be consistent with the boolean model of
[env.satml] but it may be a strict extension of it. *)

mutable unknown_reason : Sat_solver_sig.unknown_reason option;
(** The reason why satml raised [I_dont_know] if it does; [None] by
default. *)
Expand All @@ -81,7 +90,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
stack is never empty. *)
}

let bmodel_snapshot env =
(* Helper function that produces an independent copy of the current boolean
model of [env.satml]. *)
let capture_bmodel env =
List.map
(fun Atom.{ lit; neg = { lit = nlit; _ }; _ } ->
let rec a = { lit; neg }
Expand Down Expand Up @@ -1034,11 +1045,89 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
end

let update_model_and_return_unknown env compute_model ~unknown_reason =
env.last_saved_bmodel <- Some (bmodel_snapshot env);
env.last_saved_bmodel <- Some (capture_bmodel env);
may_update_last_saved_model env compute_model;
Options.Time.unset_timeout ();
i_dont_know env unknown_reason

let rec unsat_rec env : unit =
try SAT.solve env.satml; assert false
with
| Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc))
| Util.Timeout -> i_dont_know env (Timeout ProofSearch)
| Util.Step_limit_reached n -> i_dont_know env (Step_limit n)
| Satml.Sat ->
try
do_case_split env Util.BeforeMatching;
may_update_last_saved_model env (Options.get_every_interpretation ());
let () =
env.nb_mrounds <- env.nb_mrounds + 1
[@ocaml.ppwarning
"TODO: first intantiation a la DfsSAT before \
searching ..."]
in
if Options.get_profiling() then Profiling.instantiation env.nb_mrounds;
let strat =
if env.nb_mrounds - env.last_forced_greedy > 1000 then Force_greedy
else
if env.nb_mrounds - env.last_forced_normal > 50 then Force_normal
else Auto
in
(*let strat = Auto in*)
let dec_lvl = SAT.decision_level env.satml in
let updated = instantiation env strat dec_lvl in
do_case_split env Util.AfterMatching;
let updated =
if not updated && strat != Auto then instantiation env Auto dec_lvl
else updated
in
let dec_lvl' = SAT.decision_level env.satml in
let () =
if strat == Auto && dec_lvl' = dec_lvl then
(* increase chances of forcing Normal each time Auto
instantiation doesn't allow to backjump *)
env.last_forced_normal <- env.last_forced_normal - 1
in
if not updated then
update_model_and_return_unknown
env (Options.get_last_interpretation ())
~unknown_reason:Incomplete; (* may becomes ModelGen *)
unsat_rec env

with
| Util.Timeout -> i_dont_know env (Timeout ProofSearch)
| Util.Step_limit_reached n -> i_dont_know env (Step_limit n)
| Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc))
| Ex.Inconsistent (expl, _cls) -> (*may be raised during matching or CS*)
begin
try
SAT.conflict_analyze_and_fix env.satml (Satml.C_theory expl);
unsat_rec env
with
| Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc))
| Util.Timeout -> i_dont_know env (Timeout ProofSearch)
| Util.Step_limit_reached n -> i_dont_know env (Step_limit n)
end

(* copied from sat_solvers.ml *)
let max_term_depth_in_sat env =
let aux mx f = Stdlib.max mx (E.depth f) in
ME.fold (fun f _ mx -> aux mx f) env.gamma 0

let checks_implemented_features () =
let fails msg =
let msg =
Format.sprintf
"%S is not implemented in CDCL solver ! \
Please use the old Tableaux-like SAT solver instead."
msg
in
Errors.run_error (Errors.Unsupported_feature msg)
in
let open Options in
if get_save_used_context () then fails "save_used_context";
if get_unsat_core () then fails "unsat_core"

let create_guard env =
let expr_guard = E.fresh_name Ty.Tbool in
let ff, axs, new_vars =
Expand All @@ -1057,9 +1146,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
expr_guard, atom_guard
| _ -> assert false

let add_guard env gf =
let current_guard = env.guards.current_guard in
{gf with E.ff = E.mk_imp current_guard gf.E.ff}
let declare env id =
env.declare_top <- id :: env.declare_top

let push env to_push =
Util.loop ~f:(fun _n () () ->
Expand Down Expand Up @@ -1106,6 +1194,10 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
~elt:()
~init:()

let add_guard env gf =
let current_guard = env.guards.current_guard in
{gf with E.ff = E.mk_imp current_guard gf.E.ff}

exception Give_up of (E.t * E.t * bool * bool) list

(* Getting [unknown] after a query can mean two things:
Expand Down Expand Up @@ -1181,75 +1273,20 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
else mk_gt ty_op
end

let rec unsat_rec env : unit =
try SAT.solve env.satml; assert false
with
| Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc))
| Util.Timeout -> i_dont_know env (Timeout ProofSearch)
| Util.Step_limit_reached n -> i_dont_know env (Step_limit n)
| Satml.Sat ->
try
do_case_split env Util.BeforeMatching;
may_update_last_saved_model env (Options.get_every_interpretation ());
let () =
env.nb_mrounds <- env.nb_mrounds + 1
[@ocaml.ppwarning
"TODO: first intantiation a la DfsSAT before \
searching ..."]
in
if Options.get_profiling() then Profiling.instantiation env.nb_mrounds;
let strat =
if env.nb_mrounds - env.last_forced_greedy > 1000 then Force_greedy
else
if env.nb_mrounds - env.last_forced_normal > 50 then Force_normal
else Auto
in
(*let strat = Auto in*)
let dec_lvl = SAT.decision_level env.satml in
let updated = instantiation env strat dec_lvl in
do_case_split env Util.AfterMatching;
let updated =
if not updated && strat != Auto then instantiation env Auto dec_lvl
else updated
in
let dec_lvl' = SAT.decision_level env.satml in
let () =
if strat == Auto && dec_lvl' = dec_lvl then
(* increase chances of forcing Normal each time Auto
instantiation doesn't allow to backjump *)
env.last_forced_normal <- env.last_forced_normal - 1
in
if not updated then
update_model_and_return_unknown
env (Options.get_last_interpretation ())
~unknown_reason:Incomplete; (* may becomes ModelGen *)
unsat_rec env

with
| Util.Timeout -> i_dont_know env (Timeout ProofSearch)
| Util.Step_limit_reached n -> i_dont_know env (Step_limit n)
| Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc))
| Ex.Inconsistent (expl, _cls) -> (*may be raised during matching or CS*)
begin
try
SAT.conflict_analyze_and_fix env.satml (Satml.C_theory expl);
unsat_rec env
with
| Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc))
| Util.Timeout -> i_dont_know env (Timeout ProofSearch)
| Util.Step_limit_reached n -> i_dont_know env (Step_limit n)
end

exception Best of t * Models.t option * Objective.Model.t option * Shostak.Literal.t atom list

(* This function is called after catching [I_dont_know] exception threw into
[unsat_rec]. It may re-raise this exception. *)
let rec analyze_unknown_for_objectives env : unit =
let objs =
match env.last_saved_objectives with
| Some objs -> objs
| None -> raise I_dont_know
in
let rec optimize_models env =
(* Models must be saved before asserting a new formula in [env] as
they may be altered if a contradiction arises below. More precisely,
- [env.last_saved_model] needs to be forced, as the closure that
computes it depends on the current theory environment in [env.satml],
which may changed after popping an assertion level.
- [env.last_saved_objectives] is pure and only needs to be saved
without additional precautions.
- The atoms of [env.last_saved_bmodel] are mutable and part of the SAT
solver state [env.satml], which means they may be altered after
popping an assertion level. *)
let fmdl = Option.map Lazy.force env.last_saved_model in
let omdl = Option.get env.last_saved_objectives in
let bmdl = capture_bmodel env in
let acc =
try
Objective.Model.fold (fun { e; is_max; _ } value acc ->
Expand All @@ -1262,15 +1299,15 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
raise (Give_up ((e, v, is_max, false) :: acc))
| Unknown ->
assert false
) objs []
) omdl []
with Give_up acc -> acc
in
begin match acc with
| [] ->
(* The answer for the first objective is infinity. We stop here as
we cannot go beyond infinity and the next objectives with lower
priority cannot be optimized in presence of infinity values. *)
raise I_dont_know;
we cannot go beyond infinity and lower-priority objectives
cannot be optimized in the presence of infinity values. *)
env, fmdl, omdl, bmdl
| (e, tv, is_max, is_le) :: l ->
let neg =
List.fold_left
Expand All @@ -1280,91 +1317,56 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
E.Core.(or_ acc (not ((op (E.type_info e) is_max is_le) e tv)))
) (E.Core.not ((op (E.type_info e) is_max is_le) e tv)) l
in
if Options.get_debug_optimize () then
Printer.print_dbg
"The objective function %a has an optimum. We should continue \
to explore other branches to try to find a better optimum than \
%a." Expr.print e Expr.print tv;
let l = [mk_gf neg] in
(* TODO: Can we add the clause without 'cancel_until 0' ? *)
SAT.cancel_until env.satml 0;
if Options.get_debug_optimize () then
Printer.print_dbg
"We assert the formula %a to explore another branch."
E.print neg;
(* One must saved models before popping the assertion level
introducing before [analyze_unknown_for_objectives].
- [lazy_mdl] does not need to be forced as ModelMap are pure
structures.
- Objective models are also pure, so we do not need to perform
a deep copy.
- Boolean models are mutable and a part of the SAT solver state,
which means they may be alterate after popping. *)
let mdl = Option.map Lazy.force env.last_saved_model in
let omdl = env.last_saved_objectives in
let bmdl = bmodel_snapshot env in
let updated =
try assume_aux ~dec_lvl:0 env l
with IUnsat (env, _) ->
(* We can throw the explanation of [IUnsat] as we revert
this assume in [unsat_rec_prem]. *)
raise (Best (env, mdl, omdl, bmdl))
in
if not updated then begin
Printer.print_dbg
"env not updated after injection of neg! termination \
issue.@.@.";
Logs.debug ~src:Options.Sources.optimize
(fun k -> k
"The objective function %a has an optimum. We should continue \
to explore other branches to try to find a better optimum than \
%a." Expr.print e Expr.print tv);
Logs.debug ~src:Options.Sources.optimize
(fun k -> k
"We assert the formula %a to explore another branch."
E.print neg);
try
(* TODO: Can we add the clause without 'cancel_until 0' ? *)
SAT.cancel_until env.satml 0;
let updated = assume_aux ~dec_lvl:0 env [mk_gf neg] in
if not updated then
Fmt.failwith
"env not updated after injection of neg! termination issue";
unsat_rec env;
assert false
end;
Options.Time.unset_timeout ();
Options.Time.set_timeout (Options.get_timelimit ());
unsat_rec_prem env
with
| I_dont_know -> optimize_models env
| IUnsat (env, _ex) ->
(* The explanation [_ex] associated with [env] in [IUnsat] can be
discared, as we revert the assertion of formulas that led to this
contradiction in [unsat_then_optimize]. *)
env, fmdl, omdl, bmdl
end

and unsat_rec_prem env : unit =
try unsat_rec env
let unsat_then_optimize env =
try
unsat_rec env
with
| I_dont_know ->
begin
try
push env 1;
analyze_unknown_for_objectives env;
assert false
with
| Best (env, mdl, omdl, bmdl) ->
pop env 1;
env.last_saved_model <- Option.map Lazy.from_val mdl;
env.last_saved_objectives <- omdl;
env.last_saved_bmodel <- Some bmdl;
raise I_dont_know
end
| IUnsat (env, _) as e ->
if Option.is_none env.last_saved_objectives then raise e;
(* TODO: put the correct objectives *)
raise I_dont_know

(* copied from sat_solvers.ml *)
let max_term_depth_in_sat env =
let aux mx f = Stdlib.max mx (E.depth f) in
ME.fold (fun f _ mx -> aux mx f) env.gamma 0


let checks_implemented_features () =
let fails msg =
let msg =
Format.sprintf
"%S is not implemented in CDCL solver ! \
Please use the old Tableaux-like SAT solver instead."
msg
in
Errors.run_error (Errors.Unsupported_feature msg)
in
let open Options in
if get_save_used_context () then fails "save_used_context";
if get_unsat_core () then fails "unsat_core"

let declare env id =
env.declare_top <- id :: env.declare_top
(* It is more reliable to verify the presence of objectives at
the current assertion level by referring to the objective model
stored in the current theory environment, rather than checking
the emptiness of [env.last_saved_objectives]. *)
let curr_objs = Th.get_objectives @@ SAT.current_tbox env.satml in
if Objective.Model.is_empty curr_objs then
raise I_dont_know
else (
(* An additional assertion level is inserted around [optimize_models]
to revert to a consistent SAT environment after reaching an
unsatisfiable state in [optimize_models]. *)
push env 1;
let env, fmdl, omdl, bmdl = optimize_models env in
pop env 1;
env.last_saved_model <- Option.map Lazy.from_val fmdl;
env.last_saved_objectives <- Some omdl;
env.last_saved_bmodel <- Some bmdl;
raise I_dont_know)

let unsat env gf =
checks_implemented_features ();
Expand All @@ -1380,7 +1382,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
let _updated = assume_aux ~dec_lvl:0 env [gf] in
let max_t = max_term_depth_in_sat env in
env.inst <- Inst.register_max_term_depth env.inst max_t;
unsat_rec_prem env;
unsat_then_optimize env;
assert false
with
| IUnsat (_env, dep) ->
Expand Down
Loading

0 comments on commit 5fb13ae

Please sign in to comment.