#include <pre_zub.hpp>

Public Types
using	this_type = PreZUB< VT >

using	dual_type = PreZLB< VT >

using	value_type = VT

using	lower_bound_type = dual_type

using	upper_bound_type = this_type

Static Public Member Functions
CUDA static constexpr value_type	zero ()

CUDA static constexpr value_type	one ()

template<bool diagnose, class F , bool dualize = false>
static CUDA bool	interpret_tell (const F &f, value_type &tell, IDiagnostics &diagnostics)

template<bool diagnose, class F , bool dualize = false>
static CUDA bool	interpret_ask (const F &f, value_type &ask, IDiagnostics &diagnostics)

template<bool diagnose, class F , bool dualize = false>
CUDA static NI bool	interpret_type (const F &f, value_type &k, IDiagnostics &diagnostics)

template<class F >
static CUDA F	deinterpret (const value_type &v)

static CUDA constexpr Sig	sig_order ()

static CUDA constexpr Sig	sig_strict_order ()

CUDA static INLINE constexpr value_type	bot ()

CUDA static INLINE constexpr value_type	top ()

CUDA static INLINE constexpr value_type	join (value_type x, value_type y)

CUDA static INLINE constexpr value_type	meet (value_type x, value_type y)

CUDA static INLINE constexpr bool	order (value_type x, value_type y)

CUDA static INLINE constexpr bool	strict_order (value_type x, value_type y)

static CUDA constexpr value_type	next (value_type x)

static CUDA constexpr value_type	prev (value_type x)

template<bool dualize>
static CUDA constexpr value_type	dproject (Sig fun, value_type x)

static CUDA constexpr value_type	project (Sig fun, value_type x)

template<bool dualize>
static CUDA constexpr value_type	dproject (Sig fun, value_type x, value_type y)

static CUDA constexpr value_type	project (Sig fun, value_type x, value_type y)

Static Public Attributes
static constexpr const bool	is_totally_ordered = true

static constexpr const bool	preserve_bot = true

static constexpr const bool	preserve_top = true

static constexpr const bool	preserve_join = true

static constexpr const bool	preserve_meet = true

static constexpr const bool	injective_concretization = true

static constexpr const bool	preserve_concrete_covers = true

static constexpr const bool	is_lower_bound = false

static constexpr const bool	is_upper_bound = true

static constexpr const char *	name = "ZUB"

static constexpr const bool	is_arithmetic = true

Detailed Description

template<class VT>
struct lala::PreZUB< VT >

PreZUB is a pre-abstract universe \( \langle \{-\infty, \ldots, -2, -1, 0, 1, 2, \ldots, \infty\}, \leq \rangle \) totally ordered by the natural arithmetic comparison operator. It is used to represent constraints of the form \( x \leq k \) where \( k \) is an integer.

Member Typedef Documentation

◆ this_type

template<class VT >

using lala::PreZUB< VT >::this_type = PreZUB<VT>

◆ dual_type

template<class VT >

using lala::PreZUB< VT >::dual_type = PreZLB<VT>

◆ value_type

template<class VT >

using lala::PreZUB< VT >::value_type = VT

◆ lower_bound_type

template<class VT >

using lala::PreZUB< VT >::lower_bound_type = dual_type

◆ upper_bound_type

template<class VT >

using lala::PreZUB< VT >::upper_bound_type = this_type

Member Function Documentation

◆ zero()

template<class VT >

CUDA static constexpr value_type lala::PreZUB< VT >::zero ( )

inlinestaticconstexpr

◆ one()

template<class VT >

CUDA static constexpr value_type lala::PreZUB< VT >::one ( )

inlinestaticconstexpr

◆ interpret_tell()

template<class VT >

template<bool diagnose, class F , bool dualize = false>

static CUDA bool lala::PreZUB< VT >::interpret_tell	(	const F &	f,
		value_type &	tell,
		IDiagnostics &	diagnostics
	)

inlinestatic

Interpret a constant in the lattice of increasing integers according to the downset semantics. Overflows are not verified. Interpretations: Formulas of kind F::Z are interpreted exactly: \( [\![ x:\mathbb{Z} \leq k:\mathbb{Z} ]\!] = k \). Formulas of kind F::R are over-approximated: \( [\![ x:\mathbb{Z} \leq [l..u]:\mathbb{R} ]\!] = \lfloor u \rfloor \). Examples: \( [\![x <= [3.5..3.5]:R ]\!] = 3 \): there is no integer greater than 3 satisfying this constraint. \( [\![x <= [2.9..3.1]:R ]\!] = 3 \).

◆ interpret_ask()

template<class VT >

template<bool diagnose, class F , bool dualize = false>

static CUDA bool lala::PreZUB< VT >::interpret_ask	(	const F &	f,
		value_type &	ask,
		IDiagnostics &	diagnostics
	)

inlinestatic

Similar to interpret_tell but the formula is under-approximated, in particular: \( [\![ x:\mathbb{Z} \leq [l..u]:\mathbb{R} ]\!] = \lfloor u \rfloor \). Examples: \( [\![x <= [3.5..3.5]:R ]\!] = 3 \). \( [\![x <= [2.9..3.1]:R ]\!] = 2 \): the constraint is entailed only when x is less or equal to 2.9.

