From 1eb26e50913b7012c3d0fb21a8367567b85f25e2 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 21 Aug 2022 22:34:15 -0400 Subject: [PATCH] refactor(cc): cleanup a bit, smaller closures for backtracking --- src/cc/CC.ml | 27 +++++++++++++-------------- src/cc/e_node.ml | 7 ++++++- src/cc/e_node.mli | 4 ++++ src/cc/signature.ml | 2 ++ 4 files changed, 25 insertions(+), 15 deletions(-) diff --git a/src/cc/CC.ml b/src/cc/CC.ml index 24184958..0f8cfe5b 100644 --- a/src/cc/CC.ml +++ b/src/cc/CC.ml @@ -182,9 +182,11 @@ let add_signature self (s : signature) (n : e_node) : unit = on_backtrack self (fun () -> Sig_tbl.remove self.signatures_tbl s); Sig_tbl.add self.signatures_tbl s n -let[@inline] push_pending self t : unit = - Log.debugf 50 (fun k -> k "(@[cc.push-pending@ %a@])" E_node.pp t); - Vec.push self.pending t +let push_pending self (n : E_node.t) : unit = + if Option.is_some n.n_sig0 then ( + Log.debugf 50 (fun k -> k "(@[cc.push-pending@ %a@])" E_node.pp n); + Vec.push self.pending n + ) let[@inline] push_action self (a : Handler_action.t) : unit = Vec.push self.combine (CT_act a) @@ -449,7 +451,7 @@ and add_new_term_ self (t : Term.t) : e_node = Event.emit_iter self.on_new_term (self, n, t) ~f:(push_action_l self); n -(* compute the initial signature of the given e_node *) +(* compute the initial signature of the given e_node [n] *) and compute_sig0 (self : t) (n : e_node) : Signature.t option = (* add sub-term to [cc], and register [n] to its parents. Note that we return the exact sub-term, to get proper @@ -530,7 +532,7 @@ and task_pending_ self (n : e_node) : unit = | None -> () (* no-op *) | Some (Eq (a, b)) -> (* if [a=b] is now true, merge [(a=b)] and [true] *) - if same_class a b then ( + if a != b && same_class a b then ( let expl = Expl.mk_merge a b in Log.debugf 5 (fun k -> k "(@[cc.pending.eq@ %a@ :r1 %a@ :r2 %a@])" E_node.pp n E_node.pp a @@ -549,7 +551,7 @@ and task_pending_ self (n : e_node) : unit = ) | Some s0 -> (* update the signature by using [find] on each sub-e_node *) - let s = (update_sig [@inlined]) s0 in + let s = update_sig s0 in (match find_signature self s with | None -> (* add to the signature table [sig(n) --> n] *) @@ -657,13 +659,10 @@ and task_merge_ self a b e_ab : unit = assert (u.n_root == r_from); u.n_root <- r_into); (* capture current state *) - let r_into_old_next = r_into.n_next in - let r_from_old_next = r_from.n_next in let r_into_old_parents = r_into.n_parents in let r_into_old_bits = r_into.n_bits in (* swap [into.next] and [from.next], merging the classes *) - r_into.n_next <- r_from_old_next; - r_from.n_next <- r_into_old_next; + E_node.swap_next r_into r_from; r_into.n_parents <- Bag.append r_into.n_parents r_from.n_parents; r_into.n_size <- r_into.n_size + r_from.n_size; r_into.n_bits <- Bits.merge r_into.n_bits r_from.n_bits; @@ -673,8 +672,8 @@ and task_merge_ self a b e_ab : unit = k "(@[cc.undo_merge@ :from %a@ :into %a@])" E_node.pp r_from E_node.pp r_into); r_into.n_bits <- r_into_old_bits; - r_into.n_next <- r_into_old_next; - r_from.n_next <- r_from_old_next; + (* un-merge the classes *) + E_node.swap_next r_into r_from; r_into.n_parents <- r_into_old_parents; (* NOTE: this must come after the restoration of [next] pointers, otherwise we'd iterate on too big a class *) @@ -686,9 +685,9 @@ and task_merge_ self a b e_ab : unit = and [b], not their roots. *) reroot_expl self a; assert (a.n_expl = FL_none); - (* on backtracking, link may be inverted, but we delete the one - that bridges between [a] and [b] *) on_backtrack self (fun () -> + (* on backtracking, link may be inverted, but we delete the one + that bridges between [a] and [b] *) match a.n_expl, b.n_expl with | FL_some e, _ when E_node.equal e.next b -> a.n_expl <- FL_none | _, FL_some e when E_node.equal e.next a -> b.n_expl <- FL_none diff --git a/src/cc/e_node.ml b/src/cc/e_node.ml index b8979cf8..f50db6d0 100644 --- a/src/cc/e_node.ml +++ b/src/cc/e_node.ml @@ -5,7 +5,7 @@ type t = e_node let[@inline] equal (n1 : t) n2 = n1 == n2 let[@inline] hash n = Term.hash n.n_term let[@inline] term n = n.n_term -let[@inline] pp out n = Term.pp_debug out n.n_term +let[@inline] pp out n = Term.pp out n.n_term let[@inline] as_lit n = n.n_as_lit let make (t : Term.t) : t = @@ -42,6 +42,11 @@ let[@inline] iter_parents (n : e_node) : e_node Iter.t = assert (is_root n); Bag.to_iter n.n_parents +let[@inline] swap_next n1 n2 : unit = + let tmp = n1.n_next in + n1.n_next <- n2.n_next; + n2.n_next <- tmp + module Internal_ = struct let iter_class_ = iter_class_ let make = make diff --git a/src/cc/e_node.mli b/src/cc/e_node.mli index 6486c74d..524ab43a 100644 --- a/src/cc/e_node.mli +++ b/src/cc/e_node.mli @@ -55,6 +55,10 @@ val iter_parents : t -> t Iter.t val as_lit : t -> Lit.t option +val swap_next : t -> t -> unit +(** Swap the next pointer of each node. If their classes were disjoint, + they are now unioned. *) + module Internal_ : sig val iter_class_ : t -> t Iter.t val make : Term.t -> t diff --git a/src/cc/signature.ml b/src/cc/signature.ml index 8678ba04..da74564c 100644 --- a/src/cc/signature.ml +++ b/src/cc/signature.ml @@ -8,6 +8,8 @@ type t = signature let equal (s1 : t) s2 : bool = let open CC_view in + s1 == s2 + || match s1, s2 with | Bool b1, Bool b2 -> b1 = b2 | App_fun (f1, []), App_fun (f2, []) -> Const.equal f1 f2