From c3a6f2234fe374fca660aa0c3f4e4818b21cd179 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Mon, 13 May 2024 10:53:39 +0200 Subject: [PATCH] fix(CDCL): Semantic splits are always relevant Restore semantic splitting functionality introduced in #1027 and broken by #1041. --- src/lib/reasoners/satml.ml | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml index a364d2807..7107dc3af 100644 --- a/src/lib/reasoners/satml.ml +++ b/src/lib/reasoners/satml.ml @@ -681,6 +681,15 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct with Not_found -> () done + (* Variables are relevant if they are in the [lazy_cnf]. Semantic variables + are always relevant: otherwise, since they are local to the current branch + and not added to the [var_order], they would never get decided. + + Only used when [Options.get_cdcl_tableaux_inst ()] is enabled. *) + let is_relevant env (v : Atom.var) = + is_semantic v.pa || + Matoms.mem v.pa env.lazy_cnf || Matoms.mem v.na env.lazy_cnf + (* annule tout jusqu'a lvl *exclu* *) let cancel_until env lvl = if Options.get_debug_sat () then @@ -737,9 +746,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct heap. *) if Options.get_cdcl_tableaux_inst () then VH.filter_map_inplace (fun v () -> - if - Matoms.mem v.pa env.lazy_cnf || Matoms.mem v.na env.lazy_cnf - then ( + if is_relevant env v then ( insert_var_order env v; None ) else Some () @@ -1788,7 +1795,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct Note that we can only do this if [get_cdcl_tableaux_inst ()] is [true], because otherwise instantiation requires a complete boolean model. *) - if Matoms.mem v.pa env.lazy_cnf || Matoms.mem v.na env.lazy_cnf then + if is_relevant env v then make_decision env atom else ( VH.add env.irrelevants v ();