#include <cartesian_product.hpp>

Public Types
template<size_t i>
using	type_of = typename battery::tuple_element<i, battery::tuple<As...>>::type

using	this_type = CartesianProduct<As...>

using	local_type = CartesianProduct<typename As::local_type...>

using	memory_type = typename type_of<0>::memory_type

using	value_type = battery::tuple<typename As::value_type...>

Public Member Functions
constexpr	CartesianProduct ()=default

CUDA constexpr	CartesianProduct (const As &... as)

CUDA constexpr	CartesianProduct (As &&... as)

CUDA constexpr	CartesianProduct (typename As::value_type... vs)

template<class... Bs>
CUDA constexpr	CartesianProduct (const CartesianProduct< Bs... > &other)

template<class... Bs>
CUDA constexpr	CartesianProduct (CartesianProduct< Bs... > &&other)

template<class... Bs>
CUDA constexpr this_type &	operator= (const CartesianProduct< Bs... > &other)

CUDA constexpr this_type &	operator= (const this_type &other)

template<size_t i>
CUDA constexpr type_of< i > &	project ()

template<size_t i>
CUDA constexpr const type_of< i > &	project () const

CUDA constexpr value_type	value () const

CUDA constexpr local::BInc	is_top () const

CUDA constexpr local::BDec	is_bot () const

CUDA constexpr this_type &	tell_top ()

template<class M , class... Bs>
CUDA constexpr this_type &	tell (const CartesianProduct< Bs... > &other, BInc< M > &has_changed)

template<size_t i, class Ai , class M >
CUDA constexpr this_type &	tell (const Ai &a, BInc< M > &has_changed)

template<class... Bs>
CUDA constexpr this_type &	tell (const CartesianProduct< Bs... > &other)

template<size_t i, class Ai >
CUDA constexpr this_type &	tell (const Ai &a)

CUDA constexpr this_type &	dtell_bot ()

template<class M , class... Bs>
CUDA constexpr this_type &	dtell (const CartesianProduct< Bs... > &other, BInc< M > &has_changed)

template<size_t i, class Ai , class M >
CUDA constexpr this_type &	dtell (const Ai &a, BInc< M > &has_changed)

template<class... Bs>
CUDA constexpr this_type &	dtell (const CartesianProduct< Bs... > &other)

template<size_t i, class Ai >
CUDA constexpr this_type &	dtell (const Ai &a)

template<class... Bs>
CUDA constexpr bool	extract (CartesianProduct< Bs... > &ua) const

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

CUDA void	print () const

Static Public Member Functions
static CUDA constexpr local_type	bot ()

static CUDA constexpr local_type	top ()

template<size_t i, bool diagnose = false, class F , class Env , class... Bs>
static CUDA bool	interpret_one_tell (const F &f, const Env &env, CartesianProduct< Bs... > &k, IDiagnostics &diagnostics)

template<size_t i, bool diagnose = false, class F , class Env , class... Bs>
static CUDA bool	interpret_one_ask (const F &f, const Env &env, CartesianProduct< Bs... > &k, IDiagnostics &diagnostics)

template<IKind kind, bool diagnose = false, class F , class Env , class... Bs>
CUDA static NI bool	interpret (const F &f, const Env &env, CartesianProduct< Bs... > &k, IDiagnostics &diagnostics)

template<bool diagnose, class F , class Env , class... Bs>
static CUDA bool	interpret_tell (const F &f, const Env &env, CartesianProduct< Bs... > &k, IDiagnostics &diagnostics)

template<bool diagnose, class F , class Env , class... Bs>
static CUDA bool	interpret_ask (const F &f, const Env &env, CartesianProduct< Bs... > &k, IDiagnostics &diagnostics)

static CUDA constexpr bool	is_supported_fun (Sig sig)

template<Sig sig, class... Bs>
static CUDA constexpr auto	fun (const CartesianProduct< Bs... > &a)

template<Sig sig, class... As2, class... Bs>
static CUDA constexpr auto	fun (const CartesianProduct< As2... > &a, const CartesianProduct< Bs... > &b)

template<Sig sig, class... As2, class B >
static CUDA constexpr auto	fun (const CartesianProduct< As2... > &a, const B &b)

template<Sig sig, class A , class... Bs>
static CUDA constexpr auto	fun (const A &a, const CartesianProduct< Bs... > &b)

Static Public Attributes
static constexpr size_t	n = battery::tuple_size<battery::tuple<As...>>{}

static constexpr const bool	is_abstract_universe = true

static constexpr const bool	sequential = (... && As::sequential)

static constexpr const bool	is_totally_ordered = false

static constexpr const bool	preserve_bot = (... && As::preserve_bot)

static constexpr const bool	preserve_top = (... && As::preserve_top)

static constexpr const bool	preserve_join = (... && As::preserve_join)

