From 3e7ef47fabd7d2b46a08c1d2db8a0367e3e66ecf Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 11 Jun 2019 10:26:04 -0500 Subject: [PATCH] feat: add CC.merge_t --- src/cc/Sidekick_cc.ml | 3 +++ src/core/Sidekick_core.ml | 3 +++ 2 files changed, 6 insertions(+) diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index 66ec066a..3d1c5443 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -832,6 +832,9 @@ module Make(CC_A: ARG) = struct (fun k->k "(@[cc.theory.merge@ :n1 %a@ :n2 %a@ :expl %a@])" N.pp n1 N.pp n2 Expl.pp expl); merge_classes cc n1 n2 expl + let[@inline] merge_t cc t1 t2 expl = + merge cc (add_term cc t1) (add_term cc t2) expl + let on_merge cc f = cc.on_merge <- f :: cc.on_merge let on_new_term cc f = cc.on_new_term <- f :: cc.on_new_term let on_conflict cc f = cc.on_conflict <- f :: cc.on_conflict diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 37c1c453..b508c856 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -273,6 +273,9 @@ module type CC_S = sig It must be a theory tautology that [expl ==> n1 = n2]. To be used in theories. *) + val merge_t : t -> term -> term -> Expl.t -> unit + (** Shortcut for adding + merging *) + val check : t -> actions -> unit (** Perform all pending operations done via {!assert_eq}, {!assert_lit}, etc. Will use the {!actions} to propagate literals, declare conflicts, etc. *)