feat(cc): have 2 phases of pre-merge events

the first phase observes plugin data unchanged; the second one
is used to update plugin data themselves. This fix a bug that manifests
itself depending on implementation details of Event, where some theory's
event handler fires too late and observes a state that has already
changed.

src/cc/Sidekick_cc.ml

@@ -351,6 +351,10 @@ module Make (A : ARG) :
       ( t * E_node.t * E_node.t * Expl.t,
         Handler_action.or_conflict )
       Event.Emitter.t;
+    on_pre_merge2:
+      ( t * E_node.t * E_node.t * Expl.t,
+        Handler_action.or_conflict )
+      Event.Emitter.t;
     on_post_merge:
       (t * E_node.t * E_node.t, Handler_action.t list) Event.Emitter.t;
     on_new_term: (t * E_node.t * term, Handler_action.t list) Event.Emitter.t;
@@ -900,14 +904,22 @@ module Make (A : ARG) :
 
       (* call [on_pre_merge] functions, and merge theory data items *)
       (* explanation is [a=ra & e_ab & b=rb] *)
-      let expl =
-        Expl.mk_list [ e_ab; Expl.mk_merge a ra; Expl.mk_merge b rb ]
-      in
-      Event.emit_iter self.on_pre_merge (self, r_into, r_from, expl)
-        ~f:(function
-        | Ok l -> push_action_l self l
-        | Error (Handler_action.Conflict expl) ->
-          raise_conflict_from_expl self expl);
+      (let expl =
+         Expl.mk_list [ e_ab; Expl.mk_merge a ra; Expl.mk_merge b rb ]
+       in
+
+       let handle_act = function
+         | Ok l -> push_action_l self l
+         | Error (Handler_action.Conflict expl) ->
+           raise_conflict_from_expl self expl
+       in
+
+       Event.emit_iter self.on_pre_merge
+         (self, r_into, r_from, expl)
+         ~f:handle_act;
+       Event.emit_iter self.on_pre_merge2
+         (self, r_into, r_from, expl)
+         ~f:handle_act);
 
       (* TODO: merge plugin data here, _after_ the pre-merge hooks are called,
          so they have a chance of observing pre-merge plugin data *)
@@ -1095,6 +1107,7 @@ module Make (A : ARG) :
     Expl_state.to_resolved_expl expl_st
 
   let[@inline] on_pre_merge self = Event.of_emitter self.on_pre_merge
+  let[@inline] on_pre_merge2 self = Event.of_emitter self.on_pre_merge2
   let[@inline] on_post_merge self = Event.of_emitter self.on_post_merge
   let[@inline] on_new_term self = Event.of_emitter self.on_new_term
   let[@inline] on_conflict self = Event.of_emitter self.on_conflict
@@ -1118,6 +1131,7 @@ module Make (A : ARG) :
         signatures_tbl = Sig_tbl.create size;
         bitgen;
         on_pre_merge = Event.Emitter.create ();
+        on_pre_merge2 = Event.Emitter.create ();
         on_post_merge = Event.Emitter.create ();
         on_new_term = Event.Emitter.create ();
         on_conflict = Event.Emitter.create ();

src/cc/plugin/sidekick_cc_plugin.ml

@@ -147,7 +147,7 @@ module Make (M : MONOID_PLUGIN_ARG) :
     (* setup *)
     let () =
       Event.on (CC.on_new_term cc) ~f:(fun (_, r, t) -> on_new_term cc r t);
-      Event.on (CC.on_pre_merge cc) ~f:(fun (_, ra, rb, expl) ->
+      Event.on (CC.on_pre_merge2 cc) ~f:(fun (_, ra, rb, expl) ->
           on_pre_merge cc ra rb expl);
       ()
   end

src/sigs/cc/sidekick_sigs_cc.ml

@@ -301,6 +301,12 @@ module type S = sig
   (** [Ev_on_pre_merge acts n1 n2 expl] is emitted right before [n1]
       and [n2] are merged with explanation [expl].  *)
 
+  val on_pre_merge2 :
+    t -> (t * E_node.t * E_node.t * Expl.t, Handler_action.or_conflict) Event.t
+  (** Second phase of "on pre merge". This runs after {!on_pre_merge}
+      and is used by Plugins. {b NOTE}: Plugin state might be observed as already
+      changed in these handlers. *)
+
   val on_post_merge :
     t -> (t * E_node.t * E_node.t, Handler_action.t list) Event.t
   (** [ev_on_post_merge acts n1 n2] is emitted right after [n1]

src/smt-solver/Sidekick_smt_solver.ml

@@ -102,7 +102,6 @@ module Make (A : ARG) :
   type term = Term.t
   type ty = Ty.t
   type lit = Lit.t
-  type rule = Proof_trace.A.rule
   type step_id = Proof_trace.A.step_id
   type proof_trace = Proof_trace.t
 
@@ -118,8 +117,6 @@ module Make (A : ARG) :
       merged because of the current model so it's not a "true" conflict
       and doesn't need to kill the current trail. *)
 
-  exception Semantic_conflict of th_combination_conflict
-
   (* the full argument to the congruence closure *)
   module CC_arg = struct
     module T = T

src/th-data/Sidekick_th_data.ml

@@ -1,6 +1,5 @@
 (** Theory for datatypes. *)
 
-open Sidekick_sigs_smt
 include Th_intf
 
 let name = "th-data"
@@ -462,7 +461,6 @@ module Make (A : ARG) : S with module A = A = struct
     | _ -> assert false
 
   let on_pre_merge (self : t) (cc, n1, n2, expl) : _ result =
-    let exception E_confl of SI.CC.Expl.t in
     let acts = ref [] in
     let merge_is_a n1 (c1 : Monoid_cstor.t) n2 (is_a2 : Monoid_parents.is_a) =
       let is_true = A.Cstor.equal c1.c_cstor is_a2.is_a_cstor in
@@ -534,11 +532,9 @@ module Make (A : ARG) : S with module A = A = struct
         List.iter (fun is_a2 -> merge_is_a n1 c1 n2 is_a2) p2.parent_is_a;
         List.iter (fun s2 -> merge_select n1 c1 n2 s2) p2.parent_select
     in
-    try
-      merge_c_p n1 n2;
-      merge_c_p n2 n1;
-      Ok !acts
-    with E_confl e -> Error (SI.CC.Handler_action.Conflict e)
+    merge_c_p n1 n2;
+    merge_c_p n2 n1;
+    Ok !acts
 
   module Acyclicity_ = struct
     type repr = N.t

src/util/Event.ml

@@ -6,15 +6,15 @@ let nop_handler_ _ = assert false
 module Emitter = struct
   type nonrec ('a, 'b) t = ('a, 'b) t
 
-  let emit (self : (_, unit) t) x = Vec.rev_iter self.h ~f:(fun h -> h x)
+  let emit (self : (_, unit) t) x = Vec.iter self.h ~f:(fun h -> h x)
 
   let emit_collect (self : _ t) x : _ list =
     let l = ref [] in
-    Vec.rev_iter self.h ~f:(fun h -> l := h x :: !l);
+    Vec.iter self.h ~f:(fun h -> l := h x :: !l);
     !l
 
   let emit_iter self x ~f =
-    Vec.rev_iter self.h ~f:(fun h ->
+    Vec.iter self.h ~f:(fun h ->
         let y = h x in
         f y)