#include <nbitset.hpp>

Public Types
using	memory_type = Mem

using	bitset_type = battery::bitset< N, Mem, T >

using	this_type = NBitset< N, Mem, T >

template<class M >
using	this_type2 = NBitset< N, M, T >

using	local_type = this_type2< battery::local_memory >

using	LB = local::ZLB

using	UB = local::ZUB

using	value_type = typename LB::value_type

Public Member Functions
constexpr CUDA	NBitset ()

constexpr CUDA	NBitset (const this_type &other)

constexpr	NBitset (this_type &&)=default

constexpr CUDA	NBitset (value_type x)

constexpr CUDA	NBitset (value_type lb, value_type ub)

template<class M >
constexpr CUDA	NBitset (const this_type2< M > &other)

template<class M >
constexpr CUDA	NBitset (this_type2< M > &&other)

template<class M >
constexpr CUDA	NBitset (const battery::bitset< N, M, T > &bits)

template<class M >
constexpr CUDA this_type &	operator= (const this_type2< M > &other)

constexpr CUDA this_type &	operator= (const this_type &other)

constexpr CUDA local::B	is_top () const

constexpr CUDA local::B	is_bot () const

constexpr CUDA const bitset_type &	value () const

constexpr CUDA LB	lb () const

constexpr CUDA UB	ub () const

constexpr CUDA local_type	complement () const

constexpr CUDA void	join_top ()

template<class A >
constexpr CUDA bool	join_lb (const A &lb)

template<class A >
constexpr CUDA bool	join_ub (const A &ub)

template<class M >
constexpr CUDA bool	join (const this_type2< M > &other)

constexpr CUDA void	meet_bot ()

template<class A >
constexpr CUDA bool	meet_lb (const A &lb)

template<class A >
constexpr CUDA bool	meet_ub (const A &ub)

template<class M >
constexpr CUDA bool	meet (const this_type2< M > &other)

template<class M >
constexpr CUDA bool	extract (this_type2< M > &ua) const

template<class Env , class Allocator = typename Env::allocator_type>
CUDA TFormula< Allocator >	deinterpret (AVar x, const Env &env, const Allocator &allocator=Allocator()) const

template<class F >
CUDA NI F	deinterpret () const

CUDA NI void	print () const

constexpr CUDA void	neg (const local_type &x)

constexpr CUDA void	abs (const local_type &x)

constexpr CUDA void	project (Sig fun, const local_type &x)

constexpr CUDA void	additive_inverse (const local_type &x)

constexpr CUDA void	project (Sig fun, const local_type &x, const local_type &y)

constexpr CUDA local_type	width () const

constexpr CUDA local_type	median () const

Static Public Member Functions
constexpr static CUDA this_type	from_set (const battery::vector< int > &values)

constexpr static CUDA local_type	eq_zero ()

constexpr static CUDA local_type	eq_one ()

constexpr static CUDA local_type	bot ()

constexpr static CUDA local_type	top ()

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

template<bool diagnose = false, class F , class Env , class M >
CUDA static NI bool	interpret_ask (const F &f, const Env &env, this_type2< M > &k, IDiagnostics &diagnostics)

template<IKind kind, bool diagnose = false, class F , class Env , class M >
CUDA static NI bool	interpret (const F &f, const Env &env, this_type2< M > &k, IDiagnostics &diagnostics)

CUDA constexpr static NI bool	is_trivial_fun (Sig sig)

Static Public Attributes
constexpr static const bool	is_abstract_universe = true

constexpr static const bool	sequential = Mem::sequential

constexpr static const bool	is_totally_ordered = false

constexpr static const bool	preserve_bot = true

constexpr static const bool	preserve_top = true

constexpr static const bool	preserve_join = true

constexpr static const bool	preserve_meet = true

constexpr static const bool	injective_concretization = true

constexpr static const bool	preserve_concrete_covers = false

constexpr static const bool	complemented = true

constexpr static const bool	is_arithmetic = true

constexpr static const char *	name = "NBitset"

Friends
template<size_t N2, class Mem2 , class T2 >
class	NBitset

Detailed Description

template<size_t N, class Mem, class T = unsigned long long>
class lala::NBitset< N, Mem, T >

This class represents a set of integer values with a fixed-size bitset. In order to have well-defined arithmetic operations preserving bottom and top elements, the first and last bits (written L and R below) of the bitset are reserved. The meaning of L is to include all negative integers and the meaning of R is to include all integers greater than the size of the bitset. Given a bitset \( Lb_0b_1...b_nR \) of size n + 3, the concretization function is given as follows: \( \gamma(Lb_0b_1...b_nR) = \{ i \in \mathbb{Z} \mid 0 \leq i \leq n \land b_i = 1 \} \cup \{ i \in \mathbb{Z} \;|\; i < 0 \land L = 1 \} \cup \{ i \in \mathbb{Z} \;|\; i > n \land R = 1 \} \)

Member Typedef Documentation

◆ memory_type

template<size_t N, class Mem , class T = unsigned long long>

using lala::NBitset< N, Mem, T >::memory_type = Mem

◆ bitset_type

template<size_t N, class Mem , class T = unsigned long long>

using lala::NBitset< N, Mem, T >::bitset_type = battery::bitset<N, Mem, T>

◆ this_type

template<size_t N, class Mem , class T = unsigned long long>

using lala::NBitset< N, Mem, T >::this_type = NBitset<N, Mem, T>

◆ this_type2

template<size_t N, class Mem , class T = unsigned long long>

template<class M >

using lala::NBitset< N, Mem, T >::this_type2 = NBitset<N, M, T>

◆ local_type

template<size_t N, class Mem , class T = unsigned long long>

using lala::NBitset< N, Mem, T >::local_type = this_type2<battery::local_memory>

◆ LB

template<size_t N, class Mem , class T = unsigned long long>

using lala::NBitset< N, Mem, T >::LB = local::ZLB

◆ UB

template<size_t N, class Mem , class T = unsigned long long>

using lala::NBitset< N, Mem, T >::UB = local::ZUB

◆ value_type

template<size_t N, class Mem , class T = unsigned long long>

using lala::NBitset< N, Mem, T >::value_type = typename LB::value_type

Constructor & Destructor Documentation

◆ NBitset() [1/8]

template<size_t N, class Mem , class T = unsigned long long>

constexpr CUDA lala::NBitset< N, Mem, T >::NBitset ( )

inlineconstexpr

Initialize to top (all bits at 1).

◆ NBitset() [2/8]

template<size_t N, class Mem , class T = unsigned long long>

constexpr CUDA lala::NBitset< N, Mem, T >::NBitset ( const this_type & other )

inlineconstexpr

◆ NBitset() [3/8]

template<size_t N, class Mem , class T = unsigned long long>

constexpr lala::NBitset< N, Mem, T >::NBitset ( this_type && )

constexprdefault

◆ NBitset() [4/8]

template<size_t N, class Mem , class T = unsigned long long>

constexpr CUDA lala::NBitset< N, Mem, T >::NBitset ( value_type x )

inlineconstexpr

Given a value \( x \in U \) where \( U \) is the universe of discourse, we initialize a singleton bitset \( 0_0..1_{x+1}...0_n \).

◆ NBitset() [5/8]

template<size_t N, class Mem , class T = unsigned long long>

constexpr CUDA lala::NBitset< N, Mem, T >::NBitset	(	value_type	lb,
		value_type	ub
	)

inlineconstexpr

◆ NBitset() [6/8]

template<size_t N, class Mem , class T = unsigned long long>

template<class M >

constexpr CUDA lala::NBitset< N, Mem, T >::NBitset ( const this_type2< M > & other )

inlineconstexpr

◆ NBitset() [7/8]

template<size_t N, class Mem , class T = unsigned long long>

template<class M >

constexpr CUDA lala::NBitset< N, Mem, T >::NBitset ( this_type2< M > && other )

inlineconstexpr

◆ NBitset() [8/8]

template<size_t N, class Mem , class T = unsigned long long>

template<class M >

constexpr CUDA lala::NBitset< N, Mem, T >::NBitset ( const battery::bitset< N, M, T > & bits )

inlineconstexpr

Member Function Documentation

◆ from_set()

template<size_t N, class Mem , class T = unsigned long long>

constexpr static CUDA this_type lala::NBitset< N, Mem, T >::from_set ( const battery::vector< int > & values )

inlinestaticconstexpr