◆ interpret_type()

template<class VT >

template<bool diagnose, class F , bool dualize = false>

CUDA static NI bool lala::PreZUB< VT >::interpret_type	(	const F &	f,
		value_type &	k,
		IDiagnostics &	diagnostics
	)

inlinestatic

Verify if the type of a variable, introduced by an existential quantifier, is compatible with the current abstract universe. Variables of type Int are interpreted exactly ( \( \mathbb{Z} = \gamma(\top) \)). Note that we assume there is no overflow, that might be taken into account the future.

◆ deinterpret()

template<class VT >

template<class F >

static CUDA F lala::PreZUB< VT >::deinterpret ( const value_type & v )

inlinestatic

Given an Integer value, create a logical constant representing that value. Note that the lattice order has no influence here.

Precondition: v != bot() and v != top().

◆ sig_order()

template<class VT >

static CUDA constexpr Sig lala::PreZUB< VT >::sig_order ( )

inlinestaticconstexpr

The logical predicate symbol corresponding to the order of this pre-universe. We have \( a \leq_\mathit{ZUB} b \Leftrightarrow a \leq b \).

Returns: The logical symbol LEQ.

◆ sig_strict_order()

template<class VT >

static CUDA constexpr Sig lala::PreZUB< VT >::sig_strict_order ( )

inlinestaticconstexpr

The logical predicate symbol corresponding to the strict order of this pre-universe. We have \( a <_\mathit{ZUB} b \Leftrightarrow a < b \).

Returns: The logical symbol LT.

◆ bot()

template<class VT >

CUDA static INLINE constexpr value_type lala::PreZUB< VT >::bot ( )

inlinestaticconstexpr

\( \bot \) is represented by the minimal representable value of the underlying value type.

◆ top()

template<class VT >

CUDA static INLINE constexpr value_type lala::PreZUB< VT >::top ( )

inlinestaticconstexpr

\( \top \) is represented by the maximal representable value of the underlying value type.

◆ join()

template<class VT >

CUDA static INLINE constexpr value_type lala::PreZUB< VT >::join	(	value_type	x,
		value_type	y
	)

inlinestaticconstexpr

Returns: \( x \sqcup y \) defined as \( \mathit{max}(x, y) \).

◆ meet()

template<class VT >

CUDA static INLINE constexpr value_type lala::PreZUB< VT >::meet	(	value_type	x,
		value_type	y
	)

inlinestaticconstexpr

Returns: \( x \sqcap y \) defined as \( \mathit{min}(x, y) \).

◆ order()

template<class VT >

CUDA static INLINE constexpr bool lala::PreZUB< VT >::order	(	value_type	x,
		value_type	y
	)

inlinestaticconstexpr

Returns: \( \mathit{true} \) if \( x \leq_\mathit{ZUB} y \) where the order \( \leq_\mathit{ZUB} \) is the natural arithmetic ordering, otherwise returns \( \mathit{false} \).

◆ strict_order()

template<class VT >

CUDA static INLINE constexpr bool lala::PreZUB< VT >::strict_order	(	value_type	x,
		value_type	y
	)

inlinestaticconstexpr

Returns: \( \mathit{true} \) if \( x <_\mathit{ZUB} y \) where the order \( <_\mathit{ZUB} \) is the natural arithmetic ordering, otherwise returns \( \mathit{false} \).

◆ next()

template<class VT >

static CUDA constexpr value_type lala::PreZUB< VT >::next ( value_type x )

inlinestaticconstexpr

From a lattice perspective, next: ZUB -> ZUB returns an element next(x) such that x is covered by next(x).

Parameters

x	The element covering the returned element.

Returns: The next value of x in the discrete increasing chain bot, ..., -2, -1, 0, 1, ..., top.

Remarks: The next value of bot is bot and the next value of top is top.; There is no element \( x \neq \top \) such that \( \mathit{next}(x) = \top \), but it can occur in case of overflow which is not checked.

◆ prev()

template<class VT >

static CUDA constexpr value_type lala::PreZUB< VT >::prev ( value_type x )

inlinestaticconstexpr

From a lattice perspective, prev: ZUB -> ZUB returns an element prev(x) such that x covers prev(x).

Parameters

x	The element covered by the returned element.

Returns: The previous value of x in the discrete increasing chain bot, ..., -2, -1, 0, 1, ..., top.

Remarks: The previous value of bot is bot and the previous value of top is top.; There is no element \( x \neq \bot \) such that \( \mathit{prev}(x) = \bot \), but it can occur in case of overflow which is not checked.

◆ dproject() [1/2]

template<class VT >

template<bool dualize>

static CUDA constexpr value_type lala::PreZUB< VT >::dproject	(	Sig	fun,
		value_type	x
	)

inlinestaticconstexpr

◆ project() [1/2]

template<class VT >

static CUDA constexpr value_type lala::PreZUB< VT >::project	(	Sig	fun,
		value_type	x
	)

