Make (alt-ergo-lib.AltErgoLib.Domains.Make)

Parameters

module NF : Domains_intf.NormalForm

module D : 
  Domains_intf.Domain
    with type var = NF.Composite.t
     and type atom = NF.Atom.t
     and type constant = NF.constant

module W : Domains_intf.OrderedType

Signature

include Uf.GlobalDomain

type t

The type of global domains.

val pp : t Fmt.t

Pretty-printer for global domains.

type Uf.id +=

| Id : t Uf.id
(*
Unique identifier for this module. Used for dispatch by the union-find.
Warning: This identifier must be unique; do not re-export the Id from another module (e.g. through include).
*)

val empty : t

The empty domain.

val filter_ty : Ty.t -> bool

Limit the type of terms that this module cares about. Only substitutions of representatives for which filter_ty (type_info r) holds will be propagated to this module.

val init : Uf.r -> t -> t

init r t is called when the representative r is added to the union-find, if it has a type that matches filter_ty.

Note: unlike Relation.add, this function is called even for "dynamic" representatives added by X.make or AC normalization.

exception Inconsistent of Explanation.t

Raised by subst below when an inconsistency is found while merging the domains.

val subst : ex:Explanation.t -> Uf.r -> Uf.r -> t -> t

subst ~ex rr nrr t is called when the representatives rr and nrr are merged with explanation ex. nrr is the new representative; rr should no longer be tracked and the intersection of domains should be associated with nrr.

The explanation ex justifies the equality rr = nrr.

raises Inconsistent
if the domains for rr and nrr are incompatible.

val get : AltErgoLib.Domains_intf.X.r -> t -> D.t

get r t returns the domain associated with semantic value r.

val watch : W.t -> AltErgoLib.Domains_intf.X.r -> t -> t

watch w r t associated the watch w with the domain of semantic value r. The watch w is triggered whenever the domain associated with r changes, and is preserved across substitutions (i.e. if r becomes nr, w will be transfered to nr).

Note: The watch w is also immediately triggered for a first propagation.

val unwatch : W.t -> t -> t

unwatch w removes w from all watch lists. It will no longer be triggered.

Note: If w has already been triggered, it is not removed from the triggered list.

val needs_propagation : t -> bool

Returns true if the domains needs propagation, i.e. if any variable's domain has changed.

val variables : t -> NF.Atom.Set.t

Returns the set of atomic variables that are currently being tracked.

val parents : t -> NF.Composite.Set.t NF.Atom.Map.t

Returns a map from atomic variables to all the composite variables that contain them and are currently being tracked.

module Ephemeral : sig ... end

val edit : 
  events:(NF.Atom.t, NF.Composite.t, W.t) Domains_intf.events ->
  t ->
  Ephemeral.t

edit ~events t returns an ephemeral copy of the domains for edition.

The events argument is used to notify the caller about domain changes and watches being triggered.

Note: Any domain that has changed or watches that have been triggered through the persistent API (e.g. due to substitutions) are immediately notified through the appropriare events callback.

val snapshot : Ephemeral.t -> t

Converts back an ephemeral domain into a persistent one.