Lattice Land Powerdomains Library
Loading...
Searching...
No Matches
Classes | Public Types | Public Member Functions | Static Public Member Functions | Static Public Attributes | Friends | List of all members
lala::Tables< A, U, Allocator > Class Template Reference

#include <tables.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 = Tables<sub_type, universe_type, allocator_type>
 
using table_type
 
using table_headers = battery::vector<battery::vector<int, allocator_type>, allocator_type>
 
using table_collection_type = battery::vector<table_type, allocator_type>
 
using bitset_type = battery::dynamic_bitset<memory_type, allocator_type>
 

Public Member Functions

CUDA Tables (AType uid, AType store_aty, sub_ptr sub, const allocator_type &alloc=allocator_type())
 
CUDA Tables (AType uid, sub_ptr sub, const allocator_type &alloc=allocator_type())
 
template<class A2 , class U2 , class Alloc2 , class... Allocators>
CUDA NI Tables (const Tables< 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_table, battery::vector< battery::vector< local_universe, Alloc >, Alloc > &ask_table, const F &f, Env &env, IDiagnostics &diagnostics) 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)
 
template<class Alloc >
CUDA local::BInc ask (const ask_type< Alloc > &a) const
 
template<class Mem >
CUDA void crefine (size_t table_num, size_t col, BInc< Mem > &has_changed)
 
template<class Mem >
CUDA void lrefine (size_t table_num, size_t row, size_t col, BInc< Mem > &has_changed)
 
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 = "Tables"
 

Friends

template<class A2 , class U2 , class Alloc2 >
class Tables
 

Detailed Description

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

The tables 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.

Member Typedef Documentation

◆ allocator_type

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

◆ sub_allocator_type

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
using lala::Tables< A, U, Allocator >::sub_allocator_type = typename A::allocator_type

◆ universe_type

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

◆ local_universe

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
using lala::Tables< A, U, Allocator >::local_universe = typename universe_type::local_type

◆ sub_universe_type

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
using lala::Tables< A, U, Allocator >::sub_universe_type = typename A::universe_type

◆ sub_local_universe

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
using lala::Tables< A, U, Allocator >::sub_local_universe = typename sub_universe_type::local_type

◆ memory_type

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
using lala::Tables< A, U, Allocator >::memory_type = typename universe_type::memory_type

◆ sub_type

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
using lala::Tables< A, U, Allocator >::sub_type = A

◆ sub_ptr

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
using lala::Tables< A, U, Allocator >::sub_ptr = abstract_ptr<sub_type>

◆ this_type

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
using lala::Tables< A, U, Allocator >::this_type = Tables<sub_type, universe_type, allocator_type>

◆ table_type

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
using lala::Tables< A, U, Allocator >::table_type
Initial value:
battery::vector<
battery::vector<universe_type, allocator_type>,
allocator_type>
lala::Tables::allocator_type
Allocator allocator_type
Definition tables.hpp:34

◆ table_headers

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
using lala::Tables< A, U, Allocator >::table_headers = battery::vector<battery::vector<int, allocator_type>, allocator_type>

◆ table_collection_type

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
using lala::Tables< A, U, Allocator >::table_collection_type = battery::vector<table_type, allocator_type>

◆ bitset_type

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
using lala::Tables< A, U, Allocator >::bitset_type = battery::dynamic_bitset<memory_type, allocator_type>

Constructor & Destructor Documentation

◆ Tables() [1/3]

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
CUDA lala::Tables< A, U, Allocator >::Tables ( AType uid,
AType store_aty,
sub_ptr sub,
const allocator_type & alloc = allocator_type() )
inline

◆ Tables() [2/3]

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
CUDA lala::Tables< A, U, Allocator >::Tables ( AType uid,
sub_ptr sub,
const allocator_type & alloc = allocator_type() )
inline

◆ Tables() [3/3]

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
template<class A2 , class U2 , class Alloc2 , class... Allocators>
CUDA NI lala::Tables< A, U, Allocator >::Tables ( const Tables< A2, U2, Alloc2 > & other,
AbstractDeps< Allocators... > & deps )
inline

Member Function Documentation

◆ aty()

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
CUDA AType lala::Tables< A, U, Allocator >::aty ( ) const
inline

