#include <interval.hpp>

Public Types
using	LB = U

using	UB = typename LB::dual_type

using	this_type = Interval<LB>

using	local_type = Interval<typename LB::local_type>

using	CP = CartesianProduct<LB, UB>

using	value_type = typename CP::value_type

using	memory_type = typename CP::memory_type

Public Member Functions
CUDA constexpr	Interval ()

CUDA constexpr	Interval (const typename U::value_type &x)

CUDA constexpr	Interval (const LB &lb, const UB &ub)

template<class A >
CUDA constexpr	Interval (const Interval< A > &other)

template<class A >
CUDA constexpr	Interval (Interval< A > &&other)

template<class A >
CUDA constexpr this_type &	operator= (const Interval< A > &other)

CUDA constexpr this_type &	operator= (const this_type &other)

CUDA constexpr local::BInc	is_top () const

CUDA constexpr local::BDec	is_bot () const

CUDA constexpr const CP &	as_product () const

CUDA constexpr value_type	value () const

CUDA constexpr LB &	lb ()

CUDA constexpr UB &	ub ()

CUDA constexpr const LB &	lb () const

CUDA constexpr const UB &	ub () const

CUDA constexpr this_type &	tell_top ()

template<class A , class M >
CUDA constexpr this_type &	tell_lb (const A &lb, BInc< M > &has_changed)

template<class A , class M >
CUDA constexpr this_type &	tell_ub (const A &ub, BInc< M > &has_changed)

template<class A >
CUDA constexpr this_type &	tell_lb (const A &lb)

template<class A >
CUDA constexpr this_type &	tell_ub (const A &ub)

template<class A , class M >
CUDA constexpr this_type &	tell (const Interval< A > &other, BInc< M > &has_changed)

template<class A >
CUDA constexpr this_type &	tell (const Interval< A > &other)

CUDA constexpr this_type &	dtell_bot ()

template<class A , class M >
CUDA constexpr this_type &	dtell_lb (const A &lb, BInc< M > &has_changed)

template<class A , class M >
CUDA constexpr this_type &	dtell_ub (const A &ub, BInc< M > &has_changed)

template<class A >
CUDA constexpr this_type &	dtell_lb (const A &lb)

template<class A >
CUDA constexpr this_type &	dtell_ub (const A &ub)

template<class A , class M >
CUDA constexpr this_type &	dtell (const Interval< A > &other, BInc< M > &has_changed)

template<class A >
CUDA constexpr this_type &	dtell (const Interval< A > &other)

template<class A >
CUDA constexpr bool	extract (Interval< A > &ua) const

template<class Env >
CUDA TFormula< typename Env::allocator_type >	deinterpret (AVar x, const Env &env) const

template<class F >
CUDA NI F	deinterpret () const

CUDA NI void	print () const

CUDA constexpr local_type	width () const

CUDA constexpr local_type	median () const

Static Public Member Functions
CUDA static constexpr local_type	eq_zero ()

CUDA static constexpr local_type	eq_one ()

CUDA static constexpr local_type	bot ()

CUDA static constexpr local_type	top ()

template<bool diagnose = false, class F , class Env , class U2 >
CUDA static NI bool	interpret_tell (const F &f, const Env &env, Interval< U2 > &k, IDiagnostics &diagnostics)

template<bool diagnose = false, class F , class Env , class U2 >
CUDA static NI bool	interpret_ask (const F &f, const Env &env, Interval< U2 > &k, IDiagnostics &diagnostics)

template<IKind kind, bool diagnose = false, class F , class Env , class U2 >
CUDA static NI bool	interpret (const F &f, const Env &env, Interval< U2 > &k, IDiagnostics &diagnostics)

CUDA NI static constexpr bool	is_supported_fun (Sig sig)

CUDA static constexpr local_type	additive_inverse (const this_type &x)

template<class L >
CUDA static constexpr local_type	reverse (const Interval< L > &x)

template<class L >
CUDA static constexpr local_type	neg (const Interval< L > &x)

template<class L >
CUDA static constexpr local_type	abs (const Interval< L > &x)

template<Sig sig, class L >
CUDA static constexpr local_type	fun (const Interval< L > &x)

template<class L , class K >
CUDA static constexpr local_type	add (const Interval< L > &x, const Interval< K > &y)

