fix(cc): fix bugs in congruence closure and explanations

also, simplify API for backtracking

src/sat/Dagon_sat.ml

@@ -43,7 +43,6 @@ type ('form, 'proof) actions = ('form,'proof) Theory_intf.actions = Actions of {
   push_persistent : 'form IArray.t -> 'proof -> unit;
   push_local : 'form IArray.t -> 'proof -> unit;
   on_backtrack: (unit -> unit) -> unit;
-  at_level_0 : unit -> bool;
   propagate : 'form -> 'form list -> 'proof -> unit;
 }
 

src/sat/Internal.ml

@@ -146,14 +146,10 @@ module Make
   }
 
   let[@inline] theory st = Lazy.force st.th
-  let[@inline] on_backtrack st f : unit = Vec.push st.backtrack f
   let[@inline] at_level_0 st : bool = Vec.is_empty st.backtrack_levels
-
+  let[@inline] on_backtrack st f : unit =
-  (* schedule [f] as a backtrack action, iff the solver's current
-     level is not 0. *)
-  let[@inline] on_backtrack_if_not_at_0 st f =
     if not (at_level_0 st) then (
-      on_backtrack st f;
+      Vec.push st.backtrack f
     )
 
   let[@inline] st t = t.st
@@ -196,7 +192,7 @@ module Make
     if not (Var.in_heap v) && Var.level v < 0 then (
       (* new variable that is not assigned, add to heap.
          remember to remove variable when we backtrack *)
-      on_backtrack_if_not_at_0 st (fun () -> H.remove st.order v);
+      on_backtrack st (fun () -> H.remove st.order v);
       H.insert st.order v;
     )
 
@@ -350,11 +346,10 @@ module Make
   let attach_clause (self:t) (c:clause) : unit =
     if not (Clause.attached c) then (
       Log.debugf 5 (fun k -> k "(@[sat.attach_clause@ %a@])" Clause.debug c);
-      if not (at_level_0 self) then (
       on_backtrack self
         (fun () ->
-             Clause.set_attached c false)
+           Log.debugf 5 (fun k->k "(@[sat.detach_clause@ %a@])" Clause.debug c);
-      );
+           Clause.set_attached c false);
       Vec.push c.atoms.(0).neg.watched c;
       Vec.push c.atoms.(1).neg.watched c;
       Clause.set_attached c true;
@@ -380,7 +375,8 @@ module Make
      i.e we want to go back to the state the solver was in
          when decision level [lvl] was created. *)
   let cancel_until st lvl =
-    Log.debugf 5 (fun k -> k "(@[@{<yellow>sat.cancel_until@}@ :level %d@])" lvl);
+    Log.debugf 5
+      (fun k -> k "(@[@{<yellow>sat.cancel_until@}@ :lvl %d :cur-decision-lvl %d@])" lvl @@ decision_level st);
     assert (lvl >= base_level st);
     (* Nothing to do if we try to backtrack to a non-existent level. *)
     if decision_level st <= lvl then (
@@ -471,15 +467,15 @@ module Make
      Wrapper function for adding a new propagated formula. *)
   let enqueue_bool st a reason : unit =
     if a.neg.is_true then (
-      Util.errorf "(@[sat.enqueue_bool@ :false-literal %a@])" Atom.debug a
+      Util.errorf "(@[sat.enqueue_bool.error@ :false-literal %a@])" Atom.debug a
     );
-    let level = Vec.size st.trail in
+    let level = decision_level st in
     Log.debugf 5
       (fun k->k "(@[sat.enqueue_bool@ :lvl %d@ %a@])" level Atom.debug a);
     let reason = if at_level_0 st then simpl_reason reason else reason in
     (* backtrack assignment if needed. Trail is backtracked automatically. *)
     assert (not a.is_true && a.var.v_level < 0 && a.var.reason = None);
