#include <pre_fub.hpp>

Public Types
using	this_type = PreFUB<VT>

using	dual_type = PreFLB<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 >
static CUDA bool	interpret_tell (const F &f, value_type &k, IDiagnostics &diagnostics)

template<bool diagnose, class F >
static CUDA bool	interpret_ask (const F &f, value_type &k, 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 ()

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)

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

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 = false

static constexpr const bool	is_lower_bound = false

static constexpr const bool	is_upper_bound = true

static constexpr const char *	name = "FUB"

static constexpr const bool	is_arithmetic = true

Detailed Description

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

PreFUB is a pre-abstract universe \( \langle \mathbb{F}\setminus\{NaN\}, \leq \rangle \) totally ordered by the floating-point arithmetic comparison operator. We work on a subset of floating-point numbers without NaN. It is used to represent (and possibly approximate) constraints of the form \( x \leq k \) where \( k \) is a real number.

Member Typedef Documentation

◆ this_type

template<class VT >

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

◆ dual_type

template<class VT >

using lala::PreFUB< VT >::dual_type = PreFLB<VT>

◆ value_type

template<class VT >

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

◆ lower_bound_type

template<class VT >

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

◆ upper_bound_type

template<class VT >

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

Member Function Documentation

◆ zero()

template<class VT >

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

inlinestaticconstexpr

◆ one()

template<class VT >

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

inlinestaticconstexpr

◆ interpret_tell()

template<class VT >

template<bool diagnose, class F >

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

inlinestatic

Interpret a constant in the lattice of increasing floating-point numbers FInc according to the downset semantics. Interpretations: Formulas of kind F::Z might be over-approximated (if the integer cannot be represented in a floating-point number because it is too large). Formulas of kind F::R might be over-approximated to the upper bound of the interval (if the real number is represented by an interval [lb..ub] where lb != ub). Other kind of formulas are not supported.

◆ interpret_ask()

template<class VT >

template<bool diagnose, class F >

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

inlinestatic

Same as interpret_tell but the constant is under-approximated instead.

◆ interpret_type()

template<class VT >

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

CUDA static NI bool lala::PreFUB< 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. Interpretations: Variables of type Int are always over-approximated ( \( \mathbb{Z} \subseteq \gamma(\top) \)). Variables of type Real are represented exactly (only initially because \( \mathbb{R} = \gamma(\top) \)).

◆ deinterpret()

template<class VT >

template<class F >

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

inlinestatic

Given a floating-point value, create a logical constant representing that value. The constant is represented by a singleton interval of double [v..v]. 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::PreFUB< VT >::sig_order ( )

inlinestaticconstexpr

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

Returns: The logical symbol LEQ.

◆ sig_strict_order()

template<class VT >

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

inlinestaticconstexpr

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

Returns: The logical symbol LT.

◆ bot()

template<class VT >

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

inlinestaticconstexpr

\( \bot \) is represented by the floating-point negative infinity value.

◆ top()

template<class VT >

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

inlinestaticconstexpr

\( \top \) is represented by the floating-point positive infinity value.

◆ join()

template<class VT >

static CUDA constexpr value_type lala::PreFUB< 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::PreFUB< 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::PreFUB< VT >::order	(	value_type	x,
		value_type	y )

inlinestaticconstexpr

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

◆ strict_order()

template<class VT >

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

inlinestaticconstexpr

Returns: \( \mathit{true} \) if \( x <_\mathit{FInc} 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::PreFUB< VT >::next ( value_type x )

inlinestaticconstexpr

From a lattice perspective, this function returns an element \( y \) such that \( y \) is a cover of \( x \).

Returns: The next value of \( x \) in the floating-point increasing chain \( -\infty, \ldots, prev(-2.0), -2.0, next(-2.0), \ldots, \infty \) is the next representable value of \( x \) when \( x \not\in \{\infty, -\infty\} \) and \( x \) otherwise. Note that \( 0 \) is considered to be represented by a single value.

◆ prev()

template<class VT >

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

inlinestaticconstexpr

From a lattice perspective, this function returns an element \( y \) such that \( x \) is a cover of \( y \).

Returns: The previous value of \( x \) in the floating-point increasing chain \( -\infty, \ldots, prev(-2.0), -2.0, next(-2.0), \ldots, \infty \) is the previous representable value of \( x \) when \( x \not\in \{\infty, -\infty\} \) and \( x \) otherwise. \( 0 \) is considered to be represented by a single value.

◆ project() [1/2]

template<class VT >

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

inlinestaticconstexpr

◆ project() [2/2]

template<class VT >

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

inlinestaticconstexpr

Member Data Documentation

◆ is_totally_ordered

template<class VT >

const bool lala::PreFUB< VT >::is_totally_ordered = true

staticconstexpr

◆ preserve_bot

template<class VT >

const bool lala::PreFUB< VT >::preserve_bot = true

staticconstexpr

◆ preserve_top

template<class VT >

const bool lala::PreFUB< VT >::preserve_top = true

staticconstexpr

◆ preserve_join

template<class VT >

const bool lala::PreFUB< VT >::preserve_join = true

staticconstexpr

◆ preserve_meet

template<class VT >

const bool lala::PreFUB< VT >::preserve_meet = true

staticconstexpr

◆ injective_concretization

template<class VT >

const bool lala::PreFUB< VT >::injective_concretization = true

staticconstexpr

Note that -0 and +0 are treated as the same element.

◆ preserve_concrete_covers

template<class VT >

const bool lala::PreFUB< VT >::preserve_concrete_covers = false

staticconstexpr

◆ is_lower_bound

template<class VT >

const bool lala::PreFUB< VT >::is_lower_bound = false

staticconstexpr

◆ is_upper_bound

template<class VT >

const bool lala::PreFUB< VT >::is_upper_bound = true

staticconstexpr

◆ name

template<class VT >

const char* lala::PreFUB< VT >::name = "FUB"

staticconstexpr

◆ is_arithmetic

template<class VT >

const bool lala::PreFUB< VT >::is_arithmetic = true

staticconstexpr

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

include/lala/universes/pre_flb.hpp
include/lala/universes/pre_fub.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()

◆ project() [1/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