Module Intervals.Int

Union-of-intervals over integers.

include Intervals_intf.EuclideanRing with type explanation := Explanation.t and type value := Z.t and type 'a union = 'a union

Given an explanation e (see Intervals_intf.Explanations), we say that an interval I is forbidden for a variable x by e if M(x) is never in I when M is a model such that M(e) is true, i.e. if the following implication holds:

\forall M, M(e) \Rightarrow M(x) \not\in I

Given a current context C (a set of explanations) and an implicit variable x, we say that an interval I is forbidden if it is forbidden by an union of explanations in C, and that it is allowed otherwise.

It is always sound to weaken a forbidden interval interval: if M(e_1) \Rightarrow M(e_2) and I is forbidden by e_2, it is also forbidden by e_1.

(Note that in terms of explanations, this means adding more terms in the explanation, since Explanation.empty is true in all contexts and since Explanation.union e1 e2 evaluates to M(e_1) \wedge M(e_2).)

The union type below internally keeps track of both allowed and forbidden intervals, where each forbidden interval is annotated by a specific explanation (true in the current context) that forbids it, but the functions in this module provide abstractions to deal with the unions without having to worry about explanations (and forbidden intervals) directly.

In order to avoid having to worry about variables while reasoning about intervals, we define a contextual evaluation function for unions (and set of intervals); the evaluation of an allowed interval I is always I in all contexts, and the evaluation of a forbidden interval I is I in contexts where the associated explanation does not hold, and the empty set otherwise (in particular, it is the empty set in the current context).

Note that the evaluation of a forbidden interval is a subset of the interval in any context.

type bnd

The type of bounds.

type 'a union = 'a union
type t = bnd union

The type of unions.

module Interval : Intervals_intf.Interval with type value = Z.t and type bnd = bnd

Intervals over the value type.

val pp : t Fmt.t

Pretty-printer for unions.

Creation

The following functions are used to create unions.

val of_interval : ?ex:Explanation.t -> bnd Intervals_intf.interval -> t

Build an union from an interval.

of_interval ?ex:None i evaluates to i in all contexts.

of_interval ~ex i evaluates to i in contexts where ex holds (including the current context) and to the full set otherwise.

val of_bounds : ?ex:Explanation.t -> Z.t Intervals_intf.bound -> Z.t Intervals_intf.bound -> t

of_bounds ?ex lb ub is a shortcut for of_interval ?ex @@ Interval.of_bounds lb ub

Build an union from the complement of an interval.

The explanation, if provided, justifies that the value is not in the interval; the resulting union evaluates to the complement of the interval in any model where the explanation holds, and to the full set otherwise.

If the provided interval covers the full domain, the resulting union is empty and an Empty kind is returned; otherwise, the resulting union is NonEmpty.

Inspection

The following functions are used to inspect the global bounds of an union of intervals.

val lower_bound : t -> Z.t Intervals_intf.bound * Explanation.t

lower_bound u returns a pair lb, ex of a global lower bound and an explanation that justifies that this lower bound is valid.

val upper_bound : t -> Z.t Intervals_intf.bound * Explanation.t

upper_bound u returns a pair lb, ex of a global upper bound and an explanation that justifies that this upper bound is valid.

val value_opt : t -> (Z.t * Explanation.t) option

If u is a singleton in the current context, value_opt u returns a pair (v, ex) where v is the value of u in the current context and ex justifies v being both a lower and upper bound.

This is more efficient than checking if the values returned by lower_bound and upper_bound are equal.

Iteration

The following functions are used to iterate over the maximal disjoint intervals composing the union in the current context.

val to_seq : t -> bnd Intervals_intf.interval Stdlib.Seq.t

Convert an union of interval to a sequence of maximal disjoint and non-adjacent intervals.

Warning: The sequence of intervals is only valid in the current context.

val iter : (bnd Intervals_intf.interval -> unit) -> t -> unit

iter f u calls f on each of the maximal disjoint and non-adjacent intervals that make up the union u in the current context.

val fold : ('a -> bnd Intervals_intf.interval -> 'a) -> 'a -> t -> 'a

fold f acc u folds f over each of the maximal disjoint and non-adjacent intervals that make up the union u in the current context.

Comparison

The following functions are used to compare intervals in the current context.

val subset : ?strict:bool -> t -> t -> bool

subset ?strict u1 u2 returns true if u1 is a subset of u2 in the current context. subset ignores all explanations.

If set, the strict flag (false by default) checks for strict inclusion.

val equal : t -> t -> bool

equal u1 u2 returns true if u1 is equal to u2 in the current context. equal ignores all explanations.

Set manipulation

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

add_explanation ~ex u adds the explanation ex to the union u.

More precisely: add_explanation ~ex u is equivalent to u in models where ex holds, and is Interval.full otherwise.

