#include <_pre_sinc.hpp>

Public Types
using	this_type = PreSInc<N, VT>

using	dual_type = PreSDec<N, VT>

using	value_type = battery::bitset<N, battery::LocalMemory, VT>

template<class Mem >
using	atomic_type = battery::bitset<N, Mem, VT>

using	increasing_type = this_type

template<class F >
using	iresult = IResult<value_type, F>

Static Public Member Functions
template<class F >
static CUDA iresult< F >	interpret_tell (const F &f)

template<class F >
static CUDA iresult< F >	interpret_ask (const F &f)

template<class F >
static CUDA iresult< F >	interpret_type (const F &f)

static CUDA constexpr Sig	sig_order ()

static CUDA constexpr Sig	sig_strict_order ()

static CUDA constexpr value_type	top ()

static CUDA constexpr value_type	bot ()

template<class Mem1 , class Mem2 >
static CUDA constexpr value_type	meet (const atomic_type< Mem1 > &x, const atomic_type< Mem2 > &y)

template<class Mem1 , class Mem2 >
static CUDA constexpr value_type	join (const atomic_type< Mem1 > &x, const atomic_type< Mem2 > &y)

template<class Mem1 , class Mem2 >
static CUDA constexpr bool	order (const atomic_type< Mem1 > &x, const atomic_type< Mem2 > &y)

template<class Mem1 , class Mem2 >
static CUDA constexpr bool	strict_order (const atomic_type< Mem1 > &x, const atomic_type< Mem2 > &y)

static CUDA constexpr bool	is_supported_fun (Sig sig)

template<Sig sig>
static CUDA constexpr value_type	fun (value_type x)

template<Sig sig>
static CUDA constexpr value_type	fun (value_type x, value_type y)

Static Public Attributes
static constexpr const bool	is_totally_ordered = false

static constexpr const bool	preserve_top = true

static constexpr const bool	preserve_bot = false

static constexpr const bool	injective_concretization = true

static constexpr const bool	preserve_concrete_covers = true

static constexpr const bool	complemented = true

static constexpr const bool	increasing = true

static constexpr const char *	name = "SInc"

static constexpr const bool	is_arithmetic = false

Detailed Description

template<size_t N, class VT = unsigned long long>
struct lala::PreSInc< N, VT >

PreSInc is a pre-abstract universe \( \langle \mathcal{P}(\mathbb{Z}), \subseteq \rangle \) ordered by the set inclusion operation. It is used to represent constraints of the form \( x \supseteq k \) where \( k \) is a set of integers.

Member Typedef Documentation

◆ this_type

template<size_t N, class VT = unsigned long long>

using lala::PreSInc< N, VT >::this_type = PreSInc<N, VT>

◆ dual_type

template<size_t N, class VT = unsigned long long>

using lala::PreSInc< N, VT >::dual_type = PreSDec<N, VT>

◆ value_type

template<size_t N, class VT = unsigned long long>

using lala::PreSInc< N, VT >::value_type = battery::bitset<N, battery::LocalMemory, VT>

◆ atomic_type

template<size_t N, class VT = unsigned long long>

template<class Mem >

using lala::PreSInc< N, VT >::atomic_type = battery::bitset<N, Mem, VT>

◆ increasing_type

template<size_t N, class VT = unsigned long long>

using lala::PreSInc< N, VT >::increasing_type = this_type

◆ iresult

template<size_t N, class VT = unsigned long long>

template<class F >

using lala::PreSInc< N, VT >::iresult = IResult<value_type, F>

Member Function Documentation

◆ interpret_tell()

template<size_t N, class VT = unsigned long long>

template<class F >

static CUDA iresult< F > lala::PreSInc< N, VT >::interpret_tell ( const F & f )

inlinestatic

Interpret a constant in the lattice of increasing sets of integers according to the upset semantics (see universe.hpp for explanation). Only formulas of kind F::S(F::Z) are supported: \( [\![ x:\mathcal{P}(\mathbb{Z}) \supseteq \{k_1,\ldots,k_n\}:\mathcal{P}(\mathbb{Z}) ]\!] = \{k_1,\ldots,k_n\} \).

◆ interpret_ask()

template<size_t N, class VT = unsigned long long>

template<class F >

static CUDA iresult< F > lala::PreSInc< N, VT >::interpret_ask ( const F & f )

inlinestatic

The same as interpret_tell because the constraint are interpreted exactly.

◆ interpret_type()

template<size_t N, class VT = unsigned long long>

template<class F >

static CUDA iresult< F > lala::PreSInc< N, VT >::interpret_type ( const F & f )

inlinestatic

Verify if the type of a variable, introduced by an existential quantifier, is compatible with the current abstract universe. Variables of type Set(Int) are interpreted exactly ( \( \mathcal{P}(\mathbb{Z}) = \gamma(\top) \)).

◆ sig_order()

template<size_t N, class VT = unsigned long long>

static CUDA constexpr Sig lala::PreSInc< N, VT >::sig_order ( )

inlinestaticconstexpr

◆ sig_strict_order()

template<size_t N, class VT = unsigned long long>

static CUDA constexpr Sig lala::PreSInc< N, VT >::sig_strict_order ( )

inlinestaticconstexpr

◆ top()

template<size_t N, class VT = unsigned long long>

static CUDA constexpr value_type lala::PreSInc< N, VT >::top ( )

inlinestaticconstexpr

◆ bot()

template<size_t N, class VT = unsigned long long>

static CUDA constexpr value_type lala::PreSInc< N, VT >::bot ( )

inlinestaticconstexpr

◆ meet()

template<size_t N, class VT = unsigned long long>

template<class Mem1 , class Mem2 >

static CUDA constexpr value_type lala::PreSInc< N, VT >::meet	(	const atomic_type< Mem1 > &	x,
		const atomic_type< Mem2 > &	y )

inlinestaticconstexpr

◆ join()

template<size_t N, class VT = unsigned long long>

template<class Mem1 , class Mem2 >

static CUDA constexpr value_type lala::PreSInc< N, VT >::join	(	const atomic_type< Mem1 > &	x,
		const atomic_type< Mem2 > &	y )

inlinestaticconstexpr

◆ order()

template<size_t N, class VT = unsigned long long>

template<class Mem1 , class Mem2 >

static CUDA constexpr bool lala::PreSInc< N, VT >::order	(	const atomic_type< Mem1 > &	x,
		const atomic_type< Mem2 > &	y )

inlinestaticconstexpr

◆ strict_order()

template<size_t N, class VT = unsigned long long>

template<class Mem1 , class Mem2 >

static CUDA constexpr bool lala::PreSInc< N, VT >::strict_order	(	const atomic_type< Mem1 > &	x,
		const atomic_type< Mem2 > &	y )

inlinestaticconstexpr

◆ is_supported_fun()

template<size_t N, class VT = unsigned long long>

static CUDA constexpr bool lala::PreSInc< N, VT >::is_supported_fun ( Sig sig )

inlinestaticconstexpr

◆ fun() [1/2]

template<size_t N, class VT = unsigned long long>

template<Sig sig>

static CUDA constexpr value_type lala::PreSInc< N, VT >::fun ( value_type x )

inlinestaticconstexpr

fun: value_type -> SInc is an abstract function on SInc over-approximating the function denoted by sig on the concrete domain.

Template Parameters

sig	The signature of the function to over-approximate, can be either `CARD` or `HULL`.

Parameters

x	The argument of the function, which is a constant value in the underlying universe of discourse.

Note: Since x is a constant, we do not check for equality with top() or bot().

◆ fun() [2/2]

template<size_t N, class VT = unsigned long long>

template<Sig sig>

static CUDA constexpr value_type lala::PreSInc< N, VT >::fun	(	value_type	x,
		value_type	y )

inlinestaticconstexpr

fun: value_type X value_type -> ZInc is similar to its unary version but with an arity of 2.

Member Data Documentation

◆ is_totally_ordered

template<size_t N, class VT = unsigned long long>

const bool lala::PreSInc< N, VT >::is_totally_ordered = false

staticconstexpr

◆ preserve_top

template<size_t N, class VT = unsigned long long>

const bool lala::PreSInc< N, VT >::preserve_top = true

staticconstexpr

◆ preserve_bot

template<size_t N, class VT = unsigned long long>

const bool lala::PreSInc< N, VT >::preserve_bot = false

staticconstexpr

◆ injective_concretization

template<size_t N, class VT = unsigned long long>

const bool lala::PreSInc< N, VT >::injective_concretization = true

staticconstexpr

◆ preserve_concrete_covers

template<size_t N, class VT = unsigned long long>

const bool lala::PreSInc< N, VT >::preserve_concrete_covers = true

staticconstexpr

◆ complemented

template<size_t N, class VT = unsigned long long>

const bool lala::PreSInc< N, VT >::complemented = true

staticconstexpr

◆ increasing

template<size_t N, class VT = unsigned long long>

const bool lala::PreSInc< N, VT >::increasing = true

staticconstexpr

◆ name

template<size_t N, class VT = unsigned long long>

const char* lala::PreSInc< N, VT >::name = "SInc"

staticconstexpr

◆ is_arithmetic

template<size_t N, class VT = unsigned long long>

const bool lala::PreSInc< N, VT >::is_arithmetic = false

staticconstexpr

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

include/lala/universes/_pre_sinc.hpp

Public Types

Static Public Member Functions

Static Public Attributes

Detailed Description

Member Typedef Documentation

◆ this_type

◆ dual_type

◆ value_type

◆ atomic_type

◆ increasing_type

◆ iresult

Member Function Documentation

◆ interpret_tell()

◆ interpret_ask()

◆ interpret_type()

◆ sig_order()

◆ sig_strict_order()

◆ top()

◆ bot()

◆ meet()

◆ join()

◆ order()

◆ strict_order()

◆ is_supported_fun()

◆ fun() [1/2]

◆ fun() [2/2]

Member Data Documentation

◆ is_totally_ordered

◆ preserve_top

◆ preserve_bot

◆ injective_concretization

◆ preserve_concrete_covers

◆ complemented

◆ increasing

◆ name

◆ is_arithmetic