#include <pc.hpp>

Classes
struct	interpreted_type

struct	snapshot_type

Public Types
using	sub_type = A

using	universe_type = typename A::universe_type

using	local_universe_type = typename universe_type::local_type

using	allocator_type = Allocator

using	sub_allocator_type = typename A::allocator_type

using	this_type = PC<sub_type, allocator_type>

using	sub_ptr = abstract_ptr<sub_type>

template<class Alloc >
using	formula_seq = battery::vector<pc::Formula<A, Alloc>, Alloc>

template<class Alloc >
using	term_seq = battery::vector<pc::Term<A, Alloc>, Alloc>

template<class Alloc >
using	tell_type = interpreted_type<Alloc, typename sub_type::template tell_type<Alloc>>

template<class Alloc >
using	ask_type = interpreted_type<Alloc, typename sub_type::template ask_type<Alloc>>

Public Member Functions
CUDA	PC (AType atype, sub_ptr sub, const allocator_type &alloc=allocator_type{})

CUDA	PC (PC &&other)

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

CUDA allocator_type	get_allocator () const

CUDA AType	aty () 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<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, const Env &env, ask_type< Alloc2 > &ask, IDiagnostics &diagnostics) const

template<class Alloc2 >
CUDA local::B	deduce (const tell_type< Alloc2 > &t)

CUDA bool	embed (AVar x, const universe_type &dom)

template<class Alloc2 >
CUDA local::B	ask (const ask_type< Alloc2 > &t) const

CUDA local::B	ask (size_t i) const

CUDA size_t	num_deductions () const

CUDA local::B	deduce (size_t i)

CUDA local::B	is_bot () const

CUDA local::B	is_top () const

CUDA auto	operator[] (int x) const

CUDA auto	project (AVar x) const

template<class Univ >
CUDA void	project (AVar x, Univ &u) const

CUDA size_t	vars () 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 ExtractionStrategy = NonAtomicExtraction>
CUDA bool	is_extractable (const ExtractionStrategy &strategy=ExtractionStrategy()) const

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

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

template<class I , class Env , class Allocator2 = typename Env::allocator_type>
CUDA NI TFormula< Allocator2 >	deinterpret (const I &intermediate, const Env &env, Allocator2 allocator=Allocator2()) 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 = true

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 = "PC"

Friends
template<class A2 , class Alloc2 >
class	PC

Detailed Description

template<class A, class Allocator = typename A::allocator_type>
class lala::PC< A, Allocator >

PC is an abstract transformer built on top of an abstract domain A. It is expected that A has a projection function u = project(x). We also expect a tell(x, u, has_changed) function to join the abstract universe u in the domain of the variable x. An example of abstract domain satisfying these requirements is VStore<Interval<ZInc>>.

Member Typedef Documentation

◆ sub_type

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

using lala::PC< A, Allocator >::sub_type = A

◆ universe_type

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

using lala::PC< A, Allocator >::universe_type = typename A::universe_type

◆ local_universe_type

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

using lala::PC< A, Allocator >::local_universe_type = typename universe_type::local_type

◆ allocator_type

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

using lala::PC< A, Allocator >::allocator_type = Allocator

◆ sub_allocator_type

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

using lala::PC< A, Allocator >::sub_allocator_type = typename A::allocator_type

◆ this_type

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

using lala::PC< A, Allocator >::this_type = PC<sub_type, allocator_type>

◆ sub_ptr

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

using lala::PC< A, Allocator >::sub_ptr = abstract_ptr<sub_type>

◆ formula_seq

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

template<class Alloc >

using lala::PC< A, Allocator >::formula_seq = battery::vector<pc::Formula<A, Alloc>, Alloc>

◆ term_seq

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

template<class Alloc >

using lala::PC< A, Allocator >::term_seq = battery::vector<pc::Term<A, Alloc>, Alloc>

◆ tell_type

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

template<class Alloc >

using lala::PC< A, Allocator >::tell_type = interpreted_type<Alloc, typename sub_type::template tell_type<Alloc>>

◆ ask_type

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

template<class Alloc >

using lala::PC< A, Allocator >::ask_type = interpreted_type<Alloc, typename sub_type::template ask_type<Alloc>>

Constructor & Destructor Documentation

◆ PC() [1/3]

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

CUDA lala::PC< A, Allocator >::PC	(	AType	atype,
		sub_ptr	sub,
		const allocator_type &	alloc = allocator_type{} )

inline

◆ PC() [2/3]

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

