fix problems with slices in the SAT core

src/main/main.ml

@@ -121,9 +121,10 @@ let main () =
   Util.setup_gc();
   let solver =
     let theories = match syn with
-      | Dimacs -> []
+      | Dimacs ->
+        [Dagon_th_bool.th]
       | Smtlib ->
-        [] (* TODO: more theories *)
+        [Dagon_th_bool.th] (* TODO: more theories *)
     in
     Dagon_smt.Solver.create ~theories ()
   in

src/sat/Internal.ml

@@ -905,9 +905,9 @@ module Make
       )
     done
 
-  let slice_iter st (f:_ -> unit) : unit =
+  let slice_iter st (hd:int) (f:_ -> unit) : unit =
     let n = Vec.size st.trail in
-    for i = st.th_head to n-1 do
+    for i = hd to n-1 do
       let a = Vec.get st.trail i in
       f a.lit
     done
@@ -941,13 +941,13 @@ module Make
         (Util.pp_list Atom.debug) l
     )
 
-  let current_slice st = Theory_intf.Slice_acts {
+  let current_slice st head = Theory_intf.Slice_acts {
-    slice_iter = slice_iter st;
+    slice_iter = slice_iter st head;
   }
 
   (* full slice, for [if_sat] final check *)
   let full_slice st = Theory_intf.Slice_acts {
-    slice_iter = slice_iter st;
+    slice_iter = slice_iter st 0;
   }
 
   let act_at_level_0 st () = at_level_0 st
@@ -987,7 +987,7 @@ module Make
     if st.th_head = st.elt_head then (
       None (* fixpoint/no propagation *)
     ) else (
-      let slice = current_slice st in
+      let slice = current_slice st st.th_head in
       st.th_head <- st.elt_head; (* catch up *)
       match Th.assume (theory st) slice with
       | Theory_intf.Sat ->

src/smt/Bag.mli

@@ -6,7 +6,10 @@
     A data structure where we can have duplicate elements, optimized for
     fast concatenation and size. *)
 
-type +'a t
+type +'a t = private
+  | E
+  | L of 'a
+  | N of 'a t * 'a t * int (* size *)
 
 val empty : 'a t
 

src/smt/Congruence_closure.ml

@@ -545,7 +545,7 @@ let explain_loop (cc : t) : Lit.Set.t =
   done;
   cc.ps_lits
 
-let explain_unfold cc (seq:explanation Sequence.t): Lit.Set.t =
+let explain_unfold_seq cc (seq:explanation Sequence.t): Lit.Set.t =
   Log.debugf 5
     (fun k->k "(@[explain_confict@ (@[<hv>%a@])@])"
         (Util.pp_seq Explanation.pp) seq);
@@ -553,6 +553,18 @@ let explain_unfold cc (seq:explanation Sequence.t): Lit.Set.t =
   Sequence.iter (decompose_explain cc) seq;
   explain_loop cc
 
+let explain_unfold_bag cc (b:explanation Bag.t) : Lit.Set.t =
+  Log.debugf 5
+    (fun k->k "(@[explain_confict@ (@[<hv>%a@])@])"
+        (Util.pp_seq Explanation.pp) (Bag.to_seq b));
+  match b with
+  | Bag.E -> Lit.Set.empty
+  | Bag.L (E_lit lit) -> Lit.Set.singleton lit
+  | _ ->
+    ps_clear cc;
+    Sequence.iter (decompose_explain cc) (Bag.to_seq b);
+    explain_loop cc
+
 (* check satisfiability, update congruence closure *)
 let check (cc:t) : unit =
   Log.debug 5 "(cc.check)";

src/smt/Congruence_closure.mli

@@ -71,6 +71,8 @@ val check : t -> unit
 
 val final_check : t -> unit
 
-val explain_unfold: t -> explanation Sequence.t -> Lit.Set.t
+val explain_unfold_bag : t -> explanation Bag.t -> Lit.Set.t
+
+val explain_unfold_seq : t -> explanation Sequence.t -> Lit.Set.t
 (** Unfold those explanations into a complete set of
     literals implying them *)

src/smt/Theory_combine.ml

@@ -64,8 +64,7 @@ let cdcl_return_res (self:t) : _ Sat_solver.res =
       Sat_solver.Sat
     | Some c ->
       let lit_set =
-        Bag.to_seq c
+        Congruence_closure.explain_unfold_bag (cc self) c
-        |> Congruence_closure.explain_unfold (cc self)
       in
       let conflict_clause =
         Lit.Set.to_list lit_set
@@ -74,27 +73,35 @@ let cdcl_return_res (self:t) : _ Sat_solver.res =
       Sat_solver.Log.debugf 3
         (fun k->k "(@[<1>conflict@ clause: %a@])"
             Theory.Clause.pp conflict_clause);
+      self.conflict <- None;
       Sat_solver.Unsat (IArray.to_list conflict_clause, Proof.default)
   end
 
 let[@inline] check (self:t) : unit =
   Congruence_closure.check (cc self)
 
-(* propagation from the bool solver *)
+let with_conflict_catch self f =
-let assume_real (self:t) (slice:_ Sat_solver.slice_actions) =
-  (* TODO if Config.progress then print_progress(); *)
-  let Sat_solver.Slice_acts slice = slice in
   begin
     try
-      slice.slice_iter (assume_lit self);
+      f ()
-      (* now check satisfiability *)
-      check self;
     with Exn_conflict c ->
       assert (CCOpt.is_none self.conflict);
       self.conflict <- Some c;
   end;
   cdcl_return_res self
 
+(* propagation from the bool solver *)
+let assume_real (self:t) (slice:_ Sat_solver.slice_actions) =
+  (* TODO if Config.progress then print_progress(); *)
+  let Sat_solver.Slice_acts slice = slice in
+  Log.debugf 5 (fun k->k "(th_combine.assume :len %d)" (Sequence.length slice.slice_iter));
+  with_conflict_catch self
+    (fun () ->
+       slice.slice_iter (assume_lit self);
+       (* now check satisfiability *)
+       check self
+    )
+
 (* propagation from the bool solver *)
 let assume (self:t) (slice:_ Sat_solver.slice_actions) =
   match self.conflict with
@@ -112,9 +119,10 @@ let if_sat (self:t) (slice:_) : _ Sat_solver.res =
     r.slice_iter
   in
   (* final check for each theory *)
+  with_conflict_catch self
+    (fun () ->
        theories self
-    (fun (Theory.State th) -> th.final_check th.st forms);
+         (fun (Theory.State th) -> th.final_check th.st forms))
-  cdcl_return_res self
 
 (** {2 Various helpers} *)
 
@@ -122,8 +130,7 @@ let if_sat (self:t) (slice:_) : _ Sat_solver.res =
 let act_propagate (self:t) f guard : unit =
   let Sat_solver.Actions r = self.cdcl_acts in
   let guard =
-    Bag.to_seq guard
+    Congruence_closure.explain_unfold_bag (cc self) guard
-    |> Congruence_closure.explain_unfold (cc self)
     |> Lit.Set.to_list
   in
   Sat_solver.Log.debugf 2
@@ -142,8 +149,7 @@ let on_merge_from_cc (self:t) r1 r2 e : unit =
 
 let mk_cc_actions (self:t) : Congruence_closure.actions =
   let Sat_solver.Actions r = self.cdcl_acts in
-  {
+  { Congruence_closure.
-    Congruence_closure.
     on_backtrack = r.on_backtrack;
     at_lvl_0 = r.at_level_0;
     on_merge = on_merge_from_cc self;