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