CUDA lala::PC< A, Allocator >::PC ( PC< A, Allocator > && other )

inline

◆ PC() [3/3]

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

template<class A2 , class Alloc2 , class... Allocators>

CUDA lala::PC< A, Allocator >::PC	(	const PC< A2, Alloc2 > &	other,
		AbstractDeps< Allocators... > &	deps )

inline

Member Function Documentation

◆ get_allocator()

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

CUDA allocator_type lala::PC< A, Allocator >::get_allocator ( ) const

inline

◆ aty()

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

CUDA AType lala::PC< A, Allocator >::aty ( ) const

inline

◆ bot() [1/2]

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

static CUDA this_type lala::PC< A, 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 Allocator = typename A::allocator_type>

static CUDA this_type lala::PC< A, 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 Allocator = typename A::allocator_type>

template<class Env >

static CUDA this_type lala::PC< A, 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 Allocator = typename A::allocator_type>

template<class Env >

static CUDA this_type lala::PC< A, Allocator >::top	(	Env &	env,
		const allocator_type &	alloc = allocator_type(),
		const sub_allocator_type &	sub_alloc = sub_allocator_type() )

inlinestatic

◆ interpret()

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

template<IKind kind, bool diagnose = false, class F , class Env , class I >

CUDA NI bool lala::PC< A, Allocator >::interpret	(	const F &	f,
		Env &	env,
		I &	intermediate,
		IDiagnostics &	diagnostics ) const

inline

◆ interpret_tell()

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

template<bool diagnose = false, class F , class Env , class Alloc2 >

CUDA NI bool lala::PC< A, Allocator >::interpret_tell	(	const F &	f,
		Env &	env,
		tell_type< Alloc2 > &	tell,
		IDiagnostics &	diagnostics ) const

inline

PC expects a non-conjunctive formula \( c \) which can either be interpreted in the sub-domain A or in the current domain.

◆ interpret_ask()

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

template<bool diagnose = false, class F , class Env , class Alloc2 >

CUDA NI bool lala::PC< A, Allocator >::interpret_ask	(	const F &	f,
		const Env &	env,
		ask_type< Alloc2 > &	ask,
		IDiagnostics &	diagnostics ) const

inline

◆ deduce() [1/2]

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

template<class Alloc2 >

CUDA local::B lala::PC< A, Allocator >::deduce ( const tell_type< Alloc2 > & t )

inline

Note that we cannot add propagators in parallel (but modifying the underlying domain is ok). This is a current limitation that we should fix later on. Notes for later: To implement "telling of propagators", we would need to check if a propagator has already been added or not (for idempotency).

Walk through the existing propagators to check which ones are already in.
If a propagator has the same shape but different constant U, meet them in place.

◆ embed()

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

CUDA bool lala::PC< A, Allocator >::embed	(	AVar	x,
		const universe_type &	dom )

inline

◆ ask() [1/2]

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

template<class Alloc2 >

CUDA local::B lala::PC< A, Allocator >::ask ( const ask_type< Alloc2 > & t ) const

inline

◆ ask() [2/2]

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

CUDA local::B lala::PC< A, Allocator >::ask ( size_t i ) const

inline

◆ num_deductions()

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

CUDA size_t lala::PC< A, Allocator >::num_deductions ( ) const

inline

◆ deduce() [2/2]

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

CUDA local::B lala::PC< A, Allocator >::deduce ( size_t i )

inline

◆ is_bot()

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

CUDA local::B lala::PC< A, Allocator >::is_bot ( ) const

inline

true if the underlying abstract element is bot, false otherwise.

◆ is_top()

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

CUDA local::B lala::PC< A, Allocator >::is_top ( ) const

inline

true if the underlying abstract element is top and there is no deduction function, false otherwise.

◆ operator[]()

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

CUDA auto lala::PC< A, Allocator >::operator[] ( int x ) const

inline

◆ project() [1/2]

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

CUDA auto lala::PC< A, Allocator >::project ( AVar x ) const

inline

◆ project() [2/2]

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

template<class Univ >

CUDA void lala::PC< A, Allocator >::project	(	AVar	x,
		Univ &	u ) const

inline

◆ vars()

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

CUDA size_t lala::PC< A, Allocator >::vars ( ) const

inline

◆ snapshot()

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

template<class Alloc2 = allocator_type>

CUDA snapshot_type< Alloc2 > lala::PC< A, Allocator >::snapshot ( const Alloc2 & alloc = Alloc2() ) const

inline

◆ restore()

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