-    on_backtrack_if_not_at_0 st
+    on_backtrack st
       (fun () ->
          a.var.v_level <- -1;
          a.is_true <- false;
@@ -653,7 +649,7 @@ module Make
       | fuip :: _ ->
         let lclause = Clause.make_l cr.cr_learnt (History cr.cr_history) in
         Vec.push st.clauses_learnt lclause;
-        attach_clause st lclause;
+        redo_down_to_level_0 st (fun () -> attach_clause st lclause);
         clause_bump_activity st lclause;
         if cr.cr_is_uip then (
           enqueue_bool st fuip (Bcp lclause)
@@ -712,21 +708,23 @@ module Make
         (* Since we cannot propagate the atom [a], in order to not lose
            the information that [a] must be true, we add clause to the list
            of clauses to add, so that it will be e-examined later. *)
-        Log.debug 5 "Unit clause, report failure";
+        Log.debug 5 "(sat.false-unit-clause@ report failure)";
         report_unsat st clause
       ) else if a.is_true then (
         (* If the atom is already true, then it should be because of a local hyp.
            However it means we can't propagate it at level 0. In order to not lose
            that information, we store the clause in a stack of clauses that we will
            add to the solver at the next pop. *)
-        Log.debug 5 "Unit clause, adding to root clauses";
+        Log.debug 5 "(sat.unit-clause@ adding to root clauses)";
         assert (0 < a.var.v_level && a.var.v_level <= base_level st);
-        on_backtrack_if_not_at_0 st (fun () -> Vec.pop vec_for_clause);
+        on_backtrack st
+          (fun () ->
+             Vec.pop vec_for_clause);
         Vec.push vec_for_clause clause;
       ) else (
         Log.debugf 5
           (fun k->k "(@[sat.add_clause.unit-clause@ :propagating %a@])" Atom.debug a);
-        on_backtrack_if_not_at_0 st (fun () -> Vec.pop vec_for_clause);
+        on_backtrack st (fun () -> Vec.pop vec_for_clause);
         Vec.push vec_for_clause clause;
         enqueue_bool st a (Bcp clause)
       )
@@ -803,7 +801,7 @@ module Make
             (fun () -> enqueue_bool st a (Bcp clause))
         )
       | a::b::_ ->
-        on_backtrack_if_not_at_0 st (fun () -> Vec.pop vec_for_clause);
+        on_backtrack st (fun () -> Vec.pop vec_for_clause);
         Vec.push vec_for_clause clause;
         (* Atoms need to be sorted in decreasing order of decision level,
            or we might watch the wrong literals. *)
@@ -902,7 +900,9 @@ module Make
   let act_push_ ~permanent st (l:formula IArray.t) (lemma:proof): unit =
     let atoms = IArray.to_array_map (new_atom ~permanent st) l in
     let c = Clause.make atoms (Lemma lemma) in
-    Log.debugf 3 (fun k->k "(@[sat.push_clause@ %a@])" Clause.debug c);
+    Log.debugf 3
+      (fun k->k "(@[sat.push_clause_from_theory@ :permanent %B@ %a@])"
+          permanent Clause.debug c);
     add_clause ~permanent st c
 
   (* TODO: ensure that the clause is removed upon backtracking *)
@@ -943,7 +943,6 @@ module Make
     push_persistent = act_push_persistent st;
     push_local = act_push_local st;
     on_backtrack = on_backtrack st;
-    at_level_0 = act_at_level_0 st;
     propagate = act_propagate st;
   }
 
@@ -1000,7 +999,7 @@ module Make
       while st.elt_head < Vec.size st.trail do
         let a = Vec.get st.trail st.elt_head in
         incr num_props;
-        Log.debugf 5 (fun k->k "(@[sat.propagate_atom@ %a@])" Atom.pp a);
+        Log.debugf 5 (fun k->k "(@[sat.bcp.propagate_atom@ %a@])" Atom.pp a);
         propagate_atom st a;
         st.elt_head <- st.elt_head + 1;
       done;
@@ -1052,7 +1051,7 @@ module Make
         if Vec.size st.trail = St.nb_elt st.st
         then raise Sat;
         if n_of_conflicts > 0 && !conflictC >= n_of_conflicts then (
-          Log.debug 3 "Restarting...";
+          Log.debug 3 "(sat.restarting)";
           cancel_until st (base_level st);
           raise Restart
         );
