#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

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

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

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

constexpr	CartesianProduct (const CartesianProduct< As... > &)=default

constexpr	CartesianProduct (CartesianProduct< As... > &&)=default

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

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

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

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

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

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

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

constexpr CUDA value_type	value () const

constexpr CUDA local::B	is_top () const

constexpr CUDA local::B	is_bot () const

constexpr CUDA void	join_top ()

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

template<size_t i, class Ai >
constexpr CUDA bool	join (const Ai &a)

constexpr CUDA void	meet_bot ()

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

template<size_t i, class Ai >
constexpr CUDA bool	meet (const Ai &a)

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

template<class... Bs>
constexpr CUDA void	project (Sig fun, const CartesianProduct< Bs... > &a)

template<class... As2, class... Bs>
constexpr CUDA void	project (Sig fun, const CartesianProduct< As2... > &a, const CartesianProduct< Bs... > &b)

template<class... As2, class B >
constexpr CUDA void	project (Sig fun, const CartesianProduct< As2... > &a, const B &b)

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

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

CUDA void	print () const

Static Public Member Functions
static constexpr CUDA local_type	bot ()

static constexpr CUDA 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 constexpr CUDA bool	is_trivial_fun (Sig fun)

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

constexpr static const bool	is_abstract_universe = true

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

constexpr static const bool	is_totally_ordered = false

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

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

constexpr static const bool	preserve_join = false

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

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

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

constexpr static 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/8]

template<class... As>

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

constexprdefault

Initialize a Cartesian product to top using default constructors.

◆ CartesianProduct() [2/8]

template<class... As>

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

inlineconstexpr

◆ CartesianProduct() [3/8]

template<class... As>

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

inlineconstexpr

◆ CartesianProduct() [4/8]

template<class... As>

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

inlineconstexpr

◆ CartesianProduct() [5/8]

template<class... As>

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

constexprdefault

◆ CartesianProduct() [6/8]

template<class... As>

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

constexprdefault

◆ CartesianProduct() [7/8]

template<class... As>

template<class... Bs>

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

inlineconstexpr

◆ CartesianProduct() [8/8]

template<class... As>

template<class... Bs>

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

inlineconstexpr

Member Function Documentation

◆ operator=() [1/3]

template<class... As>

template<class... Bs>

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

template<class... As>

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

constexprdefault

◆ operator=() [3/3]

template<class... As>

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

constexprdefault

◆ bot()

template<class... As>

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

inlinestaticconstexpr

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

◆ top()

template<class... As>

static constexpr CUDA 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/6]

template<class... As>

template<size_t i>

constexpr CUDA 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/6]

template<class... As>

template<size_t i>

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

inlineconstexpr

◆ value()

template<class... As>

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

inlineconstexpr

◆ is_top()

template<class... As>

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

inlineconstexpr

Returns: true if \( \forall{j},~\gamma(a_j) = U \) with U the universe of discourse of \( a_j \), false otherwise. @parallel @order-preserving @increasing

◆ is_bot()

template<class... As>

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

inlineconstexpr

Returns: true if \( \exists{j},~\gamma(a_j) = \{\} \), false otherwise. @parallel @order-preserving @decreasing

◆ join_top()

template<class... As>

constexpr CUDA void lala::CartesianProduct< As >::join_top ( )

inlineconstexpr

◆ join() [1/2]

template<class... As>

template<class... Bs>

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

inlineconstexpr

◆ join() [2/2]

template<class... As>

template<size_t i, class Ai >

constexpr CUDA bool lala::CartesianProduct< As >::join ( const Ai & a )

inlineconstexpr

◆ meet_bot()

template<class... As>

constexpr CUDA void lala::CartesianProduct< As >::meet_bot ( )

inlineconstexpr

◆ meet() [1/2]

template<class... As>

template<class... Bs>

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

inlineconstexpr

◆ meet() [2/2]

template<class... As>

template<size_t i, class Ai >

constexpr CUDA bool lala::CartesianProduct< As >::meet ( const Ai & a )

inlineconstexpr

◆ extract()

template<class... As>

template<class... Bs>

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

inlineconstexpr

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

