Interval Reasoning

This library provides several abstract domains for interval reasoning over integer and real numbers. We aim to be general enough to be reused across fields:

• Constraint programming: Enforce bound(Z) and bound(R) consistencies on interval domains (see e.g. Choi et al. 2006).
• Abstract interpretation: Provide interval abstractions of integer and real numbers, including forward and backward interval arithmetics (see e.g. Cousot, 2021).
• Conflict-free replicated data type: Provide simple anonymous state-based CRDTs with LB and UB.
• Asynchronous fixpoint iterations: Provide lock-free join and meet operations, compatible with execution on GPU hardware (see Talbot et al., 2022).

Abstract Universes

We propose abstractions of the universe of discourse of integers $\mathbb{Z}$ and real numbers $\mathbb{R}$. Let $\mathbb{A}$ be either $\mathbb{Z}$ or $\mathbb{R}$. The following abstractions are approximating any subset of the universe of discourse:

• Lower bound abstract universe: LB approximates a set $S \subseteq \mathbb{A}$ by taking its lower bound $\mathit{min}~S$ if it is a bounded set, and $-\infty$ otherwise.
• Upper bound abstract universe: UB approximates a set $S \subseteq \mathbb{A}$ by taking its upper bound $\mathit{max}~S$ if it is a bounded set, and $\infty$ otherwise.
• Boolean abstract universes: LB<bool> is a two-elements lattice with the top element to false and bottom to true. Dually, we have UB<bool> where top is true and bottom is false.
• Integer interval abstract universe: ZInterval approximates the lower and upper bounds of a set $S \subseteq \mathbb{Z}$.
• Floating-point interval abstract universe: FInterval approximates the lower and upper bounds of a set $S \subseteq \mathbb{R}$.

We represent infinities ${-\infty, \infty}$ using the minimum and maximum representable values on the underlying arithmetic type: for integers type I we rely on std::numeric_limits<I>::min() and std::numeric_limits<I>::max(), and for floating-point type F we rely on -std::numeric_limits<F>::infinity() and std::numeric_limits<F>::infinity().

Lattice Operations

We have a unified interface for standard lattice operations. Let L be one of the abstract universes above.

Operation	Mathematical notation	Programming notation
Bottom	$\bot$	L::bot()
Top	$\top$	L::top() or default constructor L()
Partial order	$a \leq b$	a.leq(b)
Strict partial order	$a < b$	a.lt(b)
Meet	$a \sqcap b$	meet(a,b) or a.meet(b) (in-place)
Join	$a \sqcup b$	join(a,b) or a.join(b) (in-place)

The following operations are mostly there for optimization purposes, but could be easily recovered from the previous lattice operations.

Operation	Mathematical notation	Programming notation
Equality	$a = b$	a == b
Disequality	$a \neq b$	a != b
Meet bottom	$a \sqcap \bot$	a.meet_bot() (in-place)
Join top	$a \sqcup \top$	a.join_top() (in-place)
Bottom test	$a = \bot$	a.is_bot()
Top test	$a = \top$	a.is_top()

Interval Lattice

In this library, the bottom element of the interval abstract universe denotes the equivalence class of all empty intervals $\set{[\ell,u] | \ell > u }$, the function is_bot is true on all such intervals. The lattice operations are defined in the following table.

Operation	Definition	Programming notation
$\textnormal{isbot}([\ell, u])$	$\ell > u \lor \ell = \infty \lor u = -\infty$	a.is_bot()
$[\ell, u] = [\ell', u']$	$(\textnormal{isbot}([\ell, u]) \land \textnormal{isbot}([\ell', u'])) \lor (\ell = \ell' \land u = u')$	a.eq(b)
$[\ell, u] \leq [\ell', u']$	$\textnormal{isbot}([\ell, u]) \lor (\ell \geq \ell' \land u \leq u')$	a.leq(b)
$a < b$	$a \leq b \land \lnot (a = b)$	a.lt(b)
$[\ell, u] \sqcap [\ell', u']$	$[\max(\ell, \ell'), \min(u,u')]$	meet(a,b) or a.meet(b) (in-place)
$a \sqcup b$	$\textnormal{join}(a,b)$ (see below)	join(a,b) or a.join(b) (in-place)

With the join defined as:

$$\textnormal{join}([\ell, u], [\ell', u']) \triangleq \begin{cases} [\ell, u] &\text{if } \textnormal{isbot}([\ell', u']) \\\ [\ell', u'] &\text{if } \textnormal{isbot}([\ell, u]) \\\ [\min(\ell, \ell'), \max(u, u')] & \text{otherwise} \end{cases}$$

The lattice operations must take care of the cases where the arguments are in the bottom equivalence class. If the user is sure none of the arguments is bottom, we provide more efficient versions named *_nobot (e.g. join_nobot) which simplifies the definition above by ignoring the bottom cases.

