Lattice Land Core Library
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

constexpr CUDA FlatUniverse ()
 
constexpr CUDA FlatUniverse (value_type k)
 
constexpr CUDA FlatUniverse (const this_type &other)
 
constexpr CUDA FlatUniverse (this_type &&other)
 
template<class M >
constexpr CUDA FlatUniverse (const this_type2< M > &other)
 
template<class M >
constexpr CUDA FlatUniverse (const ArithBound< pre_universe, M > &other)
 
template<class M >
constexpr CUDA FlatUniverse (const ArithBound< typename pre_universe::dual_type, M > &other)
 
template<class M >
constexpr CUDA this_type & operator= (const this_type2< M > &other)
 
constexpr CUDA this_type & operator= (const this_type &other)
 
constexpr CUDA value_type value () const
 
constexpr CUDA operator value_type () const
 
constexpr CUDA local::B is_top () const
 
constexpr CUDA local::B is_bot () const
 
constexpr CUDA void join_top ()
 
template<class M1 >
constexpr CUDA bool join (const this_type2< M1 > &other)
 
constexpr CUDA void meet_bot ()
 
template<class M1 >
constexpr CUDA bool meet (const this_type2< M1 > &other)
 
template<class Env , class Allocator = typename Env::allocator_type>
CUDA NI TFormula< Allocator > deinterpret (AVar avar, const Env &env, const Allocator &allocator=Allocator()) const
 
template<class F >
CUDA NI F deinterpret () const
 
constexpr CUDA bool extract (local_type &ua) const
 
CUDA NI void print () const
 
constexpr CUDA void project (Sig fun, const local_type &a)
 
constexpr CUDA void project (Sig fun, const local_type &a, const local_type &b)
 

Static Public Member Functions

static constexpr CUDA local_type eq_k (value_type k)
 
static constexpr CUDA local_type bot ()
 
static constexpr CUDA 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 Public Attributes

constexpr static const bool is_abstract_universe = true
 
constexpr static const bool sequential = Mem::sequential
 
constexpr static const bool is_totally_ordered = false
 
constexpr static const bool preserve_bot = true
 
constexpr static const bool preserve_top = true
 
constexpr static const bool preserve_join = true
 
constexpr static const bool preserve_meet = false
 
constexpr static const bool injective_concretization = pre_universe::injective_concretization
 
constexpr static const bool preserve_concrete_covers = true
 
constexpr static const char * name = "Flat"
 
constexpr static 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 >
constexpr CUDA lala::FlatUniverse< PreUniverse, Mem >::FlatUniverse ( )
inlineconstexpr

Initialize to the top of the flat lattice.

◆ FlatUniverse() [2/7]

template<class PreUniverse , class Mem >
constexpr CUDA 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 >
constexpr CUDA lala::FlatUniverse< PreUniverse, Mem >::FlatUniverse ( const this_type &  other)
inlineconstexpr

◆ FlatUniverse() [4/7]

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

◆ FlatUniverse() [5/7]

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

◆ FlatUniverse() [6/7]

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

◆ FlatUniverse() [7/7]

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

Member Function Documentation

◆ eq_k()

template<class PreUniverse , class Mem >
static constexpr CUDA 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 constexpr CUDA local_type lala::FlatUniverse< PreUniverse, Mem >::bot ( )
inlinestaticconstexpr

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

◆ top()

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

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

◆ operator=() [1/2]

template<class PreUniverse , class Mem >
template<class M >
constexpr CUDA 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 >
constexpr CUDA this_type& lala::FlatUniverse< PreUniverse, Mem >::operator= ( const this_type &  other)
inlineconstexpr

◆ value()

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

◆ operator value_type()

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

◆ is_top()

template<class PreUniverse , class Mem >
constexpr CUDA local::B lala::FlatUniverse< PreUniverse, Mem >::is_top ( ) const
inlineconstexpr
Returns
true whenever \( a = \top \), false otherwise. @parallel @order-preserving @increasing

◆ is_bot()

template<class PreUniverse , class Mem >
constexpr CUDA local::B lala::FlatUniverse< PreUniverse, Mem >::is_bot ( ) const
inlineconstexpr
Returns
true whenever \( a = \bot \), false otherwise. @parallel @order-preserving @decreasing

◆ join_top()

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

◆ join()

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

◆ meet_bot()

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

◆ meet()

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

◆ deinterpret() [1/2]

template<class PreUniverse , class Mem >
template<class Env , class Allocator = typename Env::allocator_type>
CUDA NI TFormula<Allocator> lala::FlatUniverse< PreUniverse, Mem >::deinterpret ( AVar  avar,
const Env &  env,
const Allocator &  allocator = Allocator() 
) const
inline
Returns
\( x = k \) where x is a variable's name and k the current value. true is returned whenever \( a = \top \), and false is returned whenever \( a = \bot \). 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 >
constexpr CUDA 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 top).

◆ 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

◆ project() [1/2]

template<class PreUniverse , class Mem >
constexpr CUDA void lala::FlatUniverse< PreUniverse, Mem >::project ( Sig  fun,
const local_type &  a 
)
inlineconstexpr

In-place projection of the result of the unary function fun(a).

◆ project() [2/2]

template<class PreUniverse , class Mem >
constexpr CUDA void lala::FlatUniverse< PreUniverse, Mem >::project ( Sig  fun,
const local_type &  a,
const local_type &  b 
)
inlineconstexpr

In-place projection of the result of the binary function fun(a, b).

Friends And Related Function 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 static const bool lala::FlatUniverse< PreUniverse, Mem >::is_abstract_universe = true
staticconstexpr

◆ sequential

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

◆ is_totally_ordered

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

◆ preserve_bot

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

◆ preserve_top

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

◆ preserve_join

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

◆ preserve_meet

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

◆ injective_concretization

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

◆ preserve_concrete_covers

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

◆ name

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

◆ is_arithmetic

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