Module Libabsolute.Dom

This module defines the different kinds of definition domains of variables

type t =
  1. | Finite of Q.t * Q.t
    (*

    [a;b]

    *)
  2. | Minf of Q.t
    (*

    ]-oo; a]

    *)
  3. | Inf of Q.t
    (*

    [a; +oo[

    *)
  4. | Set of Q.t list
    (*

    {x1; x2; ...; xn}

    *)
  5. | Top
    (*

    ]-oo; +oo[

    *)

main type

Constructors

val interval : Q.t -> Q.t -> t

[a;b]

val of_ints : int -> int -> t
val of_floats : float -> float -> t
val inf : Q.t -> t

semi-open interval : [x;+oo[

val set : Q.t list -> t

finite sets of values {x1; x2; ...; xn}

val minf : Q.t -> t

semi-open interval : ]-oo;x]

val top : t

]-oo;+oo[

Predicates

val belong : Q.t -> t -> bool

checks if a given rational belongs to a domain

val is_bounded : t -> bool

Operations

Given a variable name v and a domain d, builds the weakest constraint that v should respect to be in d.

val to_constraint : string -> t -> Constraint.t

Given a variable name v and a domain d, builds the weakest constraint that v should respect to be in d.

Printing

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

printer

val to_string : t -> string

Conversion to a string