Namespaces
namespace	local

Classes
class	AbstractDeps

struct	AtomicExtraction

class	AVar

class	CartesianProduct

struct	DispatchIndex

class	FlatUniverse

class	GaussSeidelIteration

struct	HashMapVarIndex

class	IDiagnostics

class	Interval

struct	ListVarIndex

class	NBitset

struct	NonAtomicExtraction

struct	PreBDec

struct	PreBInc

struct	PreFDec

struct	PreFInc

struct	PreSDec

struct	PreSInc

struct	PreZDec

struct	PreZInc

class	PrimitiveUpset

class	Simplifier

struct	Sort

class	TFormula

class	VarEnv

struct	Variable

class	VStore

Typedefs
template<class A >
using	abstract_ptr = battery::shared_ptr<A, typename A::allocator_type>

template<class Allocator >
using	LVar = battery::string<Allocator>

using	AType = int

using	logic_bool = bool

using	logic_int = long long int

using	logic_real = battery::tuple<double, double>

template<class F >
using	logic_set = battery::vector<battery::tuple<F, F>, typename F::allocator_type>

template<class VT , class Mem >
using	ZFlat = FlatUniverse<PreZInc<VT>, Mem>

template<class VT , class Mem >
using	FFlat = FlatUniverse<PreFInc<VT>, Mem>

template<class VT , class Mem >
using	ZInc = PrimitiveUpset<PreZInc<VT>, Mem>

template<class VT , class Mem >
using	ZDec = PrimitiveUpset<PreZDec<VT>, Mem>

template<class VT , class Mem >
using	FInc = PrimitiveUpset<PreFInc<VT>, Mem>

template<class VT , class Mem >
using	FDec = PrimitiveUpset<PreFDec<VT>, Mem>

template<class Mem >
using	BInc = PrimitiveUpset<PreBInc, Mem>

template<class Mem >
using	BDec = PrimitiveUpset<PreBDec, Mem>

Enumerations
enum class	IKind { ASK , TELL }

enum	Sig { NEG , ABS , ADD , SUB , MUL , POW , MIN , MAX , SQRT , EXP , LN , NROOT , LOG , SIN , COS , TAN , ASIN , ACOS , ATAN , SINH , COSH , TANH , ASINH , ACOSH , ATANH , DIV , MOD , TDIV , TMOD , FDIV , FMOD , CDIV , CMOD , EDIV , EMOD , UNION , INTERSECTION , DIFFERENCE , SYMMETRIC_DIFFERENCE , COMPLEMENT , SUBSET , SUBSETEQ , SUPSET , SUPSETEQ , IN , CARD , HULL , CONVEX , EQ , NEQ , LEQ , GEQ , LT , GT , AND , OR , IMPLY , EQUIV , NOT , XOR , ITE , MAXIMIZE , MINIMIZE }

Functions
template<size_t i, class... As>
CUDA constexpr const CartesianProduct< As... >::template type_of< i > &	project (const CartesianProduct< As... > &cp)
	Similar to `cp.template project<i>()`, just to avoid the ".template" syntax.

template<size_t i, class... As>
CUDA constexpr CartesianProduct< As... >::template type_of< i > &	project (CartesianProduct< As... > &cp)

template<class... As, class... Bs>
CUDA constexpr auto	join (const CartesianProduct< As... > &a, const CartesianProduct< Bs... > &b)

template<class... As, class... Bs>
CUDA constexpr auto	meet (const CartesianProduct< As... > &a, const CartesianProduct< Bs... > &b)

template<class... As, class... Bs>
CUDA constexpr bool	operator< (const CartesianProduct< As... > &a, const CartesianProduct< Bs... > &b)

template<class... As, class... Bs>
CUDA constexpr bool	operator> (const CartesianProduct< As... > &a, const CartesianProduct< Bs... > &b)

template<class... As, class... Bs>
CUDA constexpr bool	operator== (const CartesianProduct< As... > &a, const CartesianProduct< Bs... > &b)

template<class A , class... As>
std::ostream &	operator<< (std::ostream &s, const CartesianProduct< A, As... > &cp)

template<class L , IKind kind, bool diagnose = false, class F >
CUDA bool	ginterpret_true (const F &f, IDiagnostics &diagnostics)

template<IKind kind, bool diagnose = false, class A , class F , class Env , class I >
CUDA bool	ginterpret_in (const A &a, const F &f, Env &env, I &intermediate, IDiagnostics &diagnostics)

template<IKind kind, bool diagnose = false, class F , class Env , class U >
CUDA bool	ginterpret_in (const F &f, const Env &env, U &value, IDiagnostics &diagnostics)

template<IKind kind, bool diagnose = false, class A , class F , class Env , class I >
CUDA bool	top_level_ginterpret_in (const A &a, const F &f, Env &env, I &intermediate, IDiagnostics &diagnostics)

template<class A , class Alloc = battery::standard_allocator, class Env >
CUDA A	make_bot (Env &env, Alloc alloc=Alloc{})

template<bool diagnose = false, class TellAlloc = battery::standard_allocator, class F , class Env , class L >
CUDA bool	interpret_and_tell (const F &f, Env &env, L &value, IDiagnostics &diagnostics, TellAlloc tell_alloc=TellAlloc{})

template<class A , bool diagnose = false, class F , class Env , class TellAlloc = typename A::allocator_type>
CUDA std::optional< A >	create_and_interpret_and_tell (const F &f, Env &env, IDiagnostics &diagnostics, typename A::allocator_type alloc=typename A::allocator_type{}, TellAlloc tell_alloc=TellAlloc{})

template<class L , class K >
CUDA constexpr auto	join (const Interval< L > &a, const Interval< K > &b)

template<class L , class K >
CUDA constexpr auto	meet (const Interval< L > &a, const Interval< K > &b)

template<class L , class K >
CUDA constexpr bool	operator< (const Interval< L > &a, const Interval< K > &b)