template<class Alloc2 >

CUDA void lala::PC< A, Allocator >::restore ( const snapshot_type< Alloc2 > & snap )

inline

◆ is_extractable()

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

template<class ExtractionStrategy = NonAtomicExtraction>

CUDA bool lala::PC< A, Allocator >::is_extractable ( const ExtractionStrategy & strategy = ExtractionStrategy() ) const

inline

An abstract element is extractable when it is not equal to bot, if all propagators are entailed and if the underlying abstract element is extractable.

◆ extract()

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

template<class B >

CUDA void lala::PC< A, Allocator >::extract ( B & ua ) const

inline

Extract the current element into ua.

Precondition: is_extractable() must be true. For efficiency reason, if B is a propagator completion, the propagators are not copied in ua. (It is OK, since they are entailed, they don't bring information anymore.)

◆ deinterpret() [1/2]

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

template<class Env , class Allocator2 = typename Env::allocator_type>

CUDA NI TFormula< Allocator2 > lala::PC< A, Allocator >::deinterpret	(	const Env &	env,
		Allocator2	allocator = Allocator2() ) const

inline

◆ deinterpret() [2/2]

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

template<class I , class Env , class Allocator2 = typename Env::allocator_type>

CUDA NI TFormula< Allocator2 > lala::PC< A, Allocator >::deinterpret	(	const I &	intermediate,
		const Env &	env,
		Allocator2	allocator = Allocator2() ) const

inline

Friends And Related Symbol Documentation

◆ PC

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

template<class A2 , class Alloc2 >

friend class PC

friend

Member Data Documentation

◆ is_abstract_universe

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

const bool lala::PC< A, Allocator >::is_abstract_universe = false

staticconstexpr

◆ sequential

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

const bool lala::PC< A, Allocator >::sequential = sub_type::sequential

staticconstexpr

◆ is_totally_ordered

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

const bool lala::PC< A, Allocator >::is_totally_ordered = false

staticconstexpr

◆ preserve_bot

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

const bool lala::PC< A, Allocator >::preserve_bot = true

staticconstexpr

◆ preserve_top

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

const bool lala::PC< A, Allocator >::preserve_top = sub_type::preserve_top

staticconstexpr

◆ preserve_join

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

const bool lala::PC< A, Allocator >::preserve_join = sub_type::preserve_join

staticconstexpr

◆ preserve_meet

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

const bool lala::PC< A, Allocator >::preserve_meet = sub_type::preserve_meet

staticconstexpr

◆ injective_concretization

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

const bool lala::PC< A, Allocator >::injective_concretization = sub_type::injective_concretization

staticconstexpr

◆ preserve_concrete_covers

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

const bool lala::PC< A, Allocator >::preserve_concrete_covers = sub_type::preserve_concrete_covers

staticconstexpr

◆ name

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

const char* lala::PC< A, Allocator >::name = "PC"

staticconstexpr

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

include/lala/pc.hpp

Classes

Public Types

Public Member Functions

Static Public Member Functions

Static Public Attributes

Friends

Detailed Description

Member Typedef Documentation

◆ sub_type

◆ universe_type

◆ local_universe_type

◆ allocator_type

◆ sub_allocator_type

◆ this_type

◆ sub_ptr

◆ formula_seq

◆ term_seq

◆ tell_type

◆ ask_type

Constructor & Destructor Documentation

◆ PC() [1/3]

◆ PC() [2/3]

◆ PC() [3/3]

Member Function Documentation

◆ get_allocator()

◆ aty()

◆ bot() [1/2]

◆ top() [1/2]

◆ bot() [2/2]

◆ top() [2/2]

◆ interpret()

◆ interpret_tell()

◆ interpret_ask()

◆ deduce() [1/2]

◆ embed()

◆ ask() [1/2]

◆ ask() [2/2]

◆ num_deductions()

◆ deduce() [2/2]

◆ is_bot()

◆ is_top()

◆ operator[]()

◆ project() [1/2]

◆ project() [2/2]

◆ vars()

◆ snapshot()

◆ restore()

◆ is_extractable()

◆ extract()

◆ deinterpret() [1/2]

◆ deinterpret() [2/2]

Friends And Related Symbol Documentation

◆ PC

Member Data Documentation

◆ is_abstract_universe

◆ sequential

◆ is_totally_ordered

◆ preserve_bot

◆ preserve_top

◆ preserve_join

◆ preserve_meet

◆ injective_concretization

◆ preserve_concrete_covers

◆ name