static constexpr const bool	preserve_meet = false

static constexpr const bool	injective_concretization = (... && As::injective_concretization)

static constexpr const bool	preserve_concrete_covers = (... && As::preserve_concrete_covers)

static constexpr const bool	complemented = false

static constexpr const char *	name = "CartesianProduct"

Friends
template<class... Bs>
class	CartesianProduct

Detailed Description

template<class... As>
class lala::CartesianProduct< As >

The Cartesian product abstract domain is a domain transformer combining several abstract domains. Concretization function: \( \gamma((a_1, \ldots, a_n)) = \bigcap_{i \leq n} \gamma_i(a_i) \).

Member Typedef Documentation

◆ type_of

template<class... As>

template<size_t i>

using lala::CartesianProduct< As >::type_of = typename battery::tuple_element<i, battery::tuple<As...>>::type

◆ this_type

template<class... As>

using lala::CartesianProduct< As >::this_type = CartesianProduct<As...>

◆ local_type

template<class... As>

using lala::CartesianProduct< As >::local_type = CartesianProduct<typename As::local_type...>

◆ memory_type

template<class... As>

using lala::CartesianProduct< As >::memory_type = typename type_of<0>::memory_type

◆ value_type

template<class... As>

using lala::CartesianProduct< As >::value_type = battery::tuple<typename As::value_type...>

Constructor & Destructor Documentation

◆ CartesianProduct() [1/6]

template<class... As>

constexpr lala::CartesianProduct< As >::CartesianProduct ( )

constexprdefault

Initialize a Cartesian product to bottom using default constructors.

◆ CartesianProduct() [2/6]

template<class... As>

CUDA constexpr lala::CartesianProduct< As >::CartesianProduct ( const As &... as )

inlineconstexpr

◆ CartesianProduct() [3/6]

template<class... As>

CUDA constexpr lala::CartesianProduct< As >::CartesianProduct ( As &&... as )

inlineconstexpr

◆ CartesianProduct() [4/6]

template<class... As>

CUDA constexpr lala::CartesianProduct< As >::CartesianProduct ( typename As::value_type... vs )

inlineconstexpr

◆ CartesianProduct() [5/6]

template<class... As>

template<class... Bs>

CUDA constexpr lala::CartesianProduct< As >::CartesianProduct ( const CartesianProduct< Bs... > & other )

inlineconstexpr

◆ CartesianProduct() [6/6]

template<class... As>

template<class... Bs>

CUDA constexpr lala::CartesianProduct< As >::CartesianProduct ( CartesianProduct< Bs... > && other )

inlineconstexpr

Member Function Documentation

◆ operator=() [1/2]

template<class... As>

template<class... Bs>

CUDA constexpr this_type & lala::CartesianProduct< As >::operator= ( const CartesianProduct< Bs... > & other )

inlineconstexpr

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

◆ operator=() [2/2]

template<class... As>

CUDA constexpr this_type & lala::CartesianProduct< As >::operator= ( const this_type & other )

inlineconstexpr

◆ bot()

template<class... As>

static CUDA constexpr local_type lala::CartesianProduct< As >::bot ( )

inlinestaticconstexpr

Cartesian product initialized to \( (\bot_1, \ldots, \bot_n) \).

◆ top()

template<class... As>

static CUDA constexpr local_type lala::CartesianProduct< As >::top ( )

inlinestaticconstexpr

Cartesian product initialized to \( (\top_1, \ldots, \top_n) \).

◆ interpret_one_tell()

template<class... As>

template<size_t i, bool diagnose = false, class F , class Env , class... Bs>

static CUDA bool lala::CartesianProduct< As >::interpret_one_tell	(	const F &	f,
		const Env &	env,
		CartesianProduct< Bs... > &	k,
		IDiagnostics &	diagnostics )

inlinestatic

◆ interpret_one_ask()

template<class... As>

template<size_t i, bool diagnose = false, class F , class Env , class... Bs>

static CUDA bool lala::CartesianProduct< As >::interpret_one_ask	(	const F &	f,
		const Env &	env,
		CartesianProduct< Bs... > &	k,
		IDiagnostics &	diagnostics )

inlinestatic

◆ interpret()

template<class... As>

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

CUDA static NI bool lala::CartesianProduct< As >::interpret	(	const F &	f,
		const Env &	env,
		CartesianProduct< Bs... > &	k,
		IDiagnostics &	diagnostics )

inlinestatic

◆ interpret_tell()

template<class... As>

template<bool diagnose, class F , class Env , class... Bs>

static CUDA bool lala::CartesianProduct< As >::interpret_tell	(	const F &	f,
		const Env &	env,
		CartesianProduct< Bs... > &	k,
		IDiagnostics &	diagnostics )

inlinestatic

Interpret the formula f in all sub-universes in which f is interpretable.

◆ interpret_ask()