template<class L , class K >
CUDA constexpr bool	operator> (const Interval< L > &a, const Interval< K > &b)

template<class L , class K >
CUDA constexpr bool	operator== (const Interval< L > &a, const Interval< K > &b)

template<class L >
std::ostream &	operator<< (std::ostream &s, const Interval< L > &itv)

template<class Allocator , class ExtendedSig >
CUDA NI bool	is_v_op_constant (const TFormula< Allocator, ExtendedSig > &f, Sig sig)

template<class Allocator , class ExtendedSig >
CUDA NI bool	is_v_op_z (const TFormula< Allocator, ExtendedSig > &f, Sig sig)

template<class Allocator , class ExtendedSig >
CUDA NI bool	is_var_equality (const TFormula< Allocator, ExtendedSig > &f)

template<class Allocator >
CUDA NI TFormula< Allocator >	make_v_op_z (LVar< Allocator > v, Sig sig, logic_int z, AType aty=UNTYPED, const Allocator &allocator=Allocator())

template<class Allocator >
CUDA NI TFormula< Allocator >	make_v_op_z (AVar v, Sig sig, logic_int z, AType aty=UNTYPED, const Allocator &allocator=Allocator())

template<class Allocator >
CUDA Sig	geq_of_constant (const TFormula< Allocator > &f)

template<class Allocator >
CUDA Sig	leq_of_constant (const TFormula< Allocator > &f)

template<typename Allocator , typename ExtendedSig >
CUDA const TFormula< Allocator, ExtendedSig > &	var_in (const TFormula< Allocator, ExtendedSig > &f)

template<class F >
CUDA NI int	num_vars (const F &f)

template<class F >
CUDA int	num_quantified_vars (const F &f)

template<class F >
CUDA int	num_quantified_vars (const F &f, AType aty)

template<class F >
CUDA NI AType	type_of_conjunction (const typename F::Sequence &seq)

template<class F >
CUDA NI battery::tuple< F, F >	extract_ty (const F &f, AType ty)

template<class F >
CUDA NI thrust::optional< F >	negate (const F &f)

template<class F >
CUDA NI thrust::optional< F >	de_morgan_law (Sig sig_neg, const F &f)

template<class F >
CUDA NI thrust::optional< F >	negate_eq (const F &f)

CUDA Sig	negate_arithmetic_comparison (Sig sig)

template<class F >
CUDA NI bool	is_arithmetic_comparison (const F &f)

template<class F >
CUDA NI bool	is_set_comparison (const F &f)

template<class F >
CUDA NI bool	is_comparison (const F &f)

CUDA NI Sig	converse_comparison (Sig sig)

template<class F >
CUDA NI F	move_constants_on_rhs (const F &f)

template<class F , class Env >
CUDA NI void	map_avar_to_lvar (F &f, const Env &env, bool erase_type=false)

template<class F >
CUDA NI F	eval (const F &f)

CUDA NI const char *	string_of_sig (Sig sig)

CUDA NI constexpr bool	is_prefix (Sig sig)

CUDA NI constexpr bool	is_division (Sig sig)

CUDA NI constexpr bool	is_modulo (Sig sig)

CUDA NI constexpr bool	is_associative (Sig sig)

template<typename Allocator , typename ExtendedSig >
CUDA bool	operator== (const TFormula< Allocator, ExtendedSig > &lhs, const TFormula< Allocator, ExtendedSig > &rhs)

template<class F , class Env >
CUDA NI thrust::optional< const typename Env::variable_type & >	var_in (const F &f, const Env &env)

template<class Alloc1 , class Alloc2 >
CUDA NI bool	operator== (const Sort< Alloc1 > &lhs, const Sort< Alloc2 > &rhs)

template<class Pre , class M1 , class M2 >
CUDA constexpr FlatUniverse< Pre, battery::local_memory >	join (const FlatUniverse< Pre, M1 > &a, const FlatUniverse< Pre, M2 > &b)

template<class Pre , class M1 , class M2 >
CUDA constexpr FlatUniverse< Pre, battery::local_memory >	meet (const FlatUniverse< Pre, M1 > &a, const FlatUniverse< Pre, M2 > &b)

template<class Pre , class M1 , class M2 >
CUDA constexpr bool	operator< (const FlatUniverse< Pre, M1 > &a, const FlatUniverse< Pre, M2 > &b)

template<class Pre , class M1 , class M2 >
CUDA constexpr bool	operator> (const FlatUniverse< Pre, M1 > &a, const FlatUniverse< Pre, M2 > &b)

template<class Pre , class M1 , class M2 >
CUDA constexpr bool	operator== (const FlatUniverse< Pre, M1 > &a, const FlatUniverse< Pre, M2 > &b)

template<class Pre , class M >
std::ostream &	operator<< (std::ostream &s, const FlatUniverse< Pre, M > &a)

template<size_t N, class M1 , class M2 , class T >
CUDA constexpr NBitset< N, battery::local_memory, T >	join (const NBitset< N, M1, T > &a, const NBitset< N, M2, T > &b)

template<size_t N, class M1 , class M2 , class T >
CUDA constexpr NBitset< N, battery::local_memory, T >	meet (const NBitset< N, M1, T > &a, const NBitset< N, M2, T > &b)

template<size_t N, class M1 , class M2 , class T >
CUDA constexpr bool	operator< (const NBitset< N, M1, T > &a, const NBitset< N, M2, T > &b)

template<size_t N, class M1 , class M2 , class T >
CUDA constexpr bool	operator> (const NBitset< N, M1, T > &a, const NBitset< N, M2, T > &b)

template<size_t N, class M1 , class M2 , class T >
CUDA constexpr bool	operator== (const NBitset< N, M1, T > &a, const NBitset< N, M2, T > &b)

template<size_t N, class M , class T >
std::ostream &	operator<< (std::ostream &s, const NBitset< N, M, T > &a)

template<class LDual , class L >
CUDA constexpr LDual	dual (const L &x)

