Lattice Land Core Library
|
#include <pre_zdec.hpp>
Public Types | |
using | this_type = PreZDec<VT> |
using | dual_type = PreZInc<VT> |
using | value_type = VT |
using | increasing_type = dual_type |
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 > | |
static CUDA 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) |
static CUDA constexpr bool | is_supported_fun (Sig sig) |
template<Sig sig> | |
static CUDA constexpr value_type | fun (value_type x) |
template<Sig sig> | |
static CUDA 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 = 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 bool | complemented = false |
static constexpr const bool | increasing = false |
static constexpr const char * | name = "ZDec" |
static constexpr const bool | is_arithmetic = true |
PreZDec
is a pre-abstract universe \( \langle \{\infty, \ldots, 2, 1, 0, -1, -2, \ldots, -\infty\}, \leq \rangle \) totally ordered by the reversed natural arithmetic comparison operator. It is used to represent constraints of the form \( x \leq k \) where \( k \) is an integer.
using lala::PreZDec< VT >::this_type = PreZDec<VT> |
using lala::PreZDec< VT >::dual_type = PreZInc<VT> |
using lala::PreZDec< VT >::value_type = VT |
using lala::PreZDec< VT >::increasing_type = dual_type |
|
inlinestaticconstexpr |
|
inlinestaticconstexpr |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestatic |
|
inlinestaticconstexpr |
|
inlinestaticconstexpr |
|
inlinestaticconstexpr |
|
inlinestaticconstexpr |
|
inlinestaticconstexpr |
|
inlinestaticconstexpr |
|
inlinestaticconstexpr |
|
inlinestaticconstexpr |
|
inlinestaticconstexpr |
|
inlinestaticconstexpr |
|
inlinestaticconstexpr |
|
inlinestaticconstexpr |
|
inlinestaticconstexpr |
|
staticconstexpr |
|
staticconstexpr |
|
staticconstexpr |
|
staticconstexpr |
|
staticconstexpr |
|
staticconstexpr |
|
staticconstexpr |
|
staticconstexpr |
|
staticconstexpr |
|
staticconstexpr |
|
staticconstexpr |