val intersect : t -> t -> (t, Explanation.t) Intervals_intf.kind

intersect u1 u2 computes the intersection of u1 and u2.

The resulting intersection is valid in all models.

Image by monotone functions

The following functions can compute the image of an union by monotone function on bounds.

val map_strict_inc : ('a -> bnd) -> 'a union -> t

map_strict_inc f u computes the image of u by the strictly increasing function f.

This function is very efficient and should be used when possible.

val map_strict_dec : ('a -> bnd) -> 'a union -> t

map_strict_dec f u computes the image of u by the strictly decreasing function f.

This function is very efficient and should be used when possible.

val partial_map_inc : ('a -> bnd) -> ('a -> bnd) -> 'a union -> (t, Explanation.t) Intervals_intf.kind

partial_map_inc f_lb f_ub u computes the image of u by a partial (weakly) increasing function f.

f is represented by the pair (f_lb, f_ub) of functions that are such that for any x, f_lb x = f x = f_ub x if x is in the domain of f, and f_ub x < f_lb x otherwise.

Warning: The functions f_lb and f_ub must themselve be (weakly) increasing. Moreover, the inequality f_ub x <= f_lb x must hold everywhere; if f_lb and f_ub are imprecise approximations of f, use approx_map_inc_to_set instead.

val partial_map_dec : ('a -> bnd) -> ('a -> bnd) -> 'a union -> (t, Explanation.t) Intervals_intf.kind

partial_map_dec f_lb f_ub u computes the image of u by a partial (weakly) decreasing function f.

f is represented by the pair (f_lb, f_ub) of functions that are such that for any x, f_lb x = f x = f_ub x if x is in the domain of f, and f_ub x < f_lb x otherwise.

Warning: The functions f_lb and f_ub must themselve be (weakly) decreasing. Moreover, the inequality f_ub x <= f_lb x must hold everywhere; if f_lb and f_ub are imprecise approximations of f, use approx_map_dec_to_set instead.

Image by arbitrary functions

When computing the image of an union by non-monotone functions and multi-variate functions, work needs to be done to convert intermediate results into a normalized form of disjoint intervals (because applying the function to initially disjoint intervals can create arbitrary unions).

In such cases, the following family of to_set functions should be used. The use the set type to represent intermediate results, which can be converted back to an union using the of_set family of functions as needed.

type set

The set type represents a (possibly empty) set of intervals.

Unlike an union, it is not normalized: it is an intermediate type not intended to be manipulated directly, except in the process of building an union. Use the of_set family of functions to convert it to an union as needed.

val empty_set : set

empty_set represents an empty set of intervals.

val interval_set : bnd Intervals_intf.interval -> set

interval_set i represents the interval i as a set.

val union_set : set -> set -> set

union_set f1 f2 computes the union of the sets of intervals represented by f1 and f2.

map_set f s applies the function f to all the intervals in s.

val of_set_checked : set -> (t, Explanation.t) Intervals_intf.kind

Converts a set to a nonempty union. Returns Empty ex if the set is currently empty, and NonEmpty u otherwise.

If a NonEmpty value is returned, the resulting union is guaranteed to be nonempty in the current context.

val of_set_nonempty : set -> t

Converts a set to an union, assuming that it is nonempty in the current context.

  • raises Invalid_argument

    if the set represents an union that is empty in the current context.

val map_to_set : ('a Intervals_intf.interval -> set) -> 'a union -> set

map_to_set f u computes the image of u by f.

Conceptually, this computes the union of f x for each x in u, although this is not possible to compute when u might not be finite. Instead, we represent f by a function from intervals to sets that must be isotone (i.e. monotone with respect to inclusion):

I_1 \subseteq I_2 \Rightarrow f(I_1) \subseteq f(I_2)

There are no restrictions on f (except that it be isotone), which means that map_to_set needs to call f on currently allowed intervals, but also on some intervals that are currently impossible but would be possible in other contexts (depending on explanations).

When possible, prefer using a more specialized variant of map_to_set that use properties of the function f to avoid certain calls to f.

val map_mon_to_set : ('a Intervals_intf.interval -> set) -> 'a union -> set

map_mon_to_set is a variant of map_to_set when the function f is monotone.

More precisely, we require that for any pair of intervals (i1, i2) the interval hull of f i1 and f i2 is included in the image of the interval hull of i1 and i2 by f.

It is often more convenient to use approx_map_inc_to_set or approx_map_dec_to_set instead, to lift a function on values to a function on unions without going through intervals.

val approx_map_inc_to_set : ('a -> bnd) -> ('a -> bnd) -> 'a union -> set

approx_map_inc_to_set f_lb f_ub u is a variant of map_to_set that is appropriate for (weakly) increasing functions.

The (weakly) increasing function f is represented by a pair (f_lb, f_ub) of functions such that for all x in the domain of f, f_lb x <= f x <= f_ub x (and f_ub x < f_lb x otherwise).

Note that, unlike partial_map_inc, this function can be used with imprecise approximations: we allow f_lb x < f x < f_ub x (this is useful for radicals).

val approx_map_dec_to_set : ('a -> bnd) -> ('a -> bnd) -> 'a union -> set

approx_map_inc_to_set f_lb f_ub u is a variant of map_to_set that is appropriate for (weakly) decreasing functions.

The (weakly) decreasing function f is represented by a pair (f_lb, f_ub) of functions such that for all x in the domain of f, f_lb x <= f x <= f_ub x (and f_ub x < f_lb x otherwise).

Note that, unlike partial_map_dec, this function can be used with imprecise approximations: we allow f_lb x < f x < f_ub x.

val map_inc_to_set : ('a -> bnd) -> 'a union -> set

map_inc_to_set f u is a variant of approx_map_inc_to_set when the underlying function is total and precisely known.

See also map_strict_inc.

Note that strict monotony is not required for map_inc_to_set.

val map_dec_to_set : ('a -> bnd) -> 'a union -> set

map_dec_to_set f u is a variant of approx_map_dec_to_set when the underlying function is total and precisely known.

See also map_strict_dec.

Note that strict monotony is not required for map_dec_to_set.

val trisection_map_to_set : bnd -> t -> (t -> set) -> (unit -> set) -> (t -> set) -> set

trisection_map_to_set v u f_lt f_eq f_gt constructs an union of intervals by combining the image of f_lt on the fragment of u that only contains values strictly less than v, the image of f_gt on the fragment of u that only contains values strictly greater than v, and the image of f_eq if v is contained in u.

It is helpful to build piecewise monotone functions such as multiplication, where trisection around 0 can be used.

Ring interface

val neg : t -> t

neg u evaluates to \{ -x \mid x \in S \} when u evaluates to S.

val add : t -> t -> t

add u1 u2 evaluates to \{ x + y \mid x \in S_1, y \in S_2 \} when u1 evaluates to S_1 and u2 evaluates to S_2.

val sub : t -> t -> t

sub u1 u2 evaluates to \{ x - y \mid x \in S_1, y \in S_2 \} when u1 evaluates to S_1 and u2 evaluates to S_2.

val scale : Z.t -> t -> t

scale v u evaluates to \{ v \times x \mid x \in S \} when u evaluates to S.

  • raises Invalid_argument

    if v is zero.

val mul : t -> t -> t

mul u1 u2 evaluates to \{ x \times y \mid x \in S_1, y \in S_2 \} when u1 evaluates to S_1 and u2 evaluates to S_2.

val pow : int -> t -> t

pow n u evaluates to \{ x^n \mid x \in S \} when u evaluates to S.

  • raises Invalid_argument

    if n is nonpositive.

Euclidean division

val ediv : ?div0:bnd Intervals_intf.interval -> t -> t -> t

ediv u1 u2 computes the image of euclidean division of a value in u1 by a value in u2.

div0 (defaults to the full interval) is used as the image of division by zero.

Bit-vector helpers

These functions are intended for the BV theory. They can only be used with integer intervals. Some of these functions return intervals "of width n", where n is computed from the parameters of the function. This means that the returned interval is contained in the range [0, n)] ([0] inclusive, [n] exclusive).

val lognot : t -> t

Bitwise logical negation. lognot u always returns -u - 1.

val extract : t -> ofs:int -> len:int -> t

extract s i j returns the bits of s from position i to j, inclusive.

Represents the function fun x -> floor(x / 2^i) % 2^(j - i + 1).

Requires 0 <= i <= j and returns an interval of width j - i + 1.

Note: The interval s must be an integer interval, but is allowed to be unbounded (in which case extract s i j returns the full interval [0, 2^(j - i + 1) - 1]).

val bvudiv : size:int -> t -> t -> t

bvudiv sz s t computes an overapproximation of integer division for bit-vectors of width sz as defined in the FixedSizeBitVectors SMT-LIB theory, i.e. where bvudiv n 0 is 2^sz - 1.

s and t must be within the 0, 2^sz - 1 range.

val bvurem : t -> t -> t

bvurem sz s t computes an overapproximation of integer remainder for bit-vectors of width sz as defined in the FixedSizeBitVectors SMT-LIB theory, i.e. where bvurem n 0 is n.

s and t must be within the 0, 2^sz - 1 range.

val bvshl : size:int -> t -> t -> t

shl sz s t computes an overapproximation of the left shift s lsl t, truncating the result to sz bits.

s and t must only contain non-negative integers.

val lshr : t -> t -> t

lshr s t computes an approximation of the logical right shift s lsr t.

Note that the result of logical right shift is independent of bit width.

s and t must only contain non-negative integers.