Lattice Land Core Library
Loading...
Searching...
No Matches
Public Types | Public Member Functions | Static Public Member Functions | Static Public Attributes | Friends | List of all members
lala::FlatUniverse< PreUniverse, Mem > Class Template Reference

#include <flat_universe.hpp>

Public Types

using pre_universe = PreUniverse
 
using value_type = typename pre_universe::value_type
 
using memory_type = Mem
 
using this_type = FlatUniverse<pre_universe, memory_type>
 
template<class M >
using this_type2 = FlatUniverse<pre_universe, M>
 
using local_type = this_type2<battery::local_memory>
 

Public Member Functions

CUDA constexpr FlatUniverse ()
 
CUDA constexpr FlatUniverse (value_type k)
 
CUDA constexpr FlatUniverse (const this_type &other)
 
CUDA constexpr FlatUniverse (this_type &&other)
 
template<class M >
CUDA constexpr FlatUniverse (const this_type2< M > &other)
 
template<class M >
CUDA constexpr FlatUniverse (const PrimitiveUpset< pre_universe, M > &other)
 
template<class M >
CUDA constexpr FlatUniverse (const PrimitiveUpset< typename pre_universe::dual_type, M > &other)
 
template<class M >
CUDA constexpr this_type & operator= (const this_type2< M > &other)
 
CUDA constexpr this_type & operator= (const this_type &other)
 
CUDA constexpr value_type value () const
 
CUDA constexpr operator value_type () const
 
CUDA constexpr local::BInc is_top () const
 
CUDA constexpr local::BDec is_bot () const
 
CUDA constexpr this_type & tell_top ()
 
template<class M1 , class M2 >
CUDA constexpr this_type & tell (const this_type2< M1 > &other, BInc< M2 > &has_changed)
 
template<class M1 >
CUDA constexpr this_type & tell (const this_type2< M1 > &other)
 
CUDA constexpr this_type & dtell_bot ()
 
template<class M1 , class M2 >
CUDA constexpr this_type & dtell (const this_type2< M1 > &other, BInc< M2 > &has_changed)
 
template<class M1 >
CUDA constexpr this_type & dtell (const this_type2< M1 > &other)
 
template<class Env >
CUDA NI TFormula< typename Env::allocator_type > deinterpret (AVar avar, const Env &env) const
 
template<class F >
CUDA NI F deinterpret () const
 
CUDA constexpr bool extract (local_type &ua) const
 
CUDA NI void print () const
 

Static Public Member Functions

static CUDA constexpr local_type eq_k (value_type k)
 
static CUDA constexpr local_type bot ()
 
static CUDA constexpr local_type top ()
 
template<bool diagnose = false, class F , class Env , class M2 >
CUDA static NI bool interpret_tell (const F &f, const Env &env, this_type2< M2 > &tell, IDiagnostics &diagnostics)
 
template<bool diagnose = false, class F , class Env , class M2 >
CUDA static NI bool interpret_ask (const F &f, const Env &env, this_type2< M2 > &ask, IDiagnostics &diagnostics)
 
template<IKind kind, bool diagnose = false, class F , class Env , class M2 >
CUDA static NI bool interpret (const F &f, const Env &env, this_type2< M2 > &value, IDiagnostics &diagnostics)
 
static CUDA constexpr bool is_supported_fun (Sig sig)
 
template<Sig sig, class M1 >
static CUDA constexpr local_type fun (const this_type2< M1 > &u)
 
template<Sig sig, class M1 , class M2 >
static CUDA constexpr local_type fun (const this_type2< M1 > &l, const this_type2< M2 > &k)
 

Static Public Attributes

static constexpr const bool is_abstract_universe = true
 
static constexpr const bool sequential = Mem::sequential
 
static constexpr const bool is_totally_ordered = false
 
static constexpr const bool preserve_bot = true
 
static constexpr const bool preserve_top = true
 
static constexpr const bool preserve_join = true
 
static constexpr const bool preserve_meet = false
 
static constexpr const bool injective_concretization = pre_universe::injective_concretization
 
static constexpr const bool preserve_concrete_covers = true
 
static constexpr const bool complemented = false
 
static constexpr const char * name = "Flat"
 
static constexpr const bool is_arithmetic = pre_universe::is_arithmetic
 

Friends