template<class L , class K >
CUDA static constexpr local_type	sub (const Interval< L > &x, const Interval< K > &y)

template<class L , class K >
CUDA static constexpr local_type	mul (const Interval< L > &l, const Interval< K > &k)

template<Sig divsig, class L , class K >
CUDA static constexpr local_type	div (const Interval< L > &l, const Interval< K > &k)

template<Sig modsig, class L , class K >
CUDA static constexpr local_type	mod (const Interval< L > &l, const Interval< K > &k)

template<class L , class K >
CUDA static constexpr local_type	pow (const Interval< L > &l, const Interval< K > &k)

template<Sig sig, class L , class K >
CUDA static constexpr local_type	fun (const Interval< L > &x, const Interval< K > &y)

Static Public Attributes
static constexpr const bool	is_abstract_universe = true

static constexpr const bool	sequential = CP::sequential

static constexpr const bool	is_totally_ordered = false

static constexpr const bool	preserve_bot = CP::preserve_bot

static constexpr const bool	preserve_top = true

static constexpr const bool	preserve_join = true

static constexpr const bool	preserve_meet = false

static constexpr const bool	injective_concretization = CP::injective_concretization

static constexpr const bool	preserve_concrete_covers = CP::preserve_concrete_covers

static constexpr const bool	complemented = false

static constexpr const char *	name = "Interval"

Friends
template<class A >
class	Interval

Detailed Description

template<class U>
class lala::Interval

An interval is a Cartesian product of a lower and upper bounds, themselves represented as lattices. One difference, is that the \( \top \) can be represented by multiple interval elements, whenever \( l > u \), therefore some operations are different than on the Cartesian product, e.g., \( [3..2] \equiv [4..1] \) in the interval lattice.

Member Typedef Documentation

◆ LB

template<class U >

using lala::Interval::LB = U

◆ UB

template<class U >

using lala::Interval::UB = typename LB::dual_type

◆ this_type

template<class U >

using lala::Interval::this_type = Interval<LB>

◆ local_type

template<class U >

using lala::Interval::local_type = Interval<typename LB::local_type>

◆ CP

template<class U >

using lala::Interval::CP = CartesianProduct<LB, UB>

◆ value_type

template<class U >

using lala::Interval::value_type = typename CP::value_type

◆ memory_type

template<class U >

using lala::Interval::memory_type = typename CP::memory_type

Constructor & Destructor Documentation

◆ Interval() [1/5]

template<class U >

CUDA constexpr lala::Interval::Interval ( )

inlineconstexpr

Initialize the interval to bottom using the default constructor of the bounds.

◆ Interval() [2/5]

template<class U >

CUDA constexpr lala::Interval::Interval ( const typename U::value_type & x )

inlineconstexpr

Given a value \( x \in U \) where \( U \) is the universe of discourse, we initialize a singleton interval \( [x..x] \).

◆ Interval() [3/5]

template<class U >

CUDA constexpr lala::Interval< U >::Interval	(	const LB &	lb,
		const UB &	ub )

inlineconstexpr

◆ Interval() [4/5]

template<class U >

template<class A >

CUDA constexpr lala::Interval::Interval ( const Interval< A > & other )

inlineconstexpr

◆ Interval() [5/5]

template<class U >

template<class A >

CUDA constexpr lala::Interval::Interval ( Interval< A > && other )

inlineconstexpr

Member Function Documentation

◆ operator=() [1/2]

template<class U >

template<class A >

CUDA constexpr this_type & lala::Interval::operator= ( const Interval< A > & other )

inlineconstexpr

The assignment operator can only be used in a sequential context. It is monotone but not extensive.

◆ operator=() [2/2]

template<class U >

CUDA constexpr this_type & lala::Interval::operator= ( const this_type & other )

inlineconstexpr

◆ eq_zero()

template<class U >

CUDA static constexpr local_type lala::Interval::eq_zero ( )

inlinestaticconstexpr

Pre-interpreted formula x == 0.

◆ eq_one()

template<class U >

CUDA static constexpr local_type lala::Interval::eq_one ( )

inlinestaticconstexpr

Pre-interpreted formula x == 1.

◆ bot()

template<class U >

CUDA static constexpr local_type lala::Interval::bot ( )

inlinestaticconstexpr