@@ -1088,7 +1087,7 @@ module Make
   (* fixpoint of propagation and decisions until a model is found, or a
      conflict is reached *)
   let solve (st:t) : unit =
-    Log.debug 5 "solve";
+    Log.debug 5 "(sat.solve)";
     if is_unsat st then raise Unsat;
     let n_of_conflicts = ref (to_float restart_first) in
     let n_of_learnts = ref ((to_float (nb_clauses st)) *. learntsize_factor) in
@@ -1145,17 +1144,17 @@ module Make
 
   (* create a factice decision level for local assumptions *)
   let push st : unit =
-    Log.debug 5 "Pushing a new user level";
+    Log.debug 5 "(sat.push-new-user-level)";
     cancel_until st (base_level st);
     Log.debugf 5
-      (fun k -> k "@[<v>Status:@,@[<hov 2>trail: %d - %d@,%a@]"
+      (fun k -> k "(@[<v>sat.status@ :trail %d - %d@ %a@]"
           st.elt_head st.th_head (Vec.print ~sep:"" Atom.debug) st.trail);
     begin match propagate st with
       | Some confl ->
         report_unsat st confl
       | None ->
         pp_trail st;
-        Log.debug 3 "Creating new user level";
+        Log.debug 3 "(sat.create-new-user-level)";
         new_decision_level st;
         Vec.push st.user_levels (Vec.size st.clauses_temp);
         assert (decision_level st = base_level st)
@@ -1215,7 +1214,7 @@ module Make
     let res = Array.exists (fun x -> x) tmp in
     if not res then (
       Log.debugf 5
-        (fun k -> k "Clause not satisfied: @[<hov>%a@]" Clause.debug c);
+        (fun k -> k "(@[sat.check-clause.error@ :not-satisfied %a@])" Clause.debug c);
       false
     ) else
       true

src/sat/Theory_intf.ml

@@ -52,9 +52,6 @@ type ('form, 'proof) actions = Actions of {
   on_backtrack: (unit -> unit) -> unit;
   (** [on_backtrack f] calls [f] when the main solver backtracks *)
 
-  at_level_0 : unit -> bool;
-  (** Are we at level 0? *)
-
   propagate : 'form -> 'form list -> 'proof -> unit;
   (** [propagate lit causes proof] informs the solver to propagate [lit], with the reason
       that the clause [causes => lit] is a theory tautology. It is faster than pushing

src/smt/Congruence_closure.ml

@@ -22,9 +22,6 @@ type actions = {
   on_backtrack:(unit -> unit) -> unit;
   (** Register a callback to be invoked upon backtracking below the current level *)
 
-  at_lvl_0:unit -> bool;
-  (** Are we currently at backtracking level 0? *)
-
   on_merge:repr -> repr -> explanation -> unit;
   (** Call this when two classes are merged *)
 
@@ -65,10 +62,7 @@ type t = {
    several times.
    See "fast congruence closure and extensions", Nieuwenhis&al, page 14 *)
 
-let[@inline] on_backtrack_if_not_lvl_0 cc f : unit =
+let[@inline] on_backtrack cc f : unit = cc.acts.on_backtrack f
-  if not (cc.acts.at_lvl_0 ()) then (
-    cc.acts.on_backtrack f
-  )
 
 let[@inline] is_root_ (n:node) : bool = n.n_root == n
 
@@ -90,7 +84,7 @@ let rec find_rec cc (n:node) : repr =
     let root = find_rec cc old_root in
     (* path compression *)
     if (root :> node) != old_root then (
-      on_backtrack_if_not_lvl_0 cc (fun () -> n.n_root <- old_root);
+      on_backtrack cc (fun () -> n.n_root <- old_root);
       n.n_root <- (root :> node);
     );
     root
@@ -155,7 +149,7 @@ let add_signature cc (t:term) (r:repr): unit = match signature cc t with
     (* add, but only if not present already *)
     begin match Sig_tbl.get cc.signatures_tbl s with
       | None ->
-        on_backtrack_if_not_lvl_0 cc
+        on_backtrack cc
           (fun () -> Sig_tbl.remove cc.signatures_tbl s);
         Sig_tbl.add cc.signatures_tbl s r;
       | Some r' ->
@@ -172,13 +166,13 @@ let push_pending cc t : unit =
 
 let push_combine cc t u e : unit =
   Log.debugf 5
-    (fun k->k "(@[<hv1>cc.push_combine@ %a@ %a@ expl: %a@])"
+    (fun k->k "(@[<hv1>cc.push_combine@ :t1 %a@ :t2 %a@ :expl %a@])"
       Equiv_class.pp t Equiv_class.pp u Explanation.pp e);
   Vec.push cc.combine (t,u,e)
 
 let push_propagation cc (lit:lit) (expl:explanation Bag.t): unit =
   Log.debugf 5
-    (fun k->k "(@[<hv1>cc.push_propagate@ %a@ expl: (@[<hv>%a@])@])"
+    (fun k->k "(@[<hv1>cc.push_propagate@ %a@ :expl (@[<hv>%a@])@])"
       Lit.pp lit (Util.pp_seq Explanation.pp) @@ Bag.to_seq expl);
   cc.acts.propagate lit expl
 
@@ -192,8 +186,7 @@ let[@inline] union cc (a:node) (b:node) (e:explanation): unit =
    postcondition: [n.n_expl = None] *)
 let rec reroot_expl (cc:t) (n:node): unit =
   let old_expl = n.n_expl in
-  on_backtrack_if_not_lvl_0 cc
+  on_backtrack cc (fun () -> n.n_expl <- old_expl);
-    (fun () -> n.n_expl <- old_expl);
   begin match old_expl with
     | E_none -> () (* already root *)
     | E_some {next=u; expl=e_n_u} ->
@@ -254,7 +247,7 @@ let ps_clear (cc:t) =
   ()
 
 let rec decompose_explain cc (e:explanation): unit =
-  Log.debugf 5 (fun k->k "(@[decompose_expl@ %a@])" Explanation.pp e);
+  Log.debugf 5 (fun k->k "(@[cc.decompose_expl@ %a@])" Explanation.pp e);
   begin match e with
     | E_reduction -> ()
     | E_lit lit -> ps_add_lit cc lit
@@ -305,7 +298,7 @@ let explain_loop (cc : t) : Lit.Set.t =
   while not (Vec.is_empty cc.ps_queue) do
     let a, b = Vec.pop_last cc.ps_queue in
     Log.debugf 5
-      (fun k->k "(@[explain_loop at@ %a@ %a@])" Equiv_class.pp a Equiv_class.pp b);
+      (fun k->k "(@[cc.explain_loop at@ %a@ %a@])" Equiv_class.pp a Equiv_class.pp b);
     assert (Equiv_class.equal (find cc a) (find cc b));
     let c = find_common_ancestor a b in
     explain_along_path cc a c;
@@ -352,9 +345,9 @@ let explain_unfold_bag ?(init=Lit.Set.empty) cc (b:explanation Bag.t) : Lit.Set.
 let add_tag_n cc (n:node) (tag:int) (expl:explanation) : unit =
   assert (is_root_ n);
   if not (Util.Int_map.mem tag n.n_tags) then (
-    on_backtrack_if_not_lvl_0 cc
+    on_backtrack cc
       (fun () -> n.n_tags <- Util.Int_map.remove tag n.n_tags);
-    n.n_tags <- Util.Int_map.add tag expl n.n_tags;
+    n.n_tags <- Util.Int_map.add tag (n,expl) n.n_tags;
   )
 
 (* conflict because [expl => t1 ≠ t2] but they are the same *)
@@ -396,7 +389,7 @@ and update_combine cc =
     let rb = find cc b in
     if not (Equiv_class.equal ra rb) then (
       assert (is_root_ ra);
-      assert (is_root_ (rb:>node));
+      assert (is_root_ rb);
       (* We will merge [r_from] into [r_into].
          we try to ensure that [size ra <= size rb] in general, unless
          it clashes with the invariant that the representative must
@@ -412,13 +405,19 @@ and update_combine cc =
       in
       let new_tags =
         Util.Int_map.union
-          (fun _i e1 e2 ->
+          (fun _i (n1,e1) (n2,e2) ->
              (* both maps contain same tag [_i]. conflict clause:
                  [e1 & e2 & e_ab] impossible *)
-             Log.debugf 5 (fun k->k "(cc.merge.distinct_conflict@ :tag %d@])" _i);
+             Log.debugf 5
+               (fun k->k "(@[<hv>cc.merge.distinct_conflict@ :tag %d@ \
+                          @[:r1 %a@ :e1 %a@]@ @[:r2 %a@ :e2 %a@]@ :e_ab %a@])"
+                   _i Equiv_class.pp n1 Explanation.pp e1
+                   Equiv_class.pp n2 Explanation.pp e2 Explanation.pp e_ab);
              let lits = explain_unfold cc e1 in
              let lits = explain_unfold ~init:lits cc e2 in
              let lits = explain_unfold ~init:lits cc e_ab in
+             let lits = explain_eq_n ~init:lits cc a n1 in
+             let lits = explain_eq_n ~init:lits cc b n2 in
              raise_conflict cc lits)
           ra.n_tags rb.n_tags
       in
@@ -462,8 +461,11 @@ and update_combine cc =
         let r_into = (r_into :> node) in
         let r_into_old_parents = r_into.n_parents in
         let r_into_old_tags = r_into.n_tags in
-        on_backtrack_if_not_lvl_0 cc
+        on_backtrack cc
           (fun () ->
+             Log.debugf 5
+               (fun k->k "(@[cc.undo_merge@ :of %a :into %a@])"
+                   Term.pp r_from.n_term Term.pp r_into.n_term);
              r_from.n_root <- r_from;
              r_into.n_tags <- r_into_old_tags;
              r_into.n_parents <- r_into_old_parents);
@@ -475,7 +477,7 @@ and update_combine cc =
       begin
         reroot_expl cc a;
         assert (a.n_expl = E_none);
-        on_backtrack_if_not_lvl_0 cc (fun () -> a.n_expl <- E_none);
+        on_backtrack cc (fun () -> a.n_expl <- E_none);
         a.n_expl <- E_some {next=b; expl=e_ab};
       end;
       (* notify listeners of the merge *)
@@ -501,15 +503,6 @@ and eval_pending (t:term): unit =
     theories
    *)
 
-(* FIXME: remove?
-(* main CC algo: add missing terms to the congruence class *)
-and update_add (cc:t) terms () =
-  while not (Queue.is_empty cc.terms_to_add) do
-    let t = Queue.pop cc.terms_to_add in
-    add cc t
-  done
-*)
-
 (* add [t] to [cc] when not present already *)
 and add_new_term cc (t:term) : node =
   assert (not @@ mem cc t);
@@ -517,7 +510,7 @@ and add_new_term cc (t:term) : node =
   (* how to add a subterm *)
   let add_to_parents_of_sub_node (sub:node) : unit =
     let old_parents = sub.n_parents in
-    on_backtrack_if_not_lvl_0 cc
+    on_backtrack cc
       (fun () -> sub.n_parents <- old_parents);
     sub.n_parents <- Bag.cons n sub.n_parents;
     push_pending cc sub
@@ -541,7 +534,7 @@ and add_new_term cc (t:term) : node =
       tc.tc_t_relevant view add_sub_t
   end;
   (* remove term when we backtrack *)
-  on_backtrack_if_not_lvl_0 cc (fun () -> Term.Tbl.remove cc.tbl t);
+  on_backtrack cc (fun () -> Term.Tbl.remove cc.tbl t);
   (* add term to the table *)
   Term.Tbl.add cc.tbl t n;
   (* [n] might be merged with other equiv classes *)
@@ -571,6 +564,10 @@ let assert_lit cc lit : unit = match Lit.view lit with
     (* equate t and true/false *)
     let rhs = if sign then true_ cc else false_ cc in
     let n = add cc t in
+    (* TODO: ensure that this is O(1).
+       basically, just have [n] point to true/false and thus acquire
+       the corresponding value, so its superterms (like [ite]) can evaluate
+       properly *)
     push_combine cc n rhs (E_lit lit);
     ()
 
@@ -612,14 +609,6 @@ module Distinct_ = struct
         mutable tags: Int_set.t;
       }
 
-  let get (n:Equiv_class.t) : Int_set.t =
-    Equiv_class.payload_find
-      ~f:(function
-        | P_dist {tags} -> Some tags
-        | _ -> None)
-      n
-    |> CCOpt.get_or ~default:Int_set.empty
-
   let add_tag (tag:int) (n:Equiv_class.t) : unit =
     if not @@
       CCList.exists
@@ -633,7 +622,6 @@ module Distinct_ = struct
 end
 
 let create ?(size=2048) ~actions (tst:Term.state) : t =
-  assert (actions.at_lvl_0 ());
   let nd = Equiv_class.dummy in
   let rec cc = {
     tst;

src/smt/Congruence_closure.mli

@@ -15,9 +15,6 @@ type actions = {
   on_backtrack:(unit -> unit) -> unit;
   (** Register a callback to be invoked upon backtracking below the current level *)
 
-  at_lvl_0:unit -> bool;
-  (** Are we currently at backtracking level 0? *)
-
   on_merge:repr -> repr -> explanation -> unit;
   (** Call this when two classes are merged *)
 

src/smt/Solver_types.ml

@@ -88,7 +88,7 @@ and cc_node = {
   mutable n_root: cc_node; (* representative of congruence class (itself if a representative) *)
   mutable n_expl: explanation_forest_link; (* the rooted forest for explanations *)
   mutable n_payload: cc_node_payload list; (* list of theory payloads *)
-  mutable n_tags: explanation Util.Int_map.t; (* "distinct" tags (i.e. set of `(distinct t1…tn)` terms this belongs to *)
+  mutable n_tags: (cc_node * explanation) Util.Int_map.t; (* "distinct" tags (i.e. set of `(distinct t1…tn)` terms this belongs to *)
 }
 
 (** Theory-extensible payloads *)

src/smt/Theory.ml

@@ -38,9 +38,6 @@ type actions = {
   on_backtrack: (unit -> unit) -> unit;
   (** Register an action to do when we backtrack *)
 
-  at_lvl_0: unit -> bool;
-  (** Are we at level 0 of backtracking? *)
-
   raise_conflict: 'a. conflict -> 'a;
   (** Give a conflict clause to the solver *)
 

src/smt/Theory_combine.ml

@@ -52,7 +52,7 @@ let assume_lit (self:t) (lit:Lit.t) : unit =
     | Lit_atom {term_cell=Bool true; _} -> ()
     | Lit_atom {term_cell=Bool false; _} -> ()
     | Lit_atom _ ->
-      (* transmit to CC and theories *)
+      (* transmit to theories. *)
       Congruence_closure.assert_lit (cc self) lit;
       theories self (fun (Theory.State th) -> th.on_assert th.st lit);
   end
@@ -148,7 +148,6 @@ let mk_cc_actions (self:t) : Congruence_closure.actions =
   let Sat_solver.Actions r = self.cdcl_acts in
   { Congruence_closure.
     on_backtrack = r.on_backtrack;
-    at_lvl_0 = r.at_level_0;
     on_merge = on_merge_from_cc self;
     raise_conflict = act_raise_conflict;
     propagate = act_propagate self;
@@ -170,7 +169,7 @@ let create (cdcl_acts:_ Sat_solver.actions) : t =
     theories = [];
     conflict = None;
   } in
-  ignore @@ Lazy.force @@ self.cc;
+  ignore (Lazy.force @@ self.cc : Congruence_closure.t);
   self
 
 (** {2 Interface to individual theories} *)
@@ -203,7 +202,6 @@ let mk_theory_actions (self:t) : Theory.actions =
   let Sat_solver.Actions r = self.cdcl_acts in
   { Theory.
     on_backtrack = r.on_backtrack;
-    at_lvl_0 = r.at_level_0;
     raise_conflict = act_raise_conflict;
     propagate = act_propagate self;
     all_classes = act_all_classes self;