refactor(cc): merge the two task queues

src/smt/Congruence_closure.ml

@@ -16,9 +16,6 @@ end
 
 module Sig_tbl = CCHashtbl.Make(Signature)
 
-type merge_op = node * node * explanation
-(* a merge operation to perform *)
-
 module type ACTIONS = sig
   val on_backtrack: (unit -> unit) -> unit
   (** Register a callback to be invoked upon backtracking below the current level *)
@@ -35,6 +32,10 @@ end
 
 type actions = (module ACTIONS)
 
+type task =
+  | T_pending of node
+  | T_merge of node * node * explanation
+
 type t = {
   tst: Term.state;
   acts: actions;
@@ -48,10 +49,8 @@ type t = {
      The critical property is that all members of an equivalence class
      that have the same "shape" (including head symbol)
      have the same signature *)
-  pending: node Vec.t;
+  tasks: task Vec.t;
-  (* nodes to check, maybe their new signature is in {!signatures_tbl} *)
+  (* tasks to perform *)
-  combine: merge_op Vec.t;
-  (* pairs of terms to merge *)
   mutable ps_lits: Lit.Set.t;
   (* proof state *)
   ps_queue: (node*node) Vec.t;
@@ -146,22 +145,18 @@ let add_signature cc (t:term) (r:node): unit =
         assert (same_class cc r r');
     end
 
-let[@inline] is_done (cc:t): bool =
-  Vec.is_empty cc.pending &&
-  Vec.is_empty cc.combine
-
 let push_pending cc t : unit =
   if not @@ Equiv_class.get_field Equiv_class.field_is_pending t then (
     Log.debugf 5 (fun k->k "(@[<hv1>cc.push_pending@ %a@])" Equiv_class.pp t);
     Equiv_class.set_field Equiv_class.field_is_pending true t;
-    Vec.push cc.pending t
+    Vec.push cc.tasks (T_pending t)
   )
 
 let push_combine cc t u e : unit =
   Log.debugf 5
     (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)
+  Vec.push cc.tasks @@ T_merge (t,u,e)
 
 (* re-root the explanation tree of the equivalence class of [n]
    so that it points to [n].
@@ -296,108 +291,106 @@ let add_tag_n cc (n:node) (tag:int) (expl:explanation) : unit =
 
 (* main CC algo: add terms from [pending] to the signature table,
    check for collisions *)
-let rec update_pending (cc:t): unit =
+let rec update_tasks (cc:t): unit =
   (* step 2 deal with pending (parent) terms whose equiv class
      might have changed *)
-  while not (Vec.is_empty cc.pending) do
+  while not (Vec.is_empty cc.tasks) do
-    let n = Vec.pop_last cc.pending in
+    let task = Vec.pop_last cc.tasks in
-    Equiv_class.set_field Equiv_class.field_is_pending false n;
+    match task with 
-    (* check if some parent collided *)
+    | T_pending n -> task_pending_ cc n
-    begin match find_by_signature cc n.n_term with
+    | T_merge (t,u,expl) -> task_merge_ cc t u expl
-      | None ->
+  done
-        (* add to the signature table [sig(n) --> n] *)
+
-        add_signature cc n.n_term n
+and task_pending_ cc n =
-      | Some u when n == u -> ()
+  Equiv_class.set_field Equiv_class.field_is_pending false n;
-      | Some u ->
+  (* check if some parent collided *)
-        (* must combine [t] with [r] *)
+  begin match find_by_signature cc n.n_term with
-        if not @@ same_class cc n u then (
+    | None ->
-          (* [t1] and [t2] must be applications of the same symbol to
+      (* add to the signature table [sig(n) --> n] *)
-             arguments that are pairwise equal *)
+      add_signature cc n.n_term n
-          assert (n != u);
+    | Some u when n == u -> ()
-          let expl = match n.n_term.term_view, u.n_term.term_view with
+    | Some u ->
-            | App_cst (f1, a1), App_cst (f2, a2) ->
+      (* must combine [t] with [r] *)
-              assert (Cst.equal f1 f2);
+      if not @@ same_class cc n u then (
-              assert (IArray.length a1 = IArray.length a2);
+        (* [t1] and [t2] must be applications of the same symbol to
-              Explanation.mk_merges @@ IArray.map2 (fun u1 u2 -> add_ cc u1, add_ cc u2) a1 a2
+           arguments that are pairwise equal *)
-            | If _, _ | App_cst _, _ | Bool _, _
+        assert (n != u);
-              -> assert false
+        let expl = match n.n_term.term_view, u.n_term.term_view with
-          in
+          | App_cst (f1, a1), App_cst (f2, a2) ->
-          push_combine cc n u expl
+            assert (Cst.equal f1 f2);
-        )
+            assert (IArray.length a1 = IArray.length a2);
-    end;
+            Explanation.mk_merges @@ IArray.map2 (fun u1 u2 -> add_ cc u1, add_ cc u2) a1 a2
-    (* FIXME: when to actually evaluate?
+          | If _, _ | App_cst _, _ | Bool _, _
-    eval_pending cc;
+            -> assert false
-    *)
+        in
-  done;
+        push_combine cc n u expl
-  if not (is_done cc) then (
+      )
-    update_combine cc (* repeat *)
+  end;
-  )
+  (* FIXME: when to actually evaluate?
+     eval_pending cc;
+  *)
+  ()
 
 (* main CC algo: merge equivalence classes in [st.combine].
    @raise Exn_unsat if merge fails *)
-and update_combine cc =
+and task_merge_ cc a b e_ab : unit =
-  while not (Vec.is_empty cc.combine) do
+  let ra = find cc a in
-    let a, b, e_ab = Vec.pop_last cc.combine in
+  let rb = find cc b in
-    let ra = find cc a in
+  if not (Equiv_class.equal ra rb) then (
-    let rb = find cc b in
+    assert (is_root_ ra);
-    if not (Equiv_class.equal ra rb) then (
+    assert (is_root_ rb);
-      assert (is_root_ ra);
+    (* We will merge [r_from] into [r_into].
-      assert (is_root_ rb);
+       we try to ensure that [size ra <= size rb] in general *)
-      (* We will merge [r_from] into [r_into].
+    let r_from, r_into = if size_ ra > size_ rb then rb, ra else ra, rb in
-         we try to ensure that [size ra <= size rb] in general *)
+    let new_tags =
-      let r_from, r_into = if size_ ra > size_ rb then rb, ra else ra, rb in
+      Util.Int_map.union
-      let new_tags =
+        (fun _i (n1,e1) (n2,e2) ->
-        Util.Int_map.union
+           (* both maps contain same tag [_i]. conflict clause:
-          (fun _i (n1,e1) (n2,e2) ->
+               [e1 & e2 & e_ab] impossible *)
-             (* both maps contain same tag [_i]. conflict clause:
+           Log.debugf 5
-                 [e1 & e2 & e_ab] impossible *)
+             (fun k->k "(@[<hv>cc.merge.distinct_conflict@ :tag %d@ \
-             Log.debugf 5
+                        @[:r1 %a@ :e1 %a@]@ @[:r2 %a@ :e2 %a@]@ :e_ab %a@])"
-               (fun k->k "(@[<hv>cc.merge.distinct_conflict@ :tag %d@ \
+                 _i Equiv_class.pp n1 Explanation.pp e1
-                          @[:r1 %a@ :e1 %a@]@ @[:r2 %a@ :e2 %a@]@ :e_ab %a@])"
+                 Equiv_class.pp n2 Explanation.pp e2 Explanation.pp e_ab);
-                   _i Equiv_class.pp n1 Explanation.pp e1
+           let lits = explain_unfold cc e1 in
-                   Equiv_class.pp n2 Explanation.pp e2 Explanation.pp e_ab);
+           let lits = explain_unfold ~init:lits cc e2 in
-             let lits = explain_unfold cc e1 in
+           let lits = explain_unfold ~init:lits cc e_ab in
-             let lits = explain_unfold ~init:lits cc e2 in
+           let lits = explain_eq_n ~init:lits cc a n1 in
-             let lits = explain_unfold ~init:lits cc e_ab in
+           let lits = explain_eq_n ~init:lits cc b n2 in
-             let lits = explain_eq_n ~init:lits cc a n1 in
+           raise_conflict cc @@ Lit.Set.elements lits)
-             let lits = explain_eq_n ~init:lits cc b n2 in
+        ra.n_tags rb.n_tags
-             raise_conflict cc @@ Lit.Set.elements lits)
+    in
-          ra.n_tags rb.n_tags
+    (* remove [ra.parents] from signature, put them into [st.pending] *)
-      in
+    begin
-      (* remove [ra.parents] from signature, put them into [st.pending] *)
+      Bag.to_seq r_from.n_parents
-      begin
+        (fun parent -> push_pending cc parent)
-        Bag.to_seq r_from.n_parents
+    end;
-          (fun parent -> push_pending cc parent)
+    (* perform [union ra rb] *)
-      end;
+    begin
-      (* perform [union ra rb] *)
+      let r_into_old_parents = r_into.n_parents in
-      begin
+      let r_into_old_tags = r_into.n_tags in
-        let r_into_old_parents = r_into.n_parents in
+      on_backtrack cc
-        let r_into_old_tags = r_into.n_tags in
+        (fun () ->
-        on_backtrack cc
+           Log.debugf 15
-          (fun () ->
+             (fun k->k "(@[cc.undo_merge@ :of %a :into %a@])"
-             Log.debugf 15
+                 Term.pp r_from.n_term Term.pp r_into.n_term);
-               (fun k->k "(@[cc.undo_merge@ :of %a :into %a@])"
+           r_from.n_root <- r_from;
-                   Term.pp r_from.n_term Term.pp r_into.n_term);
+           r_into.n_tags <- r_into_old_tags;
-             r_from.n_root <- r_from;
+           r_into.n_parents <- r_into_old_parents);
-             r_into.n_tags <- r_into_old_tags;
+      r_from.n_root <- r_into;
-             r_into.n_parents <- r_into_old_parents);
+      r_into.n_tags <- new_tags;
-        r_from.n_root <- r_into;
+      r_from.n_parents <- Bag.append r_into_old_parents r_from.n_parents;
-        r_into.n_tags <- new_tags;
+    end;
-        r_from.n_parents <- Bag.append r_into_old_parents r_from.n_parents;
+    (* update explanations (a -> b), arbitrarily *)
-      end;
+    begin
-      (* update explanations (a -> b), arbitrarily *)
+      reroot_expl cc a;
-      begin
+      assert (a.n_expl = E_none);
-        reroot_expl cc a;
+      on_backtrack cc (fun () -> a.n_expl <- E_none);
-        assert (a.n_expl = E_none);
+      a.n_expl <- E_some {next=b; expl=e_ab};
-        on_backtrack cc (fun () -> a.n_expl <- E_none);
+    end;
-        a.n_expl <- E_some {next=b; expl=e_ab};
+    (* notify listeners of the merge *)
-      end;
+    notify_merge cc r_from ~into:r_into e_ab;
-      (* notify listeners of the merge *)
+  )
-      notify_merge cc r_from ~into:r_into e_ab;
-    )
-  done;
-  (* now update pending terms again *)
-  update_pending cc
 
 (* Checks if [ra] and [~into] have compatible normal forms and can
    be merged w.r.t. the theories.
@@ -452,12 +445,12 @@ and[@inline] add_ cc t : node =
 
 let add cc t : node =
   let n = add_ cc t in
-  update_pending cc;
+  update_tasks cc;
   n
 
 let add_seq cc seq =
   seq (fun t -> ignore @@ add_ cc t);
-  update_pending cc
+  update_tasks cc
 
 (* assert that this boolean literal holds *)
 let assert_lit cc lit : unit =
@@ -473,7 +466,7 @@ let assert_lit cc lit : unit =
      the corresponding value, so its superterms (like [ite]) can evaluate
      properly *)
   push_combine cc n rhs (E_lit lit);
