Union (alt-ergo-lib.AltErgoLib.Intervals

Parameters

module OT : Intervals_intf.OrderedType

Signature

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 = OT.t

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 = OT.finite 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 -> 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 ->
  OT.finite Intervals_intf.bound ->
  OT.finite Intervals_intf.bound ->
  t

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

val of_complement : 
  ?ex:explanation ->
  bnd Intervals_intf.interval ->
  (t, explanation) Intervals_intf.kind

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 -> OT.finite Intervals_intf.bound * explanation

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 -> OT.finite Intervals_intf.bound * explanation

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 -> (OT.finite * explanation) 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

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

val map_set : 
  (bnd Intervals_intf.interval -> bnd Intervals_intf.interval) ->
  set ->
  set

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

val of_set_checked : set -> (t, explanation) 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.