3#ifndef LALA_CORE_ARITH_BOUND_HPP
4#define LALA_CORE_ARITH_BOUND_HPP
10#include "../logic/logic.hpp"
16#include "battery/memory.hpp"
43template<
class PreUniverse,
class Mem>
46template<
class PreUniverse,
class Mem>
50template<
class VT,
class Mem>
54template<
class VT,
class Mem>
58template<
class VT,
class Mem>
62template<
class VT,
class Mem>
76 struct is_arith_bound {
77 static constexpr bool value =
false;
80 template<
class PreUniverse,
class Mem>
81 struct is_arith_bound<ArithBound<PreUniverse, Mem>> {
82 static constexpr bool value =
true;
86 inline constexpr bool is_arith_bound_v = is_arith_bound<T>::value;
90template <
class A,
class R = A>
97template <
class A,
class R = A>
109template <
class LDual,
class L>
111 if(x.is_bot())
return LDual::bot();
112 if(x.is_top())
return LDual::top();
113 return LDual(x.value());
116template<
class PreUniverse,
class Mem>
119 using U = PreUniverse;
147 constexpr static const char*
name = pre_universe::name;
151 static_assert(
is_totally_ordered,
"The underlying pre-universe must be totally ordered.");
152 static_assert(
is_arithmetic,
"The underlying pre-universe must be arithmetic (e.g. integers, floating-point numbers).");
162 "The pre-interpreted formula x >= k is only available over abstract universe modelling lower bounds.");
172 "The pre-interpreted formula x <= k is only available over abstract universe modelling upper bounds.");
200 memory_type::store(val, other.
value());
217 return value() == U::top();
224 return value() == U::bot();
228 memory_type::store(val, U::top());
235 if(U::strict_order(r1, r2)) {
236 memory_type::store(val, r2);
243 memory_type::store(val, U::bot());
250 if(U::strict_order(r2, r1)) {
251 memory_type::store(val, r2);
261 template<
class Env,
class Allocator =
typename Env::allocator_type>
265 return F::make_true();
268 return F::make_false();
270 return F::make_binary(
280 return pre_universe::template deinterpret<F>(
value());
305 template<
bool diagnose = false,
class F,
class M2>
306 CUDA NI
static bool interpret_tell_x_op_k(
const F& f, this_type2<M2>& tell,
IDiagnostics& diagnostics) {
308 bool res = pre_universe::template interpret_tell<diagnose>(f.seq(1),
value, diagnostics);
310 if(f.sig() ==
EQ || f.sig() == U::sig_order()) {
313 else if(f.sig() == U::sig_strict_order()) {
329 template<
bool diagnose = false,
class F,
class M2>
330 CUDA NI
static bool interpret_ask_x_op_k(
const F& f, this_type2<M2>& tell, IDiagnostics& diagnostics) {
332 bool res = pre_universe::template interpret_ask<diagnose>(f.seq(1),
value, diagnostics);
334 if(f.sig() == U::sig_order()) {
337 else if(f.sig() ==
NEQ || f.sig() == U::sig_strict_order()) {
349 template<
bool diagnose = false,
class F,
class M2>
350 CUDA NI
static bool interpret_tell_set(
const F& f, this_type2<M2>& tell, IDiagnostics& diagnostics) {
351 if(!f.seq(1).is(F::S)) {
354 const auto& set = f.seq(1).s();
355 if(set.size() == 0) {
362 for(
int i = 0; i < set.size(); ++i) {
363 auto bound = battery::get<bound_index>(set[i]);
365 bool res = pre_universe::template interpret_tell<diagnose>(bound, set_element, diagnostics);
369 join_s = pre_universe::join(join_s, set_element);
380 template<
bool diagnose = false,
class F,
class Env,
class M2>
383 typename U::value_type val;
384 bool res = pre_universe::template interpret_type<diagnose>(f, val, diagnostics);
391 if(f.is_binary() && f.seq(0).is_variable() && f.seq(1).is_constant()) {
394 return interpret_tell_set<diagnose>(f, tell, diagnostics);
397 return interpret_tell_x_op_k<diagnose>(f, tell, diagnostics);
401 RETURN_INTERPRETATION_ERROR(
"Only binary formulas of the form `x <sig> k` where if x is a variable and k is a constant are supported.");
409 template<
bool diagnose = false,
class F,
class Env,
class M2>
411 if(f.is_binary() && f.seq(0).is_variable() && f.seq(1).is_constant()) {
412 return interpret_ask_x_op_k<diagnose>(f, ask, diagnostics);
415 RETURN_INTERPRETATION_ERROR(
"Only binary formulas of the form `x <sig> k` where if x is a variable and k is a constant are supported.");
419 template<IKind kind,
bool diagnose = false,
class F,
class Env,
class M2>
422 return interpret_tell<diagnose>(f, env,
value, diagnostics);
425 return interpret_ask<diagnose>(f, env,
value, diagnostics);
475 if(fun ==
MIN || fun ==
MAX || fun ==
ADD) {
487 template<
class Pre2,
class Mem2>
493template<
class Pre,
class M1,
class M2>
498template<
class Pre,
class M1,
class M2>
503template<
class Pre,
class M1,
class M2>
504CUDA
constexpr bool operator<=(
const ArithBound<Pre, M1>& a,
const ArithBound<Pre, M2>& b) {
505 return Pre::order(a.value(), b.value());
508template<
class Pre,
class M1,
class M2>
510 return Pre::strict_order(a.
value(), b.
value());
513template<
class Pre,
class M1,
class M2>
514CUDA
constexpr bool operator>=(
const ArithBound<Pre, M1>& a,
const ArithBound<Pre, M2>& b) {
515 return Pre::order(b.value(), a.value());
518template<
class Pre,
class M1,
class M2>
520 return Pre::strict_order(b.
value(), a.
value());
523template<
class Pre,
class M1,
class M2>
528template<
class Pre,
class M1,
class M2>
529CUDA
constexpr bool operator!=(
const ArithBound<Pre, M1>& a,
const ArithBound<Pre, M2>& b) {
530 return a.value() != b.value();
533template<
class Pre,
class M>
Definition arith_bound.hpp:118
CUDA NI F deinterpret() const
Definition arith_bound.hpp:279
static CUDA constexpr local_type next(const this_type2< Mem > &a)
Definition arith_bound.hpp:430
static CUDA constexpr bool is_order_preserving_fun(Sig fun)
Definition arith_bound.hpp:469
CUDA constexpr bool join(const this_type2< M1 > &other)
Definition arith_bound.hpp:232
CUDA constexpr local::B is_top() const
Definition arith_bound.hpp:216
static constexpr const bool is_totally_ordered
Definition arith_bound.hpp:138
this_type2< battery::local_memory > local_type
Definition arith_bound.hpp:130
static CUDA constexpr bool is_trivial_fun(Sig fun)
Definition arith_bound.hpp:464
CUDA constexpr bool meet(const this_type2< M1 > &other)
Definition arith_bound.hpp:247
constexpr ArithBound(const this_type &other)=default
static constexpr const bool preserve_top
Definition arith_bound.hpp:140
CUDA constexpr ArithBound(const this_type2< M > &other)
Definition arith_bound.hpp:194
CUDA constexpr bool extract(local_type &ua) const
Definition arith_bound.hpp:285
Mem memory_type
Definition arith_bound.hpp:123
static CUDA constexpr this_type leq_k(value_type k)
Definition arith_bound.hpp:166
static constexpr const bool is_abstract_universe
Definition arith_bound.hpp:136
static constexpr const char * name
Definition arith_bound.hpp:147
memory_type::template atomic_type< value_type > atomic_type
Definition arith_bound.hpp:176
CUDA constexpr value_type value() const
Definition arith_bound.hpp:206
static constexpr const bool is_lower_bound
Definition arith_bound.hpp:145
CUDA constexpr ArithBound(value_type x)
Definition arith_bound.hpp:189
static constexpr const bool preserve_bot
Definition arith_bound.hpp:139
CUDA static NI bool interpret_tell(const F &f, const Env &, this_type2< M2 > &tell, IDiagnostics &diagnostics)
Definition arith_bound.hpp:381
constexpr this_type & operator=(const this_type &other)=default
static constexpr const bool preserve_concrete_covers
Definition arith_bound.hpp:144
CUDA NI TFormula< Allocator > deinterpret(AVar avar, const Env &env, const Allocator &allocator=Allocator()) const
Definition arith_bound.hpp:262
constexpr ArithBound(this_type &&other)=default
static CUDA constexpr local_type bot()
Definition arith_bound.hpp:182
static constexpr const bool sequential
Definition arith_bound.hpp:137
static constexpr const bool injective_concretization
Definition arith_bound.hpp:143
ArithBound< pre_universe, memory_type > this_type
Definition arith_bound.hpp:124
CUDA constexpr void project(Sig fun, const local_flat_type &a)
Definition arith_bound.hpp:443
CUDA constexpr atomic_type & atomic()
Definition arith_bound.hpp:208
CUDA constexpr ArithBound()
Definition arith_bound.hpp:187
static CUDA constexpr local_type prev(const this_type2< Mem > &a)
Definition arith_bound.hpp:434
PreUniverse pre_universe
Definition arith_bound.hpp:121
CUDA constexpr void join_top()
Definition arith_bound.hpp:227
CUDA static NI bool interpret_ask(const F &f, const Env &, this_type2< M2 > &ask, IDiagnostics &diagnostics)
Definition arith_bound.hpp:410
CUDA NI void print() const
Definition arith_bound.hpp:291
static constexpr const bool preserve_join
Definition arith_bound.hpp:141
CUDA static NI bool interpret(const F &f, const Env &env, this_type2< M2 > &value, IDiagnostics &diagnostics)
Definition arith_bound.hpp:420
static CUDA constexpr this_type geq_k(value_type k)
Definition arith_bound.hpp:156
static constexpr const bool preserve_meet
Definition arith_bound.hpp:142
CUDA constexpr void project(Sig fun, const local_type &a)
Definition arith_bound.hpp:480
CUDA constexpr void project(Sig fun, const local_type &a, const local_type &b)
Definition arith_bound.hpp:473
CUDA constexpr void project(Sig fun, const local_flat_type &a, const local_flat_type &b)
Definition arith_bound.hpp:456
CUDA constexpr void meet_bot()
Definition arith_bound.hpp:242
typename pre_universe::value_type value_type
Definition arith_bound.hpp:122
CUDA constexpr local::B is_bot() const
Definition arith_bound.hpp:223
static CUDA constexpr local_type top()
Definition arith_bound.hpp:185
CUDA constexpr this_type & operator=(const this_type2< M > &other)
Definition arith_bound.hpp:199
static constexpr const bool is_arithmetic
Definition arith_bound.hpp:149
static constexpr const bool is_upper_bound
Definition arith_bound.hpp:146
Definition flat_universe.hpp:30
CUDA constexpr local::B is_top() const
Definition flat_universe.hpp:115
CUDA constexpr value_type value() const
Definition flat_universe.hpp:108
CUDA constexpr local::B is_bot() const
Definition flat_universe.hpp:122
Definition diagnostics.hpp:19
#define RETURN_INTERPRETATION_ERROR(MSG)
Definition diagnostics.hpp:155
CUDA NI void print(const lala::Sig &sig)
Definition ast.hpp:264
Definition abstract_deps.hpp:14
std::ostream & operator<<(std::ostream &s, const CartesianProduct< A, As... > &cp)
Definition cartesian_product.hpp:531
CUDA constexpr LDual dual_bound(const L &x)
Definition arith_bound.hpp:110
CUDA constexpr auto fjoin(const CartesianProduct< As... > &a, const CartesianProduct< Bs... > &b)
Definition cartesian_product.hpp:464
CUDA constexpr bool operator==(const CartesianProduct< As... > &a, const CartesianProduct< Bs... > &b)
Definition cartesian_product.hpp:504
R project_fun(Sig fun, const A &a, const A &b)
Definition arith_bound.hpp:91
@ NEQ
Equality relations.
Definition ast.hpp:112
@ EQ
Unary arithmetic function symbols.
Definition ast.hpp:112
@ ADD
Unary arithmetic function symbols.
Definition ast.hpp:97
@ IN
Set membership predicate.
Definition ast.hpp:108
@ MIN
Unary arithmetic function symbols.
Definition ast.hpp:97
@ MAX
Binary arithmetic function symbols.
Definition ast.hpp:97
@ ABS
Unary arithmetic function symbols.
Definition ast.hpp:96
CUDA constexpr bool operator<(const CartesianProduct< As... > &a, const CartesianProduct< Bs... > &b)
Definition cartesian_product.hpp:485
CUDA NI const char * string_of_sig(Sig sig)
Definition ast.hpp:121
CUDA constexpr auto fmeet(const CartesianProduct< As... > &a, const CartesianProduct< Bs... > &b)
Definition cartesian_product.hpp:471
CUDA constexpr bool operator>(const CartesianProduct< As... > &a, const CartesianProduct< Bs... > &b)
Definition cartesian_product.hpp:498
#define UNTYPED
Definition sort.hpp:21