#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

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)

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

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

CUDA constexpr local::B	is_bot () const

CUDA constexpr local::B	is_top () const

CUDA constexpr value_type	value () const

CUDA INLINE constexpr LB &	lb ()

CUDA INLINE constexpr UB &	ub ()

CUDA INLINE constexpr const LB &	lb () const

CUDA INLINE constexpr const UB &	ub () const

CUDA constexpr void	join_top ()

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

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

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

CUDA constexpr void	meet_bot ()

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

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

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

template<class A >
CUDA constexpr 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

CUDA constexpr void	additive_inverse (const this_type &x)

CUDA constexpr void	neg (const local_type &x)

CUDA constexpr void	abs (const local_type &x)

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

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

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

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

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

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

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

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

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)

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

static CUDA constexpr bool	is_trivial_fun (Sig fun)

Static Public Attributes
static constexpr const bool	is_abstract_universe = true

static constexpr const bool	sequential = LB::sequential

static constexpr const bool	is_totally_ordered = false

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

static constexpr const bool	preserve_bot = true

static constexpr const bool	preserve_meet = true

static constexpr const bool	preserve_join = false

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

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

static constexpr const bool	complemented = false

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

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>

◆ 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 >

lala::Interval::Interval ( )

constexprdefault

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

◆ Interval() [2/7]

template<class U >

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

constexprdefault

◆ Interval() [3/7]

template<class U >

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

constexprdefault

◆ Interval() [4/7]

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

template<class U >

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

inlineconstexpr

◆ Interval() [6/7]

template<class U >

template<class A >

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

inlineconstexpr

◆ Interval() [7/7]

template<class U >

template<class A >

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

inlineconstexpr

Member Function Documentation

◆ operator=() [1/3]

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

template<class U >

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

constexprdefault

◆ operator=() [3/3]

template<class U >

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

constexprdefault

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

template<class U >

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

inlineconstexpr

◆ is_top()

template<class U >

CUDA constexpr local::B lala::Interval::is_top ( ) 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 INLINE constexpr 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 INLINE constexpr UB & lala::Interval::ub ( )

inlineconstexpr

◆ lb() [2/2]

template<class U >

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

inlineconstexpr

◆ ub() [2/2]

template<class U >

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

inlineconstexpr

◆ join_top()

template<class U >

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

inlineconstexpr

◆ join_lb()

template<class U >

template<class A >

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

inlineconstexpr

◆ join_ub()

template<class U >

template<class A >

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

inlineconstexpr

◆ join()

template<class U >

template<class A >

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

inlineconstexpr

◆ meet_bot()

template<class U >

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

inlineconstexpr

◆ meet_lb()

template<class U >

template<class A >

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

inlineconstexpr

◆ meet_ub()

template<class U >

template<class A >

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

inlineconstexpr

◆ meet()

template<class U >

template<class A >

CUDA constexpr bool lala::Interval::meet ( 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 , 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 >

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

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

inlinestaticconstexpr

◆ neg()

template<class U >

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

inlineconstexpr

◆ abs()

template<class U >

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

inlineconstexpr

◆ project() [1/2]

template<class U >

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

inlineconstexpr

◆ add()

template<class U >

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

inlineconstexpr

◆ sub()

template<class U >

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

inlineconstexpr

◆ mul()

template<class U >

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

inlineconstexpr

◆ div()

template<class U >

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

inlineconstexpr

◆ mod()

template<class U >

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

inlineconstexpr

◆ pow()

template<class U >

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

inlineconstexpr

◆ is_trivial_fun()

template<class U >

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

inlinestaticconstexpr

◆ project() [2/2]

template<class U >

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

inlineconstexpr

◆ 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 >

const bool lala::Interval::is_abstract_universe = true

staticconstexpr

◆ sequential

template<class U >

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

staticconstexpr

◆ is_totally_ordered

template<class U >

const bool lala::Interval::is_totally_ordered = false

staticconstexpr

◆ preserve_top

template<class U >

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

staticconstexpr

◆ preserve_bot

template<class U >

const bool lala::Interval::preserve_bot = true

staticconstexpr

◆ preserve_meet

template<class U >

const bool lala::Interval::preserve_meet = true

staticconstexpr

◆ preserve_join

template<class U >

const bool lala::Interval::preserve_join = false

staticconstexpr

◆ injective_concretization

template<class U >

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

staticconstexpr

◆ preserve_concrete_covers

template<class U >

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

staticconstexpr

◆ complemented

template<class U >

const bool lala::Interval::complemented = false

staticconstexpr

◆ is_arithmetic

template<class U >

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

staticconstexpr

◆ name

template<class U >

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

◆ 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 Symbol 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

◆ is_arithmetic