#include <table.hpp>

Classes
struct	ask_type

struct	snapshot_type

struct	tell_type

Public Types
using	allocator_type = Allocator

using	sub_allocator_type = typename A::allocator_type

using	universe_type = U

using	local_universe = typename universe_type::local_type

using	sub_universe_type = typename A::universe_type

using	sub_local_universe = typename sub_universe_type::local_type

using	memory_type = typename universe_type::memory_type

using	sub_type = A

using	sub_ptr = abstract_ptr< sub_type >

using	this_type = Table< sub_type, universe_type, allocator_type >

using	table_type = battery::vector< universe_type, allocator_type >

using	bitset_type = battery::dynamic_bitset< memory_type, allocator_type >

Public Member Functions
CUDA	Table (AType uid, AType store_aty, sub_ptr sub, const allocator_type &alloc=allocator_type())

CUDA	Table (AType uid, sub_ptr sub, const allocator_type &alloc=allocator_type())

template<class A2 , class U2 , class Alloc2 , class... Allocators>
CUDA NI	Table (const Table< A2, U2, Alloc2 > &other, AbstractDeps< Allocators... > &deps)

CUDA AType	aty () const

CUDA allocator_type	get_allocator () const

CUDA sub_ptr	subdomain () const

CUDA local::BDec	is_bot () const

CUDA local::BInc	is_top () const

template<class Alloc2 = allocator_type>
CUDA snapshot_type< Alloc2 >	snapshot (const Alloc2 &alloc=Alloc2()) const

template<class Alloc2 >
CUDA void	restore (const snapshot_type< Alloc2 > &snap)

template<class F >
CUDA void	flatten_and (const F &f, typename F::Sequence &conjuncts) const

template<class F >
CUDA void	flatten_or (const F &f, typename F::Sequence &disjuncts) const

template<class F >
CUDA F	flatten (const F &f, const typename F::allocator_type &alloc) const

template<IKind kind, bool diagnose = false, class F , class Env , class Alloc >
CUDA NI bool	interpret_atom (battery::vector< AVar, Alloc > &header, battery::vector< battery::vector< local_universe, Alloc >, Alloc > &tell_table2, battery::vector< battery::vector< local_universe, Alloc >, Alloc > &ask_table2, const F &f, Env &env, IDiagnostics &diagnostics) const

template<class Alloc1 , class Alloc2 >
CUDA battery::vector< local_universe, Alloc2 >	flatten_table (const battery::vector< battery::vector< local_universe, Alloc1 >, Alloc1 > &table, const Alloc2 &alloc) const

template<IKind kind, bool diagnose = false, class F , class Env , class I >
CUDA NI bool	interpret (const F &f2, Env &env, I &intermediate, IDiagnostics &diagnostics) const

template<bool diagnose = false, class F , class Env , class Alloc >
CUDA NI bool	interpret_ask (const F &f, const Env &env, ask_type< Alloc > &ask, IDiagnostics &diagnostics) const

template<bool diagnose = false, class F , class Env , class Alloc >
CUDA NI bool	interpret_tell (const F &f, Env &env, tell_type< Alloc > &tell, IDiagnostics &diagnostics) const

CUDA const sub_universe_type &	operator[] (int x) const

CUDA size_t	vars () const

CUDA size_t	num_tables () const

template<class Alloc , class Mem >
CUDA this_type &	tell (const tell_type< Alloc > &t, BInc< Mem > &has_changed)

template<class Alloc >
CUDA this_type &	tell (const tell_type< Alloc > &t)

CUDA this_type &	tell (AVar x, const sub_universe_type &dom)

template<class Mem >
CUDA this_type &	tell (AVar x, const sub_universe_type &dom, BInc< Mem > &has_changed)

CUDA size_t	to1D (int i, int j) const

template<class Alloc >
CUDA local::BInc	ask (const ask_type< Alloc > &a) const

CUDA size_t	num_refinements () const

template<class Mem >
CUDA void	refine (size_t i, BInc< Mem > &has_changed)

template<class ExtractionStrategy = NonAtomicExtraction>
CUDA bool	is_extractable (const ExtractionStrategy &strategy=ExtractionStrategy()) const

template<class B >
CUDA void	extract (B &ua) const

CUDA sub_universe_type	project (AVar x) const

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

Static Public Member Functions
static CUDA this_type	bot (AType atype=UNTYPED, AType atype_sub=UNTYPED, const allocator_type &alloc=allocator_type(), const sub_allocator_type &sub_alloc=sub_allocator_type())

static CUDA this_type	top (AType atype=UNTYPED, AType atype_sub=UNTYPED, const allocator_type &alloc=allocator_type(), const sub_allocator_type &sub_alloc=sub_allocator_type())

template<class Env >
static CUDA this_type	bot (Env &env, const allocator_type &alloc=allocator_type(), const sub_allocator_type &sub_alloc=sub_allocator_type())

template<class Env >
static CUDA this_type	top (Env &env, const allocator_type &alloc=allocator_type(), const sub_allocator_type &sub_alloc=sub_allocator_type())

Static Public Attributes
static constexpr const bool	is_abstract_universe = false

static constexpr const bool	sequential = sub_type::sequential

static constexpr const bool	is_totally_ordered = false

static constexpr const bool	preserve_bot = sub_type::preserve_bot

static constexpr const bool	preserve_top = sub_type::preserve_top

static constexpr const bool	preserve_join = sub_type::preserve_join

static constexpr const bool	preserve_meet = sub_type::preserve_meet

static constexpr const bool	injective_concretization = sub_type::injective_concretization

static constexpr const bool	preserve_concrete_covers = sub_type::preserve_concrete_covers

static constexpr const char *	name = "Table"

Friends
template<class A2 , class U2 , class Alloc2 >
class	Table

Detailed Description

template<class A, class U = typename A::universe_type, class Allocator = typename A::allocator_type>
class lala::Table< A, U, Allocator >

The table abstract domain is designed to represent predicates in extension by listing all their solutions explicitly. It is inspired by the table global constraint and generalizes it by lifting each element of the table to a lattice element. We expect U to be equally or less expressive than A::universe_type, this is because we compute the meet in A::universe_type and not in U.