Module Types.SAtom

module SAtom: sig .. end

Interface for the conjunctions of atoms seen as sets of atoms. This module is mutually recursive with Atom because of the if-then-else

include Set.S

Attention: the function add performs some simple semantic simplifications, so it is advised to not use this module for real sets of atoms.

val equal : t -> t -> bool

val hash : t -> int

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

Apply the substitution given in argument to the conjunction

val variables : t -> Variable.Set.t

returns the existential variables of the given conjunction

val variables_proc : t -> Variable.Set.t

same as variables but only return skolemized variables of the form #i

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

prints a conjunction

val print_inline : Format.formatter -> t -> unit

prints a conjunction on a signle line