lala::ArithBound< PreUniverse, Mem > Class Template Reference

#include <arith_bound.hpp>

Public Types
using	pre_universe = PreUniverse
using	value_type = typename pre_universe::value_type
using	memory_type = Mem
using	this_type = ArithBound<pre_universe, memory_type>
using	dual_type = ArithBound<typename pre_universe::dual_type, memory_type>
template<class M >
using	this_type2 = ArithBound<pre_universe, M>
using	local_type = this_type2<battery::local_memory>
template<class M >
using	flat_type = FlatUniverse<typename pre_universe::upper_bound_type, M>
using	local_flat_type = flat_type<battery::local_memory>
using	atomic_type = memory_type::template atomic_type<value_type>

Public Member Functions
CUDA constexpr	ArithBound ()
CUDA constexpr	ArithBound (value_type x)
CUDA constexpr	ArithBound (const this_type &other)
constexpr	ArithBound (this_type &&other)=default
template<class M >
CUDA constexpr	ArithBound (const this_type2< M > &other)
template<class M >
CUDA constexpr this_type &	operator= (const this_type2< M > &other)
CUDA constexpr this_type &	operator= (const this_type &other)
CUDA constexpr value_type	value () const
CUDA constexpr atomic_type &	atomic ()
CUDA constexpr	operator value_type () const
CUDA constexpr local::B	is_top () const
CUDA constexpr local::B	is_bot () const
CUDA constexpr void	join_top ()
template<class M1 >
CUDA constexpr bool	join (const this_type2< M1 > &other)
CUDA constexpr void	meet_bot ()
template<class M1 >
CUDA constexpr bool	meet (const this_type2< M1 > &other)
template<class Env , class Allocator = typename Env::allocator_type>
CUDA NI TFormula< Allocator >	deinterpret (AVar avar, const Env &env, const Allocator &allocator=Allocator()) const
template<class F >
CUDA NI F	deinterpret () const
CUDA constexpr bool	extract (local_type &ua) const
CUDA NI void	print () const
CUDA constexpr void	project (Sig fun, const local_flat_type &a)
CUDA constexpr void	project (Sig fun, const local_flat_type &a, const local_flat_type &b)
CUDA constexpr void	project (Sig fun, const local_type &a, const local_type &b)
CUDA constexpr void	project (Sig fun, const local_type &a)

Static Public Member Functions
static CUDA constexpr this_type	geq_k (value_type k)
static CUDA constexpr this_type	leq_k (value_type k)
static CUDA constexpr local_type	bot ()
static CUDA constexpr local_type	top ()
template<bool diagnose = false, class F , class Env , class M2 >
CUDA static NI bool	interpret_tell (const F &f, const Env &, this_type2< M2 > &tell, IDiagnostics &diagnostics)
template<bool diagnose = false, class F , class Env , class M2 >
CUDA static NI bool	interpret_ask (const F &f, const Env &, this_type2< M2 > &ask, IDiagnostics &diagnostics)
template<IKind kind, bool diagnose = false, class F , class Env , class M2 >
CUDA static NI bool	interpret (const F &f, const Env &env, this_type2< M2 > &value, IDiagnostics &diagnostics)
static CUDA constexpr local_type	next (const this_type2< Mem > &a)
static CUDA constexpr local_type	prev (const this_type2< Mem > &a)
static CUDA constexpr bool	is_trivial_fun (Sig fun)
static CUDA constexpr bool	is_order_preserving_fun (Sig fun)

Static Public Attributes
static constexpr const bool	is_abstract_universe = true
static constexpr const bool	sequential = Mem::sequential
static constexpr const bool	is_totally_ordered = pre_universe::is_totally_ordered
static constexpr const bool	preserve_bot = pre_universe::preserve_bot
static constexpr const bool	preserve_top = pre_universe::preserve_top
static constexpr const bool	preserve_join = pre_universe::preserve_join
static constexpr const bool	preserve_meet = pre_universe::preserve_meet
static constexpr const bool	injective_concretization = pre_universe::injective_concretization
static constexpr const bool	preserve_concrete_covers = pre_universe::preserve_concrete_covers
static constexpr const bool	is_lower_bound = pre_universe::is_lower_bound
static constexpr const bool	is_upper_bound = pre_universe::is_upper_bound
static constexpr const char *	name = pre_universe::name
static constexpr const bool	is_arithmetic = pre_universe::is_arithmetic

Friends
template<class Pre2 , class Mem2 >
class	ArithBound

Member Typedef Documentation

pre_universe

template<class PreUniverse , class Mem >

using lala::ArithBound< PreUniverse, Mem >::pre_universe = PreUniverse

