#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	value_type = battery::tuple< typename LB::value_type, typename UB::value_type >

using	memory_type = typename LB::memory_type

Public Member Functions
constexpr	Interval ()=default

constexpr	Interval (const this_type &)=default

constexpr	Interval (this_type &&)=default

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

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

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

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

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

constexpr this_type &	operator= (const this_type &)=default

constexpr this_type &	operator= (this_type &&)=default

constexpr CUDA local::B	is_bot () const

constexpr CUDA local::B	is_top () const

constexpr CUDA value_type	value () const

CUDA constexpr INLINE LB &	lb ()

CUDA constexpr INLINE UB &	ub ()

CUDA constexpr INLINE const LB &	lb () const

CUDA constexpr INLINE const UB &	ub () const

constexpr CUDA void	join_top ()

template<class A >
constexpr CUDA bool	join_lb (const A &lb)

template<class A >
constexpr CUDA bool	join_ub (const A &ub)

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

constexpr CUDA void	meet_bot ()

template<class A >
constexpr CUDA bool	meet_lb (const A &lb)

template<class A >
constexpr CUDA bool	meet_ub (const A &ub)

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

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

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

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

CUDA NI void	print () const

constexpr CUDA void	additive_inverse (const this_type &x)

constexpr CUDA void	neg (const local_type &x)

constexpr CUDA void	abs (const local_type &x)

constexpr CUDA void	project (Sig fun, const local_type &x)

constexpr CUDA void	add (const local_type &x, const local_type &y)

constexpr CUDA void	sub (const local_type &x, const local_type &y)

constexpr CUDA void	mul (const local_type &a, const local_type &b)

constexpr CUDA void	div (Sig divfun, const local_type &a, const local_type &b)

constexpr CUDA void	mod (Sig modfun, const local_type &a, const local_type &b)

constexpr CUDA void	pow (const local_type &a, const local_type &b)

constexpr CUDA void	project (Sig fun, const local_type &x, const local_type &y)

constexpr CUDA local_type	width () const

constexpr CUDA local_type	median () const

Static Public Member Functions
constexpr static CUDA local_type	eq_zero ()

constexpr static CUDA local_type	eq_one ()

constexpr static CUDA local_type	bot ()

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

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

static constexpr CUDA bool	is_trivial_fun (Sig fun)

Static Public Attributes
constexpr static const bool	is_abstract_universe = true

constexpr static const bool	sequential = LB::sequential

constexpr static const bool	is_totally_ordered = false

constexpr static const bool	preserve_top = LB::preserve_top && UB::preserve_top

constexpr static const bool	preserve_bot = true

constexpr static const bool	preserve_meet = true

constexpr static const bool	preserve_join = false

constexpr static const bool	injective_concretization = LB::injective_concretization && UB::injective_concretization

constexpr static const bool	preserve_concrete_covers = LB::preserve_concrete_covers && UB::preserve_concrete_covers

constexpr static const bool	complemented = false

constexpr static const bool	is_arithmetic = LB::is_arithmetic && UB::is_arithmetic

constexpr static 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>

◆ value_type

template<class U >

using lala::Interval::value_type = battery::tuple<typename LB::value_type, typename UB::value_type>

◆ memory_type

template<class U >

using lala::Interval::memory_type = typename LB::memory_type

Constructor & Destructor Documentation

◆ Interval() [1/7]

template<class U >

constexpr lala::Interval::Interval ( )

constexprdefault

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

◆ Interval() [2/7]

template<class U >

constexpr lala::Interval::Interval ( const this_type & )

constexprdefault

◆ Interval() [3/7]

template<class U >

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

constexprdefault

◆ Interval() [4/7]

template<class U >

constexpr CUDA 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() [5/7]

template<class U >

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

inlineconstexpr

◆ Interval() [6/7]

template<class U >

template<class A >

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

inlineconstexpr

◆ Interval() [7/7]

template<class U >

template<class A >

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

