Lattice Land Core Library
|
#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::B | is_top () const |
CUDA constexpr local::B | is_bot () const |
CUDA constexpr void | join_top () |
template<class... Bs> | |
CUDA constexpr bool | join (const CartesianProduct< Bs... > &other) |
template<size_t i, class Ai > | |
CUDA constexpr bool | join (const Ai &a) |
CUDA constexpr void | meet_bot () |
template<class... Bs> | |
CUDA constexpr bool | meet (const CartesianProduct< Bs... > &other) |
template<size_t i, class Ai > | |
CUDA constexpr bool | meet (const Ai &a) |
template<class... Bs> | |
CUDA constexpr bool | extract (CartesianProduct< Bs... > &ua) const |
template<class... Bs> | |
CUDA constexpr void | project (Sig fun, const CartesianProduct< Bs... > &a) |
template<class... As2, class... Bs> | |
CUDA constexpr void | project (Sig fun, const CartesianProduct< As2... > &a, const CartesianProduct< Bs... > &b) |
template<class... As2, class B > | |
CUDA constexpr void | project (Sig fun, const CartesianProduct< As2... > &a, const B &b) |
template<class A , class... Bs> | |
CUDA constexpr 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 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_trivial_fun (Sig fun) |
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 = false |
static constexpr const bool | preserve_meet = (... && As::preserve_meet) |
static constexpr const bool | injective_concretization = (... && As::injective_concretization) |
static constexpr const bool | preserve_concrete_covers = (... && As::preserve_concrete_covers) |
static constexpr const char * | name = "CartesianProduct" |
Friends | |
template<class... Bs> | |
class | CartesianProduct |
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) \).
using lala::CartesianProduct< As >::type_of = typename battery::tuple_element<i, battery::tuple<As...>>::type |
using lala::CartesianProduct< As >::this_type = CartesianProduct<As...> |
using lala::CartesianProduct< As >::local_type = CartesianProduct<typename As::local_type...> |
using lala::CartesianProduct< As >::memory_type = typename type_of<0>::memory_type |
using lala::CartesianProduct< As >::value_type = battery::tuple<typename As::value_type...> |
|
constexprdefault |
Initialize a Cartesian product to top using default constructors.
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
The assignment operator can only be used in a sequential context. It is monotone but not extensive.
|
inlineconstexpr |
|
inlinestaticconstexpr |
Cartesian product initialized to \( (\bot_1, \ldots, \bot_n) \).
|
inlinestaticconstexpr |
Cartesian product initialized to \( (\top_1, \ldots, \top_n) \).
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
Interpret the formula f
in all sub-universes in which f
is interpretable.
|
inlinestatic |
|
inlineconstexpr |
You must use the lattice interface (tell methods) to modify the projected type, if you use assignment you violate the PCCP model.
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
true
if \( \forall{j},~\gamma(a_j) = U \) with U the universe of discourse of \( a_j \), false
otherwise. @parallel @order-preserving @increasing
|
inlineconstexpr |
true
if \( \exists{j},~\gamma(a_j) = \{\} \), false
otherwise. @parallel @order-preserving @decreasing
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
|
inlineconstexpr |
For correctness, the parameter ua
must be stored in a local memory.
|
inlinestaticconstexpr |
|
inlineconstexpr |
Given a product \( (x_1, \ldots, x_n) \), join in-place \( (fun(x_1), \ldots, fun(x_n)) \).
|
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)) \).
|
inlineconstexpr |
|
inlineconstexpr |
|
inline |
|
inline |
|
staticconstexpr |
|
staticconstexpr |
|
staticconstexpr |
|
staticconstexpr |
|
staticconstexpr |
|
staticconstexpr |
|
staticconstexpr |
|
staticconstexpr |
|
staticconstexpr |
|
staticconstexpr |
|
staticconstexpr |