inlinestaticconstexpr

project: value_type -> value_type is an abstract function on ZUB over-approximating the function denoted by fun on the concrete domain.

Template Parameters

fun	The signature of the function to over-approximate (only `NEG`).

Parameters

x	The argument of the function, which is a constant value in the underlying universe of discourse, or top().

◆ dproject() [2/2]

template<class VT >

template<bool dualize>

static CUDA constexpr value_type lala::PreZUB< VT >::dproject	(	Sig	fun,
		value_type	x,
		value_type	y
	)

inlinestaticconstexpr

The projection of a function fun on two arguments x and y is simply the standard application of the operation, with specific cases for infinities. When the function fun is not supported, we return top().

We deal with infinities in the "standard" way. The rules below are tried in order (so we apply inf - X even if X is inf or -inf). For addition: inf + X = inf, -inf + X = -inf, X + inf = inf, X + -inf = -inf. For subtraction: inf - X = inf, -inf - X = -inf, X - inf = -inf, X - -inf = inf. For multiplication and division, we look at the sign (see the table infs). For division, we expect y != 0 (but it returns 0 if it happens). For division, when dividing by infinity, it actually depends on whether we are computing a lower or upper bound and the sign of infinity; not sure of the exact rules so we overapproximate to top. For min and max, it is trivial. For modulus and ipow, we expect x and y to be non-infinities.

◆ project() [2/2]

template<class VT >

static CUDA constexpr value_type lala::PreZUB< VT >::project	(	Sig	fun,
		value_type	x,
		value_type	y
	)

inlinestaticconstexpr

Member Data Documentation

◆ is_totally_ordered

template<class VT >

constexpr const bool lala::PreZUB< VT >::is_totally_ordered = true

staticconstexpr

◆ preserve_bot

template<class VT >

constexpr const bool lala::PreZUB< VT >::preserve_bot = true

staticconstexpr

true if \( \gamma(\bot) = \{\} \).

◆ preserve_top

template<class VT >

constexpr const bool lala::PreZUB< VT >::preserve_top = true

staticconstexpr

true if \( \gamma(\top) = U \).

◆ preserve_join

template<class VT >

constexpr const bool lala::PreZUB< VT >::preserve_join = true

staticconstexpr

true if \( \gamma(a \sqcup b) = \gamma(a) \cup \gamma(b) \) .

◆ preserve_meet

template<class VT >

constexpr const bool lala::PreZUB< VT >::preserve_meet = true

staticconstexpr

true if \( \gamma(a \sqcap b) = \gamma(a) \cap \gamma(b) \) .

◆ injective_concretization

template<class VT >

constexpr const bool lala::PreZUB< VT >::injective_concretization = true

staticconstexpr

The concretization is injective when each abstract element maps to a distinct concrete element. This is important for the correctness of prev and next because we suppose \( \gamma(x) != \gamma(\mathit{next}(x)) \) when \( x \neq \bot \land x \neq \top \).

◆ preserve_concrete_covers

template<class VT >

constexpr const bool lala::PreZUB< VT >::preserve_concrete_covers = true

staticconstexpr

true if concrete covers are preserved by the concretization function, i.e., \( \gamma(\mathit{next}(x)) \) is a cover of \( \gamma(x) \), and dually for \( \mathit{prev}(x) \).

Remarks: preserve_concrete_covers implies injective_concretization.

◆ is_lower_bound

template<class VT >

constexpr const bool lala::PreZUB< VT >::is_lower_bound = false

staticconstexpr

true if this lattice aims to represents lower bounds of concrete sets.

◆ is_upper_bound

template<class VT >

constexpr const bool lala::PreZUB< VT >::is_upper_bound = true

staticconstexpr

◆ name

template<class VT >

constexpr const char* lala::PreZUB< VT >::name = "ZUB"

staticconstexpr

◆ is_arithmetic

template<class VT >

constexpr const bool lala::PreZUB< VT >::is_arithmetic = true

staticconstexpr

The documentation for this struct was generated from the following files:

include/lala/universes/pre_zlb.hpp
include/lala/universes/pre_zub.hpp

Public Types

Static Public Member Functions

Static Public Attributes

Detailed Description

Member Typedef Documentation

◆ this_type

◆ dual_type

◆ value_type

◆ lower_bound_type

◆ upper_bound_type

Member Function Documentation

◆ zero()

◆ one()

◆ interpret_tell()

◆ interpret_ask()

◆ interpret_type()

◆ deinterpret()

◆ sig_order()

◆ sig_strict_order()

◆ bot()

◆ top()

◆ join()

◆ meet()

◆ order()

◆ strict_order()

◆ next()

◆ prev()

◆ dproject() [1/2]

◆ project() [1/2]

◆ dproject() [2/2]

◆ project() [2/2]

Member Data Documentation

◆ is_totally_ordered

◆ preserve_bot

◆ preserve_top

◆ preserve_join

◆ preserve_meet

◆ injective_concretization

◆ preserve_concrete_covers

◆ is_lower_bound

◆ is_upper_bound

◆ name

◆ is_arithmetic