#include <pre_binc.hpp>

Public Types
using	this_type = PreBInc

using	dual_type = PreBDec

using	value_type = bool

using	increasing_type = PreBInc

Static Public Member Functions
CUDA static constexpr value_type	zero ()

CUDA static constexpr value_type	one ()

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

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

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

template<class F >
static CUDA F	deinterpret (const value_type &v)

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

static constexpr const bool	preserve_bot = true

static constexpr const bool	preserve_top = false

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 bool	complemented = false

static constexpr const bool	increasing = true

static constexpr const char *	name = "BInc"

static constexpr const bool	is_arithmetic = true

Detailed Description

PreBInc is a pre-abstract universe \( \langle \{\mathit{true}, \mathit{false}\}, \leq \rangle \) such that \( \mathit{false} \leq \mathit{true} \). It is used to represent Boolean variables which truth's value progresses from \( \mathit{false} \) to \( \mathit{true} \). Note that this type is unable to represent Boolean domain which requires four states: unknown (bot), true, false and failed (top). To obtain such a domain, you should use Interval<BInc>.

Member Typedef Documentation

◆ this_type

using lala::PreBInc::this_type = PreBInc

◆ dual_type

using lala::PreBInc::dual_type = PreBDec

◆ value_type

using lala::PreBInc::value_type = bool

◆ increasing_type

using lala::PreBInc::increasing_type = PreBInc

Member Function Documentation

◆ zero()

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

inlinestaticconstexpr

◆ one()

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

inlinestaticconstexpr

◆ interpret_tell()

template<bool diagnose, class F >

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

inlinestatic

Interpret a formula into an upset Boolean lattice.

Returns: The result of the interpretation when the formula f is a constant of type Bool. Otherwise it returns an explanation of the error.

◆ interpret_ask()

template<bool diagnose, class F >

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

inlinestatic

In this domain, the ask version of any constraint is the same as the tell version. This is because this domain can exactly represent Boolean values.

◆ interpret_type()

template<bool diagnose, class F >

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

inlinestatic

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.

◆ deinterpret()

template<class F >

static CUDA F lala::PreBInc::deinterpret ( const value_type & v )

inlinestatic

Given a Boolean value, create a logical constant representing that value. Note that the lattice order has no influence here.

◆ sig_order()

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

inlinestaticconstexpr

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::PreBInc::sig_strict_order ( )

inlinestaticconstexpr

◆ bot()

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

inlinestaticconstexpr

\( \bot \) is represented by false.

◆ top()

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

inlinestaticconstexpr

\( \top \) is represented by true.

◆ join()

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

inlinestaticconstexpr

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

◆ meet()

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

inlinestaticconstexpr

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

◆ order()

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

inlinestaticconstexpr

◆ fun() [1/2]

template<Sig sig>

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

inlinestaticconstexpr

◆ fun() [2/2]

template<Sig sig>

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

inlinestaticconstexpr

Member Data Documentation

◆ is_totally_ordered

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

staticconstexpr

◆ preserve_bot

constexpr const bool lala::PreBInc::preserve_bot = true

staticconstexpr

◆ preserve_top

constexpr const bool lala::PreBInc::preserve_top = false

staticconstexpr

◆ preserve_join

constexpr const bool lala::PreBInc::preserve_join = true

staticconstexpr

◆ preserve_meet

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

staticconstexpr

◆ injective_concretization

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

staticconstexpr

◆ preserve_concrete_covers

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

staticconstexpr

◆ complemented

constexpr const bool lala::PreBInc::complemented = false

staticconstexpr

◆ increasing

constexpr const bool lala::PreBInc::increasing = true

staticconstexpr

◆ name

constexpr const char* lala::PreBInc::name = "BInc"

staticconstexpr

◆ is_arithmetic

constexpr const bool lala::PreBInc::is_arithmetic = true

staticconstexpr

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

include/lala/universes/pre_binc.hpp

Public Types

Static Public Member Functions

Static Public Attributes

Detailed Description

Member Typedef Documentation

◆ this_type

◆ dual_type

◆ value_type

◆ increasing_type

Member Function Documentation

◆ zero()

◆ one()

◆ interpret_tell()

◆ interpret_ask()

◆ interpret_type()

◆ deinterpret()

◆ 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_totally_ordered

◆ preserve_bot

◆ preserve_top

◆ preserve_join

◆ preserve_meet

◆ injective_concretization

◆ preserve_concrete_covers

◆ complemented

◆ increasing

◆ name

◆ is_arithmetic