Module Sat.Domain

A subset of the integers.

type t

Internally, represented as a sorted, non-adjacent list of intervals.

val of_interval : ?lb:int -> ?ub:int -> unit -> t

An integer interval from lower and upper bounds.

  • with both: \{ x \mid \mathtt{lb} \leq x \leq \mathtt{ub} \} ,
  • with lb only: \{ x \mid \mathtt{lb} \leq x \} ,
  • with ub only: \{ x \mid x \leq \mathtt{ub} \} , and
  • with neither or lb >= ub: \emptyset .
val of_intervals : (int * int) list -> t

A union of intervals from (lb, ub) pairs.

val of_values : int list -> t

One of a set of values.

val (@) : t -> t -> t

Union of two intervals.

val union : t list -> t

Union of a list of intervals.

val to_string : t -> string

Return a string representing the domain.

val pp : Stdlib.Format.formatter -> t -> unit

Pretty-printer for domains.