Module Atom

module Atom: sig  end

Atomic predicates.
Author(s): Harald Ruess

type atom =

`\|`	`TT`
`\|`	`Equal of Term.t * Term.t`
`\|`	`Diseq of Term.t * Term.t`
`\|`	`Nonneg of Term.t`
`\|`	`Pos of Term.t`
`\|`	`FF`

An atomic predicate is either

one of the constants True or False,
an equality a = b,
a disequality a <> b, or
an arithmetic inequality a > 0 or a >= 0.

type t

For each atom, a unique index is maintained. That is,

Atom.equala b holds iff i = j with i, j the indices associated with a, b, respectively.

val atom_of : t -> atom

Retrieve the atom from an atom-index pair.

Parameters:

? : t

val index_of : t -> int

Retrieve the unique index from an atom-index pair.

Parameters:

? : t

val of_atom : atom -> t

Construct an atom-index pair with unique index from an atom.

Parameters:

a : atom

val of_index : int -> t

of_index n returns an atom-index pair of index n if such and atom-index pair has been created since the last Tools.do_at_reset. Otherwise, the result is undefined.

Parameters:

i : int

val mk_true : t

Atom-index pair for representing the true atom.

val mk_false : t

Atom-index pair for representing the false atom.

val mk_equal : Term.t * Term.t -> t

The atom-index pair mk_equal (a, b) represents the equality a = b.

Parameters:

(a,b) : Term.t * Term.t

val mk_diseq : Term.t * Term.t -> t

The atom-index pair mk_diseq (a, b) represents the disequality a <> b.

Parameters:

(a,b) : Term.t * Term.t

val mk_nonneg : Term.t -> t

The atom-index pair mk_nonneg a represents the nonnegativity constraint a >= 0.

Parameters:

a : Term.t

val mk_pos : Term.t -> t

The atom-index pair mk_nonneg a represents the positivity constraint a > 0.

Parameters:

a : Term.t

val is_true : t -> bool

is_true atm holds iff atm represents the true atom.

Parameters:

? : t

val is_false : t -> bool

is_false atm holds iff atm represents the false atom.

Parameters:

? : t

val equal : t -> t -> bool

Equality on atoms.

Parameters:

?	:	`t`
?	:	`t`

val is_negatable : t -> bool

is_negatable atm is always true. Not deleted, because it is called by SAT solver

Parameters:

() : t

val negate : (Term.t -> Term.t) -> t -> t

negate f atm ...

Parameters:

mk_neg	:	`Term.t -> Term.t`
?	:	`t`

val vars_of : t -> Term.Var.Set.t

vars_of atm collects all variables in atm.

Parameters:

? : t

val is_connected : t -> t -> bool

is_connected atm1 atm2 holds iff vars_of atm1 and vars_of atm2 not disjoint.

Parameters:

?	:	`t`
?	:	`t`

val pp : t Pretty.printer

Pretty-printing an atom.

Parameters:

fmt	:	`Format.formatter`
(atm,())	:	`atom * 'a`

val to_string : t -> string

Pretty-printing an atom to a string.

Parameters:

a : t

module Set: sig  end

Sets of atoms.

module Map: sig  end

Maplets with atoms as keys.