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

#include <search_tree.hpp>

Classes

struct  snapshot_type
 
struct  tell_type
 

Public Types

using allocator_type = Allocator
 
using sub_allocator_type = typename A::allocator_type
 
using split_type = Split
 
using branch_type = typename split_type::branch_type
 
using universe_type = typename A::universe_type
 
using local_universe = typename universe_type::local_type
 
using sub_type = A
 
using sub_ptr = abstract_ptr<sub_type>
 
using split_ptr = abstract_ptr<split_type>
 
using this_type = SearchTree<sub_type, split_type, allocator_type>
 
template<class Alloc >
using ask_type = typename A::template ask_type<Alloc>
 

Public Member Functions

CUDA SearchTree (AType uid, sub_ptr a, split_ptr split, const allocator_type &alloc=allocator_type())
 
template<class A2 , class S2 , class Alloc2 , class... Allocators>
CUDA NI SearchTree (const SearchTree< A2, S2, Alloc2 > &other, AbstractDeps< Allocators... > &deps)
 
CUDA AType aty () const
 
CUDA allocator_type get_allocator () const
 
CUDA local::B is_singleton () const
 
CUDA local::B is_top () const
 
CUDA local::B is_bot () 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<bool diagnose = false, class F , class Env , class Alloc2 >
CUDA NI bool interpret_tell (const F &f, Env &env, tell_type< Alloc2 > &tell, IDiagnostics &diagnostics) const
 
template<bool diagnose = false, class F , class Env , class Alloc2 >
CUDA NI bool interpret_ask (const F &f, Env &env, ask_type< Alloc2 > &ask, IDiagnostics &diagnostics) const
 
template<IKind kind, bool diagnose = false, class F , class Env , class I >
CUDA NI bool interpret (const F &f, Env &env, I &intermediate, IDiagnostics &diagnostics) const
 
template<class Alloc >
CUDA local::B deduce (const tell_type< Alloc > &t)
 
CUDA bool deduce ()
 
template<class ExtractionStrategy = NonAtomicExtraction>
CUDA bool is_extractable (const ExtractionStrategy &strategy=ExtractionStrategy()) const
 
template<class B >
CUDA void extract (B &ua) const
 
CUDA local_universe project (AVar x) const
 
template<class Univ >
CUDA void project (AVar x, Univ &r) const
 
CUDA size_t depth () const
 

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 = true
 
static constexpr const bool preserve_top = true
 
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 = "SearchTree"
 

Friends

template<class A2 , class S2 , class Alloc2 >
class SearchTree
 

Member Typedef Documentation

◆ allocator_type

template<class A , class Split , class Allocator = typename A::allocator_type>
using lala::SearchTree< A, Split, Allocator >::allocator_type = Allocator

◆ sub_allocator_type

template<class A , class Split , class Allocator = typename A::allocator_type>
using lala::SearchTree< A, Split, Allocator >::sub_allocator_type = typename A::allocator_type

◆ split_type

template<class A , class Split , class Allocator = typename A::allocator_type>
using lala::SearchTree< A, Split, Allocator >::split_type = Split

◆ branch_type

template<class A , class Split , class Allocator = typename A::allocator_type>
using lala::SearchTree< A, Split, Allocator >::branch_type = typename split_type::branch_type

◆ universe_type

template<class A , class Split , class Allocator = typename A::allocator_type>
using lala::SearchTree< A, Split, Allocator >::universe_type = typename A::universe_type

◆ local_universe

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

◆ sub_type

template<class A , class Split , class Allocator = typename A::allocator_type>
using lala::SearchTree< A, Split, Allocator >::sub_type = A

◆ sub_ptr

template<class A , class Split , class Allocator = typename A::allocator_type>
using lala::SearchTree< A, Split, Allocator >::sub_ptr = abstract_ptr<sub_type>

◆ split_ptr

template<class A , class Split , class Allocator = typename A::allocator_type>
using lala::SearchTree< A, Split, Allocator >::split_ptr = abstract_ptr<split_type>

◆ this_type

template<class A , class Split , class Allocator = typename A::allocator_type>
using lala::SearchTree< A, Split, Allocator >::this_type = SearchTree<sub_type, split_type, allocator_type>

◆ ask_type

template<class A , class Split , class Allocator = typename A::allocator_type>
template<class Alloc >
using lala::SearchTree< A, Split, Allocator >::ask_type = typename A::template ask_type<Alloc>

Constructor & Destructor Documentation

◆ SearchTree() [1/2]

template<class A , class Split , class Allocator = typename A::allocator_type>
CUDA lala::SearchTree< A, Split, Allocator >::SearchTree ( AType uid,
sub_ptr a,
split_ptr split,
const allocator_type & alloc = allocator_type() )
inline

◆ SearchTree() [2/2]

template<class A , class Split , class Allocator = typename A::allocator_type>
template<class A2 , class S2 , class Alloc2 , class... Allocators>
CUDA NI lala::SearchTree< A, Split, Allocator >::SearchTree ( const SearchTree< A2, S2, Alloc2 > & other,
AbstractDeps< Allocators... > & deps )
inline

Member Function Documentation