ZInterval: Abstract Operations

Also known as abstract transformers in the field of abstract interpretation. In constraint programming, those operations can be used to design propagators, see below.

Note: To project the interval of an expression, e.g. y + z, initialize the result variable to top (e.g. ZInterval<int> x;) and call the forward operator on it: x.add(y,z).

In the following, we let x,y,z be integer intervals of type ZInterval.

Operation	Constraint	Forward operator	Left backward operator	Right backward operator
Identity	$x = y$	x.meet(y)	y.meet(x)	n/a
Negation	$x = \mathord{-}y$	x.neg(y)	y.neg(x)	n/a
Addition	$x = y + z$	x.add(y,z)	y.sub(x,z)	z.sub(x,y)
Subtraction	$x = y - z$	x.sub(y,z)	y.add(x,z)	z.sub(y,x)
Multiplication	$x = y * z$	x.mul(y, z)	y.mul_back(x,z)	z.mul_back(x,y)
Floor division	$x = \textnormal{fdiv}(y,z)$	x.fdiv(y, z)1	y.fdiv_num(x, z)1	z.fdiv_den(x,y)
Ceiling division	$x = \textnormal{cdiv}(y,z)$	x.cdiv(y, z)1	y.cdiv_num(x, z)1	z.cdiv_den(x,y)
Truncated division	$x = \textnormal{tdiv}(y,z)$	x.tdiv(y, z)1	y.tdiv_num(x, z)1	z.tdiv_den(x,y)
Euclidean division	$x = \textnormal{ediv}(y,z)$	x.ediv(y, z)1	y.ediv_num(x, z)1	z.ediv_den(x,y)
Maximum	$x = \textnormal{max}(y, z)$	x.max(y, z)	y.max_back(x,z)	z.max_back(x,y)
Minimum	$x = \textnormal{min}(y, z)$	x.min(y, z)	y.min_back(x,z)	z.min_back(x,y)
Reified Equality	$x = (y = z)$	x.req(y, z)2	y.req_back(x,z)2	z.req_back(x,y)2
Reified Inequality	$x = (y \leq z)$	x.rleq(y, z)2	y.rleq_lback(x,z)2	z.rleq_rback(x,y)2

Semantics of Division Operators

Let $\frac{.}{.}$ be the division over the real numbers, $\lfloor . \rfloor \in \mathbb{R} \to \mathbb{Z}$ be the function rounding downwards a real number, and $\lceil . \rceil \in \mathbb{R} \to \mathbb{Z}$ be the function rounding upwards a real number.

• Semantics of floor division

$$x = \textnormal{fdiv}(y,z) \Leftrightarrow x = \lfloor \frac{y}{z} \rfloor$$

• Semantics of ceiling division

$$x = \textnormal{cdiv}(y,z) \Leftrightarrow x = \lceil \frac{y}{z} \rceil$$

• Semantics of truncated division

$$x = \textnormal{tdiv}(y,z) \Leftrightarrow x=\begin{cases} \lfloor\frac{y}{z}\rfloor&\text{if }\frac{y}{z}\geq 0\\\ \lceil\frac{y}{z}\rceil&\text{if }\frac{y}{z}< 0 \end{cases}$$

• Semantics of Euclidean division

$$x = \textnormal{ediv}(y,z) \Leftrightarrow x=\begin{cases} \lfloor\frac{y}{z}\rfloor&\text{if }z> 0\\\ \lceil\frac{y}{z}\rceil&\text{if }z< 0 \end{cases}$$

FInterval: Abstract Operations

In the following, we let x,y,z be floating-point intervals of type FInterval.

Operation	Constraint	Forward operator	Left backward operator	Right backward operator
Identity	$x = y$	x.meet(y)	y.meet(x)	n/a
Negation	$x = \mathord{-}y$	x.neg(y)	y.neg(x)	n/a
Addition	$x = y + z$	x.add(y,z)	y.sub(x,z)	z.sub(x,y)
Subtraction	$x = y - z$	x.sub(y,z)	y.add(x,z)	z.sub(y,x)
Multiplication	$x = y * z$	x.mul(y, z)	y.mul_back(x,z)	z.mul_back(x,y)
Division	$x = y / z$	x.div(y, z)	y.mul(x, z)	z.div_rback(y,x)
Maximum	$x = \textnormal{max}(y, z)$	x.max(y, z)	y.max_back(x,z)	z.max_back(x,y)
Minimum	$x = \textnormal{min}(y, z)$	x.min(y, z)	y.min_back(x,z)	z.min_back(x,y)
Reified Equality	$x = (y = z)$	x.req(y, z)	y.req_back(x,z)	z.req_back(x,y)
Reified Inequality	$x = (y \leq z)$	x.rleq(y, z)	y.rleq_lback(x,z)	z.rleq_rback(x,y)