◆ get_allocator()

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
CUDA allocator_type lala::Tables< A, U, Allocator >::get_allocator ( ) const
inline

◆ subdomain()

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
CUDA sub_ptr lala::Tables< A, U, Allocator >::subdomain ( ) const
inline

◆ is_bot()

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
CUDA local::BDec lala::Tables< A, U, Allocator >::is_bot ( ) const
inline

◆ is_top()

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
CUDA local::BInc lala::Tables< A, U, Allocator >::is_top ( ) const
inline

◆ bot() [1/2]

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
static CUDA this_type lala::Tables< A, U, Allocator >::bot ( AType atype = UNTYPED,
AType atype_sub = UNTYPED,
const allocator_type & alloc = allocator_type(),
const sub_allocator_type & sub_alloc = sub_allocator_type() )
inlinestatic

◆ top() [1/2]

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
static CUDA this_type lala::Tables< A, U, Allocator >::top ( AType atype = UNTYPED,
AType atype_sub = UNTYPED,
const allocator_type & alloc = allocator_type(),
const sub_allocator_type & sub_alloc = sub_allocator_type() )
inlinestatic

A special symbolic element representing top.

◆ bot() [2/2]

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
template<class Env >
static CUDA this_type lala::Tables< A, U, Allocator >::bot ( Env & env,
const allocator_type & alloc = allocator_type(),
const sub_allocator_type & sub_alloc = sub_allocator_type() )
inlinestatic

◆ top() [2/2]

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
template<class Env >
static CUDA this_type lala::Tables< A, U, Allocator >::top ( Env & env,
const allocator_type & alloc = allocator_type(),
const sub_allocator_type & sub_alloc = sub_allocator_type() )
inlinestatic

◆ snapshot()

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
template<class Alloc2 = allocator_type>
CUDA snapshot_type< Alloc2 > lala::Tables< A, U, Allocator >::snapshot ( const Alloc2 & alloc = Alloc2()) const
inline

◆ restore()

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
template<class Alloc2 >
CUDA void lala::Tables< A, U, Allocator >::restore ( const snapshot_type< Alloc2 > & snap)
inline

◆ flatten_and()

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
template<class F >
CUDA void lala::Tables< A, U, Allocator >::flatten_and ( const F & f,
typename F::Sequence & conjuncts ) const
inline

◆ flatten_or()

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
template<class F >
CUDA void lala::Tables< A, U, Allocator >::flatten_or ( const F & f,
typename F::Sequence & disjuncts ) const
inline

◆ flatten()

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
template<class F >
CUDA F lala::Tables< A, U, Allocator >::flatten ( const F & f,
const typename F::allocator_type & alloc ) const
inline

◆ interpret_atom()

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
template<IKind kind, bool diagnose = false, class F , class Env , class Alloc >
CUDA NI bool lala::Tables< A, U, Allocator >::interpret_atom ( battery::vector< AVar, Alloc > & header,
battery::vector< battery::vector< local_universe, Alloc >, Alloc > & tell_table,
battery::vector< battery::vector< local_universe, Alloc >, Alloc > & ask_table,
const F & f,
Env & env,
IDiagnostics & diagnostics ) const
inline

◆ interpret()

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
template<IKind kind, bool diagnose = false, class F , class Env , class I >
CUDA NI bool lala::Tables< A, U, Allocator >::interpret ( const F & f2,
Env & env,
I & intermediate,
IDiagnostics & diagnostics ) const
inline

◆ interpret_ask()

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
template<bool diagnose = false, class F , class Env , class Alloc >
CUDA NI bool lala::Tables< A, U, Allocator >::interpret_ask ( const F & f,
const Env & env,
ask_type< Alloc > & ask,
IDiagnostics & diagnostics ) const
inline

◆ interpret_tell()

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
template<bool diagnose = false, class F , class Env , class Alloc >
CUDA NI bool lala::Tables< A, U, Allocator >::interpret_tell ( const F & f,
Env & env,
tell_type< Alloc > & tell,
IDiagnostics & diagnostics ) const
inline

◆ operator[]()

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
CUDA const sub_universe_type & lala::Tables< A, U, Allocator >::operator[] ( int x) const
inline

◆ vars()

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
CUDA size_t lala::Tables< A, U, Allocator >::vars ( ) const
inline

