module ArrayAtom:sig..end
Interface for the conjunctions of atoms seen as arrays of atoms. This is usefull for efficiently applying substitutions
typet =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 -> boolsubset 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 -> ttransforms a conjunction if the form of a set of atoms to an equivalent representation with an array
val to_satom : t -> Types.SAtom.treturns the set of atoms corresponding to the conjuntion encoded in the array
val union : t -> t -> tin fact concatenation, equivalent to taking the conjunctions of two conjunctinos
val apply_subst : Variable.subst -> t -> tEfficient application of substitution
val nb_diff : t -> t -> intreturns 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 -> intcompare_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 -> intcompare_nb_common a t1 t2: compares the "level of proximity" with a.
This is also used for heuristics
val diff : t -> t -> tarray form of set difference
val alpha : t -> Variable.t list -> Variable.t list * talpha renaming of process variables
val print : Format.formatter -> t -> unitprints the conjunction corresponding to the array of atoms