template<class Pre2 , class Mem2 >
class FlatUniverse
 

Member Typedef Documentation

◆ pre_universe

template<class PreUniverse , class Mem >
using lala::FlatUniverse< PreUniverse, Mem >::pre_universe = PreUniverse

◆ value_type

template<class PreUniverse , class Mem >
using lala::FlatUniverse< PreUniverse, Mem >::value_type = typename pre_universe::value_type

◆ memory_type

template<class PreUniverse , class Mem >
using lala::FlatUniverse< PreUniverse, Mem >::memory_type = Mem

◆ this_type

template<class PreUniverse , class Mem >
using lala::FlatUniverse< PreUniverse, Mem >::this_type = FlatUniverse<pre_universe, memory_type>

◆ this_type2

template<class PreUniverse , class Mem >
template<class M >
using lala::FlatUniverse< PreUniverse, Mem >::this_type2 = FlatUniverse<pre_universe, M>

◆ local_type

template<class PreUniverse , class Mem >
using lala::FlatUniverse< PreUniverse, Mem >::local_type = this_type2<battery::local_memory>

Constructor & Destructor Documentation

◆ FlatUniverse() [1/7]

template<class PreUniverse , class Mem >
CUDA constexpr lala::FlatUniverse< PreUniverse, Mem >::FlatUniverse ( )
inlineconstexpr

Initialize to the bottom of the flat lattice.

◆ FlatUniverse() [2/7]

template<class PreUniverse , class Mem >
CUDA constexpr lala::FlatUniverse< PreUniverse, Mem >::FlatUniverse ( value_type k)
inlineconstexpr

Similar to \([\![x = k]\!]\) for any name x where \( = \) is the equality.

◆ FlatUniverse() [3/7]

template<class PreUniverse , class Mem >
CUDA constexpr lala::FlatUniverse< PreUniverse, Mem >::FlatUniverse ( const this_type & other)
inlineconstexpr

◆ FlatUniverse() [4/7]

template<class PreUniverse , class Mem >
CUDA constexpr lala::FlatUniverse< PreUniverse, Mem >::FlatUniverse ( this_type && other)
inlineconstexpr

◆ FlatUniverse() [5/7]

template<class PreUniverse , class Mem >
template<class M >
CUDA constexpr lala::FlatUniverse< PreUniverse, Mem >::FlatUniverse ( const this_type2< M > & other)
inlineconstexpr

◆ FlatUniverse() [6/7]

template<class PreUniverse , class Mem >
template<class M >
CUDA constexpr lala::FlatUniverse< PreUniverse, Mem >::FlatUniverse ( const PrimitiveUpset< pre_universe, M > & other)
inlineconstexpr

◆ FlatUniverse() [7/7]

template<class PreUniverse , class Mem >
template<class M >
CUDA constexpr lala::FlatUniverse< PreUniverse, Mem >::FlatUniverse ( const PrimitiveUpset< typename pre_universe::dual_type, M > & other)
inlineconstexpr

Member Function Documentation

◆ eq_k()

template<class PreUniverse , class Mem >
static CUDA constexpr local_type lala::FlatUniverse< PreUniverse, Mem >::eq_k ( value_type k)
inlinestaticconstexpr

A pre-interpreted formula x = value ready to use. This is mainly for optimization purpose to avoid calling interpret each time we need it.

◆ bot()

template<class PreUniverse , class Mem >
static CUDA constexpr local_type lala::FlatUniverse< PreUniverse, Mem >::bot ( )
inlinestaticconstexpr

Similar to \([\![\mathit{true}]\!]\).

◆ top()

template<class PreUniverse , class Mem >
static CUDA constexpr local_type lala::FlatUniverse< PreUniverse, Mem >::top ( )
inlinestaticconstexpr

Similar to \([\![\mathit{false}]\!]\).

◆ operator=() [1/2]

template<class PreUniverse , class Mem >
template<class M >
CUDA constexpr this_type & lala::FlatUniverse< PreUniverse, Mem >::operator= ( const this_type2< M > & other)
inlineconstexpr

The assignment operator can only be used in a sequential context. It is monotone but not extensive.

◆ operator=() [2/2]

template<class PreUniverse , class Mem >
CUDA constexpr this_type & lala::FlatUniverse< PreUniverse, Mem >::operator= ( const this_type & other)
inlineconstexpr