template<class... As>

template<bool diagnose, class F , class Env , class... Bs>

static CUDA bool lala::CartesianProduct< As >::interpret_ask	(	const F &	f,
		const Env &	env,
		CartesianProduct< Bs... > &	k,
		IDiagnostics &	diagnostics )

inlinestatic

◆ project() [1/2]

template<class... As>

template<size_t i>

CUDA constexpr type_of< i > & lala::CartesianProduct< As >::project ( )

inlineconstexpr

You must use the lattice interface (tell methods) to modify the projected type, if you use assignment you violate the PCCP model.

◆ project() [2/2]

template<class... As>

template<size_t i>

CUDA constexpr const type_of< i > & lala::CartesianProduct< As >::project ( ) const

inlineconstexpr

◆ value()

template<class... As>

CUDA constexpr value_type lala::CartesianProduct< As >::value ( ) const

inlineconstexpr

◆ is_top()

template<class... As>

CUDA constexpr local::BInc lala::CartesianProduct< As >::is_top ( ) const

inlineconstexpr

true if \( \exists{j \geq i},~\gamma(a_j) = \top^\flat \), false otherwise.

◆ is_bot()

template<class... As>

CUDA constexpr local::BDec lala::CartesianProduct< As >::is_bot ( ) const

inlineconstexpr

true if \( \forall{j \geq i},~\gamma(a_j) = \bot^\flat \), false otherwise.

◆ tell_top()

template<class... As>

CUDA constexpr this_type & lala::CartesianProduct< As >::tell_top ( )

inlineconstexpr

◆ tell() [1/4]

template<class... As>

template<class M , class... Bs>

CUDA constexpr this_type & lala::CartesianProduct< As >::tell	(	const CartesianProduct< Bs... > &	other,
		BInc< M > &	has_changed )

inlineconstexpr

◆ tell() [2/4]

template<class... As>

template<size_t i, class Ai , class M >

CUDA constexpr this_type & lala::CartesianProduct< As >::tell	(	const Ai &	a,
		BInc< M > &	has_changed )

inlineconstexpr

◆ tell() [3/4]

template<class... As>

template<class... Bs>

CUDA constexpr this_type & lala::CartesianProduct< As >::tell ( const CartesianProduct< Bs... > & other )

inlineconstexpr

◆ tell() [4/4]

template<class... As>

template<size_t i, class Ai >

CUDA constexpr this_type & lala::CartesianProduct< As >::tell ( const Ai & a )

inlineconstexpr

◆ dtell_bot()

template<class... As>

CUDA constexpr this_type & lala::CartesianProduct< As >::dtell_bot ( )

inlineconstexpr

◆ dtell() [1/4]

template<class... As>

template<class M , class... Bs>

CUDA constexpr this_type & lala::CartesianProduct< As >::dtell	(	const CartesianProduct< Bs... > &	other,
		BInc< M > &	has_changed )

inlineconstexpr

◆ dtell() [2/4]

template<class... As>

template<size_t i, class Ai , class M >

CUDA constexpr this_type & lala::CartesianProduct< As >::dtell	(	const Ai &	a,
		BInc< M > &	has_changed )

inlineconstexpr

◆ dtell() [3/4]

template<class... As>

template<class... Bs>

CUDA constexpr this_type & lala::CartesianProduct< As >::dtell ( const CartesianProduct< Bs... > & other )

inlineconstexpr

◆ dtell() [4/4]

template<class... As>

template<size_t i, class Ai >

CUDA constexpr this_type & lala::CartesianProduct< As >::dtell ( const Ai & a )

inlineconstexpr

◆ extract()

template<class... As>

template<class... Bs>

CUDA constexpr bool lala::CartesianProduct< As >::extract ( CartesianProduct< Bs... > & ua ) const

inlineconstexpr

For correctness, the parameter ua must be stored in a local memory.

◆ is_supported_fun()

template<class... As>

static CUDA constexpr bool lala::CartesianProduct< As >::is_supported_fun ( Sig sig )

inlinestaticconstexpr

◆ fun() [1/4]

template<class... As>

template<Sig sig, class... Bs>

static CUDA constexpr auto lala::CartesianProduct< As >::fun ( const CartesianProduct< Bs... > & a )

inlinestaticconstexpr

Given a product \( (x_1, \ldots, x_n) \), returns \( (f(x_1), \ldots, f(x_n)) \).

◆ fun() [2/4]

template<class... As>

template<Sig sig, class... As2, class... Bs>

static CUDA constexpr auto lala::CartesianProduct< As >::fun	(	const CartesianProduct< As2... > &	a,
		const CartesianProduct< Bs... > &	b )

inlinestaticconstexpr

