From 252345a939ddac50e04c7b6ec0e32b1020ff0020 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 17 Feb 2025 11:30:10 +0100 Subject: [PATCH] Add assertion levels in SatML `Satml_frontend` assumes that `assume` and `check_sat` are always called on a SatML environment with no prior decisions. It works in the current codebase because, in the presence of pop/push, we always restart from a fresh environment. The assertion: ```ocaml assert (SAT.decision_level env.satml == 0) ``` is replaced with: ```ocaml assert (SAT.decision_level env.satml <= SAT.assertion_level env.satml) ``` Notice that we cannot enforce the assertion: ```ocaml assert (SAT.decision_level env.satml = SAT.assertion_level env.satml) ``` Consider for instance: ```ocaml let env = SAT.env () in SAT.push env 1; SAT.assume env f; (* <--- HERE *) ... ``` Internally, `SAT.assume env f` adds the formula `g => f` into the environment of SatML where `g` is a guard formula introduced in `SAT.push`. But `SatML.assume` does not decide the guard formula [g], so the decision level is 0 but the assertion level is 1. Guards are decided (with the highest priority) in `SatML.solve`, which is called by `SAT.unsat`. I didn't add the new assertion into `SAT.assume_th_elt` because this function is only used for handling the theory concept in native language and we always invoke it at the assertion level 0. --- src/lib/reasoners/satml.ml | 2 ++ src/lib/reasoners/satml.mli | 9 +++++++++ src/lib/reasoners/satml_frontend.ml | 4 ++-- 3 files changed, 13 insertions(+), 2 deletions(-) diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml index cd061c17c9..f4ad833324 100644 --- a/src/lib/reasoners/satml.ml +++ b/src/lib/reasoners/satml.ml @@ -121,6 +121,7 @@ module type SAT_ML = sig val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> unit val decision_level : t -> int + val assertion_level : t -> int val cancel_until : t -> int -> unit val exists_in_lazy_cnf : t -> FF.t -> bool @@ -583,6 +584,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct end let decision_level env = Vec.size env.trail_lim + let[@inline always] assertion_level env = Vec.size env.increm_guards let nb_choices env = env.nchoices let nb_assigns env = Vec.size env.trail - nb_choices env diff --git a/src/lib/reasoners/satml.mli b/src/lib/reasoners/satml.mli index 166b2ff5a7..e3b91a919e 100644 --- a/src/lib/reasoners/satml.mli +++ b/src/lib/reasoners/satml.mli @@ -77,6 +77,11 @@ module type SAT_ML = sig val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> unit val decision_level : t -> int + + val assertion_level : t -> int + (** Returns the number of active assertion levels, that is the number of + levels introduced with [push] that have not yet been popped. *) + val cancel_until : t -> int -> unit val exists_in_lazy_cnf : t -> Flat_Formula.t -> bool @@ -90,7 +95,11 @@ module type SAT_ML = sig val conflict_analyze_and_fix : t -> conflict_origin -> unit val push : t -> Satml_types.Atom.atom -> unit + (** [push env g] adds a new assertion level. The formula [g] is used in + [Satml_frontend] to guard all formulas asserted at this level. *) + val pop : t -> unit + (** [pop env] pops the latest assertion level. *) val optimize : t -> Objective.Function.t -> unit (** [optimize env fn] adds the objection [fn] to the environment diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index c0b448983c..4691c7ce73 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -1328,6 +1328,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct {gf with E.ff = E.mk_imp current_guard gf.E.ff} let unsat env gf = + assert (SAT.decision_level env.satml <= SAT.assertion_level env.satml); checks_implemented_features (); let gf = add_guard env gf in Debug.unsat gf; @@ -1337,7 +1338,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct Inst.add_terms env.inst (E.max_ground_terms_rec_of_form gf.E.ff) gf; try - assert (SAT.decision_level env.satml == 0); 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; @@ -1357,7 +1357,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let assume env gf _dep = (* dep currently not used. No unsat-cores in satML yet *) - assert (SAT.decision_level env.satml == 0); + assert (SAT.decision_level env.satml <= SAT.assertion_level env.satml); try ignore (assume_aux ~dec_lvl:0 env [add_guard env gf]) with | IUnsat (_env, dep) -> raise (Unsat dep) | Util.Timeout ->