#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 int	depth () const

CUDA bool	push (branch_type &&branch)

CUDA bool	pop (bool pruned)

CUDA bool	commit_left ()

CUDA bool	commit_right ()

CUDA bool	backtrack ()

CUDA bool	deduce_root ()

CUDA bool	replay ()

Public Attributes
split_ptr	split

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 int lala::SearchTree< A, Split, Allocator >::depth ( ) const

inline

Returns: the current depth of the search tree. The root node has a depth of 0.

◆ push()

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

CUDA bool lala::SearchTree< A, Split, Allocator >::push ( branch_type && branch )

inline

Returns: true if the current node is pruned, and false if a new branch was pushed.

◆ pop()

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

CUDA bool lala::SearchTree< A, Split, Allocator >::pop ( bool pruned )

inline

If the current node was pruned, we need to backtrack, otherwise we just consider the next node along the branch.

◆ commit_left()

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

CUDA bool lala::SearchTree< A, Split, Allocator >::commit_left ( )

inline

Given the current node, commit to the node on the left. If we are on the root node, we save a snapshot of root before committing to the left node.

◆ commit_right()

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

CUDA bool lala::SearchTree< A, Split, Allocator >::commit_right ( )

inline

We explore the next node of the search tree available (after we backtracked, so it cannot be a left node).

◆ backtrack()

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

CUDA bool lala::SearchTree< A, Split, Allocator >::backtrack ( )

inline

Goes from the current node to root.

◆ deduce_root()

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

CUDA bool lala::SearchTree< A, Split, Allocator >::deduce_root ( )

inline

We do not always have access to the root node, so formulas that are added to the search tree are kept in root_tell. During backtracking, root is available through a, and we add to root the formulas stored until now, so they become automatically available to the remaining nodes in the search tree.

◆ replay()

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

CUDA bool lala::SearchTree< A, Split, Allocator >::replay ( )

inline

Goes from root to the new node to be explored.

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>

constexpr const bool lala::SearchTree< A, Split, Allocator >::is_abstract_universe = false

staticconstexpr

◆ sequential

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

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

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

constexpr const bool lala::SearchTree< A, Split, Allocator >::preserve_bot = true

staticconstexpr

◆ preserve_top

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

constexpr const bool lala::SearchTree< A, Split, Allocator >::preserve_top = true

staticconstexpr

◆ preserve_join

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

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

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

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

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

constexpr const char* lala::SearchTree< A, Split, Allocator >::name = "SearchTree"

staticconstexpr

◆ split

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

split_ptr lala::SearchTree< A, Split, Allocator >::split

The documentation for this class was generated from the following file:

include/lala/search_tree.hpp

Classes

Public Types

Public Member Functions

Public Attributes

Static Public Attributes

Friends

Member Typedef Documentation

◆ allocator_type

◆ sub_allocator_type

◆ split_type

◆ branch_type

◆ universe_type

◆ local_universe

◆ sub_type

◆ sub_ptr

◆ split_ptr

◆ this_type

◆ ask_type

Constructor & Destructor Documentation

◆ SearchTree() [1/2]

◆ SearchTree() [2/2]

Member Function Documentation

◆ aty()

◆ get_allocator()

◆ is_singleton()

◆ is_top()

◆ is_bot()

◆ snapshot()

◆ restore()

◆ interpret_tell()

◆ interpret_ask()

◆ interpret()

◆ deduce() [1/2]

◆ deduce() [2/2]

◆ is_extractable()

◆ extract()

◆ project() [1/2]

◆ project() [2/2]

◆ depth()

◆ push()

◆ pop()

◆ commit_left()

◆ commit_right()

◆ backtrack()

◆ deduce_root()

◆ replay()

Friends And Related Symbol Documentation

◆ SearchTree

Member Data Documentation

◆ is_abstract_universe

◆ sequential

◆ is_totally_ordered

◆ preserve_bot

◆ preserve_top

◆ preserve_join

◆ preserve_meet

◆ injective_concretization

◆ preserve_concrete_covers

◆ name

◆ split