◆ top()

template<class U >

CUDA static constexpr local_type lala::Interval::top ( )

inlinestaticconstexpr

◆ is_top()

template<class U >

CUDA constexpr local::BInc lala::Interval::is_top ( ) const

inlineconstexpr

◆ is_bot()

template<class U >

CUDA constexpr local::BDec lala::Interval::is_bot ( ) const

inlineconstexpr

◆ as_product()

template<class U >

CUDA constexpr const CP & lala::Interval::as_product ( ) const

inlineconstexpr

◆ value()

template<class U >

CUDA constexpr value_type lala::Interval::value ( ) const

inlineconstexpr

◆ interpret_tell()

template<class U >

template<bool diagnose = false, class F , class Env , class U2 >

CUDA static NI bool lala::Interval< U >::interpret_tell	(	const F &	f,
		const Env &	env,
		Interval< U2 > &	k,
		IDiagnostics &	diagnostics )

inlinestatic

Support the same language than the Cartesian product, and more:

var x:B when the underlying universe is arithmetic and preserve concrete covers. Therefore, the element k is always in \( \gamma(lb) \cap \gamma(ub) \).

◆ interpret_ask()

template<class U >

template<bool diagnose = false, class F , class Env , class U2 >

CUDA static NI bool lala::Interval< U >::interpret_ask	(	const F &	f,
		const Env &	env,
		Interval< U2 > &	k,
		IDiagnostics &	diagnostics )

inlinestatic

Support the same language than the Cartesian product, and more:

x != k is under-approximated by interpreting x != k in the lower bound.
x == k is interpreted by over-approximating x == k in both bounds and then verifying both bounds are the same.
x in {[l..u]} is interpreted by under-approximatingx >= landx <= u`.

◆ interpret()

template<class U >

template<IKind kind, bool diagnose = false, class F , class Env , class U2 >

CUDA static NI bool lala::Interval< U >::interpret	(	const F &	f,
		const Env &	env,
		Interval< U2 > &	k,
		IDiagnostics &	diagnostics )

inlinestatic

◆ lb() [1/2]

template<class U >

CUDA constexpr LB & lala::Interval::lb ( )

inlineconstexpr

You must use the lattice interface (tell methods) to modify the lower and upper bounds, if you use assignment you violate the PCCP model.

◆ ub() [1/2]

template<class U >

CUDA constexpr UB & lala::Interval::ub ( )

inlineconstexpr

◆ lb() [2/2]

template<class U >

CUDA constexpr const LB & lala::Interval::lb ( ) const

inlineconstexpr

◆ ub() [2/2]

template<class U >

CUDA constexpr const UB & lala::Interval::ub ( ) const

inlineconstexpr

◆ tell_top()

template<class U >

CUDA constexpr this_type & lala::Interval::tell_top ( )

inlineconstexpr

◆ tell_lb() [1/2]

template<class U >

template<class A , class M >

CUDA constexpr this_type & lala::Interval< U >::tell_lb	(	const A &	lb,
		BInc< M > &	has_changed )

inlineconstexpr

◆ tell_ub() [1/2]

template<class U >

template<class A , class M >

CUDA constexpr this_type & lala::Interval< U >::tell_ub	(	const A &	ub,
		BInc< M > &	has_changed )

inlineconstexpr

◆ tell_lb() [2/2]

template<class U >

template<class A >

CUDA constexpr this_type & lala::Interval::tell_lb ( const A & lb )

inlineconstexpr

◆ tell_ub() [2/2]

template<class U >

template<class A >

CUDA constexpr this_type & lala::Interval::tell_ub ( const A & ub )

inlineconstexpr

◆ tell() [1/2]

template<class U >

template<class A , class M >

CUDA constexpr this_type & lala::Interval< U >::tell	(	const Interval< A > &	other,
		BInc< M > &	has_changed )

inlineconstexpr

◆ tell() [2/2]

template<class U >

template<class A >

CUDA constexpr this_type & lala::Interval::tell ( const Interval< A > & other )

inlineconstexpr

◆ dtell_bot()

template<class U >

CUDA constexpr this_type & lala::Interval::dtell_bot ( )

inlineconstexpr

◆ dtell_lb() [1/2]

template<class U >

template<class A , class M >

CUDA constexpr this_type & lala::Interval< U >::dtell_lb	(	const A &	lb,
		BInc< M > &	has_changed )

inlineconstexpr

◆ dtell_ub() [1/2]

template<class U >

template<class A , class M >

CUDA constexpr this_type & lala::Interval< U >::dtell_ub	(	const A &	ub,
		BInc< M > &	has_changed )

inlineconstexpr

◆ dtell_lb() [2/2]

template<class U >

template<class A >

CUDA constexpr this_type & lala::Interval::dtell_lb ( const A & lb )

inlineconstexpr

◆ dtell_ub() [2/2]

template<class U >

template<class A >

CUDA constexpr this_type & lala::Interval::dtell_ub ( const A & ub )

inlineconstexpr

◆ dtell() [1/2]

template<class U >

template<class A , class M >

CUDA constexpr this_type & lala::Interval< U >::dtell	(	const Interval< A > &	other,
		BInc< M > &	has_changed )

inlineconstexpr

◆ dtell() [2/2]

template<class U >

template<class A >

CUDA constexpr this_type & lala::Interval::dtell ( const Interval< A > & other )

inlineconstexpr

◆ extract()

template<class U >

template<class A >

CUDA constexpr bool lala::Interval::extract ( Interval< A > & ua ) const

inlineconstexpr

◆ deinterpret() [1/2]

template<class U >

template<class Env >

CUDA TFormula< typename Env::allocator_type > lala::Interval< U >::deinterpret	(	AVar	x,
		const Env &	env ) const

inline

◆ deinterpret() [2/2]

template<class U >

template<class F >

CUDA NI F lala::Interval::deinterpret ( ) const

inline

Deinterpret the current value to a logical constant. The lower bound is deinterpreted, and it is up to the user to check that interval is a singleton. A special case is made for real numbers where the both bounds are used, since the logical interpretation uses interval.

◆ print()

template<class U >

CUDA NI void lala::Interval::print ( ) const

inline

◆ is_supported_fun()

template<class U >

CUDA NI static constexpr bool lala::Interval::is_supported_fun ( Sig sig )

inlinestaticconstexpr

◆ additive_inverse()

template<class U >

CUDA static constexpr local_type lala::Interval::additive_inverse ( const this_type & x )

inlinestaticconstexpr

The additive inverse is obtained by pairwise negation of the components. Equivalent to neg(reverse(x)). Note that the inverse of bot is bot, simply because bot has no mathematical inverse.

◆ reverse()

template<class U >

template<class L >

CUDA static constexpr local_type lala::Interval::reverse ( const Interval< L > & x )

inlinestaticconstexpr

◆ neg()

template<class U >

template<class L >

CUDA static constexpr local_type lala::Interval::neg ( const Interval< L > & x )

inlinestaticconstexpr

◆ abs()

template<class U >

template<class L >

CUDA static constexpr local_type lala::Interval::abs ( const Interval< L > & x )

inlinestaticconstexpr

◆ fun() [1/2]

template<class U >

template<Sig sig, class L >

CUDA static constexpr local_type lala::Interval::fun ( const Interval< L > & x )

inlinestaticconstexpr

◆ add()

template<class U >

template<class L , class K >

CUDA static constexpr local_type lala::Interval< U >::add	(	const Interval< L > &	x,
		const Interval< K > &	y )

inlinestaticconstexpr

◆ sub()

template<class U >

template<class L , class K >

CUDA static constexpr local_type lala::Interval< U >::sub	(	const Interval< L > &	x,
		const Interval< K > &	y )

inlinestaticconstexpr

◆ mul()

template<class U >

template<class L , class K >

CUDA static constexpr local_type lala::Interval< U >::mul	(	const Interval< L > &	l,
		const Interval< K > &	k )

inlinestaticconstexpr

◆ div()

template<class U >

template<Sig divsig, class L , class K >

CUDA static constexpr local_type lala::Interval< U >::div	(	const Interval< L > &	l,
		const Interval< K > &	k )

inlinestaticconstexpr

◆ mod()

template<class U >

template<Sig modsig, class L , class K >

CUDA static constexpr local_type lala::Interval< U >::mod	(	const Interval< L > &	l,
		const Interval< K > &	k )

inlinestaticconstexpr

◆ pow()

template<class U >

template<class L , class K >

CUDA static constexpr local_type lala::Interval< U >::pow	(	const Interval< L > &	l,
		const Interval< K > &	k )

inlinestaticconstexpr

◆ fun() [2/2]

template<class U >

template<Sig sig, class L , class K >

CUDA static constexpr local_type lala::Interval< U >::fun	(	const Interval< L > &	x,
		const Interval< K > &	y )

inlinestaticconstexpr

◆ width()

template<class U >

CUDA constexpr local_type lala::Interval::width ( ) const

inlineconstexpr

◆ median()

template<class U >

CUDA constexpr local_type lala::Interval::median ( ) const

inlineconstexpr

Returns: The median value of the interval, which is computed by lb() + ((ub() - lb()) / 2).

Friends And Related Symbol Documentation

◆ Interval

template<class U >

template<class A >

friend class Interval

friend

Member Data Documentation

◆ is_abstract_universe

template<class U >

constexpr const bool lala::Interval::is_abstract_universe = true

staticconstexpr

◆ sequential

template<class U >

constexpr const bool lala::Interval::sequential = CP::sequential

staticconstexpr

◆ is_totally_ordered

template<class U >

constexpr const bool lala::Interval::is_totally_ordered = false

staticconstexpr

◆ preserve_bot

template<class U >

constexpr const bool lala::Interval::preserve_bot = CP::preserve_bot

staticconstexpr

◆ preserve_top

template<class U >

constexpr const bool lala::Interval::preserve_top = true

staticconstexpr

◆ preserve_join

template<class U >

constexpr const bool lala::Interval::preserve_join = true

staticconstexpr

◆ preserve_meet

template<class U >

constexpr const bool lala::Interval::preserve_meet = false

staticconstexpr

◆ injective_concretization

template<class U >

constexpr const bool lala::Interval::injective_concretization = CP::injective_concretization

staticconstexpr

◆ preserve_concrete_covers

template<class U >

constexpr const bool lala::Interval::preserve_concrete_covers = CP::preserve_concrete_covers

staticconstexpr

◆ complemented

template<class U >

constexpr const bool lala::Interval::complemented = false

staticconstexpr

◆ name

template<class U >

constexpr const char* lala::Interval::name = "Interval"

staticconstexpr

The documentation for this class was generated from the following file:

include/lala/interval.hpp

Public Types

Public Member Functions

Static Public Member Functions

Static Public Attributes

Friends

Detailed Description

Member Typedef Documentation

◆ LB

◆ UB

◆ this_type

◆ local_type

◆ CP

◆ value_type

◆ memory_type

Constructor & Destructor Documentation

◆ Interval() [1/5]

◆ Interval() [2/5]

◆ Interval() [3/5]

◆ Interval() [4/5]

◆ Interval() [5/5]

Member Function Documentation

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ eq_zero()

◆ eq_one()

◆ bot()

◆ top()

◆ is_top()

◆ is_bot()

◆ as_product()

◆ value()

◆ interpret_tell()

◆ interpret_ask()

◆ interpret()

◆ lb() [1/2]

◆ ub() [1/2]

◆ lb() [2/2]

◆ ub() [2/2]

◆ tell_top()

◆ tell_lb() [1/2]

◆ tell_ub() [1/2]

◆ tell_lb() [2/2]

◆ tell_ub() [2/2]

◆ tell() [1/2]

◆ tell() [2/2]

◆ dtell_bot()

◆ dtell_lb() [1/2]

◆ dtell_ub() [1/2]

◆ dtell_lb() [2/2]

◆ dtell_ub() [2/2]

◆ dtell() [1/2]

◆ dtell() [2/2]

◆ extract()

◆ deinterpret() [1/2]

◆ deinterpret() [2/2]

◆ print()

◆ is_supported_fun()

◆ additive_inverse()

◆ reverse()

◆ neg()

◆ abs()

◆ fun() [1/2]

◆ add()

◆ sub()

◆ mul()

◆ div()

◆ mod()

◆ pow()

◆ fun() [2/2]

◆ width()

◆ median()

Friends And Related Symbol Documentation

◆ Interval

Member Data Documentation

◆ is_abstract_universe

◆ sequential

◆ is_totally_ordered

◆ preserve_bot

◆ preserve_top

◆ preserve_join