template<class Pre , class M1 , class M2 >
CUDA constexpr PrimitiveUpset< Pre, battery::local_memory >	join (const PrimitiveUpset< Pre, M1 > &a, const PrimitiveUpset< Pre, M2 > &b)

template<class Pre , class M1 , class M2 >
CUDA constexpr PrimitiveUpset< Pre, battery::local_memory >	meet (const PrimitiveUpset< Pre, M1 > &a, const PrimitiveUpset< Pre, M2 > &b)

template<class Pre , class M1 , class M2 >
CUDA constexpr bool	operator< (const PrimitiveUpset< Pre, M1 > &a, const PrimitiveUpset< Pre, M2 > &b)

template<class Pre , class M1 , class M2 >
CUDA constexpr bool	operator> (const PrimitiveUpset< Pre, M1 > &a, const PrimitiveUpset< Pre, M2 > &b)

template<class Pre , class M1 , class M2 >
CUDA constexpr bool	operator== (const PrimitiveUpset< Pre, M1 > &a, const PrimitiveUpset< Pre, M2 > &b)

template<class Pre , class M >
std::ostream &	operator<< (std::ostream &s, const PrimitiveUpset< Pre, M > &upset)

template<class L , class K , class Alloc >
CUDA auto	join (const VStore< L, Alloc > &a, const VStore< K, Alloc > &b)

template<class L , class K , class Alloc >
CUDA auto	meet (const VStore< L, Alloc > &a, const VStore< K, Alloc > &b)

template<class L , class K , class Alloc1 , class Alloc2 >
CUDA bool	operator< (const VStore< L, Alloc1 > &a, const VStore< K, Alloc2 > &b)

template<class L , class K , class Alloc1 , class Alloc2 >
CUDA bool	operator> (const VStore< L, Alloc1 > &a, const VStore< K, Alloc2 > &b)

template<class L , class K , class Alloc1 , class Alloc2 >
CUDA bool	operator== (const VStore< L, Alloc1 > &a, const VStore< K, Alloc2 > &b)

template<class L , class Alloc >
std::ostream &	operator<< (std::ostream &s, const VStore< L, Alloc > &vstore)

Detailed Description

This file provides an extended interface to interpret formulas in abstract domains and abstract universes. It also provides a unified interface for tell and ask interpretation using a template parameter IKind.

A pre-abstract universe is a lattice (with usual operations join, order, ...) equipped with a simple logical interpretation function and a next/prev functions. We consider totally ordered pre-abstract universes with an upset semantics. For any lattice \( L \), we consider an element \( a \in L \) to represent all the concrete elements equal to or above it. This set is called the upset of \( a \) and is denoted \( \mathord{\uparrow}{a} \). The concretization function \( \gamma \) formalizes this idea: \( \gamma(a) = \{x \mapsto b \;|\; b \in \mathord{\uparrow}{a} \cap U \} \) where \( U \) is the universe of discourse. The intersection with \( U \) is necessary to remove potential elements in the abstract universe that are not in the concrete universe of discourse (e.g., \( -\infty, \infty \) below).

The upset semantics associates each element of a lattice to its concrete upset. It is possible to decide that each element is associated to the concrete downset instead. Doing so will reverse our usage of the lattice-theoretic operations (join instead of meet, <= instead of >=, etc.). Instead of considering the upset semantics, it is more convenient to consider the downset semantics of the dual lattice.

Example: The lattice of increasing integer \( \mathit{ZInc} = \langle \{-\infty, \ldots, -2, -1, 0, 1, 2, \ldots, \infty\}, \leq \rangle \) is ordered by the natural arithmetic comparison operator. Using the upset semantics, we can represent simple constraints such as \( x \geq 3 \), in which case the upset \( \mathord{\uparrow}{3} = \{3, 4, \ldots\} \) represents all the values of \( x \) satisfying the constraints \( x \geq 3 \), that is, the solutions of the constraints. By taking the downset semantics of \( \mathit{ZInc} \), we can represent constraints such as \( x \leq 3 \). Alternatively, we can take the dual lattice of decreasing integers \( \mathit{ZDec} = \langle \{\infty, \ldots, 2, 1, 0, -1, -2, \ldots, -\infty\}, \geq \rangle \). The upset semantics of \( \mathit{ZDec} \) corresponds to the downset semantics of \( \mathit{ZInc} \).

From a pre-abstract universe, we obtain an abstract universe using the Universe class below. We also define various aliases to abstract universes such as ZInc, ZDec, etc.

Typedef Documentation

◆ abstract_ptr

template<class A >

using lala::abstract_ptr = battery::shared_ptr<A, typename A::allocator_type>

◆ LVar

template<class Allocator >

using lala::LVar = battery::string<Allocator>

A "logical variable" is just the name of the variable.

◆ AType

using lala::AType = int

Each abstract domain is uniquely identified by an UID. We call it an abstract type. Each formula (and recursively, its subformulas) is assigned to an abstract type indicating in what abstract domain this formula should be interpreted.

◆ logic_bool

using lala::logic_bool = bool

The type of Boolean used in logic formulas.

◆ logic_int

using lala::logic_int = long long int

The type of integers used in logic formulas. Integers are represented by the set \( \{-\infty, \infty\} \cup Z (\text{ with} Z \subset \mathbb{Z}) \). The minimal and maximal values of logic_int represents \( -\infty \) and \( \infty \) respectively.

◆ logic_real

using lala::logic_real = battery::tuple<double, double>

The type of real numbers used in logic formulas. Real numbers are approximated by the set \( \mathbb{F} \times \mathbb{F} \). When a real number \( r \in \mathbb{R} \) is also a floating-point number, then it is represented by \( (r, r) \), otherwise it is represented by \( (\lfloor r \rfloor, \lceil r \rceil) \) such that \( \lfloor r \rfloor < r < \lceil r \rceil \) and there is no floating-point number \( f \) such that \( \lfloor r \rfloor < f < \lceil r \rceil \).

