Parameter Make.D

type t

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.

val equal : t -> t -> bool

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.

val pp : t Fmt.t

Pretty-printer for domains.

exception Inconsistent of Explanation.t

Exception raised by intersect when an inconsistency is detected.

val filter_ty : Ty.t -> bool

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

type constant = NF.constant

The type of constant values.

val constant : constant -> t

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

val unknown : Ty.t -> t

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

  • raises Invalid_argument

    if filter_ty ty does not hold.

val add_explanation : ex:Explanation.t -> t -> t

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.

val intersect : t -> t -> t

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).

val add_offset : t -> constant -> t

add_offset ofs d adds the offset ofs to domain d.

val sub_offset : t -> constant -> t

sub_offset ofs d removes the offset ofs from domain d.

type var = NF.Composite.t

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

type atom = NF.Atom.t

The type of atomic variables this domain applies to.

val map_domain : (atom -> t) -> var -> t

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