Union-of-intervals over integers.
include Intervals_intf.EuclideanRing
with type explanation := Explanation.t
and type value := Z.t
and type 'a union = 'a unionGiven 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 'a union = 'a unionIntervals over the value type.
The following functions are used to create unions.
val of_interval : ?ex:Explanation.t -> bnd Intervals_intf.interval -> tBuild 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 ->
tof_bounds ?ex lb ub is a shortcut for of_interval ?ex @@ Interval.of_bounds lb ub
val of_complement :
?ex:Explanation.t ->
bnd Intervals_intf.interval ->
(t, Explanation.t) Intervals_intf.kindBuild 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.
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.tlower_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.tupper_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) optionIf 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.
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 Seq.tConvert 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 -> unititer 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 -> 'afold 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.
The following functions are used to compare intervals in the current context.
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.
equal u1 u2 returns true if u1 is equal to u2 in the current context. equal ignores all explanations.
val add_explanation : ex:Explanation.t -> t -> tadd_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.kindintersect u1 u2 computes the intersection of u1 and u2.
The resulting intersection is valid in all models.
The following functions can compute the image of an union by monotone function on bounds.
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.
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.kindpartial_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.kindpartial_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.
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.
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 : setempty_set represents an empty set of intervals.
val interval_set : bnd Intervals_intf.interval -> setinterval_set i represents the interval i as a set.
union_set f1 f2 computes the union of the sets of intervals represented by f1 and f2.
val map_set :
(bnd Intervals_intf.interval -> bnd Intervals_intf.interval) ->
set ->
setmap_set f s applies the function f to all the intervals in s.
val of_set_checked : set -> (t, Explanation.t) Intervals_intf.kindConverts 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.
Converts a set to an union, assuming that it is nonempty in the current context.
val map_to_set : ('a Intervals_intf.interval -> set) -> 'a union -> setmap_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 -> setmap_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.
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).
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.
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.
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.
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.
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.
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.
scale v u evaluates to \{ v \times x \mid x \in S \} when u evaluates to S.
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 ediv : ?div0:bnd Intervals_intf.interval -> t -> t -> tediv 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.
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).
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]).
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.
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.
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.