◆ value()

template<class PreUniverse , class Mem >
CUDA constexpr value_type lala::FlatUniverse< PreUniverse, Mem >::value ( ) const
inlineconstexpr

◆ operator value_type()

template<class PreUniverse , class Mem >
CUDA constexpr lala::FlatUniverse< PreUniverse, Mem >::operator value_type ( ) const
inlineconstexpr

◆ is_top()

template<class PreUniverse , class Mem >
CUDA constexpr local::BInc lala::FlatUniverse< PreUniverse, Mem >::is_top ( ) const
inlineconstexpr

true whenever \( a = \top \), false otherwise.

◆ is_bot()

template<class PreUniverse , class Mem >
CUDA constexpr local::BDec lala::FlatUniverse< PreUniverse, Mem >::is_bot ( ) const
inlineconstexpr

true whenever \( a = \bot \), false otherwise.

◆ tell_top()

template<class PreUniverse , class Mem >
CUDA constexpr this_type & lala::FlatUniverse< PreUniverse, Mem >::tell_top ( )
inlineconstexpr

◆ tell() [1/2]

template<class PreUniverse , class Mem >
template<class M1 , class M2 >
CUDA constexpr this_type & lala::FlatUniverse< PreUniverse, Mem >::tell ( const this_type2< M1 > & other,
BInc< M2 > & has_changed )
inlineconstexpr

◆ tell() [2/2]

template<class PreUniverse , class Mem >
template<class M1 >
CUDA constexpr this_type & lala::FlatUniverse< PreUniverse, Mem >::tell ( const this_type2< M1 > & other)
inlineconstexpr

◆ dtell_bot()

template<class PreUniverse , class Mem >
CUDA constexpr this_type & lala::FlatUniverse< PreUniverse, Mem >::dtell_bot ( )
inlineconstexpr

◆ dtell() [1/2]

template<class PreUniverse , class Mem >
template<class M1 , class M2 >
CUDA constexpr this_type & lala::FlatUniverse< PreUniverse, Mem >::dtell ( const this_type2< M1 > & other,
BInc< M2 > & has_changed )
inlineconstexpr

◆ dtell() [2/2]

template<class PreUniverse , class Mem >
template<class M1 >
CUDA constexpr this_type & lala::FlatUniverse< PreUniverse, Mem >::dtell ( const this_type2< M1 > & other)
inlineconstexpr

◆ deinterpret() [1/2]

template<class PreUniverse , class Mem >
template<class Env >
CUDA NI TFormula< typename Env::allocator_type > lala::FlatUniverse< PreUniverse, Mem >::deinterpret ( AVar avar,
const Env & env ) const
inline
Returns
\( x = k \) where x is a variable's name and k the current value. true is returned whenever \( a = \bot \), and false is returned whenever \( a = \top \). We always return an exact approximation, hence for any formula \( \llbracket \varphi \rrbracket = a \), we must have \( a = \llbracket \rrbracket a \llbracket \rrbracket \) where \( \rrbracket a \llbracket \) is the deinterpretation function.

◆ deinterpret() [2/2]

template<class PreUniverse , class Mem >
template<class F >
CUDA NI F lala::FlatUniverse< PreUniverse, Mem >::deinterpret ( ) const
inline

Deinterpret the current value to a logical constant.

◆ extract()

template<class PreUniverse , class Mem >
CUDA constexpr bool lala::FlatUniverse< PreUniverse, Mem >::extract ( local_type & ua) const
inlineconstexpr

Under-approximates the current element \( a \) w.r.t. \( \rrbracket a \llbracket \) into ua. For this abstract universe, it always returns true since the current element \( a \) is an exact representation of \( \rrbracket a \llbracket \).

◆ print()

template<class PreUniverse , class Mem >
CUDA NI void lala::FlatUniverse< PreUniverse, Mem >::print ( ) const
inline

Print the current element.

◆ interpret_tell()

template<class PreUniverse , class Mem >
template<bool diagnose = false, class F , class Env , class M2 >
CUDA static NI bool lala::FlatUniverse< PreUniverse, Mem >::interpret_tell ( const F & f,
const Env & env,
this_type2< M2 > & tell,
IDiagnostics & diagnostics )
inlinestatic

