package alt-ergo-lib

The type of domains for a single value.

This is an abstract type that is instanciated by the theory. Note that it is expected that this type can carry explanations.

equal d1 d2 returns true if the domains d1 and d2 are identical. Explanations should not be taken into consideration, i.e. two domains with different explanations but identical semantics content should compare equal.

Pretty-printer for domains.

Exception raised by intersect when an inconsistency is detected.

Filter for the types of values this domain can be attached to.

The type of constant values.

constant c returns the singleton domain \{ c \}.

unknown ty returns a full domain for values of type t.

• raises Invalid_argument

  if filter_ty ty does not hold.

add_explanation ~ex d adds the justification ex to the domain d. The returned domain is identical to the domain of d, only the justifications are changed.

intersect d1 d2 returns a new domain d that subsumes both d1 and d2. Any explanation justifying that d1 and d2 apply to the same value must have been added to d1 and d2.

• raises Inconsistent

  if d1 and d2 are not compatible (the intersection would be empty).

add_offset ofs d adds the offset ofs to domain d.

sub_offset ofs d removes the offset ofs from domain d.

The type of (composite) variable this domain applies to.

The type of atomic variables this domain applies to.

map_domain f c constructs a domain for a composite variable c from a function f that returns the domain of an atom.