value_type

template<class PreUniverse , class Mem >

using lala::ArithBound< PreUniverse, Mem >::value_type = typename pre_universe::value_type

memory_type

template<class PreUniverse , class Mem >

using lala::ArithBound< PreUniverse, Mem >::memory_type = Mem

this_type

template<class PreUniverse , class Mem >

using lala::ArithBound< PreUniverse, Mem >::this_type = ArithBound<pre_universe, memory_type>

dual_type

template<class PreUniverse , class Mem >

using lala::ArithBound< PreUniverse, Mem >::dual_type = ArithBound<typename pre_universe::dual_type, memory_type>

this_type2

template<class PreUniverse , class Mem >

template<class M >

using lala::ArithBound< PreUniverse, Mem >::this_type2 = ArithBound<pre_universe, M>

local_type

template<class PreUniverse , class Mem >

using lala::ArithBound< PreUniverse, Mem >::local_type = this_type2<battery::local_memory>

flat_type

template<class PreUniverse , class Mem >

template<class M >

using lala::ArithBound< PreUniverse, Mem >::flat_type = FlatUniverse<typename pre_universe::upper_bound_type, M>

local_flat_type

template<class PreUniverse , class Mem >

using lala::ArithBound< PreUniverse, Mem >::local_flat_type = flat_type<battery::local_memory>

atomic_type

template<class PreUniverse , class Mem >

using lala::ArithBound< PreUniverse, Mem >::atomic_type = memory_type::template atomic_type<value_type>

Constructor & Destructor Documentation

ArithBound() [1/5]

template<class PreUniverse , class Mem >

CUDA constexpr lala::ArithBound< PreUniverse, Mem >::ArithBound ( )

inlineconstexpr

Initialize an upset universe to top.

ArithBound() [2/5]

template<class PreUniverse , class Mem >

CUDA constexpr lala::ArithBound< PreUniverse, Mem >::ArithBound ( value_type x )

inlineconstexpr

Similar to \([\![x \leq_A i]\!]\) for any name x where \( \leq_A \) is the lattice order.

ArithBound() [3/5]

template<class PreUniverse , class Mem >

CUDA constexpr lala::ArithBound< PreUniverse, Mem >::ArithBound ( const this_type & other )

inlineconstexpr

ArithBound() [4/5]

template<class PreUniverse , class Mem >

lala::ArithBound< PreUniverse, Mem >::ArithBound ( this_type && other )

constexprdefault

ArithBound() [5/5]

template<class PreUniverse , class Mem >

template<class M >

CUDA constexpr lala::ArithBound< PreUniverse, Mem >::ArithBound ( const this_type2< M > & other )

inlineconstexpr

Member Function Documentation

geq_k()

template<class PreUniverse , class Mem >

static CUDA constexpr this_type lala::ArithBound< PreUniverse, Mem >::geq_k ( value_type k )

inlinestaticconstexpr

A pre-interpreted formula x >= value ready to use. This is mainly for optimization purpose to avoid calling interpret each time we need it.

leq_k()

template<class PreUniverse , class Mem >

static CUDA constexpr this_type lala::ArithBound< PreUniverse, Mem >::leq_k ( value_type k )

inlinestaticconstexpr

bot()

template<class PreUniverse , class Mem >

static CUDA constexpr local_type lala::ArithBound< PreUniverse, Mem >::bot ( )

inlinestaticconstexpr

Similar to \([\![\mathit{false}]\!]\) if preserve_bot is true.

top()

template<class PreUniverse , class Mem >

static CUDA constexpr local_type lala::ArithBound< PreUniverse, Mem >::top ( )

inlinestaticconstexpr

Similar to \([\![\mathit{true}]\!]\) if preserve_top is true.

operator=() [1/2]

template<class PreUniverse , class Mem >

template<class M >

CUDA constexpr this_type & lala::ArithBound< PreUniverse, Mem >::operator= ( const this_type2< M > & other )

inlineconstexpr

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

operator=() [2/2]

template<class PreUniverse , class Mem >

CUDA constexpr this_type & lala::ArithBound< PreUniverse, Mem >::operator= ( const this_type & other )

inlineconstexpr

value()

template<class PreUniverse , class Mem >

CUDA constexpr value_type lala::ArithBound< PreUniverse, Mem >::value ( ) const

inlineconstexpr

atomic()

template<class PreUniverse , class Mem >

CUDA constexpr atomic_type & lala::ArithBound< PreUniverse, Mem >::atomic ( )

inlineconstexpr

operator value_type()

template<class PreUniverse , class Mem >

CUDA constexpr lala::ArithBound< PreUniverse, Mem >::operator value_type ( ) const

