module Variable:sig..end
Variables of the parameterized domain
typet =Hstring.t
the type of variables
typesubst =(t * t) list
the type of variable substitutions
module Set:Set.Swith type elt = t
set of variables
val compare : t -> t -> int
val compare_list : t list -> t list -> intval procs : t listpredefinied list of skolem variables #1, #2, #3, ... Their number is
controlled by Options.max_proc
val proc_vars_int : int list
val alphas : t list
val freshs : t list
val number : t -> int
val is_proc : t -> boolreturns true if the variable is a skolem process #i
val build_subst : t list -> t list -> substconstructs a variable substitution
val subst : subst -> t -> tapply a variable substitution to a variable
val is_subst_identity : subst -> boolreturns true if the substitution is the identity function
val well_formed_subst : subst -> boolreturns true if the substitution is well formed, i.e. bindings are unique
and different elements of the domain are associated to different elements of
the codomain.
val all_permutations : 'a list -> 'a list -> ('a * 'a) list listall_permutations l1 l2 returns all possible substitutions from
l1 to l2 assuming that the variables of both lists are distinct.
l2 must be longer than (or the same size as) l1
val all_instantiations : t list -> t list -> subst listsame as Variable.all_permutations but does not assume elements of l1 to be
distinct. l1 can be longer than l2.
val all_arrangements : int -> t list -> t list list
val all_arrangements_arity : Hstring.t -> t list -> t list list
val permutations_missing : t list -> t list -> subst list
val extra_vars : t list -> t list -> t list
val extra_procs : t list -> t list -> t list
val append_extra_procs : t list -> t list -> t list
val give_procs : int -> t listval print : Format.formatter -> t -> unit
val print_vars : Format.formatter -> t list -> unit
val print_subst : Format.formatter -> subst -> unit