CC (sidekick.Sidekick

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

type bitfield

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.

type t

The congruence closure object. It contains a fair amount of state and is mutable and backtrackable.

Accessors

val term_store : t -> Sidekick_core.Term.store

val proof_tracer : t -> Sidekick_proof.Tracer.t

val stat : t -> Sidekick_util.Stat.t

val find : t -> e_node -> repr

Current representative

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

val allocate_bitfield : t -> descr:string -> bitfield

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).

val get_bitfield : t -> bitfield -> E_node.t -> bool

Access the bit field of the given e_node

val set_bitfield : t -> bitfield -> bool -> E_node.t -> unit

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

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.

type ev_on_conflict = {

cc : t;
th : bool;
c : Sidekick_core.Lit.t list;

}

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.

Misc

val n_true : t -> E_node.t

Node for true

val n_false : t -> E_node.t

Node for false

val n_bool : t -> bool -> E_node.t

Node for either true or false

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.

raises E_node.t_found
if the Term.t is not already add-ed.

val add_iter : t -> Sidekick_core.Term.t Iter.t -> unit

Add a sequence of terms to the congruence closure

val all_classes : t -> repr Iter.t

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

val merge : t -> E_node.t -> E_node.t -> Expl.t -> unit

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

Main API

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.

val get_model : t -> E_node.t Iter.t Iter.t

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

module Make (_ : ARG) : BUILD

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.

parameter term_store
used to be able to create new terms. All terms interacting with this congruence closure must belong in this term state as well.

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