simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat: add CC.merge_t

Browse source
This commit is contained in:
Simon Cruanes 2019-06-11 10:26:04 -05:00
parent 1212e219eb
commit 3e7ef47fab
2 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/cc/Sidekick_cc.ml
View file

@ -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); (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 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_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_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 let on_conflict cc f = cc.on_conflict <- f :: cc.on_conflict

3
src/core/Sidekick_core.ml
View file

@ -273,6 +273,9 @@ module type CC_S = sig
It must be a theory tautology that [expl ==> n1 = n2]. It must be a theory tautology that [expl ==> n1 = n2].
To be used in theories. *) To be used in theories. *)
val merge_t : t -> term -> term -> Expl.t -> unit
(** Shortcut for adding + merging *)
val check : t -> actions -> unit val check : t -> actions -> unit
(** Perform all pending operations done via {!assert_eq}, {!assert_lit}, etc. (** Perform all pending operations done via {!assert_eq}, {!assert_lit}, etc.
Will use the {!actions} to propagate literals, declare conflicts, etc. *) Will use the {!actions} to propagate literals, declare conflicts, etc. *)