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

#include <flat_universe.hpp>

Public Types
using	pre_universe = PreUniverse
using	value_type = typename pre_universe::value_type
using	memory_type = Mem
using	this_type = FlatUniverse<pre_universe, memory_type>
template<class M >
using	this_type2 = FlatUniverse<pre_universe, M>
using	local_type = this_type2<battery::local_memory>

Public Member Functions
CUDA constexpr	FlatUniverse ()
CUDA constexpr	FlatUniverse (value_type k)
CUDA constexpr	FlatUniverse (const this_type &other)
CUDA constexpr	FlatUniverse (this_type &&other)
template<class M >
CUDA constexpr	FlatUniverse (const this_type2< M > &other)
template<class M >
CUDA constexpr	FlatUniverse (const ArithBound< pre_universe, M > &other)
template<class M >
CUDA constexpr	FlatUniverse (const ArithBound< typename pre_universe::dual_type, 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	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_type &a)
CUDA constexpr void	project (Sig fun, const local_type &a, const local_type &b)

Static Public Member Functions
static CUDA constexpr local_type	eq_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 &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 &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 Public Attributes
static constexpr const bool	is_abstract_universe = true
static constexpr const bool	sequential = Mem::sequential
static constexpr const bool	is_totally_ordered = false
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 = false
static constexpr const bool	injective_concretization = pre_universe::injective_concretization
static constexpr const bool	preserve_concrete_covers = true
static constexpr const char *	name = "Flat"
static constexpr const bool	is_arithmetic = pre_universe::is_arithmetic

Friends
template<class Pre2 , class Mem2 >
class	FlatUniverse

Member Typedef Documentation

pre_universe

template<class PreUniverse , class Mem >

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

value_type

template<class PreUniverse , class Mem >

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

memory_type

template<class PreUniverse , class Mem >

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

this_type

template<class PreUniverse , class Mem >

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

this_type2

template<class PreUniverse , class Mem >

template<class M >

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

local_type

template<class PreUniverse , class Mem >

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

Constructor & Destructor Documentation

FlatUniverse() [1/7]

template<class PreUniverse , class Mem >

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

inlineconstexpr

Initialize to the top of the flat lattice.

FlatUniverse() [2/7]

template<class PreUniverse , class Mem >

CUDA constexpr lala::FlatUniverse< PreUniverse, Mem >::FlatUniverse ( value_type k )

inlineconstexpr

Similar to \([\![x = k]\!]\) for any name x where \( = \) is the equality.

FlatUniverse() [3/7]

template<class PreUniverse , class Mem >

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

inlineconstexpr

FlatUniverse() [4/7]

template<class PreUniverse , class Mem >

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

inlineconstexpr

FlatUniverse() [5/7]

template<class PreUniverse , class Mem >

template<class M >

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

inlineconstexpr

FlatUniverse() [6/7]

template<class PreUniverse , class Mem >

template<class M >

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

inlineconstexpr

FlatUniverse() [7/7]

template<class PreUniverse , class Mem >

template<class M >

CUDA constexpr lala::FlatUniverse< PreUniverse, Mem >::FlatUniverse ( const ArithBound< typename pre_universe::dual_type, M > & other )

inlineconstexpr

Member Function Documentation

eq_k()

template<class PreUniverse , class Mem >

static CUDA constexpr local_type lala::FlatUniverse< PreUniverse, Mem >::eq_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.

bot()

template<class PreUniverse , class Mem >

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

inlinestaticconstexpr

Similar to \([\![\mathit{false}]\!]\).

top()

template<class PreUniverse , class Mem >

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

inlinestaticconstexpr

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

operator=() [1/2]

template<class PreUniverse , class Mem >

template<class M >

CUDA constexpr this_type & lala::FlatUniverse< 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::FlatUniverse< PreUniverse, Mem >::operator= ( const this_type & other )

inlineconstexpr

value()

