module ArrayAtom:`sig`

..`end`

Interface for the conjunctions of atoms seen as arrays of atoms. This is usefull for efficiently applying substitutions

type`t =`

`Types.Atom.t array`

values of this type should be constructed with the invariant that the array must be sorted at all times

`val equal : ``t -> t -> bool`

`val hash : ``t -> int`

`val subset : ``t -> t -> bool`

`subset a b`

returns `true`

if the elements of `a`

are a subsets of the
elements contained in `b`

. `a`

and `b`

must be sorted with the order
defined by `Types.Atom.compare`

`val trivial_is_implied : ``t -> t -> bool`

`val of_satom : ``Types.SAtom.t -> t`

transforms a conjunction if the form of a set of atoms to an equivalent representation with an array

`val to_satom : ``t -> Types.SAtom.t`

returns the set of atoms corresponding to the conjuntion encoded in the array

`val union : ``t -> t -> t`

in fact concatenation, equivalent to taking the conjunctions of two conjunctinos

`val apply_subst : ``Variable.subst -> t -> t`

Efficient application of substitution

`val nb_diff : ``t -> t -> int`

returns the number of differences, i.e. atoms that are in the first argument but not the second. This is a measure of "difference" used for heuristics

`val compare_nb_diff : ``t -> t -> t -> int`

`compare_nb_diff a t1 t2`

: based on the previous measure, this compares
the "level" of difference with `a`

`val compare_nb_common : ``t -> t -> t -> int`

`compare_nb_common a t1 t2`

: compares the "level of proximity" with `a`

.
This is also used for heuristics

`val diff : ``t -> t -> t`

array form of set difference

`val alpha : ``t -> Variable.t list -> Variable.t list * t`

alpha renaming of process variables

`val print : ``Format.formatter -> t -> unit`

prints the conjunction corresponding to the array of atoms