wip - test i understand try_to_bj_further

src/lib/reasoners/satml.ml

@@ -106,7 +106,6 @@ module type SAT_ML = sig
   val assume :
     t ->
     Atom.atom list list -> E.t ->
-    cnumber : int ->
     FF.Set.t -> dec_lvl:int ->
     unit
 
@@ -123,7 +122,8 @@ module type SAT_ML = sig
 
   val exists_in_lazy_cnf : t -> FF.t -> bool
 
-  val known_lazy_formulas : t -> int FF.Map.t
+  val fold_known_lazy_formulas :
+    (FF.t -> 'a -> 'a) -> t -> 'a -> 'a
 
   val reason_of_deduction: Atom.atom -> Atom.Set.t
 
@@ -167,6 +167,32 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
 
   type th = Th.t
 
+  type ffl =
+    { mutable ff_lvl : int MFF.t
+    (** Map from flat formulas to the (earliest) decision level at which they
+        were asserted. Only used with the CDCL-Tableaux solver. *)
+
+    ; mutable lvl_ff : SFF.t Util.MI.t
+    (** Map from decision level to the set of flat formulas asserted at that
+        level. Set inverse of [ff_lvl]. Only used with the CDCL-Tableaux
+        solver. *)
+    }
+
+  let create_ffl () =
+    { ff_lvl = MFF.empty
+    ; lvl_ff = Util.MI.empty }
+
+  let ffl_cancel ffl lvl =
+    match Util.MI.find lvl ffl.lvl_ff with
+    | s ->
+      ffl.ff_lvl <- SFF.fold MFF.remove s ffl.ff_lvl;
+      ffl.lvl_ff <- Util.MI.remove lvl ffl.lvl_ff
+    | exception Not_found -> ()
+
+  let ffs_at_level lvl ffl =
+    try Util.MI.find lvl ffl.lvl_ff
+    with Not_found -> SFF.empty
+
   module VH = Hashtbl.Make(struct
       type t = Atom.var
 
@@ -391,14 +417,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
       (** Checkpoint of the [relevant] field at each decision level. Only used
           with the CDCL-Tableaux solver. *)
 
-      mutable ff_lvl : int MFF.t;
-      (** Map from flat formulas to the (earliest) decision level at which they
-          were asserted. Only used with the CDCL-Tableaux solver. *)
-
-      mutable lvl_ff : SFF.t Util.MI.t;
-      (** Map from decision level to the set of flat formulas asserted at that
-          level. Set inverse of [ff_lvl]. Only used with the CDCL-Tableaux
-          solver. *)
+      ffl : ffl;
 
       increm_guards : Atom.atom Vec.t;
 
@@ -533,9 +552,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
       relevants = SFF.empty;
       relevants_queue = Vec.make 100 ~dummy:(SFF.singleton (FF.faux));
 
-      ff_lvl = MFF.empty;
-
-      lvl_ff = Util.MI.empty;
+      ffl = create_ffl ();
 
       increm_guards = Vec.make 1 ~dummy:Atom.dummy_atom;
 
@@ -663,11 +680,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
 
   let cancel_ff_lvls_until env lvl =
     for i = decision_level env downto lvl + 1 do
-      try
-        let s = Util.MI.find i env.lvl_ff in
-        SFF.iter (fun f' -> env.ff_lvl <- MFF.remove f' env.ff_lvl) s;
-        env.lvl_ff <- Util.MI.remove i env.lvl_ff;
-      with Not_found -> ()
+      ffl_cancel env.ffl i
     done
 
   (* Variables are relevant if they are in the [lazy_cnf]. Semantic variables
@@ -1965,13 +1978,12 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
     partition_aux [] [] [] init atoms
 
 
-  let add_clause env f ~cnumber atoms =
+  let add_clause env f atoms =
     if env.is_unsat then raise (Unsat env.unsat_core);
     (*if not (clause_exists atoms) then XXX TODO *)
-    let init_name = string_of_int cnumber in
     let init0 =
       if Options.get_unsat_core () then
-        [Atom.make_clause init_name atoms f false []]
+        [Atom.make_clause "0" atoms f false []]
       else
         [] (* no deps if unsat cores generation is not enabled *)
     in
@@ -2041,25 +2053,19 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
       if Options.get_profiling() then Profiling.elim true
 
 
-  let update_lazy_cnf env ~do_bcp sff ~dec_lvl =
+  let update_lazy_cnf env sff ~dec_lvl =
     if Options.get_cdcl_tableaux () && dec_lvl <= decision_level env then begin
-      let s =
-        try Util.MI.find dec_lvl env.lvl_ff
-        with Not_found -> SFF.empty
-      in
+      let s = ffs_at_level dec_lvl env.ffl in
       let lz, s =
         SFF.fold (fun ff (l, s) ->
-            assert (not (MFF.mem ff env.ff_lvl));
+            assert (not (MFF.mem ff env.ffl.ff_lvl));
             assert (not (SFF.mem ff s));
-            env.ff_lvl <- MFF.add ff dec_lvl env.ff_lvl;
+            env.ffl.ff_lvl <- MFF.add ff dec_lvl env.ffl.ff_lvl;
             add_form_to_lazy_cnf env l ff, SFF.add ff s
           ) sff (env.lazy_cnf, s)
       in
       env.lazy_cnf <- lz;
-      env.lvl_ff <- Util.MI.add dec_lvl s env.lvl_ff;
-      if do_bcp then
-        propagate_and_stabilize (*theory_propagate_opt*)
-          env all_propagations (ref 0) Auto;
+      env.ffl.lvl_ff <- Util.MI.add dec_lvl s env.ffl.lvl_ff;
     end
 
   let new_vars env ~nbv new_v cnf =
@@ -2125,7 +2131,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
       if Options.get_cdcl_tableaux () then
         better_bj env sff
 
-  let assume env cnf f ~cnumber sff ~dec_lvl =
+  let assume env cnf f sff ~dec_lvl =
     begin
       match cnf with
       | [] -> ()
@@ -2136,25 +2142,26 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
         Vec.grow_to_by_double env.learnts nbc;
         env.nb_init_clauses <- nbc;
 
-        List.iter (add_clause env f ~cnumber) cnf;
+        List.iter (add_clause env f) cnf;
 
         if Options.get_verbose () then
           Printer.print_dbg
             "%d clauses@ %d learnts"
             (Vec.size env.clauses)
             (Vec.size env.learnts);
     end;
-    (* do it after add clause and before T-propagate, disable bcp*)
-    update_lazy_cnf env ~do_bcp:false sff ~dec_lvl;
+    (* do it after add clause and before T-propagate *)
+    update_lazy_cnf env sff ~dec_lvl;
     (* do bcp globally *)
+    let prev_dec_lvl = decision_level env in
     propagate_and_stabilize env all_propagations (ref 0) Auto;
-    if dec_lvl > decision_level env then
+    if prev_dec_lvl > decision_level env then
       (*dec_lvl <> 0 and a bj have been made*)
       try_to_backjump_further env sff
 
   let exists_in_lazy_cnf env f' =
     not (Options.get_cdcl_tableaux ()) ||
-    MFF.mem f' env.ff_lvl
+    MFF.mem f' env.ffl.ff_lvl
 
   let boolean_model env = Vec.to_list env.trail
 
@@ -2197,7 +2204,8 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
     copy sv
 *)
 
-  let known_lazy_formulas env = env.ff_lvl
+  let fold_known_lazy_formulas f env acc =
+    FF.Map.fold (fun ff _ acc -> f ff acc) env.ffl.ff_lvl acc
 
   (* HYBRID SAT functions *)
   let assume_simple env cnf =
@@ -2209,7 +2217,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
       Vec.grow_to_by_double env.learnts nbc;
       env.nb_init_clauses <- nbc;
 
-      List.iter (add_clause env vraie_form ~cnumber:0) cnf;
+      List.iter (add_clause env vraie_form) cnf;
 
       if Options.get_verbose () then
         Printer.print_dbg

src/lib/reasoners/satml.mli

@@ -61,7 +61,6 @@ module type SAT_ML = sig
     t ->
     Satml_types.Atom.atom list list ->
     Expr.t ->
-    cnumber : int ->
     Flat_Formula.Set.t -> dec_lvl:int ->
     unit
 
@@ -78,7 +77,8 @@ module type SAT_ML = sig
   val cancel_until : t -> int -> unit
 
   val exists_in_lazy_cnf : t -> Flat_Formula.t -> bool
-  val known_lazy_formulas : t -> int Flat_Formula.Map.t
+  val fold_known_lazy_formulas :
+    (Flat_Formula.t -> 'a -> 'a) -> t -> 'a -> 'a
 
   val reason_of_deduction: Atom.atom -> Atom.Set.t
   val assume_simple : t -> Atom.atom list list -> unit

src/lib/reasoners/satml_frontend.ml

@@ -666,7 +666,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       SA.fold add_elit sa SE.empty
 
   let atoms_from_lazy_greedy env =
-    let aux accu ff =
+    let aux ff accu =
       let sf =
         try FF.Map.find ff env.conj |> snd
         with Not_found ->
@@ -679,14 +679,10 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       in
       SE.fold (E.atoms_rec_of_form ~only_ground:false) sf accu
     in
-    let accu =
-      FF.Map.fold
-        (fun ff _ accu -> aux accu ff)
-        (SAT.known_lazy_formulas env.satml) SE.empty
-    in
+    let accu = SAT.fold_known_lazy_formulas aux env.satml SE.empty in
     SE.union (atoms_from_lazy_sat ~frugal:true env)
       (*otherwise, we loose atoms that abstract internal axioms *)
-      (aux accu FF.vrai)
+      (aux FF.vrai accu)
     [@ocaml.ppwarning
       "improve terms / atoms extraction in lazy/non-lazy \
        and greedy/non-greedy mode. Separate atoms from terms !"]
@@ -853,8 +849,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
         in
         let nbv = FF.nb_made_vars env.ff_hcons_env in
         let cnf = SAT.new_vars env.satml ~nbv new_vars cnf in
-        (*update_lazy_cnf done inside assume at the right place *)
-        SAT.assume env.satml cnf f ~cnumber:0 activate ~dec_lvl;
+        (* update_lazy_cnf done inside assume at the right place *)
+        SAT.assume env.satml cnf f activate ~dec_lvl
       with
       | Satml.Unsat (lc) -> raise (IUnsat (env, make_explanation lc))
       | Satml.Sat -> assert false