◆ logic_set

template<class F >

using lala::logic_set = battery::vector<battery::tuple<F, F>, typename F::allocator_type>

A set is parametric in a universe of discourse. For instance, logic_set<F>, with F representing an integer constant, is a set of integers. Sets are defined in extension: we explicitly list the values belonging to the set. To avoid using too much memory with large sets, we use an interval representation, e.g., \( \{1..3, 5..5, 10..12\} = \{1, 2, 3, 5, 10, 11, 12\} \). When sets occur in intervals, they are ordered by set inclusion, e.g., \( \{\{1..2\}..\{1..4\}\} = \{\{1,2\}, \{1,2,3\}, \{1,2,4\}, \{1,2,3,4\}\} \).

◆ ZFlat

template<class VT , class Mem >

using lala::ZFlat = FlatUniverse<PreZInc<VT>, Mem>

Lattice of flat integers.

◆ FFlat

template<class VT , class Mem >

using lala::FFlat = FlatUniverse<PreFInc<VT>, Mem>

Lattice of flat floating-point numbers.

◆ ZInc

template<class VT , class Mem >

using lala::ZInc = PrimitiveUpset<PreZInc<VT>, Mem>

Lattice of increasing integers. Concretization function: \( \gamma(x) = \{_ \mapsto y \;|\; x \leq y\} \).

◆ ZDec

template<class VT , class Mem >

using lala::ZDec = PrimitiveUpset<PreZDec<VT>, Mem>

Lattice of decreasing integers. Concretization function: \( \gamma(x) = \{_ \mapsto y \;|\; x \geq y\} \).

◆ FInc

template<class VT , class Mem >

using lala::FInc = PrimitiveUpset<PreFInc<VT>, Mem>

Lattice of increasing floating-point numbers. Concretization function: \( \gamma(x) = \{_ \mapsto y \;|\; y \in \mathbb{R}, x \leq y\} \).

◆ FDec

template<class VT , class Mem >

using lala::FDec = PrimitiveUpset<PreFDec<VT>, Mem>

Lattice of decreasing floating-point numbers. Concretization function: \( \gamma(x) = \{_ \mapsto y \;|\; y \in \mathbb{R}, x \geq y\} \).

◆ BInc

template<class Mem >

using lala::BInc = PrimitiveUpset<PreBInc, Mem>

Lattice of increasing Boolean where \( \mathit{false} \leq \mathit{true} \).

◆ BDec

template<class Mem >

using lala::BDec = PrimitiveUpset<PreBDec, Mem>

Lattice of decreasing Boolean where \( \mathit{true} \leq \mathit{false} \).

Enumeration Type Documentation

◆ IKind

enum class lala::IKind

strong

The kind of interpretation operations.

Enumerator
ASK
TELL

◆ Sig

enum lala::Sig

A first-order signature is a triple \( (X, F, P) \) where \( X \) is the set of variables, \( F \) the set of function symbols and \( P \) the set of predicates. We represent \( X \) by strings (see LVar), while \( F \) and \( P \) are described in the following enumeration Sig. For programming conveniency, we suppose that logical connectors are included in the set of predicates and thus are in the signature as well. Finally, function symbols and predicates are at the "same level". Hence a predicate can occur as the argument of a function, which is convenient when modelling, consider for example a cardinality constraint: \( ((x > 4) + (y < 4) + (z = 3)) \neq 2 \).

Symbols are sometimes overloaded across different universe of discourse. For instance, ADD can be used over integers, reals and even set of integers (pairwise addition).

Division and modulus are defined as usual over continuous domains such as rational and real numbers. However, it gets more tricky when defined over discrete domains such as integers and floating-point numbers, since there is not a single definition of division and modulus. The various kinds of discrete divisions are explained in (Leijend D. (2003). Division and Modulus for Computer Scientists), and we add four of those definitions to the logical signature. There are several use-cases of modulus and division: If you write a constraint model, you probably want to use euclidean division and modulus (EDIV, EMOD) as this is the most "mathematical" definition. If you intend to model the semantics of a programming language, you should use the same kind of division as the one present in your programming language (most likely truncated division).

Enumerator
NEG	Unary arithmetic function symbols.
ABS	Unary arithmetic function symbols.
ADD	Unary arithmetic function symbols.
SUB	Unary arithmetic function symbols.
MUL	Unary arithmetic function symbols.
POW	Unary arithmetic function symbols.
MIN	Unary arithmetic function symbols.
MAX	Binary arithmetic function symbols.
SQRT	Unary arithmetic function symbols.
EXP	Unary arithmetic function symbols.
LN	Square root, natural exponential and natural logarithm function symbols.
NROOT	Unary arithmetic function symbols.
LOG	nth root and logarithm to base (both binary function symbols).
SIN	Unary arithmetic function symbols.
COS	Unary arithmetic function symbols.
TAN	Unary arithmetic function symbols.
ASIN	Unary arithmetic function symbols.
ACOS	Unary arithmetic function symbols.
ATAN	Unary arithmetic function symbols.
SINH	Unary arithmetic function symbols.
COSH	Unary arithmetic function symbols.
TANH	Unary arithmetic function symbols.
ASINH	Unary arithmetic function symbols.
ACOSH	Unary arithmetic function symbols.
ATANH	Trigonometric unary function symbols.
DIV	Unary arithmetic function symbols.
MOD	Division and modulus over continuous domains (e.g., floating-point numbers and rational).
TDIV	Unary arithmetic function symbols.
TMOD	Truncated division, present in most programming languages, is defined as \( a\,\mathbf{tdiv}\,b = \mathit{trunc}(a/b) \), i.e., it rounds towards zero. Modulus is defined as \( a\,\mathbf{tmod}\,b = a - b * (a\,\mathbf{tdiv}\,b) \).
FDIV	Unary arithmetic function symbols.
FMOD	Floor division (Knuth D. (1972). The Art of Computer Programming, Vol 1, Fundamental Algorithms), is defined as \( a\,\mathbf{fdiv}\,b = \lfloor a/b \rfloor \), i.e., it rounds towards negative infinity. Modulus is defined as \( a\,\mathbf{fmod}\,b = a - b * (a\,\mathbf{fdiv}\,b) \).
CDIV	Unary arithmetic function symbols.
CMOD	Ceil division is defined as \( a\,\mathbf{cdiv}\,b = \lceil a/b \rceil \). Modulus is defined as \( a\,\mathbf{cmod}\,b = a - b * (a\,\mathbf{cdiv}\,b) \).
EDIV	Unary arithmetic function symbols.
EMOD	Euclidean division (Boute T. R. (1992). The Euclidean definition of the functions div and mod). The properties satisfy by this division are: (1) \( a\,\mathbf{ediv}\,b \in \mathbb{Z} \), (2) \( a = b * (a\,\mathbf{ediv}\,b) + (a\,\mathbf{emod}\,b) \) and (3) \( 0 \leq a\,\mathbf{emod}\,b < \|b\|\). Further, note that Euclidean division satisfies \( a\,\mathbf{ediv}\,(-b) = -(a\,\mathbf{ediv}\,b) \) and \( a\,\mathbf{emod}\,(-b) = a\,\mathbf{emod}\,b \).
UNION	Unary arithmetic function symbols.
INTERSECTION	Unary arithmetic function symbols.
DIFFERENCE	Unary arithmetic function symbols.
SYMMETRIC_DIFFERENCE	Unary arithmetic function symbols.
COMPLEMENT	Set functions.
SUBSET	Unary arithmetic function symbols.
SUBSETEQ	Unary arithmetic function symbols.
SUPSET	Unary arithmetic function symbols.
SUPSETEQ	Set inclusion predicates.
IN	Set membership predicate.
CARD	Cardinality function from set to integer.
HULL	Unary function performing the convex hull of a set, e.g., \( \mathit{hull}(s) = \{x \;\|\; \mathit{min}(s) \leq x \leq \mathit{max}(s) \} \).
CONVEX	Unary predicate, requiring \( s = \mathit{hull}(s) \).
EQ	Unary arithmetic function symbols.
NEQ	Equality relations.
LEQ	Unary arithmetic function symbols.
GEQ	Unary arithmetic function symbols.
LT	Unary arithmetic function symbols.
GT	Arithmetic comparison predicates. When applied to set, it corresponds to the lexicographic ordering of the sorted set according the underlying natural ordering of the elements in the set.
AND	Unary arithmetic function symbols.
OR	Unary arithmetic function symbols.
IMPLY	Unary arithmetic function symbols.
EQUIV	Unary arithmetic function symbols.
NOT	Unary arithmetic function symbols.
XOR	Logical connector.
ITE	If-then-else.
MAXIMIZE	Unary "meta-predicate" indicating that its argument must be maximized, according to the increasing ordering of the underlying universe of discourse. This is not a predicate because it is defined on the solutions space of the whole formulas.
MINIMIZE	Same as MAXIMIZE, but for minimization.

Function Documentation

◆ project() [1/2]

template<size_t i, class... As>

CUDA constexpr const CartesianProduct< As... >::template type_of< i > & lala::project ( const CartesianProduct< As... > & cp )

constexpr

Similar to cp.template project<i>(), just to avoid the ".template" syntax.

◆ project() [2/2]

template<size_t i, class... As>

CUDA constexpr CartesianProduct< As... >::template type_of< i > & lala::project ( CartesianProduct< As... > & cp )

constexpr

◆ join() [1/6]

template<class... As, class... Bs>

CUDA constexpr auto lala::join	(	const CartesianProduct< As... > &	a,
		const CartesianProduct< Bs... > &	b )

constexpr

\( (a_1, \ldots, a_n) \sqcup (b_1, \ldots, b_n) = (a_1 \sqcup_1 b_1, \ldots, a_n \sqcup_n b_n) \)

◆ meet() [1/6]

template<class... As, class... Bs>

CUDA constexpr auto lala::meet	(	const CartesianProduct< As... > &	a,
		const CartesianProduct< Bs... > &	b )

constexpr

\( (a_1, \ldots, a_n) \sqcap (b_1, \ldots, b_n) = (a_1 \sqcap_1 b_1, \ldots, a_n \sqcap_n b_n) \)

◆ operator<() [1/6]

template<class... As, class... Bs>

CUDA constexpr bool lala::operator<	(	const CartesianProduct< As... > &	a,
		const CartesianProduct< Bs... > &	b )

constexpr

◆ operator>() [1/6]

template<class... As, class... Bs>

CUDA constexpr bool lala::operator>	(	const CartesianProduct< As... > &	a,
		const CartesianProduct< Bs... > &	b )

constexpr

◆ operator==() [1/8]

template<class... As, class... Bs>

CUDA constexpr bool lala::operator==	(	const CartesianProduct< As... > &	a,
		const CartesianProduct< Bs... > &	b )

constexpr

◆ operator<<() [1/6]

template<class A , class... As>

std::ostream & lala::operator<<	(	std::ostream &	s,
		const CartesianProduct< A, As... > &	cp )

◆ ginterpret_true()

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

CUDA bool lala::ginterpret_true	(	const F &	f,
		IDiagnostics &	diagnostics )

Interpret true in the lattice L.

Returns: true if L preserves the bottom element w.r.t. the concrete domain or if true is interpreted by under-approximation (kind == ASK).

◆ ginterpret_in() [1/2]

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

CUDA bool lala::ginterpret_in	(	const A &	a,
		const F &	f,
		Env &	env,
		I &	intermediate,
		IDiagnostics &	diagnostics )

This function provides an extended and unified interface to ask and tell interpretation of formula in abstract domains. It provides default interpretation for common formulas such as true, false and conjunction of formulas whenever A satisfies some lattice-theoretic conditions.

◆ ginterpret_in() [2/2]

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

CUDA bool lala::ginterpret_in	(	const F &	f,
		const Env &	env,
		U &	value,
		IDiagnostics &	diagnostics )

This function provides an extended and unified interface to ask and tell interpretation of formula in abstract universes. It provides default interpretation for common formulas such as true, false, conjunction and disjunction of formulas whenever U satisfies some lattice-theoretic conditions.

◆ top_level_ginterpret_in()

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

CUDA bool lala::top_level_ginterpret_in	(	const A &	a,
		const F &	f,
		Env &	env,
		I &	intermediate,
		IDiagnostics &	diagnostics )

Top-level version of ginterpret_in, we restore env and intermediate in case of failure.

◆ make_bot()

template<class A , class Alloc = battery::standard_allocator, class Env >

CUDA A lala::make_bot	(	Env &	env,
		Alloc	alloc = Alloc{} )

◆ interpret_and_tell()

template<bool diagnose = false, class TellAlloc = battery::standard_allocator, class F , class Env , class L >

CUDA bool lala::interpret_and_tell	(	const F &	f,
		Env &	env,
		L &	value,
		IDiagnostics &	diagnostics,
		TellAlloc	tell_alloc = TellAlloc{} )

◆ create_and_interpret_and_tell()

template<class A , bool diagnose = false, class F , class Env , class TellAlloc = typename A::allocator_type>

CUDA std::optional< A > lala::create_and_interpret_and_tell	(	const F &	f,
		Env &	env,
		IDiagnostics &	diagnostics,
		typename A::allocator_type	alloc = typename A::allocator_type{},
		TellAlloc	tell_alloc = TellAlloc{} )

◆ join() [2/6]

template<class L , class K >

CUDA constexpr auto lala::join	(	const Interval< L > &	a,
		const Interval< K > &	b )

constexpr

◆ meet() [2/6]

template<class L , class K >

CUDA constexpr auto lala::meet	(	const Interval< L > &	a,
		const Interval< K > &	b )

constexpr

◆ operator<() [2/6]

template<class L , class K >

CUDA constexpr bool lala::operator<	(	const Interval< L > &	a,
		const Interval< K > &	b )

constexpr

◆ operator>() [2/6]

template<class L , class K >

CUDA constexpr bool lala::operator>	(	const Interval< L > &	a,
		const Interval< K > &	b )

constexpr

◆ operator==() [2/8]

template<class L , class K >

CUDA constexpr bool lala::operator==	(	const Interval< L > &	a,
		const Interval< K > &	b )

constexpr

◆ operator<<() [2/6]

template<class L >

std::ostream & lala::operator<<	(	std::ostream &	s,
		const Interval< L > &	itv )

◆ is_v_op_constant()

template<class Allocator , class ExtendedSig >

CUDA NI bool lala::is_v_op_constant	(	const TFormula< Allocator, ExtendedSig > &	f,
		Sig	sig )

Returns: true if the formula f has the shape variable <sig> constant.

◆ is_v_op_z()

template<class Allocator , class ExtendedSig >

CUDA NI bool lala::is_v_op_z	(	const TFormula< Allocator, ExtendedSig > &	f,
		Sig	sig )

Returns: true if the formula f has the shape variable op integer constant, e.g., x < 4.

◆ is_var_equality()

template<class Allocator , class ExtendedSig >

CUDA NI bool lala::is_var_equality ( const TFormula< Allocator, ExtendedSig > & f )

Returns: true if the formula f has the shape variable = variable or variable <=> variable.

◆ make_v_op_z() [1/2]

template<class Allocator >

CUDA NI TFormula< Allocator > lala::make_v_op_z	(	LVar< Allocator >	v,
		Sig	sig,
		logic_int	z,
		AType	aty = UNTYPED,
		const Allocator &	allocator = Allocator() )

◆ make_v_op_z() [2/2]

template<class Allocator >

CUDA NI TFormula< Allocator > lala::make_v_op_z	(	AVar	v,
		Sig	sig,
		logic_int	z,
		AType	aty = UNTYPED,
		const Allocator &	allocator = Allocator() )

◆ geq_of_constant()

template<class Allocator >

CUDA Sig lala::geq_of_constant ( const TFormula< Allocator > & f )

◆ leq_of_constant()

template<class Allocator >

CUDA Sig lala::leq_of_constant ( const TFormula< Allocator > & f )

◆ var_in() [1/2]

template<typename Allocator , typename ExtendedSig >

CUDA const TFormula< Allocator, ExtendedSig > & lala::var_in ( const TFormula< Allocator, ExtendedSig > & f )

Returns: The first variable occurring in the formula, or any other subformula if the formula does not contain a variable. It returns either a logical variable, an abstract variable or a quantifier.

◆ num_vars()

template<class F >

CUDA NI int lala::num_vars ( const F & f )

Returns: The number of variables occurring in the formula F including existential quantifier, logical variables and abstract variables. Each occurrence of a variable is added up (duplicates are counted).

◆ num_quantified_vars() [1/2]

template<class F >

CUDA int lala::num_quantified_vars ( const F & f )

Returns: The number of existential quantifiers.

◆ num_quantified_vars() [2/2]

template<class F >

CUDA int lala::num_quantified_vars	(	const F &	f,
		AType	aty )

Returns: The number of variables occurring in an existential quantifier that have type aty.

◆ type_of_conjunction()

template<class F >

CUDA NI AType lala::type_of_conjunction ( const typename F::Sequence & seq )

◆ extract_ty()

template<class F >

CUDA NI battery::tuple< F, F > lala::extract_ty	(	const F &	f,
		AType	ty )

Given a conjunctive formula f of the form \( c_1 \land ... \land c_n \), it returns a pair \( \langle c_i \land .. \land c_j, c_k \land ... \land c_l \rangle \) such that the first component contains all formulas with the type ty, and the second component, all other formulas.

◆ negate()

template<class F >

CUDA NI thrust::optional< F > lala::negate ( const F & f )

◆ de_morgan_law()

template<class F >

CUDA NI thrust::optional< F > lala::de_morgan_law	(	Sig	sig_neg,
		const F &	f )

not(f1 \/ ... \/ fn) --> not(f1) /\ ... /\ not(fn) not(f1 /\ ... /\ fn) --> not(f1) \/ ... \/ not(fn)

◆ negate_eq()

template<class F >

CUDA NI thrust::optional< F > lala::negate_eq ( const F & f )

◆ negate_arithmetic_comparison()

CUDA Sig lala::negate_arithmetic_comparison ( Sig sig )

◆ is_arithmetic_comparison()

template<class F >

CUDA NI bool lala::is_arithmetic_comparison ( const F & f )

True for the operators <=, <, >, >=, =, !=

◆ is_set_comparison()

template<class F >

CUDA NI bool lala::is_set_comparison ( const F & f )

True for the operators =, !=, subset, subseteq, supset, supseteq

◆ is_comparison()

template<class F >

CUDA NI bool lala::is_comparison ( const F & f )

True for the operators <=, <, >, >=, =, !=, subset, subseteq, supset, supseteq

◆ converse_comparison()

CUDA NI Sig lala::converse_comparison ( Sig sig )

inline

Returns the converse of a comparison operator (see is_comparison).

◆ move_constants_on_rhs()

template<class F >

CUDA NI F lala::move_constants_on_rhs ( const F & f )

Given a predicate of the form t <op> u (e.g., x + y <= z + 4), it transforms it into an equivalent predicate of the form s <op> k where k is a constant (e.g., x + y - (z + 4) <= 0). If the formula is not a predicate, it is returned unchanged.

◆ map_avar_to_lvar()

template<class F , class Env >

CUDA NI void lala::map_avar_to_lvar	(	F &	f,
		const Env &	env,
		bool	erase_type = false )

Given a formula f, we transform all occurrences of AVar into logical variables.

◆ eval()

template<class F >

CUDA NI F lala::eval ( const F & f )

◆ string_of_sig()

CUDA NI const char * lala::string_of_sig ( Sig sig )

inline

◆ is_prefix()

CUDA NI constexpr bool lala::is_prefix ( Sig sig )

inlineconstexpr

◆ is_division()

CUDA NI constexpr bool lala::is_division ( Sig sig )

inlineconstexpr

◆ is_modulo()

CUDA NI constexpr bool lala::is_modulo ( Sig sig )

inlineconstexpr

◆ is_associative()

CUDA NI constexpr bool lala::is_associative ( Sig sig )

inlineconstexpr

◆ operator==() [3/8]

template<typename Allocator , typename ExtendedSig >

CUDA bool lala::operator==	(	const TFormula< Allocator, ExtendedSig > &	lhs,
		const TFormula< Allocator, ExtendedSig > &	rhs )

◆ var_in() [2/2]

template<class F , class Env >

CUDA NI thrust::optional< const typename Env::variable_type & > lala::var_in	(	const F &	f,
		const Env &	env )

Given a formula f and an environment, return the first variable occurring in f or {} if f has no variable in env.

◆ operator==() [4/8]

template<class Alloc1 , class Alloc2 >

CUDA NI bool lala::operator==	(	const Sort< Alloc1 > &	lhs,
		const Sort< Alloc2 > &	rhs )

inline

◆ join() [3/6]

template<class Pre , class M1 , class M2 >

CUDA constexpr FlatUniverse< Pre, battery::local_memory > lala::join	(	const FlatUniverse< Pre, M1 > &	a,
		const FlatUniverse< Pre, M2 > &	b )

constexpr

◆ meet() [3/6]

template<class Pre , class M1 , class M2 >

CUDA constexpr FlatUniverse< Pre, battery::local_memory > lala::meet	(	const FlatUniverse< Pre, M1 > &	a,
		const FlatUniverse< Pre, M2 > &	b )

constexpr

◆ operator<() [3/6]

template<class Pre , class M1 , class M2 >

CUDA constexpr bool lala::operator<	(	const FlatUniverse< Pre, M1 > &	a,
		const FlatUniverse< Pre, M2 > &	b )

constexpr

◆ operator>() [3/6]

template<class Pre , class M1 , class M2 >

CUDA constexpr bool lala::operator>	(	const FlatUniverse< Pre, M1 > &	a,
		const FlatUniverse< Pre, M2 > &	b )

constexpr

◆ operator==() [5/8]

template<class Pre , class M1 , class M2 >

CUDA constexpr bool lala::operator==	(	const FlatUniverse< Pre, M1 > &	a,
		const FlatUniverse< Pre, M2 > &	b )

constexpr

◆ operator<<() [3/6]

template<class Pre , class M >

std::ostream & lala::operator<<	(	std::ostream &	s,
		const FlatUniverse< Pre, M > &	a )

◆ join() [4/6]

template<size_t N, class M1 , class M2 , class T >

CUDA constexpr NBitset< N, battery::local_memory, T > lala::join	(	const NBitset< N, M1, T > &	a,
		const NBitset< N, M2, T > &	b )

constexpr

◆ meet() [4/6]

template<size_t N, class M1 , class M2 , class T >

CUDA constexpr NBitset< N, battery::local_memory, T > lala::meet	(	const NBitset< N, M1, T > &	a,
		const NBitset< N, M2, T > &	b )

constexpr

◆ operator<() [4/6]

template<size_t N, class M1 , class M2 , class T >

CUDA constexpr bool lala::operator<	(	const NBitset< N, M1, T > &	a,
		const NBitset< N, M2, T > &	b )

constexpr

◆ operator>() [4/6]

template<size_t N, class M1 , class M2 , class T >

CUDA constexpr bool lala::operator>	(	const NBitset< N, M1, T > &	a,
		const NBitset< N, M2, T > &	b )

constexpr

◆ operator==() [6/8]

template<size_t N, class M1 , class M2 , class T >

CUDA constexpr bool lala::operator==	(	const NBitset< N, M1, T > &	a,
		const NBitset< N, M2, T > &	b )

constexpr

◆ operator<<() [4/6]

template<size_t N, class M , class T >

std::ostream & lala::operator<<	(	std::ostream &	s,
		const NBitset< N, M, T > &	a )

◆ dual()

template<class LDual , class L >

CUDA constexpr LDual lala::dual ( const L & x )

constexpr

This function is useful when we need to convert a value to its dual. The dual is the downset of the current element, therefore, if we have \( x >= 10 \), the dual is given by the formula \( x <= 10 \) interpreted in the dual lattice. In that case, it just changes the type of the lattice without changing the value. A difference occurs on the bottom and top element. Indeed, by our representation of bot and top, the bottom value in a lattice L equals the top value in its dual, but we need them to remain the same, so the dual of L::bot() is LDual::bot().

◆ join() [5/6]

template<class Pre , class M1 , class M2 >

CUDA constexpr PrimitiveUpset< Pre, battery::local_memory > lala::join	(	const PrimitiveUpset< Pre, M1 > &	a,
		const PrimitiveUpset< Pre, M2 > &	b )

constexpr

◆ meet() [5/6]

template<class Pre , class M1 , class M2 >

CUDA constexpr PrimitiveUpset< Pre, battery::local_memory > lala::meet	(	const PrimitiveUpset< Pre, M1 > &	a,
		const PrimitiveUpset< Pre, M2 > &	b )

constexpr

◆ operator<() [5/6]

template<class Pre , class M1 , class M2 >

CUDA constexpr bool lala::operator<	(	const PrimitiveUpset< Pre, M1 > &	a,
		const PrimitiveUpset< Pre, M2 > &	b )

constexpr

◆ operator>() [5/6]

template<class Pre , class M1 , class M2 >

CUDA constexpr bool lala::operator>	(	const PrimitiveUpset< Pre, M1 > &	a,
		const PrimitiveUpset< Pre, M2 > &	b )

constexpr

◆ operator==() [7/8]

template<class Pre , class M1 , class M2 >

CUDA constexpr bool lala::operator==	(	const PrimitiveUpset< Pre, M1 > &	a,
		const PrimitiveUpset< Pre, M2 > &	b )

constexpr

◆ operator<<() [5/6]

template<class Pre , class M >

std::ostream & lala::operator<<	(	std::ostream &	s,
		const PrimitiveUpset< Pre, M > &	upset )

◆ join() [6/6]

template<class L , class K , class Alloc >

CUDA auto lala::join	(	const VStore< L, Alloc > &	a,
		const VStore< K, Alloc > &	b )

◆ meet() [6/6]

template<class L , class K , class Alloc >

CUDA auto lala::meet	(	const VStore< L, Alloc > &	a,
		const VStore< K, Alloc > &	b )

◆ operator<() [6/6]

template<class L , class K , class Alloc1 , class Alloc2 >

CUDA bool lala::operator<	(	const VStore< L, Alloc1 > &	a,
		const VStore< K, Alloc2 > &	b )

◆ operator>() [6/6]

template<class L , class K , class Alloc1 , class Alloc2 >

CUDA bool lala::operator>	(	const VStore< L, Alloc1 > &	a,
		const VStore< K, Alloc2 > &	b )

◆ operator==() [8/8]

template<class L , class K , class Alloc1 , class Alloc2 >

CUDA bool lala::operator==	(	const VStore< L, Alloc1 > &	a,
		const VStore< K, Alloc2 > &	b )

◆ operator<<() [6/6]

template<class L , class Alloc >

std::ostream & lala::operator<<	(	std::ostream &	s,
		const VStore< L, Alloc > &	vstore )

Namespaces

Classes

Typedefs

Enumerations

Functions

Detailed Description

Typedef Documentation

◆ abstract_ptr

◆ LVar

◆ AType

◆ logic_bool

◆ logic_int

◆ logic_real

◆ logic_set

◆ ZFlat

◆ FFlat

◆ ZInc

◆ ZDec

◆ FInc

◆ FDec

◆ BInc

◆ BDec

Enumeration Type Documentation

◆ IKind

◆ Sig

Function Documentation

◆ project() [1/2]

◆ project() [2/2]

◆ join() [1/6]

◆ meet() [1/6]

◆ operator<() [1/6]

◆ operator>() [1/6]

◆ operator==() [1/8]

◆ operator<<() [1/6]

◆ ginterpret_true()

◆ ginterpret_in() [1/2]

◆ ginterpret_in() [2/2]

◆ top_level_ginterpret_in()

◆ make_bot()

◆ interpret_and_tell()

◆ create_and_interpret_and_tell()

◆ join() [2/6]

◆ meet() [2/6]

◆ operator<() [2/6]

◆ operator>() [2/6]

◆ operator==() [2/8]

◆ operator<<() [2/6]

◆ is_v_op_constant()

◆ is_v_op_z()

◆ is_var_equality()

◆ make_v_op_z() [1/2]

◆ make_v_op_z() [2/2]

◆ geq_of_constant()

◆ leq_of_constant()

◆ var_in() [1/2]

◆ num_vars()

◆ num_quantified_vars() [1/2]

◆ num_quantified_vars() [2/2]

◆ type_of_conjunction()

◆ extract_ty()

◆ negate()

◆ de_morgan_law()

◆ negate_eq()

◆ negate_arithmetic_comparison()

◆ is_arithmetic_comparison()

◆ is_set_comparison()

◆ is_comparison()

◆ converse_comparison()

◆ move_constants_on_rhs()

◆ map_avar_to_lvar()

◆ eval()

◆ string_of_sig()

◆ is_prefix()

◆ is_division()

◆ is_modulo()

◆ is_associative()

◆ operator==() [3/8]

◆ var_in() [2/2]

◆ operator==() [4/8]

◆ join() [3/6]