#include <primitive_upset.hpp>

Public Types
using	pre_universe = PreUniverse

using	value_type = typename pre_universe::value_type

using	memory_type = Mem

using	this_type = PrimitiveUpset<pre_universe, memory_type>

using	dual_type = PrimitiveUpset<typename pre_universe::dual_type, memory_type>

template<class M >
using	this_type2 = PrimitiveUpset<pre_universe, M>

using	local_type = this_type2<battery::local_memory>

template<class M >
using	flat_type = FlatUniverse<typename pre_universe::increasing_type, M>

Public Member Functions
CUDA constexpr	PrimitiveUpset ()

CUDA constexpr	PrimitiveUpset (value_type x)

CUDA constexpr	PrimitiveUpset (const this_type &other)

constexpr	PrimitiveUpset (this_type &&other)=default

template<class M >
CUDA constexpr	PrimitiveUpset (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	operator value_type () const

CUDA constexpr local::BInc	is_top () const

CUDA constexpr local::BDec	is_bot () const

CUDA constexpr this_type &	tell_top ()

template<class M1 , class M2 >
CUDA constexpr this_type &	tell (const this_type2< M1 > &other, BInc< M2 > &has_changed)

template<class M1 >
CUDA constexpr this_type &	tell (const this_type2< M1 > &other)

CUDA constexpr this_type &	dtell_bot ()

template<class M1 , class M2 >
CUDA constexpr this_type &	dtell (const this_type2< M1 > &other, BInc< M2 > &has_changed)

template<class M1 >
CUDA constexpr this_type &	dtell (const this_type2< M1 > &other)

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

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

CUDA constexpr bool	extract (local_type &ua) const

CUDA NI void	print () const

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 bool	is_supported_fun (Sig sig)

static CUDA constexpr local_type	next (const this_type2< Mem > &a)

static CUDA constexpr local_type	prev (const this_type2< Mem > &a)

template<Sig sig, class M >
static CUDA constexpr local_type	fun (const flat_type< M > &a)

template<Sig sig, class M1 , class M2 >
static CUDA constexpr local_type	fun (const flat_type< M1 > &a, const flat_type< M2 > &b)

template<Sig sig, class Pre1 , class Mem1 , class Pre2 , class Mem2 >
static CUDA constexpr local_type	guarded_div (const PrimitiveUpset< Pre1, Mem1 > &a, const PrimitiveUpset< Pre2, Mem2 > &b)

template<Sig sig, class M1 , class M2 >
static CUDA constexpr local_type	fun (const this_type2< M1 > &a, const this_type2< M2 > &b)

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	complemented = pre_universe::complemented

static constexpr const bool	increasing = pre_universe::increasing

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	PrimitiveUpset

Member Typedef Documentation

◆ pre_universe

template<class PreUniverse , class Mem >

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

◆ value_type

template<class PreUniverse , class Mem >

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

◆ memory_type

template<class PreUniverse , class Mem >

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

◆ this_type

template<class PreUniverse , class Mem >

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

◆ dual_type

template<class PreUniverse , class Mem >

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

◆ this_type2

template<class PreUniverse , class Mem >

template<class M >

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

◆ local_type

template<class PreUniverse , class Mem >

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

◆ flat_type

template<class PreUniverse , class Mem >

template<class M >

using lala::PrimitiveUpset< PreUniverse, Mem >::flat_type = FlatUniverse<typename pre_universe::increasing_type, M>

Constructor & Destructor Documentation

◆ PrimitiveUpset() [1/5]

template<class PreUniverse , class Mem >

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

inlineconstexpr

Initialize an upset universe to bottom.

◆ PrimitiveUpset() [2/5]

template<class PreUniverse , class Mem >

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

inlineconstexpr

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

◆ PrimitiveUpset() [3/5]

template<class PreUniverse , class Mem >

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

inlineconstexpr

◆ PrimitiveUpset() [4/5]

template<class PreUniverse , class Mem >

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

constexprdefault

◆ PrimitiveUpset() [5/5]

template<class PreUniverse , class Mem >

template<class M >

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

inlineconstexpr

Member Function Documentation

◆ geq_k()

template<class PreUniverse , class Mem >

static CUDA constexpr this_type lala::PrimitiveUpset< 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::PrimitiveUpset< PreUniverse, Mem >::leq_k ( value_type k )

inlinestaticconstexpr

◆ bot()

template<class PreUniverse , class Mem >

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

inlinestaticconstexpr

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

◆ top()

template<class PreUniverse , class Mem >

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

inlinestaticconstexpr

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

◆ operator=() [1/2]

template<class PreUniverse , class Mem >

template<class M >

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

inlineconstexpr

◆ value()

template<class PreUniverse , class Mem >

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

inlineconstexpr

◆ operator value_type()

template<class PreUniverse , class Mem >

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

inlineconstexpr

◆ is_top()

template<class PreUniverse , class Mem >

CUDA constexpr local::BInc lala::PrimitiveUpset< PreUniverse, Mem >::is_top ( ) const

inlineconstexpr

true whenever \( a = \top \), false otherwise.

◆ is_bot()

template<class PreUniverse , class Mem >

CUDA constexpr local::BDec lala::PrimitiveUpset< PreUniverse, Mem >::is_bot ( ) const

inlineconstexpr

true whenever \( a = \bot \), false otherwise.

◆ tell_top()

template<class PreUniverse , class Mem >

CUDA constexpr this_type & lala::PrimitiveUpset< PreUniverse, Mem >::tell_top ( )

inlineconstexpr

◆ tell() [1/2]

template<class PreUniverse , class Mem >

template<class M1 , class M2 >

CUDA constexpr this_type & lala::PrimitiveUpset< PreUniverse, Mem >::tell	(	const this_type2< M1 > &	other,
		BInc< M2 > &	has_changed )

inlineconstexpr

◆ tell() [2/2]

template<class PreUniverse , class Mem >

template<class M1 >

CUDA constexpr this_type & lala::PrimitiveUpset< PreUniverse, Mem >::tell ( const this_type2< M1 > & other )

inlineconstexpr

◆ dtell_bot()

template<class PreUniverse , class Mem >

CUDA constexpr this_type & lala::PrimitiveUpset< PreUniverse, Mem >::dtell_bot ( )

inlineconstexpr

◆ dtell() [1/2]

template<class PreUniverse , class Mem >

template<class M1 , class M2 >

CUDA constexpr this_type & lala::PrimitiveUpset< PreUniverse, Mem >::dtell	(	const this_type2< M1 > &	other,
		BInc< M2 > &	has_changed )

inlineconstexpr

◆ dtell() [2/2]

template<class PreUniverse , class Mem >

template<class M1 >

CUDA constexpr this_type & lala::PrimitiveUpset< PreUniverse, Mem >::dtell ( const this_type2< M1 > & other )

inlineconstexpr

◆ deinterpret() [1/2]

template<class PreUniverse , class Mem >

template<class Env >

CUDA NI TFormula< typename Env::allocator_type > lala::PrimitiveUpset< PreUniverse, Mem >::deinterpret	(	AVar	avar,
		const Env &	env ) const

inline

Returns: \( x \geq i \) where x is a variable's name and i the current value. If U preserves bottom true is returned whenever \( a = \bot \), if it preserves top false is returned whenever \( a = \top \). 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::PrimitiveUpset< PreUniverse, Mem >::deinterpret ( ) const

inline

Deinterpret the current value to a logical constant.

◆ extract()

template<class PreUniverse , class Mem >

CUDA constexpr bool lala::PrimitiveUpset< 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::PrimitiveUpset< 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::PrimitiveUpset< 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, k <op> x or x in 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() and =. Existential formula \( \exists{x:T} \) can also be interpreted (only to bottom) 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::PrimitiveUpset< 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 or k <op> x, 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::PrimitiveUpset< PreUniverse, Mem >::interpret	(	const F &	f,
		const Env &	env,
		this_type2< M2 > &	value,
		IDiagnostics &	diagnostics )

inlinestatic

◆ is_supported_fun()

template<class PreUniverse , class Mem >

static CUDA constexpr bool lala::PrimitiveUpset< PreUniverse, Mem >::is_supported_fun ( Sig sig )

inlinestaticconstexpr

◆ next()

template<class PreUniverse , class Mem >

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

inlinestaticconstexpr

◆ prev()

template<class PreUniverse , class Mem >

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

inlinestaticconstexpr

◆ fun() [1/3]

template<class PreUniverse , class Mem >

template<Sig sig, class M >

static CUDA constexpr local_type lala::PrimitiveUpset< PreUniverse, Mem >::fun ( const flat_type< M > & a )

inlinestaticconstexpr

Unary function of type Sig: FlatUniverse -> PrimitiveUpset.

Returns: If a is bot, we return the bottom element of the upset lattice; and dually for top. Otherwise, we apply the function Sig to a and return the result.

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

◆ fun() [2/3]

template<class PreUniverse , class Mem >

template<Sig sig, class M1 , class M2 >

static CUDA constexpr local_type lala::PrimitiveUpset< PreUniverse, Mem >::fun	(	const flat_type< M1 > &	a,
		const flat_type< M2 > &	b )

inlinestaticconstexpr

Binary functions of type Sig: FlatUniverse x FlatUniverse -> PrimitiveUpset.

Returns: If a or b is bot, we return the bottom element of the upset lattice; and dually for top. Otherwise, we apply the function Sig to a and b and return the result.

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

◆ guarded_div()

template<class PreUniverse , class Mem >

template<Sig sig, class Pre1 , class Mem1 , class Pre2 , class Mem2 >

static CUDA constexpr local_type lala::PrimitiveUpset< PreUniverse, Mem >::guarded_div	(	const PrimitiveUpset< Pre1, Mem1 > &	a,
		const PrimitiveUpset< Pre2, Mem2 > &	b )

inlinestaticconstexpr

Given two values a and b, we perform the division while taking care of the case where b == 0. When b != 0, the result is fun<sig>(a, b). Otherwise, the result depends on the type of a and b:

`a`	`b`	local_type	Result
Inc	Inc	Inc	0
Inc	Dec	Dec	0
Dec	Dec	Inc	0
Dec	Inc	Dec	0
-	-	-	bot()

◆ fun() [3/3]

template<class PreUniverse , class Mem >

template<Sig sig, class M1 , class M2 >

static CUDA constexpr local_type lala::PrimitiveUpset< PreUniverse, Mem >::fun	(	const this_type2< M1 > &	a,
		const this_type2< M2 > &	b )

inlinestaticconstexpr

Friends And Related Symbol Documentation

◆ PrimitiveUpset

template<class PreUniverse , class Mem >

template<class Pre2 , class Mem2 >

friend class PrimitiveUpset

friend

Member Data Documentation

◆ is_abstract_universe

template<class PreUniverse , class Mem >

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

staticconstexpr

◆ sequential

template<class PreUniverse , class Mem >

constexpr const bool lala::PrimitiveUpset< PreUniverse, Mem >::sequential = Mem::sequential

staticconstexpr

◆ is_totally_ordered

template<class PreUniverse , class Mem >

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

staticconstexpr

◆ preserve_bot

template<class PreUniverse , class Mem >

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

staticconstexpr

◆ preserve_top

template<class PreUniverse , class Mem >

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

staticconstexpr

◆ preserve_join

template<class PreUniverse , class Mem >

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

staticconstexpr

◆ preserve_meet

template<class PreUniverse , class Mem >

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

staticconstexpr

◆ injective_concretization

template<class PreUniverse , class Mem >

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

staticconstexpr

◆ preserve_concrete_covers

template<class PreUniverse , class Mem >

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

staticconstexpr

◆ complemented

template<class PreUniverse , class Mem >

constexpr const bool lala::PrimitiveUpset< PreUniverse, Mem >::complemented = pre_universe::complemented

staticconstexpr

◆ increasing

template<class PreUniverse , class Mem >

constexpr const bool lala::PrimitiveUpset< PreUniverse, Mem >::increasing = pre_universe::increasing

staticconstexpr

◆ name

template<class PreUniverse , class Mem >

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

staticconstexpr

◆ is_arithmetic

template<class PreUniverse , class Mem >

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

staticconstexpr

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

include/lala/universes/primitive_upset.hpp

Public Types

Public Member Functions

Static Public Member Functions

Static Public Attributes

Friends

Member Typedef Documentation

◆ pre_universe

◆ value_type

◆ memory_type

◆ this_type

◆ dual_type

◆ this_type2

◆ local_type

◆ flat_type

Constructor & Destructor Documentation

◆ PrimitiveUpset() [1/5]

◆ PrimitiveUpset() [2/5]

◆ PrimitiveUpset() [3/5]

◆ PrimitiveUpset() [4/5]

◆ PrimitiveUpset() [5/5]

Member Function Documentation

◆ geq_k()

◆ leq_k()

◆ bot()

◆ top()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ value()

◆ operator value_type()

◆ is_top()

◆ is_bot()

◆ tell_top()

◆ tell() [1/2]

◆ tell() [2/2]

◆ dtell_bot()

◆ dtell() [1/2]

◆ dtell() [2/2]

◆ deinterpret() [1/2]

◆ deinterpret() [2/2]

◆ extract()

◆ print()

◆ interpret_tell()

◆ interpret_ask()

◆ interpret()

◆ is_supported_fun()

◆ next()

◆ prev()

◆ fun() [1/3]

◆ fun() [2/3]

◆ guarded_div()

◆ fun() [3/3]

Friends And Related Symbol Documentation

◆ PrimitiveUpset

Member Data Documentation

◆ is_abstract_universe

◆ sequential

◆ is_totally_ordered

◆ preserve_bot

◆ preserve_top

◆ preserve_join

◆ preserve_meet

◆ injective_concretization

◆ preserve_concrete_covers

◆ complemented

◆ increasing

◆ name

◆ is_arithmetic