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

feat(core): add CC.explain_eq to explain why two nodes were merged

Browse source
This commit is contained in:
Simon Cruanes 2020-11-17 18:22:51 -05:00
parent 6a0731eeb1
commit 60fe3506d5
2 changed files with 14 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/cc/Sidekick_cc.ml
View file

@ -835,6 +835,10 @@ module Make (A: CC_ARG)
let[@inline] merge_t cc t1 t2 expl = let[@inline] merge_t cc t1 t2 expl =
merge cc (add_term cc t1) (add_term cc t2) expl merge cc (add_term cc t1) (add_term cc t2) expl
let explain_eq cc n1 n2 : lit list =
let th = ref true in
explain_pair cc ~th [] n1 n2
let on_pre_merge cc f = cc.on_pre_merge <- f :: cc.on_pre_merge let on_pre_merge cc f = cc.on_pre_merge <- f :: cc.on_pre_merge
let on_post_merge cc f = cc.on_post_merge <- f :: cc.on_post_merge let on_post_merge cc f = cc.on_post_merge <- f :: cc.on_post_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

10
src/core/Sidekick_core.ml
View file

@ -280,6 +280,10 @@ module type CC_S = sig
val assert_lits : t -> lit Iter.t -> unit val assert_lits : t -> lit Iter.t -> unit
(** Addition of many literals *) (** Addition of many literals *)
val explain_eq : t -> N.t -> N.t -> lit list
(** Explain why the two nodes are equal.
Fails if they are not, in an unspecified way *)
val raise_conflict_from_expl : t -> actions -> Expl.t -> 'a val raise_conflict_from_expl : t -> actions -> Expl.t -> 'a
(** Raise a conflict with the given explanation (** Raise a conflict with the given explanation
it must be a theory tautology that [expl ==> absurd]. it must be a theory tautology that [expl ==> absurd].
@ -390,6 +394,9 @@ module type SOLVER_INTERNAL = sig
(** {3 hooks for the theory} *) (** {3 hooks for the theory} *)
val propagate : t -> actions -> lit -> reason:(unit -> lit list) -> proof -> unit val propagate : t -> actions -> lit -> reason:(unit -> lit list) -> proof -> unit
(** Propagate a literal for a reason. This is similar to asserting
the clause [reason => lit], but more lightweight, and in a way
that is backtrackable. *)
val raise_conflict : t -> actions -> lit list -> proof -> 'a val raise_conflict : t -> actions -> lit list -> proof -> 'a
(** Give a conflict clause to the solver *) (** Give a conflict clause to the solver *)
@ -429,6 +436,9 @@ module type SOLVER_INTERNAL = sig
val cc_find : t -> CC.N.t -> CC.N.t val cc_find : t -> CC.N.t -> CC.N.t
(** Find representative of the node *) (** Find representative of the node *)
val cc_are_equal : t -> term -> term -> bool
(** Are these two terms equal in the congruence closure? *)
val cc_merge : t -> actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit val cc_merge : t -> actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit
(** Merge these two nodes in the congruence closure, given this explanation. (** Merge these two nodes in the congruence closure, given this explanation.
It must be a theory tautology that [expl ==> n1 = n2]. It must be a theory tautology that [expl ==> n1 = n2].