◆ num_tables()

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
CUDA size_t lala::Tables< A, U, Allocator >::num_tables ( ) const
inline

◆ tell() [1/4]

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
template<class Alloc , class Mem >
CUDA this_type & lala::Tables< A, U, Allocator >::tell ( const tell_type< Alloc > & t,
BInc< Mem > & has_changed )
inline

◆ tell() [2/4]

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
template<class Alloc >
CUDA this_type & lala::Tables< A, U, Allocator >::tell ( const tell_type< Alloc > & t)
inline

◆ tell() [3/4]

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
CUDA this_type & lala::Tables< A, U, Allocator >::tell ( AVar x,
const sub_universe_type & dom )
inline

◆ tell() [4/4]

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
template<class Mem >
CUDA this_type & lala::Tables< A, U, Allocator >::tell ( AVar x,
const sub_universe_type & dom,
BInc< Mem > & has_changed )
inline

◆ ask()

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
template<class Alloc >
CUDA local::BInc lala::Tables< A, U, Allocator >::ask ( const ask_type< Alloc > & a) const
inline

◆ crefine()

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
template<class Mem >
CUDA void lala::Tables< A, U, Allocator >::crefine ( size_t table_num,
size_t col,
BInc< Mem > & has_changed )
inline

◆ lrefine()

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
template<class Mem >
CUDA void lala::Tables< A, U, Allocator >::lrefine ( size_t table_num,
size_t row,
size_t col,
BInc< Mem > & has_changed )
inline

◆ num_refinements()

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
CUDA size_t lala::Tables< A, U, Allocator >::num_refinements ( ) const
inline

◆ refine()

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
template<class Mem >
CUDA void lala::Tables< A, U, Allocator >::refine ( size_t i,
BInc< Mem > & has_changed )
inline

◆ is_extractable()

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
template<class ExtractionStrategy = NonAtomicExtraction>
CUDA bool lala::Tables< A, U, Allocator >::is_extractable ( const ExtractionStrategy & strategy = ExtractionStrategy()) const
inline

◆ extract()

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
template<class B >
CUDA void lala::Tables< A, U, Allocator >::extract ( B & ua) const
inline

Extract an under-approximation if the last node popped \( a \) is an under-approximation. If B is a search tree, the under-approximation consists in a search tree \( \{a\} \) with a single node, in that case, ua must be different from top.

◆ project()

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
CUDA sub_universe_type lala::Tables< A, U, Allocator >::project ( AVar x) const
inline

◆ deinterpret()

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
template<class Env >
CUDA NI TFormula< typename Env::allocator_type > lala::Tables< A, U, Allocator >::deinterpret ( const Env & env) const
inline

Friends And Related Symbol Documentation

◆ Tables

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
template<class A2 , class U2 , class Alloc2 >
friend class Tables
friend

Member Data Documentation

◆ is_abstract_universe

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
const bool lala::Tables< A, U, Allocator >::is_abstract_universe = false
staticconstexpr

◆ sequential

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
const bool lala::Tables< A, U, Allocator >::sequential = sub_type::sequential
staticconstexpr

◆ is_totally_ordered

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
const bool lala::Tables< A, U, Allocator >::is_totally_ordered = false
staticconstexpr

◆ preserve_bot

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
const bool lala::Tables< A, U, Allocator >::preserve_bot = sub_type::preserve_bot
staticconstexpr

◆ preserve_top

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
const bool lala::Tables< A, U, Allocator >::preserve_top = sub_type::preserve_top
staticconstexpr

◆ preserve_join

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
const bool lala::Tables< A, U, Allocator >::preserve_join = sub_type::preserve_join
staticconstexpr

◆ preserve_meet

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
const bool lala::Tables< A, U, Allocator >::preserve_meet = sub_type::preserve_meet
staticconstexpr

◆ injective_concretization

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
const bool lala::Tables< A, U, Allocator >::injective_concretization = sub_type::injective_concretization
staticconstexpr

◆ preserve_concrete_covers

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
const bool lala::Tables< A, U, Allocator >::preserve_concrete_covers = sub_type::preserve_concrete_covers
staticconstexpr

◆ name

template<class A , class U = typename A::universe_type, class Allocator = typename A::allocator_type>
const char* lala::Tables< A, U, Allocator >::name = "Tables"
staticconstexpr
The documentation for this class was generated from the following file: