#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
CUDA static constexpr value_type	zero ()

CUDA static constexpr 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 CUDA constexpr Sig	sig_order ()

static CUDA constexpr Sig	sig_strict_order ()

static CUDA constexpr value_type	bot ()

static CUDA constexpr value_type	top ()

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

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

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

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

static CUDA constexpr value_type	next (value_type x)

static CUDA constexpr value_type	prev (value_type x)

CUDA static NI constexpr bool	is_supported_fun (Sig sig)

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

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

Static Public Attributes
static constexpr const bool	is_natural = true

static constexpr const bool	is_totally_ordered = true

static constexpr const bool	preserve_bot = false

static constexpr const bool	preserve_top = true

static constexpr const bool	preserve_join = true

static constexpr const bool	preserve_meet = true

static constexpr const bool	injective_concretization = true

static constexpr const bool	preserve_concrete_covers = true

static constexpr const char *	name = "B"

static constexpr 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()

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

inlinestaticconstexpr

◆ one()

CUDA static constexpr 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 CUDA constexpr 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 CUDA constexpr Sig lala::PreB::sig_strict_order ( )

inlinestaticconstexpr

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

◆ bot()

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

inlinestaticconstexpr

\( \bot \) is represented by false.

◆ top()

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

inlinestaticconstexpr

\( \top \) is represented by true.

◆ join()

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

inlinestaticconstexpr

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

◆ meet()

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

inlinestaticconstexpr

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

◆ order()

static CUDA constexpr 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 CUDA constexpr 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 CUDA constexpr 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 CUDA constexpr 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 NI constexpr bool lala::PreB::is_supported_fun ( Sig sig )

inlinestaticconstexpr

◆ fun() [1/2]

template<Sig sig>

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

inlinestaticconstexpr

◆ fun() [2/2]

template<Sig sig>

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

inlinestaticconstexpr

Member Data Documentation

◆ is_natural

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

staticconstexpr

◆ is_totally_ordered

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

staticconstexpr

◆ preserve_bot

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

staticconstexpr

◆ preserve_top

constexpr 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 const bool lala::PreB::preserve_join = true

staticconstexpr

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

◆ preserve_meet

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

staticconstexpr

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

◆ injective_concretization

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

staticconstexpr

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

◆ preserve_concrete_covers

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

staticconstexpr

Each element of PreB maps to a different concrete value.

◆ name

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

staticconstexpr

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

◆ is_arithmetic

constexpr 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