◆ is_trivial_fun()

template<class... As>

static constexpr CUDA bool lala::CartesianProduct< As >::is_trivial_fun ( Sig fun )

inlinestaticconstexpr

◆ project() [3/6]

template<class... As>

template<class... Bs>

constexpr CUDA void lala::CartesianProduct< As >::project	(	Sig	fun,
		const CartesianProduct< Bs... > &	a
	)

inlineconstexpr

Given a product \( (x_1, \ldots, x_n) \), join in-place \( (fun(x_1), \ldots, fun(x_n)) \).

◆ project() [4/6]

template<class... As>

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

constexpr CUDA void lala::CartesianProduct< As >::project	(	Sig	fun,
		const CartesianProduct< As2... > &	a,
		const CartesianProduct< Bs... > &	b
	)

inlineconstexpr

Given two product \( (x_1, \ldots, x_n) \) and \( (y_1, \ldots, y_n) \), join in-place \( (fun(x_1, y_1), \ldots, fun(x_n, y_n)) \). If either the left or right operand is not a product, join in-place \( (fun(x_1, c), \ldots, fun(x_n, c)) \) or \( (fun(c, y_1), \ldots, fun(c, y_n)) \).

◆ project() [5/6]

template<class... As>

template<class... As2, class B >

constexpr CUDA void lala::CartesianProduct< As >::project	(	Sig	fun,
		const CartesianProduct< As2... > &	a,
		const B &	b
	)

inlineconstexpr

◆ project() [6/6]

template<class... As>

template<class A , class... Bs>

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

inlineconstexpr

◆ deinterpret()

template<class... As>

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

CUDA TFormula<Allocator> lala::CartesianProduct< As >::deinterpret	(	AVar	x,
		const Env &	env,
		const Allocator &	allocator = `Allocator()`
	)		const

inline

◆ print()

template<class... As>

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

inline

Friends And Related Function Documentation

◆ CartesianProduct

template<class... As>

template<class... Bs>

friend class CartesianProduct

friend

Member Data Documentation

◆ n

template<class... As>

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

staticconstexpr

◆ is_abstract_universe

template<class... As>

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

staticconstexpr

◆ sequential

template<class... As>

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

staticconstexpr

◆ is_totally_ordered

template<class... As>

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

staticconstexpr

◆ preserve_bot

template<class... As>

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

staticconstexpr

◆ preserve_top

template<class... As>

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

staticconstexpr

◆ preserve_join

template<class... As>

constexpr static const bool lala::CartesianProduct< As >::preserve_join = false

staticconstexpr

◆ preserve_meet

template<class... As>

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

staticconstexpr

◆ injective_concretization

template<class... As>

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

staticconstexpr

◆ preserve_concrete_covers

template<class... As>

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

staticconstexpr

◆ name

template<class... As>

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

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

Member Typedef Documentation

◆ type_of

◆ this_type

◆ local_type

◆ memory_type

◆ value_type

Constructor & Destructor Documentation

◆ CartesianProduct() [1/8]

◆ CartesianProduct() [2/8]

◆ CartesianProduct() [3/8]

◆ CartesianProduct() [4/8]

◆ CartesianProduct() [5/8]

◆ CartesianProduct() [6/8]

◆ CartesianProduct() [7/8]

◆ CartesianProduct() [8/8]

Member Function Documentation

◆ operator=() [1/3]

◆ operator=() [2/3]

◆ operator=() [3/3]

◆ bot()

◆ top()

◆ interpret_one_tell()

◆ interpret_one_ask()

◆ interpret()

◆ interpret_tell()

◆ interpret_ask()

◆ project() [1/6]

◆ project() [2/6]

◆ value()

◆ is_top()

◆ is_bot()

◆ join_top()

◆ join() [1/2]

◆ join() [2/2]

◆ meet_bot()

◆ meet() [1/2]

◆ meet() [2/2]

◆ extract()

◆ is_trivial_fun()

◆ project() [3/6]

◆ project() [4/6]

◆ project() [5/6]

◆ project() [6/6]

◆ deinterpret()

◆ print()

Friends And Related Function 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

◆ name

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