3#ifndef LALA_CORE_PRE_ZDEC_HPP
4#define LALA_CORE_PRE_ZDEC_HPP
24 static_assert(std::is_integral_v<value_type>,
"PreZDec only works over integer types.");
35 constexpr static const char *
name =
"ZDec";
40 template <
bool diagnose,
class F>
42 return dual_type::template interpret_ask<diagnose>(f, tell, diagnostics);
45 template <
bool diagnose,
class F>
47 return dual_type::template interpret_tell<diagnose>(f, ask, diagnostics);
50 template <
bool diagnose,
class F>
52 bool res = dual_type::template interpret_type<diagnose>(f, k, diagnostics);
62 return dual_type::template deinterpret<F>(v);
78 return dual_type::template fun<sig>(x);
Definition diagnostics.hpp:19
Definition abstract_deps.hpp:14
@ GEQ
Unary arithmetic function symbols.
Definition ast.hpp:113
@ GT
Arithmetic comparison predicates. When applied to set, it corresponds to the lexicographic ordering o...
Definition ast.hpp:113
@ ABS
Unary arithmetic function symbols.
Definition ast.hpp:96
Definition pre_zdec.hpp:18
static CUDA constexpr Sig sig_strict_order()
Definition pre_zdec.hpp:66
static constexpr const bool preserve_join
Definition pre_zdec.hpp:29
static CUDA F deinterpret(const value_type &v)
Definition pre_zdec.hpp:61
static CUDA constexpr value_type next(value_type x)
Definition pre_zdec.hpp:73
static constexpr const char * name
Definition pre_zdec.hpp:35
static constexpr const bool injective_concretization
Definition pre_zdec.hpp:31
static constexpr const bool preserve_bot
Definition pre_zdec.hpp:27
static CUDA bool interpret_type(const F &f, value_type &k, IDiagnostics &diagnostics)
Definition pre_zdec.hpp:51
static constexpr const bool is_totally_ordered
Definition pre_zdec.hpp:26
static CUDA constexpr value_type top()
Definition pre_zdec.hpp:68
static constexpr const bool is_arithmetic
Definition pre_zdec.hpp:36
static CUDA constexpr bool is_supported_fun(Sig sig)
Definition pre_zdec.hpp:75
static constexpr const bool preserve_concrete_covers
Definition pre_zdec.hpp:32
static CUDA constexpr value_type prev(value_type x)
Definition pre_zdec.hpp:74
PreZInc< VT > dual_type
Definition pre_zdec.hpp:20
static CUDA constexpr bool strict_order(value_type x, value_type y)
Definition pre_zdec.hpp:72
static CUDA constexpr Sig sig_order()
Definition pre_zdec.hpp:65
CUDA static constexpr value_type zero()
Definition pre_zdec.hpp:37
static CUDA constexpr value_type meet(value_type x, value_type y)
Definition pre_zdec.hpp:70
static CUDA constexpr value_type join(value_type x, value_type y)
Definition pre_zdec.hpp:69
static CUDA constexpr value_type bot()
Definition pre_zdec.hpp:67
VT value_type
Definition pre_zdec.hpp:21
static CUDA constexpr value_type fun(value_type x)
Definition pre_zdec.hpp:76
static CUDA bool interpret_ask(const F &f, value_type &ask, IDiagnostics &diagnostics)
Definition pre_zdec.hpp:46
CUDA static constexpr value_type one()
Definition pre_zdec.hpp:38
static CUDA constexpr value_type fun(value_type x, value_type y)
Definition pre_zdec.hpp:80
static constexpr const bool preserve_top
Definition pre_zdec.hpp:28
static constexpr const bool increasing
Definition pre_zdec.hpp:34
static constexpr const bool complemented
Definition pre_zdec.hpp:33
static CUDA bool interpret_tell(const F &f, value_type &tell, IDiagnostics &diagnostics)
Definition pre_zdec.hpp:41
static CUDA constexpr bool order(value_type x, value_type y)
Definition pre_zdec.hpp:71
static constexpr const bool preserve_meet
Definition pre_zdec.hpp:30
Definition pre_zinc.hpp:17
static CUDA constexpr bool order(value_type x, value_type y)
Definition pre_zinc.hpp:162
CUDA static NI constexpr bool is_supported_fun(Sig sig)
Definition pre_zinc.hpp:186
static CUDA constexpr value_type top()
Definition pre_zinc.hpp:151
static CUDA constexpr value_type bot()
Definition pre_zinc.hpp:146
static CUDA constexpr value_type prev(value_type x)
Definition pre_zinc.hpp:181
static CUDA constexpr value_type next(value_type x)
Definition pre_zinc.hpp:172
static CUDA constexpr value_type join(value_type x, value_type y)
Definition pre_zinc.hpp:156
static CUDA constexpr value_type meet(value_type x, value_type y)
Definition pre_zinc.hpp:159
static CUDA constexpr bool strict_order(value_type x, value_type y)
Definition pre_zinc.hpp:165