The addition, subtraction, multiplication and division forward operators are based on Hickey et al., "Interval Arithmetic: From Principles to Implementation", JACM, 2001.

Interval Bound Propagation

We have implemented various interval propagators for ternary arithmetic constraints of the form $x = y \odot z$ where $\odot$ is a binary operator. The term "propagator" stems from constraint programming, it is also sometimes called filtering function. In abstract interpretation, it is usually called test in order to deal with conditional statement.

Propagators on ZInterval

Let x,y,z be integer intervals of type ZInterval.

Constraint	Propagator	Best?
$x = y + z$	tell::zadd(x, y, z)	Yes
$x = y - z$	tell::zsub(x, y, z)	Yes
$x = y * z$	tell::zmul(x, y, z)	No
$x = \textnormal{fdiv}(y, z)$	tell::zfdiv(x, y, z)	Yes3
$x = \textnormal{cdiv}(y, z)$	tell::zcdiv(x, y, z)	Yes3
$x = \textnormal{tdiv}(y, z)$	tell::ztdiv(x, y, z)	Yes3
$x = \textnormal{ediv}(y, z)$	tell::zediv(x, y, z)	Yes3
$x = \textnormal{max}(y, z)$	tell::zmax(x, y, z)	Yes
$x = \textnormal{min}(y, z)$	tell::zmin(x, y, z)	Yes
$x = (y = z)$	tell::zreq(x, y, z)	Yes
$x = (y \leq z)$	tell::zrleq(x, y, z)	Yes

Propagators enforcing Bound(R) consistency: They are available under the namespace boundr::tell with the same names as above. They are less precise than the propagators above and are mainly available for research purposes and for testing propagators on FInterval.

Entailment Tests on ZInterval

Let x,y,z be integer intervals of type ZInterval.

Constraint	Entailment test
$x = y + z$	ask::zadd(x, y, z)
$x = y - z$	ask::zsub(x, y, z)
$x = y * z$	ask::zmul(x, y, z)
$x = \textnormal{fdiv}(y, z)$	ask::zfdiv(x, y, z)
$x = \textnormal{cdiv}(y, z)$	ask::zcdiv(x, y, z)
$x = \textnormal{tdiv}(y, z)$	ask::ztdiv(x, y, z)
$x = \textnormal{ediv}(y, z)$	ask::zediv(x, y, z)
$x = \textnormal{max}(y, z)$	ask::zmax(x, y, z)
$x = \textnormal{min}(y, z)$	ask::zmin(x, y, z)
$x = (y = z)$	ask::zreq(x, y, z)
$x = (y \leq z)$	ask::zrleq(x, y, z)

Propagators on FInterval

Let x,y,z be floating-point intervals of type FInterval.

Constraint	Propagator	Best?
$x = y + z$	tell::fadd(x, y, z)	Yes
$x = y - z$	tell::fsub(x, y, z)	Yes
$x = y * z$	tell::fmul(x, y, z)	No
$x = y / z$	tell::fdiv(x, y, z)	Yes
$x = \textnormal{max}(y, z)$	tell::fmax(x, y, z)	Yes
$x = \textnormal{min}(y, z)$	tell::fmin(x, y, z)	Yes
$x = (y = z)$	tell::freq(x, y, z)	Yes
$x = (y \leq z)$	tell::frleq(x, y, z)	Yes

Entailment Tests on FInterval

Let x,y,z be floating-point intervals of type FInterval.

Constraint	Entailment test
$x = y + z$	ask::fadd(x, y, z)
$x = y - z$	ask::fsub(x, y, z)
$x = y * z$	ask::fmul(x, y, z)
$x = y / z$	ask::fdiv(x, y, z)
$x = \textnormal{max}(y, z)$	ask::zmax(x, y, z)
$x = \textnormal{min}(y, z)$	ask::zmin(x, y, z)
$x = (y = z)$	ask::zreq(x, y, z)
$x = (y \leq z)$	ask::zrleq(x, y, z)

Footnotes

1. Precondition: the lower and upper bounds of the denominator z must be different from zero. ↩ ↩² ↩³ ↩⁴ ↩⁵ ↩⁶ ↩⁷ ↩⁸

2. Precondition: the domain of x must be included in [0,1]. ↩ ↩² ↩³ ↩⁴ ↩⁵ ↩⁶

3. This is currently a conjecture from experimental results. Faster but less precise propagators, postfixed by _fast (e.g. tell::fdiv_fast) are also available: they do not perform a splitjoin operation on z. ↩ ↩² ↩³ ↩⁴