From 0e5e40f145edd98445aa0667f501d62a7a6265d7 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 16 Feb 2021 18:35:07 -0500 Subject: [PATCH] feat(core/cc): expose more from the congruence closure --- src/cc/Sidekick_cc.ml | 2 ++ src/core/Sidekick_core.ml | 7 +++++++ src/msat-solver/Sidekick_msat_solver.ml | 1 + 3 files changed, 10 insertions(+) diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index 47c421a5..a00e3871 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -558,6 +558,8 @@ module Make (A: CC_ARG) let[@inline] add_term cc t : node = add_term_rec_ cc t + let mem_term = mem + let set_as_lit cc (n:node) (lit:lit) : unit = match n.n_as_lit with | Some _ -> () diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 7ef211bd..659ac42a 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -216,6 +216,9 @@ module type CC_S = sig (** Add the term to the congruence closure, if not present already. Will be backtracked. *) + val mem_term : t -> term -> bool + (** Returns [true] if the term is explicitly present in the congruence closure *) + type ev_on_pre_merge = t -> actions -> N.t -> N.t -> Expl.t -> unit type ev_on_post_merge = t -> actions -> N.t -> N.t -> unit type ev_on_new_term = t -> N.t -> term -> unit @@ -458,6 +461,10 @@ module type SOLVER_INTERNAL = sig (** Add/retrieve congruence closure node for this term. To be used in theories *) + val cc_mem_term : t -> term -> bool + (** Return [true] if the term is explicitly in the congruence closure. + To be used in theories *) + val on_cc_pre_merge : t -> (CC.t -> actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit) -> unit (** Callback for when two classes containing data for this key are merged (called before) *) diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index 5dc47f53..b8179236 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/src/msat-solver/Sidekick_msat_solver.ml @@ -282,6 +282,7 @@ module Make(A : ARG) let on_cc_propagate self f = CC.on_propagate (cc self) f let cc_add_term self t = CC.add_term (cc self) t + let cc_mem_term self t = CC.mem_term (cc self) t let cc_find self n = CC.find (cc self) n let cc_are_equal self t1 t2 = let n1 = cc_add_term self t1 in