◆ operator=() [1/2]

template<size_t N, class Mem , class T = unsigned long long>

template<class M >

constexpr CUDA this_type& lala::NBitset< N, Mem, T >::operator= ( const this_type2< M > & other )

inlineconstexpr

The assignment operator can only be used in a sequential context. It is monotone but not extensive.

◆ operator=() [2/2]

template<size_t N, class Mem , class T = unsigned long long>

constexpr CUDA this_type& lala::NBitset< N, Mem, T >::operator= ( const this_type & other )

inlineconstexpr

◆ eq_zero()

template<size_t N, class Mem , class T = unsigned long long>

constexpr static CUDA local_type lala::NBitset< N, Mem, T >::eq_zero ( )

inlinestaticconstexpr

Pre-interpreted formula x == 0.

◆ eq_one()

template<size_t N, class Mem , class T = unsigned long long>

constexpr static CUDA local_type lala::NBitset< N, Mem, T >::eq_one ( )

inlinestaticconstexpr

Pre-interpreted formula x == 1.

◆ bot()

template<size_t N, class Mem , class T = unsigned long long>

constexpr static CUDA local_type lala::NBitset< N, Mem, T >::bot ( )

inlinestaticconstexpr

◆ top()

template<size_t N, class Mem , class T = unsigned long long>

constexpr static CUDA local_type lala::NBitset< N, Mem, T >::top ( )

inlinestaticconstexpr

◆ is_top()

template<size_t N, class Mem , class T = unsigned long long>

constexpr CUDA local::B lala::NBitset< N, Mem, T >::is_top ( ) const

inlineconstexpr

◆ is_bot()

template<size_t N, class Mem , class T = unsigned long long>

constexpr CUDA local::B lala::NBitset< N, Mem, T >::is_bot ( ) const

inlineconstexpr

◆ value()

template<size_t N, class Mem , class T = unsigned long long>

constexpr CUDA const bitset_type& lala::NBitset< N, Mem, T >::value ( ) const

inlineconstexpr

◆ interpret_tell()

template<size_t N, class Mem , class T = unsigned long long>

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

CUDA static NI bool lala::NBitset< N, Mem, T >::interpret_tell	(	const F &	f,
		const Env &	env,
		this_type2< M > &	tell,
		IDiagnostics &	diagnostics
	)

inlinestatic

Support the following language where all constants k are integer or Boolean values:

var x:Z
var x:B
x <op> k where k is an integer constant and <op> in {==, !=, <, <=, >, >=}.
x in S where S is a set of integers. It can be over-approximated if the element k falls out of the bitset.

◆ interpret_ask()

template<size_t N, class Mem , class T = unsigned long long>

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

CUDA static NI bool lala::NBitset< N, Mem, T >::interpret_ask	(	const F &	f,
		const Env &	env,
		this_type2< M > &	k,
		IDiagnostics &	diagnostics
	)

inlinestatic

Support the same language than the "tell language" without existential.

◆ interpret()

template<size_t N, class Mem , class T = unsigned long long>

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

CUDA static NI bool lala::NBitset< N, Mem, T >::interpret	(	const F &	f,
		const Env &	env,
		this_type2< M > &	k,
		IDiagnostics &	diagnostics
	)

inlinestatic

◆ lb()

template<size_t N, class Mem , class T = unsigned long long>

constexpr CUDA LB lala::NBitset< N, Mem, T >::lb ( ) const

inlineconstexpr

◆ ub()

template<size_t N, class Mem , class T = unsigned long long>

constexpr CUDA UB lala::NBitset< N, Mem, T >::ub ( ) const

inlineconstexpr

◆ complement()

template<size_t N, class Mem , class T = unsigned long long>

constexpr CUDA local_type lala::NBitset< N, Mem, T >::complement ( ) const

inlineconstexpr

◆ join_top()

template<size_t N, class Mem , class T = unsigned long long>

constexpr CUDA void lala::NBitset< N, Mem, T >::join_top ( )

inlineconstexpr

◆ join_lb()

template<size_t N, class Mem , class T = unsigned long long>

template<class A >

constexpr CUDA bool lala::NBitset< N, Mem, T >::join_lb ( const A & lb )

inlineconstexpr

◆ join_ub()