inlineconstexpr

is_top()

template<class PreUniverse , class Mem >

CUDA constexpr local::B lala::ArithBound< PreUniverse, Mem >::is_top ( ) const

inlineconstexpr

Returns

true whenever \( a = \top \), false otherwise. @parallel @order-preserving @increasing

is_bot()

template<class PreUniverse , class Mem >

CUDA constexpr local::B lala::ArithBound< PreUniverse, Mem >::is_bot ( ) const

inlineconstexpr

Returns

true whenever \( a = \bot \), false otherwise. @parallel @order-preserving @decreasing

join_top()

template<class PreUniverse , class Mem >

CUDA constexpr void lala::ArithBound< PreUniverse, Mem >::join_top ( )

inlineconstexpr

join()

template<class PreUniverse , class Mem >

template<class M1 >

CUDA constexpr bool lala::ArithBound< PreUniverse, Mem >::join ( const this_type2< M1 > & other )

inlineconstexpr

meet_bot()

template<class PreUniverse , class Mem >

CUDA constexpr void lala::ArithBound< PreUniverse, Mem >::meet_bot ( )

inlineconstexpr

meet()

template<class PreUniverse , class Mem >

template<class M1 >

CUDA constexpr bool lala::ArithBound< PreUniverse, Mem >::meet ( const this_type2< M1 > & other )

inlineconstexpr

deinterpret() [1/2]

template<class PreUniverse , class Mem >

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

CUDA NI TFormula< Allocator > lala::ArithBound< PreUniverse, Mem >::deinterpret ( AVar avar, const Env & env, const Allocator & allocator = Allocator() ) const

inline

Returns

\( x <op> i \) where x is a variable's name, i the current value and <op> depends on the underlying universe. If U preserves top, true is returned whenever \( a = \top \), if it preserves bottom false is returned whenever \( a = \bot \). We always return an exact approximation, hence for any formula \( \llbracket \varphi \rrbracket = a \), we must have \( a = \llbracket \rrbracket a \llbracket \rrbracket \) where \( \rrbracket a \llbracket \) is the deinterpretation function.

deinterpret() [2/2]

template<class PreUniverse , class Mem >

template<class F >

CUDA NI F lala::ArithBound< PreUniverse, Mem >::deinterpret ( ) const

inline

Deinterpret the current value to a logical constant.

extract()

template<class PreUniverse , class Mem >

CUDA constexpr bool lala::ArithBound< PreUniverse, Mem >::extract ( local_type & ua ) const

inlineconstexpr

Under-approximates the current element \( a \) w.r.t. \( \rrbracket a \llbracket \) into ua. For this abstract universe, it always returns true since the current element \( a \) is an exact representation of \( \rrbracket a \llbracket \).

print()

template<class PreUniverse , class Mem >

CUDA NI void lala::ArithBound< PreUniverse, Mem >::print ( ) const

inline

Print the current element.

interpret_tell()

template<class PreUniverse , class Mem >

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

CUDA static NI bool lala::ArithBound< PreUniverse, Mem >::interpret_tell ( const F & f, const Env & , this_type2< M2 > & tell, IDiagnostics & diagnostics )

inlinestatic

Expects a predicate of the form x <op> k where x is any variable's name, and k a constant. The symbol <op> is expected to be U::sig_order(), U::sig_strict_order(), = or in. Existential formula \( \exists{x:T} \) can also be interpreted (only to top) depending on the underlying pre-universe.

interpret_ask()

template<class PreUniverse , class Mem >

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

CUDA static NI bool lala::ArithBound< PreUniverse, Mem >::interpret_ask ( const F & f, const Env & , this_type2< M2 > & ask, IDiagnostics & diagnostics )

inlinestatic

Expects a predicate of the form x <op> k where x is any variable's name, and k a constant. The symbol <op> is expected to be U::sig_order(), U::sig_strict_order() or !=.

interpret()

template<class PreUniverse , class Mem >

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

CUDA static NI bool lala::ArithBound< PreUniverse, Mem >::interpret ( const F & f, const Env & env, this_type2< M2 > & value, IDiagnostics & diagnostics )

inlinestatic

next()

template<class PreUniverse , class Mem >

static CUDA constexpr local_type lala::ArithBound< PreUniverse, Mem >::next ( const this_type2< Mem > & a )

inlinestaticconstexpr

prev()

template<class PreUniverse , class Mem >

static CUDA constexpr local_type lala::ArithBound< PreUniverse, Mem >::prev ( const this_type2< Mem > & a )

inlinestaticconstexpr

project() [1/4]

template<class PreUniverse , class Mem >

