#include <pre_b.hpp>

Public Types
using	this_type = PreB

using	dual_type = PreBD

using	value_type = bool

using	natural_order = PreB

Static Public Member Functions
constexpr static CUDA value_type	zero ()

constexpr static CUDA value_type	one ()

template<bool diagnose, class F , bool dualize = false>
static CUDA bool	interpret_tell (const F &f, value_type &tell, IDiagnostics &diagnostics)

template<bool diagnose, class F , bool dualize = false>
static CUDA bool	interpret_ask (const F &f, value_type &ask, IDiagnostics &diagnostics)

template<bool diagnose, class F , bool dualize = false>
CUDA static NI bool	interpret_type (const F &f, value_type &k, IDiagnostics &diagnostics)

static constexpr CUDA Sig	sig_order ()

static constexpr CUDA Sig	sig_strict_order ()

static constexpr CUDA value_type	bot ()

static constexpr CUDA value_type	top ()

static constexpr CUDA value_type	join (value_type x, value_type y)

static constexpr CUDA value_type	meet (value_type x, value_type y)

static constexpr CUDA bool	order (value_type x, value_type y)

static constexpr CUDA bool	strict_order (value_type x, value_type y)

static constexpr CUDA value_type	next (value_type x)

static constexpr CUDA value_type	prev (value_type x)

CUDA static constexpr NI bool	is_supported_fun (Sig sig)

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

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

Static Public Attributes
constexpr static const bool	is_natural = true

constexpr static const bool	is_totally_ordered = true

constexpr static const bool	preserve_bot = false

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 = true

constexpr static const char *	name = "B"

constexpr static const bool	is_arithmetic = true

Detailed Description

PreB is a domain abstracting the Boolean universe of discourse \( \mathbb{B}=\{true,false\} \). We overload the symbols \( \mathit{true} \) and \( \mathit{false} \) to be used in both PreB and the concrete domain ( \( \bot, \top \) can be used to specifically refer to PreB elements). We have \( PreB \triangleq \langle \{\mathit{false}, \mathit{true}\}, \implies, \land, \lor, \mathit{false}, \mathit{true} \rangle \) with the usual logical connectors (in particular, \( \mathit{false} \implies \mathit{true} \), \( \bot = \mathit{false} \) and \( \top = \mathit{true} \)).

We have a Galois connection between the concrete domain of values \( \mathcal{P}(\mathbb{B}) \) and PreB: Concretization: \( \gamma(b) \triangleq b = \top ? \{\mathit{true}, \mathit{false}\} : \{\mathit{false}\} \). Abstraction: \( \alpha(S) \triangleq \mathit{true} \in S ? \top : \bot \).

Beware that, as suggested by the concretization function, \( \top \) represents both the true and false values in the concrete domain, and should be interpreted as "I don't know yet the value".

Further, note that this lattice is unable to represent exactly Dunn/Belnap logic which requires four states (which is necessary when working in the abstract): unknown, true, false and failed. To obtain Dunn/Belnap logic with a knowledge ordering, you can use Interval<Bound<PreB>>.

Member Typedef Documentation

◆ this_type

using lala::PreB::this_type = PreB

◆ dual_type

using lala::PreB::dual_type = PreBD

◆ value_type

using lala::PreB::value_type = bool

◆ natural_order

using lala::PreB::natural_order = PreB

We consider \( \top = \mathit{true} \) is the natural order on Boolean.

Member Function Documentation

◆ zero()

constexpr static CUDA value_type lala::PreB::zero ( )

inlinestaticconstexpr

◆ one()

constexpr static CUDA value_type lala::PreB::one ( )

inlinestaticconstexpr

◆ interpret_tell()

template<bool diagnose, class F , bool dualize = false>

static CUDA bool lala::PreB::interpret_tell	(	const F &	f,
		value_type &	tell,
		IDiagnostics &	diagnostics
	)

inlinestatic

@sequential Interpret a formula into the PreB lattice.

Returns: true if an overapproximation of a Boolean constant b could be placed in tell. Otherwise it returns false with a diagnostic.

◆ interpret_ask()

template<bool diagnose, class F , bool dualize = false>

static CUDA bool lala::PreB::interpret_ask	(	const F &	f,
		value_type &	ask,
		IDiagnostics &	diagnostics
	)

inlinestatic

@sequential We can only ask if an element of this lattice is false, because it cannot exactly represent true. This operation can be dualized.

◆ interpret_type()

template<bool diagnose, class F , bool dualize = false>

CUDA static NI bool lala::PreB::interpret_type	(	const F &	f,
		value_type &	k,
		IDiagnostics &	diagnostics
	)

inlinestatic

@sequential Verify if the type of a variable, introduced by an existential quantifier, is compatible with the current abstract universe.

Returns: bot() if the type of the existentially quantified variable is Bool. Otherwise it returns an explanation of the error. This operation can be dualized.

◆ sig_order()

static constexpr CUDA Sig lala::PreB::sig_order ( )

inlinestaticconstexpr

@parallel Given a Boolean value, create a logical constant representing that value. Note that the lattice order has no influence here. The logical predicate symbol corresponding to the order of this pre-universe. We have \( a \leq_\mathit{BInc} b \Leftrightarrow a \leq b \).

Returns: The logical symbol LEQ.

◆ sig_strict_order()

static constexpr CUDA Sig lala::PreB::sig_strict_order ( )

inlinestaticconstexpr

Converse nonimplication: we have a < b only when a is false and b is true.

◆ bot()

static constexpr CUDA value_type lala::PreB::bot ( )

inlinestaticconstexpr

\( \bot \) is represented by false.

◆ top()

static constexpr CUDA value_type lala::PreB::top ( )

inlinestaticconstexpr

\( \top \) is represented by true.

◆ join()

static constexpr CUDA value_type lala::PreB::join	(	value_type	x,
		value_type	y
	)

inlinestaticconstexpr

Returns: \( x \sqcup y \) defined as \( x \lor y \).

◆ meet()

static constexpr CUDA value_type lala::PreB::meet	(	value_type	x,
		value_type	y
	)

inlinestaticconstexpr

Returns: \( x \sqcap y \) defined as \( x \land y \).

◆ order()

static constexpr CUDA bool lala::PreB::order	(	value_type	x,
		value_type	y
	)

inlinestaticconstexpr

Returns: \( \mathit{true} \) if \( x \leq_\mathit{BInc} y \) where the order \( \mathit{false} \leq_\mathit{BInc} \mathit{true} \), otherwise returns \( \mathit{false} \). Note that the order is the Boolean implication, \( x \leq y \Rightleftarrow x \Rightarrow y \).

◆ strict_order()

static constexpr CUDA bool lala::PreB::strict_order	(	value_type	x,
		value_type	y
	)

inlinestaticconstexpr

Returns: \( \mathit{true} \) if \( x \leq_\mathit{BInc} y \) where the order \( \mathit{false} \leq_\mathit{BInc} \mathit{true} \), otherwise returns \( \mathit{false} \). Note that the strict order is the Boolean converse nonimplication, \( x \leq y \Rightleftarrow x \not\Leftarrow y \).

◆ next()

static constexpr CUDA value_type lala::PreB::next ( value_type x )

inlinestaticconstexpr

From a lattice perspective, this function returns an element \( y \) such that \( y \) is a cover of \( x \).

Returns: true.

◆ prev()

static constexpr CUDA value_type lala::PreB::prev ( value_type x )

inlinestaticconstexpr

From a lattice perspective, this function returns an element \( y \) such that \( x \) is a cover of \( y \).

Returns: false.

◆ is_supported_fun()

CUDA static constexpr NI bool lala::PreB::is_supported_fun ( Sig sig )

inlinestaticconstexpr

◆ fun() [1/2]

template<Sig sig>

static constexpr CUDA value_type lala::PreB::fun ( value_type x )

inlinestaticconstexpr

◆ fun() [2/2]

template<Sig sig>

CUDA static constexpr NI value_type lala::PreB::fun	(	value_type	x,
		value_type	y
	)

inlinestaticconstexpr

Member Data Documentation

◆ is_natural

constexpr static const bool lala::PreB::is_natural = true

staticconstexpr

◆ is_totally_ordered

constexpr static const bool lala::PreB::is_totally_ordered = true

staticconstexpr

◆ preserve_bot

constexpr static const bool lala::PreB::preserve_bot = false

staticconstexpr

◆ preserve_top

constexpr static const bool lala::PreB::preserve_top = true

staticconstexpr

\( \gamma(\mathit{false}) = \{\mathit{false}\} \), therefore the empty set cannot be represented in this domain.

◆ preserve_join

constexpr static const bool lala::PreB::preserve_join = true

staticconstexpr

\( \gamma(\mathit{unknown}) = \{false, true\} \)

◆ preserve_meet

constexpr static const bool lala::PreB::preserve_meet = true

staticconstexpr

\( \gamma(x \sqcup y) = \gamma(x) \cup \gamma(y) \)

◆ injective_concretization

constexpr static const bool lala::PreB::injective_concretization = true

staticconstexpr

\( \gamma(x \sqcap y) = \gamma(x) \cap \gamma(y) \)

◆ preserve_concrete_covers

constexpr static const bool lala::PreB::preserve_concrete_covers = true

staticconstexpr

Each element of PreB maps to a different concrete value.

◆ name

constexpr static const char* lala::PreB::name = "B"

staticconstexpr

\( x \lessdot y \Leftrightarrow \gamma(x) \lessdot \gamma(y) \)

◆ is_arithmetic

constexpr static const bool lala::PreB::is_arithmetic = true

staticconstexpr

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

include/lala/universes/pre_b.hpp

Public Types

Static Public Member Functions

Static Public Attributes

Detailed Description

Member Typedef Documentation

◆ this_type

◆ dual_type

◆ value_type

◆ natural_order

Member Function Documentation

◆ zero()

◆ one()

◆ interpret_tell()

◆ interpret_ask()

◆ interpret_type()

◆ sig_order()

◆ sig_strict_order()

◆ bot()

◆ top()

◆ join()

◆ meet()

◆ order()

◆ strict_order()

◆ next()

◆ prev()

◆ is_supported_fun()

◆ fun() [1/2]

◆ fun() [2/2]

Member Data Documentation

◆ is_natural

◆ is_totally_ordered

◆ preserve_bot

◆ preserve_top

◆ preserve_join

◆ preserve_meet

◆ injective_concretization

◆ preserve_concrete_covers

◆ name

◆ is_arithmetic