Module Types.ArrayAtom (.ml)

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

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