template<size_t N, class Mem , class T = unsigned long long>

template<class A >

constexpr CUDA bool lala::NBitset< N, Mem, T >::join_ub ( const A & ub )

inlineconstexpr

◆ join()

template<size_t N, class Mem , class T = unsigned long long>

template<class M >

constexpr CUDA bool lala::NBitset< N, Mem, T >::join ( const this_type2< M > & other )

inlineconstexpr

◆ meet_bot()

template<size_t N, class Mem , class T = unsigned long long>

constexpr CUDA void lala::NBitset< N, Mem, T >::meet_bot ( )

inlineconstexpr

◆ meet_lb()

template<size_t N, class Mem , class T = unsigned long long>

template<class A >

constexpr CUDA bool lala::NBitset< N, Mem, T >::meet_lb ( const A & lb )

inlineconstexpr

◆ meet_ub()

template<size_t N, class Mem , class T = unsigned long long>

template<class A >

constexpr CUDA bool lala::NBitset< N, Mem, T >::meet_ub ( const A & ub )

inlineconstexpr

◆ meet()

template<size_t N, class Mem , class T = unsigned long long>

template<class M >

constexpr CUDA bool lala::NBitset< N, Mem, T >::meet ( const this_type2< M > & other )

inlineconstexpr

◆ extract()

template<size_t N, class Mem , class T = unsigned long long>

template<class M >

constexpr CUDA bool lala::NBitset< N, Mem, T >::extract ( this_type2< M > & ua ) const

inlineconstexpr

◆ deinterpret() [1/2]

template<size_t N, class Mem , class T = unsigned long long>

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

CUDA TFormula<Allocator> lala::NBitset< N, Mem, T >::deinterpret	(	AVar	x,
		const Env &	env,
		const Allocator &	allocator = `Allocator()`
	)		const

inline

◆ deinterpret() [2/2]

template<size_t N, class Mem , class T = unsigned long long>

template<class F >

CUDA NI F lala::NBitset< N, Mem, T >::deinterpret ( ) const

inline

Deinterpret the current value to a logical constant. The lower bound is deinterpreted, and it is up to the user to check that interval is a singleton.

◆ print()

template<size_t N, class Mem , class T = unsigned long long>

CUDA NI void lala::NBitset< N, Mem, T >::print ( ) const

inline

◆ is_trivial_fun()

template<size_t N, class Mem , class T = unsigned long long>

CUDA constexpr static NI bool lala::NBitset< N, Mem, T >::is_trivial_fun ( Sig sig )

inlinestaticconstexpr

◆ neg()

template<size_t N, class Mem , class T = unsigned long long>

constexpr CUDA void lala::NBitset< N, Mem, T >::neg ( const local_type & x )

inlineconstexpr

◆ abs()

template<size_t N, class Mem , class T = unsigned long long>

constexpr CUDA void lala::NBitset< N, Mem, T >::abs ( const local_type & x )

inlineconstexpr

◆ project() [1/2]

template<size_t N, class Mem , class T = unsigned long long>

constexpr CUDA void lala::NBitset< N, Mem, T >::project	(	Sig	fun,
		const local_type &	x
	)

inlineconstexpr

◆ additive_inverse()

template<size_t N, class Mem , class T = unsigned long long>

constexpr CUDA void lala::NBitset< N, Mem, T >::additive_inverse ( const local_type & x )

inlineconstexpr

◆ project() [2/2]

template<size_t N, class Mem , class T = unsigned long long>

constexpr CUDA void lala::NBitset< N, Mem, T >::project	(	Sig	fun,
		const local_type &	x,
		const local_type &	y
	)

inlineconstexpr

◆ width()

template<size_t N, class Mem , class T = unsigned long long>

constexpr CUDA local_type lala::NBitset< N, Mem, T >::width ( ) const

inlineconstexpr

◆ median()

template<size_t N, class Mem , class T = unsigned long long>

constexpr CUDA local_type lala::NBitset< N, Mem, T >::median ( ) const

inlineconstexpr

Returns: The median value of the bitset.

Friends And Related Function Documentation

◆ NBitset

template<size_t N, class Mem , class T = unsigned long long>

template<size_t N2, class Mem2 , class T2 >

friend class NBitset

friend

Member Data Documentation