◆ aty()

template<class A , class Split , class Allocator = typename A::allocator_type>
CUDA AType lala::SearchTree< A, Split, Allocator >::aty ( ) const
inline

◆ get_allocator()

template<class A , class Split , class Allocator = typename A::allocator_type>
CUDA allocator_type lala::SearchTree< A, Split, Allocator >::get_allocator ( ) const
inline

◆ is_singleton()

template<class A , class Split , class Allocator = typename A::allocator_type>
CUDA local::B lala::SearchTree< A, Split, Allocator >::is_singleton ( ) const
inline

◆ is_top()

template<class A , class Split , class Allocator = typename A::allocator_type>
CUDA local::B lala::SearchTree< A, Split, Allocator >::is_top ( ) const
inline

◆ is_bot()

template<class A , class Split , class Allocator = typename A::allocator_type>
CUDA local::B lala::SearchTree< A, Split, Allocator >::is_bot ( ) const
inline

◆ snapshot()

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

◆ restore()

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

◆ interpret_tell()

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

◆ interpret_ask()

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

◆ interpret()

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

◆ deduce() [1/2]

template<class A , class Split , class Allocator = typename A::allocator_type>
template<class Alloc >
CUDA local::B lala::SearchTree< A, Split, Allocator >::deduce ( const tell_type< Alloc > & t)
inline

◆ deduce() [2/2]

template<class A , class Split , class Allocator = typename A::allocator_type>
CUDA bool lala::SearchTree< A, Split, Allocator >::deduce ( )
inline

The deduction of a and split is not done here, and if needed, should be done before calling this method. This deduction operator performs one iteration of \( \mathit{pop} \circ \mathit{push} \circ \mathit{split} \). In short, it initializes a to the next node of the search tree. If we observe a from the outside of this domain, a can backtrack, and therefore does not always evolve extensively and monotonically. Nevertheless, the deduction operator of the search tree abstract domain is extensive and monotonic (if split is) over the search tree.

◆ is_extractable()

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

◆ extract()

template<class A , class Split , class Allocator = typename A::allocator_type>
template<class B >
CUDA void lala::SearchTree< A, Split, 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 bot.

◆ project() [1/2]

template<class A , class Split , class Allocator = typename A::allocator_type>
CUDA local_universe lala::SearchTree< A, Split, Allocator >::project ( AVar x) const
inline

If the search tree is empty ( \( \top \)), we return \( \top_U \). If the search tree consists of a single node \( \{a\} \), we return the projection of x in that node. Projection in a search tree with multiple nodes is currently not supported (assert false).

◆ project() [2/2]

template<class A , class Split , class Allocator = typename A::allocator_type>
template<class Univ >
CUDA void lala::SearchTree< A, Split, Allocator >::project ( AVar x,
Univ & r ) const
inline

◆ depth()

template<class A , class Split , class Allocator = typename A::allocator_type>
CUDA size_t lala::SearchTree< A, Split, Allocator >::depth ( ) const
inline
Returns
the current depth of the search tree. The root node has a depth of 0.

Friends And Related Symbol Documentation

◆ SearchTree

template<class A , class Split , class Allocator = typename A::allocator_type>
template<class A2 , class S2 , class Alloc2 >
friend class SearchTree
friend

Member Data Documentation

◆ is_abstract_universe

template<class A , class Split , class Allocator = typename A::allocator_type>
const bool lala::SearchTree< A, Split, Allocator >::is_abstract_universe = false
staticconstexpr

◆ sequential

template<class A , class Split , class Allocator = typename A::allocator_type>
const bool lala::SearchTree< A, Split, Allocator >::sequential = sub_type::sequential
staticconstexpr

◆ is_totally_ordered

template<class A , class Split , class Allocator = typename A::allocator_type>
const bool lala::SearchTree< A, Split, Allocator >::is_totally_ordered = false
staticconstexpr

◆ preserve_bot

template<class A , class Split , class Allocator = typename A::allocator_type>
const bool lala::SearchTree< A, Split, Allocator >::preserve_bot = true
staticconstexpr

◆ preserve_top

template<class A , class Split , class Allocator = typename A::allocator_type>
const bool lala::SearchTree< A, Split, Allocator >::preserve_top = true
staticconstexpr

◆ preserve_join

template<class A , class Split , class Allocator = typename A::allocator_type>
const bool lala::SearchTree< A, Split, Allocator >::preserve_join = sub_type::preserve_join
staticconstexpr

◆ preserve_meet

template<class A , class Split , class Allocator = typename A::allocator_type>
const bool lala::SearchTree< A, Split, Allocator >::preserve_meet = sub_type::preserve_meet
staticconstexpr

◆ injective_concretization

template<class A , class Split , class Allocator = typename A::allocator_type>
const bool lala::SearchTree< A, Split, Allocator >::injective_concretization = sub_type::injective_concretization
staticconstexpr

◆ preserve_concrete_covers

template<class A , class Split , class Allocator = typename A::allocator_type>
const bool lala::SearchTree< A, Split, Allocator >::preserve_concrete_covers = sub_type::preserve_concrete_covers
staticconstexpr

◆ name

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