inlineconstexpr

Member Function Documentation

◆ operator=() [1/3]

template<class U >

template<class A >

constexpr CUDA 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/3]

template<class U >

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

constexprdefault

◆ operator=() [3/3]

template<class U >

constexpr this_type& lala::Interval::operator= ( this_type && )

constexprdefault

◆ eq_zero()

template<class U >

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

inlinestaticconstexpr

Pre-interpreted formula x == 0.

◆ eq_one()

template<class U >

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

inlinestaticconstexpr

Pre-interpreted formula x == 1.

◆ bot()

template<class U >

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

inlinestaticconstexpr

◆ top()

template<class U >

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

inlinestaticconstexpr

◆ is_bot()

template<class U >

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

inlineconstexpr

◆ is_top()

template<class U >

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

inlineconstexpr

◆ value()

template<class U >

constexpr CUDA 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 INLINE LB& lala::Interval::lb ( )

inlineconstexpr

You must use the lattice interface (join/meet 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 INLINE UB& lala::Interval::ub ( )

inlineconstexpr

◆ lb() [2/2]

template<class U >

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

inlineconstexpr

◆ ub() [2/2]

template<class U >

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

inlineconstexpr

◆ join_top()

template<class U >

constexpr CUDA void lala::Interval::join_top ( )

inlineconstexpr

◆ join_lb()

template<class U >

template<class A >

constexpr CUDA bool lala::Interval::join_lb ( const A & lb )

inlineconstexpr

◆ join_ub()

template<class U >

template<class A >

constexpr CUDA bool lala::Interval::join_ub ( const A & ub )

inlineconstexpr

◆ join()

template<class U >

template<class A >

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

inlineconstexpr

◆ meet_bot()

template<class U >

constexpr CUDA void lala::Interval::meet_bot ( )

inlineconstexpr

◆ meet_lb()

template<class U >

template<class A >

constexpr CUDA bool lala::Interval::meet_lb ( const A & lb )

inlineconstexpr

◆ meet_ub()

template<class U >

template<class A >

constexpr CUDA bool lala::Interval::meet_ub ( const A & ub )

inlineconstexpr

◆ meet()

template<class U >

template<class A >

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

inlineconstexpr

◆ extract()

template<class U >

template<class A >

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

inlineconstexpr

◆ deinterpret() [1/2]

template<class U >

template<class Env , class Allocator = typename Env::allocator_type>

CUDA TFormula<Allocator> lala::Interval< U >::deinterpret	(	AVar	x,
		const Env &	env,
		const Allocator &	allocator = `Allocator()`
	)		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

◆ additive_inverse()

template<class U >

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

inlineconstexpr

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 >

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

inlinestaticconstexpr

◆ neg()

template<class U >

constexpr CUDA void lala::Interval::neg ( const local_type & x )

inlineconstexpr

◆ abs()

template<class U >

constexpr CUDA void lala::Interval::abs ( const local_type & x )

inlineconstexpr

◆ project() [1/2]

template<class U >

constexpr CUDA void lala::Interval< U >::project	(	Sig	fun,
		const local_type &	x
	)

inlineconstexpr

◆ add()

template<class U >

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

inlineconstexpr

◆ sub()

template<class U >

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

inlineconstexpr

◆ mul()

template<class U >

constexpr CUDA void lala::Interval< U >::mul	(	const local_type &	a,
		const local_type &	b
	)

inlineconstexpr

◆ div()

template<class U >

constexpr CUDA void lala::Interval< U >::div	(	Sig	divfun,
		const local_type &	a,
		const local_type &	b
	)

inlineconstexpr

◆ mod()

template<class U >

constexpr CUDA void lala::Interval< U >::mod	(	Sig	modfun,
		const local_type &	a,
		const local_type &	b
	)

inlineconstexpr

◆ pow()

template<class U >

constexpr CUDA void lala::Interval< U >::pow	(	const local_type &	a,
		const local_type &	b
	)

inlineconstexpr

◆ is_trivial_fun()

template<class U >

static constexpr CUDA bool lala::Interval::is_trivial_fun ( Sig fun )

inlinestaticconstexpr

◆ project() [2/2]

template<class U >

constexpr CUDA void lala::Interval< U >::project	(	Sig	fun,
		const local_type &	x,
		const local_type &	y
	)

inlineconstexpr

◆ width()

template<class U >

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

inlineconstexpr

◆ median()

template<class U >

constexpr CUDA 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 Function Documentation

◆ Interval

template<class U >

template<class A >

friend class Interval

friend

Member Data Documentation

◆ is_abstract_universe

template<class U >

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

staticconstexpr

◆ sequential

template<class U >

constexpr static const bool lala::Interval::sequential = LB::sequential

staticconstexpr

◆ is_totally_ordered

template<class U >

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

staticconstexpr

◆ preserve_top

template<class U >

constexpr static const bool lala::Interval::preserve_top = LB::preserve_top && UB::preserve_top

staticconstexpr

◆ preserve_bot

template<class U >

constexpr static const bool lala::Interval::preserve_bot = true

staticconstexpr

◆ preserve_meet

template<class U >

constexpr static const bool lala::Interval::preserve_meet = true

staticconstexpr

◆ preserve_join

template<class U >

constexpr static const bool lala::Interval::preserve_join = false

staticconstexpr

◆ injective_concretization

template<class U >

constexpr static const bool lala::Interval::injective_concretization = LB::injective_concretization && UB::injective_concretization

staticconstexpr

◆ preserve_concrete_covers

template<class U >

constexpr static const bool lala::Interval::preserve_concrete_covers = LB::preserve_concrete_covers && UB::preserve_concrete_covers

staticconstexpr

◆ complemented

template<class U >

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

staticconstexpr

◆ is_arithmetic

template<class U >

constexpr static const bool lala::Interval::is_arithmetic = LB::is_arithmetic && UB::is_arithmetic

staticconstexpr

◆ name

template<class U >

constexpr static 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

template<class U> class lala::Interval< U >

Member Typedef Documentation

◆ LB

◆ UB

◆ this_type

◆ local_type

◆ value_type

◆ memory_type

Constructor & Destructor Documentation

◆ Interval() [1/7]

◆ Interval() [2/7]

◆ Interval() [3/7]

◆ Interval() [4/7]

◆ Interval() [5/7]

◆ Interval() [6/7]

◆ Interval() [7/7]

Member Function Documentation

◆ operator=() [1/3]

◆ operator=() [2/3]

◆ operator=() [3/3]

◆ eq_zero()

◆ eq_one()

◆ bot()

◆ top()

◆ is_bot()

◆ is_top()

◆ value()

◆ interpret_tell()

◆ interpret_ask()

◆ interpret()

◆ lb() [1/2]

◆ ub() [1/2]

◆ lb() [2/2]

◆ ub() [2/2]

◆ join_top()

◆ join_lb()

◆ join_ub()

◆ join()

◆ meet_bot()

◆ meet_lb()

◆ meet_ub()

◆ meet()

◆ extract()

◆ deinterpret() [1/2]

◆ deinterpret() [2/2]

◆ print()

◆ additive_inverse()

◆ reverse()

◆ neg()

◆ abs()

◆ project() [1/2]

◆ add()

◆ sub()

◆ mul()

◆ div()

◆ mod()

◆ pow()

◆ is_trivial_fun()

◆ project() [2/2]

◆ width()

◆ median()

Friends And Related Function Documentation

◆ Interval

Member Data Documentation

◆ is_abstract_universe

◆ sequential

◆ is_totally_ordered

◆ preserve_top

◆ preserve_bot

◆ preserve_meet

◆ preserve_join

◆ injective_concretization

◆ preserve_concrete_covers

◆ complemented

template<class U>
class lala::Interval< U >