◆ is_abstract_universe

template<size_t N, class Mem , class T = unsigned long long>

constexpr static const bool lala::NBitset< N, Mem, T >::is_abstract_universe = true

staticconstexpr

◆ sequential

template<size_t N, class Mem , class T = unsigned long long>

constexpr static const bool lala::NBitset< N, Mem, T >::sequential = Mem::sequential

staticconstexpr

◆ is_totally_ordered

template<size_t N, class Mem , class T = unsigned long long>

constexpr static const bool lala::NBitset< N, Mem, T >::is_totally_ordered = false

staticconstexpr

◆ preserve_bot

template<size_t N, class Mem , class T = unsigned long long>

constexpr static const bool lala::NBitset< N, Mem, T >::preserve_bot = true

staticconstexpr

◆ preserve_top

template<size_t N, class Mem , class T = unsigned long long>

constexpr static const bool lala::NBitset< N, Mem, T >::preserve_top = true

staticconstexpr

◆ preserve_join

template<size_t N, class Mem , class T = unsigned long long>

constexpr static const bool lala::NBitset< N, Mem, T >::preserve_join = true

staticconstexpr

◆ preserve_meet

template<size_t N, class Mem , class T = unsigned long long>

constexpr static const bool lala::NBitset< N, Mem, T >::preserve_meet = true

staticconstexpr

◆ injective_concretization

template<size_t N, class Mem , class T = unsigned long long>

constexpr static const bool lala::NBitset< N, Mem, T >::injective_concretization = true

staticconstexpr

◆ preserve_concrete_covers

template<size_t N, class Mem , class T = unsigned long long>

constexpr static const bool lala::NBitset< N, Mem, T >::preserve_concrete_covers = false

staticconstexpr

◆ complemented

template<size_t N, class Mem , class T = unsigned long long>

constexpr static const bool lala::NBitset< N, Mem, T >::complemented = true

staticconstexpr

◆ is_arithmetic

template<size_t N, class Mem , class T = unsigned long long>

constexpr static const bool lala::NBitset< N, Mem, T >::is_arithmetic = true

staticconstexpr

◆ name

template<size_t N, class Mem , class T = unsigned long long>

constexpr static const char* lala::NBitset< N, Mem, T >::name = "NBitset"

staticconstexpr

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

include/lala/universes/nbitset.hpp

Public Types

Public Member Functions

Static Public Member Functions

Static Public Attributes

Friends

Detailed Description

template<size_t N, class Mem, class T = unsigned long long> class lala::NBitset< N, Mem, T >

Member Typedef Documentation

◆ memory_type

◆ bitset_type

◆ this_type

◆ this_type2

◆ local_type

◆ LB

◆ UB

◆ value_type

Constructor & Destructor Documentation

◆ NBitset() [1/8]

◆ NBitset() [2/8]

◆ NBitset() [3/8]

◆ NBitset() [4/8]

◆ NBitset() [5/8]

◆ NBitset() [6/8]

◆ NBitset() [7/8]

◆ NBitset() [8/8]

Member Function Documentation

◆ from_set()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ eq_zero()

◆ eq_one()

◆ bot()

◆ top()

◆ is_top()

◆ is_bot()

◆ value()

◆ interpret_tell()

◆ interpret_ask()

◆ interpret()

◆ lb()

◆ ub()

◆ complement()

◆ join_top()

◆ join_lb()

◆ join_ub()

◆ join()

◆ meet_bot()

◆ meet_lb()

◆ meet_ub()

◆ meet()

◆ extract()

◆ deinterpret() [1/2]

◆ deinterpret() [2/2]

◆ print()

◆ is_trivial_fun()

◆ neg()

◆ abs()

◆ project() [1/2]

◆ additive_inverse()

◆ project() [2/2]

◆ width()

◆ median()

Friends And Related Function Documentation

◆ NBitset

Member Data Documentation

◆ is_abstract_universe

◆ sequential

◆ is_totally_ordered

◆ preserve_bot

◆ preserve_top

◆ preserve_join

◆ preserve_meet

◆ injective_concretization

◆ preserve_concrete_covers

◆ complemented

◆ is_arithmetic

◆ name

template<size_t N, class Mem, class T = unsigned long long>
class lala::NBitset< N, Mem, T >