Expects a predicate of the form x = k or k = x, where x is any variable's name, and k a constant. Existential formula \( \exists{x:T} \) can also be interpreted (only to bottom).

◆ interpret_ask()

template<class PreUniverse , class Mem >
template<bool diagnose = false, class F , class Env , class M2 >
CUDA static NI bool lala::FlatUniverse< PreUniverse, Mem >::interpret_ask ( const F & f,
const Env & env,
this_type2< M2 > & ask,
IDiagnostics & diagnostics )
inlinestatic

Same as interpret_tell without the support for existential quantifier.

◆ interpret()

template<class PreUniverse , class Mem >
template<IKind kind, bool diagnose = false, class F , class Env , class M2 >
CUDA static NI bool lala::FlatUniverse< PreUniverse, Mem >::interpret ( const F & f,
const Env & env,
this_type2< M2 > & value,
IDiagnostics & diagnostics )
inlinestatic

◆ is_supported_fun()

template<class PreUniverse , class Mem >
static CUDA constexpr bool lala::FlatUniverse< PreUniverse, Mem >::is_supported_fun ( Sig sig)
inlinestaticconstexpr

◆ fun() [1/2]

template<class PreUniverse , class Mem >
template<Sig sig, class M1 >
static CUDA constexpr local_type lala::FlatUniverse< PreUniverse, Mem >::fun ( const this_type2< M1 > & u)
inlinestaticconstexpr

Unary function over value_type.

◆ fun() [2/2]

template<class PreUniverse , class Mem >
template<Sig sig, class M1 , class M2 >
static CUDA constexpr local_type lala::FlatUniverse< PreUniverse, Mem >::fun ( const this_type2< M1 > & l,
const this_type2< M2 > & k )
inlinestaticconstexpr

Binary functions over value_type.

Friends And Related Symbol Documentation

◆ FlatUniverse

template<class PreUniverse , class Mem >
template<class Pre2 , class Mem2 >
friend class FlatUniverse
friend

Member Data Documentation

◆ is_abstract_universe

template<class PreUniverse , class Mem >
constexpr const bool lala::FlatUniverse< PreUniverse, Mem >::is_abstract_universe = true
staticconstexpr

◆ sequential

template<class PreUniverse , class Mem >
constexpr const bool lala::FlatUniverse< PreUniverse, Mem >::sequential = Mem::sequential
staticconstexpr

◆ is_totally_ordered

template<class PreUniverse , class Mem >
constexpr const bool lala::FlatUniverse< PreUniverse, Mem >::is_totally_ordered = false
staticconstexpr

◆ preserve_bot

template<class PreUniverse , class Mem >
constexpr const bool lala::FlatUniverse< PreUniverse, Mem >::preserve_bot = true
staticconstexpr

◆ preserve_top

template<class PreUniverse , class Mem >
constexpr const bool lala::FlatUniverse< PreUniverse, Mem >::preserve_top = true
staticconstexpr

◆ preserve_join

template<class PreUniverse , class Mem >
constexpr const bool lala::FlatUniverse< PreUniverse, Mem >::preserve_join = true
staticconstexpr

◆ preserve_meet

template<class PreUniverse , class Mem >
constexpr const bool lala::FlatUniverse< PreUniverse, Mem >::preserve_meet = false
staticconstexpr

◆ injective_concretization

template<class PreUniverse , class Mem >
constexpr const bool lala::FlatUniverse< PreUniverse, Mem >::injective_concretization = pre_universe::injective_concretization
staticconstexpr

◆ preserve_concrete_covers

template<class PreUniverse , class Mem >
constexpr const bool lala::FlatUniverse< PreUniverse, Mem >::preserve_concrete_covers = true
staticconstexpr

◆ complemented

template<class PreUniverse , class Mem >
constexpr const bool lala::FlatUniverse< PreUniverse, Mem >::complemented = false
staticconstexpr

◆ name

template<class PreUniverse , class Mem >
constexpr const char* lala::FlatUniverse< PreUniverse, Mem >::name = "Flat"
staticconstexpr

◆ is_arithmetic

template<class PreUniverse , class Mem >
constexpr const bool lala::FlatUniverse< PreUniverse, Mem >::is_arithmetic = pre_universe::is_arithmetic
staticconstexpr
The documentation for this class was generated from the following file: