Module Types.Atom

module Atom: sig .. end

Interface for the atoms of the language

type t = 
| True (*

the atom false

| False (*

the atom true

| Comp of Types.Term.t * Types.op_comp * Types.Term.t (*

application of builtin predicate (=, <>, <, <=)

| Ite of Types.SAtom.t * t * t (*

if-then-else atoms that comme from computing pre-images


the type of atoms

val compare : t -> t -> int

compares two atoms. The order defined by this function is important as it gives a way to efficiently find relevant substitutions in the module Instantiation

val trivial_is_implied : t -> t -> int

return true if it can be immediately said that the atom in the first argument implies the second

val neg : t -> t

returns the negation of the atom

val hash : t -> int
val equal : t -> t -> bool
val subst : Variable.subst -> t -> t

Apply the substitution given in argument to the atom. This function is not very efficient in practice, prefer the use of ArrayAtom.apply_sust when possible.

val has_var : Variable.t -> t -> bool

returns true if the atom contains the variable given in argument

val has_vars : Variable.t list -> t -> bool

returns true if the atom contains one of the variable given in argument

val variables : t -> Variable.Set.t

returns the existential variables of the given atom

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 an atom