From 851dda696a7c295b8b867663dc91ae630f860d80 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 22 Jul 2022 21:31:42 -0400 Subject: [PATCH] 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 | 30 ++++++++++++++++++++------- src/cc/plugin/sidekick_cc_plugin.ml | 2 +- src/sigs/cc/sidekick_sigs_cc.ml | 6 ++++++ src/smt-solver/Sidekick_smt_solver.ml | 3 --- src/th-data/Sidekick_th_data.ml | 10 +++------ src/util/Event.ml | 6 +++--- 6 files changed, 35 insertions(+), 22 deletions(-) diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index 267703e8..ae1562ae 100644 --- a/src/cc/Sidekick_cc.ml +++ b/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 (); diff --git a/src/cc/plugin/sidekick_cc_plugin.ml b/src/cc/plugin/sidekick_cc_plugin.ml index 65e936d2..6ee73414 100644 --- a/src/cc/plugin/sidekick_cc_plugin.ml +++ b/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 diff --git a/src/sigs/cc/sidekick_sigs_cc.ml b/src/sigs/cc/sidekick_sigs_cc.ml index c8647ca0..3bb47ec7 100644 --- a/src/sigs/cc/sidekick_sigs_cc.ml +++ b/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] diff --git a/src/smt-solver/Sidekick_smt_solver.ml b/src/smt-solver/Sidekick_smt_solver.ml index 403a61d8..c8b439dd 100644 --- a/src/smt-solver/Sidekick_smt_solver.ml +++ b/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 diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index e0cce7da..bcf2b0b6 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/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 diff --git a/src/util/Event.ml b/src/util/Event.ml index af72dcc8..e1561b3b 100644 --- a/src/util/Event.ml +++ b/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)