CUDA constexpr void lala::ArithBound< PreUniverse, Mem >::project ( Sig fun, const local_flat_type & a )

inlineconstexpr

Unary function of type fun: FlatUniverse -> ArithBound. If a is bot, we meet with bottom in-place. Otherwise, we apply the function fun to a and meet the result.

Remarks

The result of the function is always over-approximated (or exact when possible).

project() [2/4]

template<class PreUniverse , class Mem >

CUDA constexpr void lala::ArithBound< PreUniverse, Mem >::project ( Sig fun, const local_flat_type & a, const local_flat_type & b )

inlineconstexpr

Binary functions of type project: FlatUniverse x FlatUniverse -> ArithBound. If a or b is bot, we meet bottom in-place. Otherwise, we meet fun(a,b) in-place.

Remarks

The result of the function is always over-approximated (or exact when possible).

If the function fun is partial (e.g. division), we expect the arguments a and b to be in the domain of fun (e.g. not equal to 0).

is_trivial_fun()

template<class PreUniverse , class Mem >

static CUDA constexpr bool lala::ArithBound< PreUniverse, Mem >::is_trivial_fun ( Sig fun )

inlinestaticconstexpr

In this universe, the non-trivial order-preserving functions are {min, max, +}.

is_order_preserving_fun()

template<class PreUniverse , class Mem >

static CUDA constexpr bool lala::ArithBound< PreUniverse, Mem >::is_order_preserving_fun ( Sig fun )

inlinestaticconstexpr

The functions that are order-preserving on the natural order of the universe of discourse, and its dual.

project() [3/4]

template<class PreUniverse , class Mem >

CUDA constexpr void lala::ArithBound< PreUniverse, Mem >::project ( Sig fun, const local_type & a, const local_type & b )

inlineconstexpr

project() [4/4]

template<class PreUniverse , class Mem >

CUDA constexpr void lala::ArithBound< PreUniverse, Mem >::project ( Sig fun, const local_type & a )

inlineconstexpr

Friends And Related Symbol Documentation

ArithBound

template<class PreUniverse , class Mem >

template<class Pre2 , class Mem2 >

friend class ArithBound

friend

Member Data Documentation

is_abstract_universe

template<class PreUniverse , class Mem >

const bool lala::ArithBound< PreUniverse, Mem >::is_abstract_universe = true

staticconstexpr

sequential

template<class PreUniverse , class Mem >

const bool lala::ArithBound< PreUniverse, Mem >::sequential = Mem::sequential

staticconstexpr

is_totally_ordered

template<class PreUniverse , class Mem >

const bool lala::ArithBound< PreUniverse, Mem >::is_totally_ordered = pre_universe::is_totally_ordered

staticconstexpr

preserve_bot

template<class PreUniverse , class Mem >

const bool lala::ArithBound< PreUniverse, Mem >::preserve_bot = pre_universe::preserve_bot

staticconstexpr

preserve_top

template<class PreUniverse , class Mem >

const bool lala::ArithBound< PreUniverse, Mem >::preserve_top = pre_universe::preserve_top

staticconstexpr

preserve_join

template<class PreUniverse , class Mem >

const bool lala::ArithBound< PreUniverse, Mem >::preserve_join = pre_universe::preserve_join

staticconstexpr

preserve_meet

template<class PreUniverse , class Mem >

const bool lala::ArithBound< PreUniverse, Mem >::preserve_meet = pre_universe::preserve_meet

staticconstexpr

injective_concretization

template<class PreUniverse , class Mem >

const bool lala::ArithBound< PreUniverse, Mem >::injective_concretization = pre_universe::injective_concretization

staticconstexpr

preserve_concrete_covers

template<class PreUniverse , class Mem >

const bool lala::ArithBound< PreUniverse, Mem >::preserve_concrete_covers = pre_universe::preserve_concrete_covers

staticconstexpr

is_lower_bound

template<class PreUniverse , class Mem >

const bool lala::ArithBound< PreUniverse, Mem >::is_lower_bound = pre_universe::is_lower_bound

staticconstexpr

is_upper_bound

template<class PreUniverse , class Mem >

const bool lala::ArithBound< PreUniverse, Mem >::is_upper_bound = pre_universe::is_upper_bound

staticconstexpr

name

template<class PreUniverse , class Mem >

const char* lala::ArithBound< PreUniverse, Mem >::name = pre_universe::name

staticconstexpr

is_arithmetic

template<class PreUniverse , class Mem >

const bool lala::ArithBound< PreUniverse, Mem >::is_arithmetic = pre_universe::is_arithmetic

staticconstexpr

---

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

• include/lala/universes/arith_bound.hpp