template<class PreUniverse , class Mem >

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

inlineconstexpr

operator value_type()

template<class PreUniverse , class Mem >

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

inlineconstexpr

is_top()

template<class PreUniverse , class Mem >

CUDA constexpr local::B lala::FlatUniverse< 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::FlatUniverse< 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::FlatUniverse< PreUniverse, Mem >::join_top ( )

inlineconstexpr

join()

template<class PreUniverse , class Mem >

template<class M1 >

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

inlineconstexpr

meet_bot()

template<class PreUniverse , class Mem >

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

inlineconstexpr

meet()

template<class PreUniverse , class Mem >

template<class M1 >

CUDA constexpr bool lala::FlatUniverse< 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::FlatUniverse< PreUniverse, Mem >::deinterpret ( AVar avar, const Env & env, const Allocator & allocator = Allocator() ) const

inline

Returns

\( x = k \) where x is a variable's name and k the current value. true is returned whenever \( a = \top \), and 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::FlatUniverse< PreUniverse, Mem >::deinterpret ( ) const

inline

Deinterpret the current value to a logical constant.

extract()

template<class PreUniverse , class Mem >

CUDA constexpr bool lala::FlatUniverse< 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::FlatUniverse< 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::FlatUniverse< PreUniverse, Mem >::interpret_tell ( const F & f, const Env & env, this_type2< M2 > & tell, IDiagnostics & diagnostics )

inlinestatic

Expects a predicate of the form x = k or k = x, where x is any variable's name, and k a constant. Existential formula \( \exists{x:T} \) can also be interpreted (only to top).

interpret_ask()

template<class PreUniverse , class Mem >

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

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

inlinestatic

Same as interpret_tell without the support for existential quantifier.

interpret()

template<class PreUniverse , class Mem >

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

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

inlinestatic

project() [1/2]

template<class PreUniverse , class Mem >

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

inlineconstexpr

In-place projection of the result of the unary function fun(a).

project() [2/2]

template<class PreUniverse , class Mem >

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

inlineconstexpr

In-place projection of the result of the binary function fun(a, b).

Friends And Related Symbol Documentation

FlatUniverse

template<class PreUniverse , class Mem >

template<class Pre2 , class Mem2 >

friend class FlatUniverse

friend

Member Data Documentation

is_abstract_universe

template<class PreUniverse , class Mem >

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

staticconstexpr

sequential

template<class PreUniverse , class Mem >

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

staticconstexpr

is_totally_ordered

template<class PreUniverse , class Mem >

const bool lala::FlatUniverse< PreUniverse, Mem >::is_totally_ordered = false

staticconstexpr

preserve_bot

template<class PreUniverse , class Mem >

const bool lala::FlatUniverse< PreUniverse, Mem >::preserve_bot = true

staticconstexpr

preserve_top

template<class PreUniverse , class Mem >

const bool lala::FlatUniverse< PreUniverse, Mem >::preserve_top = true

staticconstexpr

preserve_join

template<class PreUniverse , class Mem >

const bool lala::FlatUniverse< PreUniverse, Mem >::preserve_join = true

staticconstexpr

preserve_meet

template<class PreUniverse , class Mem >

const bool lala::FlatUniverse< PreUniverse, Mem >::preserve_meet = false

staticconstexpr

injective_concretization

template<class PreUniverse , class Mem >

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

staticconstexpr

preserve_concrete_covers

template<class PreUniverse , class Mem >

const bool lala::FlatUniverse< PreUniverse, Mem >::preserve_concrete_covers = true

staticconstexpr

name

template<class PreUniverse , class Mem >

const char* lala::FlatUniverse< PreUniverse, Mem >::name = "Flat"

staticconstexpr

is_arithmetic

template<class PreUniverse , class Mem >

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

staticconstexpr

---

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

• include/lala/universes/arith_bound.hpp
• include/lala/universes/flat_universe.hpp