-  update_combine cc
+  update_tasks cc
 
 let assert_eq cc (t:term) (u:term) e : unit =
   let n1 = add_ cc t in
@@ -482,7 +475,7 @@ let assert_eq cc (t:term) (u:term) e : unit =
     let e = Explanation.E_lits e in
     push_combine cc n1 n2 e;
   );
-  update_pending cc
+  update_tasks cc
 
 let assert_distinct cc (l:term list) ~neq (lit:Lit.t) : unit =
   assert (match l with[] | [_] -> false | _ -> true);
@@ -513,8 +506,7 @@ let create ?(size=2048) ~actions (tst:Term.state) : t =
     acts=actions;
     tbl = Term.Tbl.create size;
     signatures_tbl = Sig_tbl.create size;
-    pending=Vec.make_empty Equiv_class.dummy;
+    tasks=Vec.make_empty (T_pending Equiv_class.dummy);
-    combine= Vec.make_empty (nd,nd,E_reduction);
     ps_lits=Lit.Set.empty;
     ps_queue=Vec.make_empty (nd,nd);
     true_ = Equiv_class.dummy;
@@ -526,7 +518,7 @@ let create ?(size=2048) ~actions (tst:Term.state) : t =
 
 let final_check cc : unit =
   Log.debug 5 "(CC.final_check)";
-  update_pending cc
+  update_tasks cc
 
 (* model: map each uninterpreted equiv class to some ID *)
 let mk_model (cc:t) (m:Model.t) : Model.t =