Sidekick_cc.CC
Main congruence closure signature.
The congruence closure handles the theory QF_UF (uninterpreted function symbols). It is also responsible for theory combination, and provides a general framework for equality reasoning that other theories piggyback on.
For example, the theory of datatypes relies on the congruence closure to do most of the work, and "only" adds injectivity/disjointness/acyclicity lemmas when needed.
Similarly, a theory of arrays would hook into the congruence closure and assert (dis)equalities as needed.
type e_node = E_node.t
A node of the congruence closure
type repr = E_node.t
Node that is currently a representative.
type explanation = Expl.t
A field in the bitfield of this node. This should only be allocated when a theory is initialized.
Bitfields are accessed using preallocated keys. See allocate_bitfield
.
All fields are initially 0, are backtracked automatically, and are merged automatically when classes are merged.
The congruence closure object. It contains a fair amount of state and is mutable and backtrackable.
val term_store : t -> Sidekick_core.Term.store
val proof_tracer : t -> Sidekick_proof.Tracer.t
val stat : t -> Sidekick_util.Stat.t
val add_term : t -> Sidekick_core.Term.t -> e_node
Add the Term.t to the congruence closure, if not present already. Will be backtracked.
val mem_term : t -> Sidekick_core.Term.t -> bool
Returns true
if the Term.t is explicitly present in the congruence closure
Allocate a new e_node field (see E_node.bitfield
).
This field descriptor is henceforth reserved for all nodes in this congruence closure, and can be set using set_bitfield
for each class_ individually. This can be used to efficiently store some metadata on nodes (e.g. "is there a numeric value in the class" or "is there a constructor Term.t in the class").
There may be restrictions on how many distinct fields are allocated for a given congruence closure (e.g. at most Sys.int_size
fields).
Set the bitfield for the e_node. This will be backtracked. See E_node.bitfield
.
type propagation_reason =
unit ->
Sidekick_core.Lit.t list * Sidekick_proof.Pterm.delayed
module Handler_action : sig ... end
Handler Actions
module Result_action : sig ... end
Result Actions.
Events triggered by the congruence closure, to which other plugins can subscribe.
val on_pre_merge :
t ->
(t * E_node.t * E_node.t * Expl.t, Handler_action.or_conflict)
Sidekick_util.Event.t
Events emitted by the congruence closure when something changes.
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)
Sidekick_util.Event.t
Second phase of "on pre merge". This runs after on_pre_merge
and is used by Plugins. 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) Sidekick_util.Event.t
ev_on_post_merge acts n1 n2
is emitted right after n1
and n2
were merged. find cc n1
and find cc n2
will return the same E_node.t.
val on_new_term :
t ->
(t * E_node.t * Sidekick_core.Term.t, Handler_action.t list)
Sidekick_util.Event.t
ev_on_new_term n t
is emitted whenever a new Term.t t
is added to the congruence closure. Its E_node.t is n
.
Event emitted when a conflict occurs in the CC.
th
is true if the explanation for this conflict involves at least one "theory" explanation; i.e. some of the equations participating in the conflict are purely syntactic theories like injectivity of constructors.
val on_conflict : t -> (ev_on_conflict, unit) Sidekick_util.Event.t
ev_on_conflict {th; c}
is emitted when the congruence closure triggers a conflict by asserting the tautology c
.
val on_propagate :
t ->
(t * Sidekick_core.Lit.t * propagation_reason, Handler_action.t list)
Sidekick_util.Event.t
ev_on_propagate Lit.t reason
is emitted whenever reason() => Lit.t
is a propagated lemma. See CC_ACTIONS.propagate
.
val on_is_subterm :
t ->
(t * E_node.t * Sidekick_core.Term.t, Handler_action.t list)
Sidekick_util.Event.t
ev_on_is_subterm n t
is emitted when n
is a subterm of another E_node.t for the first time. t
is the Term.t corresponding to the E_node.t n
. This can be useful for theory combination.
val set_as_lit : t -> E_node.t -> Sidekick_core.Lit.t -> unit
map the given e_node to a literal.
val find_t : t -> Sidekick_core.Term.t -> repr
Current representative of the Term.t.
val add_iter : t -> Sidekick_core.Term.t Iter.t -> unit
Add a sequence of terms to the congruence closure
All current classes. This is costly, only use if there is no other solution
val explain_eq : t -> E_node.t -> E_node.t -> Resolved_expl.t
Explain why the two nodes are equal. Fails if they are not, in an unspecified way.
val explain_expl : t -> Expl.t -> Resolved_expl.t
Transform explanation into an actionable conflict clause
Merge these two nodes given this explanation. It must be a theory tautology that expl ==> n1 = n2
. To be used in theories.
val merge_t :
t ->
Sidekick_core.Term.t ->
Sidekick_core.Term.t ->
Expl.t ->
unit
Shortcut for adding + merging
val assert_eq :
t ->
Sidekick_core.Term.t ->
Sidekick_core.Term.t ->
Expl.t ->
unit
Assert that two terms are equal, using the given explanation.
val assert_lit : t -> Sidekick_core.Lit.t -> unit
Given a literal, assume it in the congruence closure and propagate its consequences. Will be backtracked.
Useful for the theory combination or the SAT solver's functor
val assert_lits : t -> Sidekick_core.Lit.t Iter.t -> unit
Addition of many literals
val check : t -> Result_action.or_conflict
Perform all pending operations done via assert_eq
, assert_lit
, etc. Will use the actions
to propagate literals, declare conflicts, etc.
val push_level : t -> unit
Push backtracking level
val pop_levels : t -> int -> unit
Restore to state n
calls to push_level
earlier. Used during backtracking.
get all the equivalence classes so they can be merged in the model
type view_as_cc =
Sidekick_core.Term.t ->
(Sidekick_core.Const.t, Sidekick_core.Term.t, Sidekick_core.Term.t list)
Sidekick_core.CC_view.t
module type ARG = sig ... end
Arguments to a congruence closure's implementation
module type BUILD = sig ... end
val create :
(module ARG) ->
?stat:Sidekick_util.Stat.t ->
?size:[ `Small | `Big ] ->
Sidekick_core.Term.store ->
Sidekick_proof.Tracer.t ->
t
Create a new congruence closure.
val create_default :
?stat:Sidekick_util.Stat.t ->
?size:[ `Small | `Big ] ->
Sidekick_core.Term.store ->
Sidekick_proof.Tracer.t ->
t
Same as create
but with the default CC view