From b10aaf05f229ab6f062f9ff462dd4c4c517fdfa5 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Wed, 20 Jul 2022 21:40:04 -0400
Subject: [PATCH] wip: expose bug caused by order of event handlers

if plugin data is updated before `Th_data.on_pre_merge` is called, it
never has a chance to observe the un-merged data and react accordingly.
we need to ensure that all handlers see the same data before any change
is made.
---
 src/th-data/Sidekick_th_data.ml | 1 +
 src/util/Vec.ml                 | 5 +++++
 src/util/Vec.mli                | 1 +
 3 files changed, 7 insertions(+)

diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml
index 736e5fab..d85c96b4 100644
--- a/src/th-data/Sidekick_th_data.ml
+++ b/src/th-data/Sidekick_th_data.ml
@@ -779,6 +779,7 @@ module Make (A : ARG) : S with module A = A = struct
     Log.debugf 1 (fun k -> k "(setup :%s)" name);
     SI.on_preprocess solver (preprocess self);
     SI.on_cc_new_term solver (on_new_term self);
+    (* note: this needs to happen before we modify the plugin data *)
     SI.on_cc_pre_merge solver (on_pre_merge self);
     SI.on_final_check solver (on_final_check self);
     SI.on_model solver ~ask:(on_model_gen self);
diff --git a/src/util/Vec.ml b/src/util/Vec.ml
index a25099bc..46750264 100644
--- a/src/util/Vec.ml
+++ b/src/util/Vec.ml
@@ -130,6 +130,11 @@ let iter ~f t =
     f (Array.unsafe_get t.data i)
   done
 
+let rev_iter ~f t =
+  for i = size t - 1 downto 0 do
+    f (Array.unsafe_get t.data i)
+  done
+
 let iteri ~f t =
   for i = 0 to size t - 1 do
     f i (Array.unsafe_get t.data i)
diff --git a/src/util/Vec.mli b/src/util/Vec.mli
index e94028a7..b3c71cd5 100644
--- a/src/util/Vec.mli
+++ b/src/util/Vec.mli
@@ -81,6 +81,7 @@ val sort : 'a t -> ('a -> 'a -> int) -> unit
 val iter : f:('a -> unit) -> 'a t -> unit
 (** Iterate on elements *)
 
+val rev_iter : f:('a -> unit) -> 'a t -> unit
 val to_iter : 'a t -> 'a Iter.t
 
 val iteri : f:(int -> 'a -> unit) -> 'a t -> unit