#include <pre_zinc.hpp>

Public Types
using	this_type = PreZInc<VT>

using	dual_type = PreZDec<VT>

using	value_type = VT

using	increasing_type = this_type

Static Public Member Functions
CUDA static constexpr value_type	zero ()

CUDA static constexpr value_type	one ()

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

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

template<bool diagnose, class F >
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 ()

static CUDA constexpr value_type	bot ()

static CUDA constexpr value_type	top ()

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

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

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

static CUDA 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)

CUDA static NI constexpr bool	is_supported_fun (Sig sig)

template<Sig sig>
static CUDA constexpr value_type	fun (value_type x)

template<Sig sig>
CUDA static NI constexpr value_type	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	complemented = false

static constexpr const bool	increasing = true

static constexpr const char *	name = "ZInc"

static constexpr const bool	is_arithmetic = true

Detailed Description

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

PreZInc 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 \geq k \) where \( k \) is an integer.

Member Typedef Documentation

◆ this_type

template<class VT >

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

◆ dual_type

template<class VT >

using lala::PreZInc< VT >::dual_type = PreZDec<VT>

◆ value_type

template<class VT >

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

◆ increasing_type

template<class VT >

using lala::PreZInc< VT >::increasing_type = this_type

Member Function Documentation

◆ zero()

template<class VT >

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

inlinestaticconstexpr

◆ one()

template<class VT >

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

inlinestaticconstexpr

◆ interpret_tell()

template<class VT >

template<bool diagnose, class F >

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

inlinestatic

Interpret a constant in the lattice of increasing integers according to the upset semantics (see universe.hpp for explanation). Overflows are not verified (issue #1). Interpretations: Formulas of kind F::Z are interpreted exactly: \( [\![ x:\mathbb{Z} \geq k:\mathbb{Z} ]\!] = k \). Formulas of kind F::R are over-approximated: \( [\![ x:\mathbb{Z} \geq [l..u]:\mathbb{R} ]\!] = \lceil l \rceil \). Note that all elements in \( [l..\lceil l \rceil[\) do not belong to \( \mathbb{Z} \), so they can be safely ignored. Examples: \( [\![x >= [2.5..2.5]:R ]\!] = 3 \). \( [\![x >= [2.9..3.1]:R ]\!] = 3 \).

◆ interpret_ask()

template<class VT >

template<bool diagnose, class F >

static CUDA bool lala::PreZInc< 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} \geq [l..u]:\mathbb{R} ]\!] = \lceil u \rceil \).

◆ interpret_type()

template<class VT >

template<bool diagnose, class F >

CUDA static NI bool lala::PreZInc< 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(\bot) \)). 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::PreZInc< 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::PreZInc< VT >::sig_order ( )

inlinestaticconstexpr

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

Returns: The logical symbol LEQ.

◆ sig_strict_order()

template<class VT >

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

inlinestaticconstexpr

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

Returns: The logical symbol LT.

◆ bot()

template<class VT >

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

inlinestaticconstexpr

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

◆ top()

template<class VT >

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

inlinestaticconstexpr

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

◆ join()

template<class VT >

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

inlinestaticconstexpr

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

◆ meet()

template<class VT >

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

inlinestaticconstexpr

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

◆ order()

template<class VT >

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

inlinestaticconstexpr

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

◆ strict_order()

template<class VT >

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

inlinestaticconstexpr

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

◆ next()

template<class VT >

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

inlinestaticconstexpr

From a lattice perspective, next: ZInc -> ZInc 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::PreZInc< VT >::prev ( value_type x )

inlinestaticconstexpr

From a lattice perspective, prev: ZInc -> ZInc 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.

◆ is_supported_fun()

template<class VT >

CUDA static NI constexpr bool lala::PreZInc< VT >::is_supported_fun ( Sig sig )

inlinestaticconstexpr

◆ fun() [1/2]

template<class VT >

template<Sig sig>

static CUDA constexpr value_type lala::PreZInc< VT >::fun ( value_type x )

inlinestaticconstexpr

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

Template Parameters

sig	The signature of the function to over-approximate, can be either `NEG` or `ABS`.

Parameters

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

Note: Since x is a constant, we do not check for equality with bot() or top().

◆ fun() [2/2]

template<class VT >

template<Sig sig>

CUDA static NI constexpr value_type lala::PreZInc< VT >::fun	(	value_type	x,
		value_type	y )

inlinestaticconstexpr

fun: value_type X value_type -> ZInc is similar to its unary version but with an arity of 2.

Member Data Documentation

◆ is_totally_ordered

template<class VT >

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

staticconstexpr

◆ preserve_bot

template<class VT >

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

staticconstexpr

true if \( \gamma(\bot) = \bot^\flat \).

◆ preserve_top

template<class VT >

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

staticconstexpr

true if \( \gamma(\top) = \top^\flat \).

◆ preserve_join

template<class VT >

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

staticconstexpr

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

◆ preserve_meet

template<class VT >

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

staticconstexpr

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

◆ injective_concretization

template<class VT >

constexpr const bool lala::PreZInc< 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::PreZInc< 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.

◆ complemented

template<class VT >

constexpr const bool lala::PreZInc< VT >::complemented = false

staticconstexpr

true if for all element \( x \in A \), there exists a unique element \( \lnot x \in A \) such that \( x \sqcup \lnot x = \top \) and \( x \sqcap \lnot x = \bot \).

◆ increasing

template<class VT >

constexpr const bool lala::PreZInc< VT >::increasing = true

staticconstexpr

true if the natural order of the universe of discourse coincides with the lattice order of this pre-universe, false if it is reversed.

◆ name

template<class VT >

constexpr const char* lala::PreZInc< VT >::name = "ZInc"

staticconstexpr

◆ is_arithmetic

template<class VT >

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

staticconstexpr

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

include/lala/universes/pre_zdec.hpp
include/lala/universes/pre_zinc.hpp

Public Types

Static Public Member Functions

Static Public Attributes

Detailed Description

Member Typedef Documentation

◆ this_type

◆ dual_type

◆ value_type

◆ increasing_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()

◆ is_supported_fun()

◆ fun() [1/2]

◆ fun() [2/2]

Member Data Documentation

◆ is_totally_ordered

◆ preserve_bot

◆ preserve_top

◆ preserve_join

◆ preserve_meet

◆ injective_concretization

◆ preserve_concrete_covers

◆ complemented

◆ increasing

◆ name

◆ is_arithmetic