Given two product \( (x_1, \ldots, x_n) \) and \( (y_1, \ldots, y_n) \), returns \( (f(x_1, y_1), \ldots, f(x_n, y_n)) \). If either the left or right operand is not a product, returns \( (f(x_1, c), \ldots, f(x_n, c)) \) or \( (f(c, y_1), \ldots, f(c, y_n)) \).

◆ fun() [3/4]

template<class... As>

template<Sig sig, class... As2, class B >

static CUDA constexpr auto lala::CartesianProduct< As >::fun	(	const CartesianProduct< As2... > &	a,
		const B &	b )

inlinestaticconstexpr

◆ fun() [4/4]

template<class... As>

template<Sig sig, class A , class... Bs>

static CUDA constexpr auto lala::CartesianProduct< As >::fun	(	const A &	a,
		const CartesianProduct< Bs... > &	b )

inlinestaticconstexpr

◆ deinterpret()

template<class... As>

template<class Env >

CUDA TFormula< typename Env::allocator_type > lala::CartesianProduct< As >::deinterpret	(	AVar	x,
		const Env &	env ) const

inline

◆ print()

template<class... As>

CUDA void lala::CartesianProduct< As >::print ( ) const

inline

Friends And Related Symbol Documentation

◆ CartesianProduct

template<class... As>

template<class... Bs>

friend class CartesianProduct

friend

Member Data Documentation

◆ n

template<class... As>

constexpr size_t lala::CartesianProduct< As >::n = battery::tuple_size<battery::tuple<As...>>{}

staticconstexpr

◆ is_abstract_universe

template<class... As>

constexpr const bool lala::CartesianProduct< As >::is_abstract_universe = true

staticconstexpr

◆ sequential

template<class... As>

constexpr const bool lala::CartesianProduct< As >::sequential = (... && As::sequential)

staticconstexpr

◆ is_totally_ordered

template<class... As>

constexpr const bool lala::CartesianProduct< As >::is_totally_ordered = false

staticconstexpr

◆ preserve_bot

template<class... As>

constexpr const bool lala::CartesianProduct< As >::preserve_bot = (... && As::preserve_bot)

staticconstexpr

◆ preserve_top

template<class... As>

constexpr const bool lala::CartesianProduct< As >::preserve_top = (... && As::preserve_top)

staticconstexpr

◆ preserve_join

template<class... As>

constexpr const bool lala::CartesianProduct< As >::preserve_join = (... && As::preserve_join)

staticconstexpr

◆ preserve_meet

template<class... As>

constexpr const bool lala::CartesianProduct< As >::preserve_meet = false

staticconstexpr

◆ injective_concretization

template<class... As>

constexpr const bool lala::CartesianProduct< As >::injective_concretization = (... && As::injective_concretization)

staticconstexpr

◆ preserve_concrete_covers

template<class... As>

constexpr const bool lala::CartesianProduct< As >::preserve_concrete_covers = (... && As::preserve_concrete_covers)

staticconstexpr

◆ complemented

template<class... As>

constexpr const bool lala::CartesianProduct< As >::complemented = false

staticconstexpr

◆ name

template<class... As>

constexpr const char* lala::CartesianProduct< As >::name = "CartesianProduct"

staticconstexpr

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

include/lala/cartesian_product.hpp

Public Types

Public Member Functions

Static Public Member Functions

Static Public Attributes

Friends

Detailed Description

Member Typedef Documentation

◆ type_of

◆ this_type

◆ local_type

◆ memory_type

◆ value_type

Constructor & Destructor Documentation

◆ CartesianProduct() [1/6]

◆ CartesianProduct() [2/6]

◆ CartesianProduct() [3/6]

◆ CartesianProduct() [4/6]

◆ CartesianProduct() [5/6]

◆ CartesianProduct() [6/6]

Member Function Documentation

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ bot()

◆ top()

◆ interpret_one_tell()

◆ interpret_one_ask()

◆ interpret()

◆ interpret_tell()

◆ interpret_ask()

◆ project() [1/2]

◆ project() [2/2]

◆ value()

◆ is_top()

◆ is_bot()

◆ tell_top()

◆ tell() [1/4]

◆ tell() [2/4]

◆ tell() [3/4]

◆ tell() [4/4]

◆ dtell_bot()

◆ dtell() [1/4]

◆ dtell() [2/4]

◆ dtell() [3/4]

◆ dtell() [4/4]

◆ extract()

◆ is_supported_fun()

◆ fun() [1/4]

◆ fun() [2/4]

◆ fun() [3/4]

◆ fun() [4/4]

◆ deinterpret()

◆ print()

Friends And Related Symbol Documentation

◆ CartesianProduct

Member Data Documentation

◆ n

◆ is_abstract_universe

◆ sequential

◆ is_totally_ordered

◆ preserve_bot

◆ preserve_top

◆ preserve_join

◆ preserve_meet

◆ injective_concretization

◆ preserve_concrete_covers

◆ complemented

◆ name