3#ifndef LALA_CORE_INTERVAL_HPP
4#define LALA_CORE_INTERVAL_HPP
20 using UB =
typename LB::dual_type;
23 using value_type = battery::tuple<typename LB::value_type, typename UB::value_type>;
32 constexpr static const bool preserve_top = LB::preserve_top && UB::preserve_top;
39 constexpr static const bool is_arithmetic = LB::is_arithmetic && UB::is_arithmetic;
40 constexpr static const char*
name =
"Interval";
43 using LB2 =
typename LB::local_type;
44 using UB2 =
typename UB::local_type;
58 CUDA
constexpr Interval(
const typename U::value_type& x): l(x), u(x) {}
88 return l.is_bot() || u.is_bot() || (!
is_top() && UB2(
lb().
value()) >
ub());
91 CUDA
constexpr value_type value()
const {
return battery::make_tuple(l.value(), u.value()); }
94 template<
class A,
class B>
97 typename A::template flat_type<battery::local_memory>(a.
lb()),
98 typename B::template flat_type<battery::local_memory>(b.
lb()));
100 typename A::template flat_type<battery::local_memory>(a.
ub()),
101 typename B::template flat_type<battery::local_memory>(b.
ub()));
105 CUDA
constexpr void flat_fun(
Sig fun,
const Interval<A>& a) {
106 lb().project(fun,
typename A::template flat_type<battery::local_memory>(a.lb()));
107 ub().project(fun,
typename A::template flat_type<battery::local_memory>(a.ub()));
114 template<
bool diagnose = false,
class F,
class Env,
class U2>
116 if constexpr(LB::preserve_concrete_covers && LB::is_arithmetic) {
118 auto sort = f.sort();
119 if(sort.has_value() && sort->is_bool()) {
120 k.
meet(
local_type(LB::geq_k(LB::pre_universe::zero()), UB::leq_k(UB::pre_universe::one())));
127 "No component of this interval can interpret this formula.",
128 (r = LB::template interpret_tell<diagnose>(f, env, k.
lb(), diagnostics),
129 r |= UB::template interpret_tell<diagnose>(f, env, k.
ub(), diagnostics),
137 template<
bool diagnose = false,
class F,
class Env,
class U2>
140 if(f.is_binary() && f.sig() ==
NEQ) {
141 return LB::template interpret_ask<diagnose>(f, env, k.
lb(), diagnostics);
143 else if(f.is_binary() && f.sig() ==
EQ) {
145 "When interpreting equality, the underlying bounds LB and UB failed to agree on the same value.",
146 (LB::template interpret_tell<diagnose>(f, env, itv.
lb(), diagnostics) &&
147 UB::template interpret_tell<diagnose>(f, env, itv.
ub(), diagnostics) &&
148 itv.
lb() == itv.
ub()),
151 else if(f.is_binary() && f.sig() ==
IN && f.seq(0).is_variable()
152 && f.seq(1).is(F::S) && f.seq(1).s().size() == 1)
154 const auto&
lb = battery::get<0>(f.seq(1).s()[0]);
155 const auto&
ub = battery::get<1>(f.seq(1).s()[0]);
158 "Failed to interpret the decomposition of set membership `x in {[v..v]}` into equality `x == v`.",
159 (interpret_ask<diagnose>(F::make_binary(f.seq(0),
EQ,
lb), env, k, diagnostics)));
162 "Failed to interpret the decomposition of set membership `x in {[l..u]}` into `x >= l /\\ x <= u`.",
163 (LB::template interpret_ask<diagnose>(F::make_binary(f.seq(0),
geq_of_constant(
lb),
lb), env, itv.
lb(), diagnostics) &&
164 UB::template interpret_ask<diagnose>(F::make_binary(f.seq(0),
leq_of_constant(
ub),
ub), env, itv.
ub(), diagnostics)),
170 "No component of this interval can interpret this formula.",
171 (r = LB::template interpret_ask<diagnose>(f, env, k.
lb(), diagnostics),
172 r |= UB::template interpret_ask<diagnose>(f, env, k.
ub(), diagnostics),
176 template<IKind kind,
bool diagnose = false,
class F,
class Env,
class U2>
179 return interpret_ask<diagnose>(f, env, k, diagnostics);
182 return interpret_tell<diagnose>(f, env, k, diagnostics);
187 CUDA INLINE
constexpr LB&
lb() {
return l; }
188 CUDA INLINE
constexpr UB&
ub() {
return u; }
190 CUDA INLINE
constexpr const LB&
lb()
const {
return l; }
191 CUDA INLINE
constexpr const UB&
ub()
const {
return u; }
210 bool r = l.join(other.l);
211 r |= u.join(other.u);
232 bool r = l.meet(other.l);
233 r |= u.meet(other.u);
239 return l.extract(ua.l) && u.extract(ua.u);
242 template<
class Env,
class Allocator =
typename Env::allocator_type>
246 return F::make_false();
249 return F::make_true();
252 return ub().deinterpret(x, env, allocator);
255 return lb().deinterpret(x, env, allocator);
257 F logical_lb =
lb().template deinterpret<F>();
258 F logical_ub =
ub().template deinterpret<F>();
260 logical_set[0] = battery::make_tuple(std::move(logical_lb), std::move(logical_ub));
261 F set = F::make_set(std::move(logical_set));
262 F var = F::make_avar(x);
263 return F::make_binary(var,
IN, std::move(set),
UNTYPED, allocator);
272 F logical_lb =
lb().template deinterpret<F>();
273 if(logical_lb.is(F::R)) {
274 F logical_ub =
ub().template deinterpret<F>();
275 battery::get<1>(logical_lb.r()) = battery::get<0>(logical_ub.r());
300 return local_type(dual_bound<LB2>(x.
ub()), dual_bound<UB2>(x.
lb()));
311 nx.meet_lb(LB2::geq_k(LB2::pre_universe::zero()));
342 CUDA
constexpr static bounds_sign sign(
const Interval<A>& a) {
343 if(a.lb() >= LB2::geq_k(LB2::pre_universe::zero())) {
344 if(a.ub() > UB2::leq_k(UB2::pre_universe::zero())) {
352 if(a.ub() >= UB2::leq_k(UB2::pre_universe::zero())) {
372 using PLB =
typename LB::pre_universe;
373 using PUB =
typename UB::pre_universe;
374 using value_t =
typename PUB::value_type;
376 value_t x1 = PUB::project(fun, a.lb().value(), b.lb().value());
377 value_t x2 = PUB::project(fun, a.lb().value(), b.ub().value());
378 value_t x3 = PUB::project(fun, a.ub().value(), b.lb().value());
379 value_t x4 = PUB::project(fun, a.ub().value(), b.ub().value());
380 meet_lb(
LB(PLB::join(PLB::join(x1, x2), PLB::join(x3, x4))));
381 meet_ub(
UB(PUB::join(PUB::join(x1, x2), PUB::join(x3, x4))));
384 value_t x1 = PLB::project(fun, a.lb().value(), b.lb().value());
385 value_t x2 = PLB::project(fun, a.lb().value(), b.ub().value());
386 value_t x3 = PLB::project(fun, a.ub().value(), b.lb().value());
387 value_t x4 = PLB::project(fun, a.ub().value(), b.ub().value());
388 meet_lb(
LB(PLB::join(PLB::join(x1, x2), PLB::join(x3, x4))));
390 x1 = PUB::project(fun, a.lb().value(), b.lb().value());
391 x2 = PUB::project(fun, a.lb().value(), b.ub().value());
392 x3 = PUB::project(fun, a.ub().value(), b.lb().value());
393 x4 = PUB::project(fun, a.ub().value(), b.ub().value());
394 meet_ub(
UB(PUB::join(PUB::join(x1, x2), PUB::join(x3, x4))));
401 piecewise_monotone_fun(
MUL, a, b);
406 constexpr auto zero = LB2::pre_universe::zero();
407 using flat_type = LB2::local_flat_type;
408 constexpr auto fzero = flat_type::eq_k(zero);
412 if(b.
lb().value() < 0 && b.
ub().value() > 0) {
418 piecewise_monotone_fun(divfun, a,
420 (b.
ub().value() == zero) ? UB2(-1) : b.
ub()));
424 flat_type al(a.
lb());
425 flat_type au(a.
ub());
426 flat_type bl(b.
lb());
427 flat_type bu(b.
ub());
430 if(bl <= fzero && bu >= fzero) {
431 if(bl == fzero && bu == fzero) {
meet_bot();
return; }
432 if(al == fzero && au == fzero) {
meet_lb(LB2::geq_k(zero));
meet_ub(UB2::leq_k(zero));
return; }
433 if(bl == fzero) {
lb().project(divfun, al, bu);
return; }
434 ub().project(divfun, al, bl);
438 piecewise_monotone_fun(divfun, a, b);
445 if(a.
lb().value() == a.
ub().value() && b.
lb().value() == b.
ub().value()) {
446 flat_fun(modfun, a, b);
452 if(a.
lb().value() == a.
ub().value() && b.
lb().value() == b.
ub().value()) {
458 return LB2::is_trivial_fun(fun) && UB2::is_trivial_fun(fun)
463 if(LB2::is_order_preserving_fun(fun) && UB2::is_order_preserving_fun(fun)) {
464 l.project(fun, x.
lb(), y.
lb());
465 u.project(fun, x.
ub(), y.
ub());
467 else if constexpr(LB::is_arithmetic) {
468 if (fun ==
SUB) {
sub(x, y); }
469 else if (fun ==
MUL) {
mul(x, y); }
472 else if (fun ==
POW) {
pow(x, y); }
477 static_assert(LB::is_totally_ordered && LB::is_arithmetic,
478 "Width is only defined for totally ordered arithmetic intervals.");
486 static_assert(LB::is_totally_ordered && LB::is_arithmetic,
487 "Median function is only defined for totally ordered arithmetic intervals.");
490 auto l =
lb().value();
491 auto u =
ub().value();
492 typename LB::value_type two{2};
493 return local_type(l + battery::fdiv((u - l), two), l + battery::cdiv((u - l), two));
499template<
class L,
class K>
502 if(a.
is_bot()) {
return b; }
503 if(b.
is_bot()) {
return a; }
507template<
class L,
class K>
513template<
class L,
class K>
514CUDA
constexpr bool operator<=(
const Interval<L>& a,
const Interval<K>& b)
516 return a.is_bot() || (a.lb() <= b.lb() && a.ub() <= b.ub());
519template<
class L,
class K>
522 return a <= b && a != b;
525template<
class L,
class K>
526CUDA
constexpr bool operator>=(
const Interval<L>& a,
const Interval<K>& b)
531template<
class L,
class K>
537template<
class L,
class K>
546 return a.
lb().value() == k && a.
ub().value() == k;
549template<
class L,
class K>
550CUDA
constexpr bool operator!=(
const Interval<L>& a,
const Interval<K>& b)
557 return s <<
"[" << itv.
lb() <<
".." << itv.
ub() <<
"]";
Definition diagnostics.hpp:19
Definition interval.hpp:17
battery::tuple< typename LB::value_type, typename UB::value_type > value_type
Definition interval.hpp:23
CUDA constexpr bool meet(const Interval< A > &other)
Definition interval.hpp:231
typename LB::dual_type UB
Definition interval.hpp:20
CUDA static NI bool interpret(const F &f, const Env &env, Interval< U2 > &k, IDiagnostics &diagnostics)
Definition interval.hpp:177
CUDA constexpr bool meet_ub(const A &ub)
Definition interval.hpp:226
CUDA static constexpr local_type eq_one()
Definition interval.hpp:82
CUDA static constexpr local_type bot()
Definition interval.hpp:84
CUDA constexpr void mul(const local_type &a, const local_type &b)
Definition interval.hpp:399
static constexpr const bool sequential
Definition interval.hpp:30
CUDA constexpr bool extract(Interval< A > &ua) const
Definition interval.hpp:238
CUDA static constexpr local_type reverse(const Interval< L > &x)
Definition interval.hpp:299
CUDA constexpr void mod(Sig modfun, const local_type &a, const local_type &b)
Definition interval.hpp:443
static constexpr const bool is_arithmetic
Definition interval.hpp:39
static constexpr const bool injective_concretization
Definition interval.hpp:36
static constexpr const bool preserve_concrete_covers
Definition interval.hpp:37
CUDA constexpr local::B is_bot() const
Definition interval.hpp:86
CUDA constexpr void div(Sig divfun, const local_type &a, const local_type &b)
Definition interval.hpp:405
constexpr this_type & operator=(this_type &&)=default
static CUDA constexpr bool is_trivial_fun(Sig fun)
Definition interval.hpp:457
CUDA constexpr void project(Sig fun, const local_type &x)
Definition interval.hpp:316
CUDA constexpr bool join_ub(const A &ub)
Definition interval.hpp:204
CUDA constexpr void additive_inverse(const this_type &x)
Definition interval.hpp:294
CUDA constexpr bool join(const Interval< A > &other)
Definition interval.hpp:209
static constexpr const bool is_totally_ordered
Definition interval.hpp:31
U LB
Definition interval.hpp:19
static constexpr const char * name
Definition interval.hpp:40
CUDA static constexpr local_type eq_zero()
Definition interval.hpp:80
static constexpr const bool preserve_top
Definition interval.hpp:32
static constexpr const bool preserve_join
Definition interval.hpp:35
typename LB::memory_type memory_type
Definition interval.hpp:24
CUDA constexpr Interval(const typename U::value_type &x)
Definition interval.hpp:58
CUDA constexpr void pow(const local_type &a, const local_type &b)
Definition interval.hpp:450
constexpr this_type & operator=(const this_type &)=default
CUDA NI void print() const
Definition interval.hpp:283
CUDA TFormula< Allocator > deinterpret(AVar x, const Env &env, const Allocator &allocator=Allocator()) const
Definition interval.hpp:243
static constexpr const bool preserve_meet
Definition interval.hpp:34
Interval< typename LB::local_type > local_type
Definition interval.hpp:22
CUDA constexpr Interval(const LB &lb, const UB &ub)
Definition interval.hpp:59
CUDA static constexpr local_type top()
Definition interval.hpp:85
CUDA constexpr void meet_bot()
Definition interval.hpp:215
CUDA INLINE constexpr LB & lb()
Definition interval.hpp:187
CUDA constexpr void add(const local_type &x, const local_type &y)
Definition interval.hpp:323
CUDA INLINE constexpr UB & ub()
Definition interval.hpp:188
CUDA constexpr void join_top()
Definition interval.hpp:193
CUDA constexpr void abs(const local_type &x)
Definition interval.hpp:308
static constexpr const bool is_abstract_universe
Definition interval.hpp:29
CUDA constexpr void project(Sig fun, const local_type &x, const local_type &y)
Definition interval.hpp:462
CUDA static NI bool interpret_ask(const F &f, const Env &env, Interval< U2 > &k, IDiagnostics &diagnostics)
Definition interval.hpp:138
CUDA constexpr local_type width() const
Definition interval.hpp:476
static constexpr const bool complemented
Definition interval.hpp:38
CUDA constexpr local_type median() const
Definition interval.hpp:485
CUDA constexpr value_type value() const
Definition interval.hpp:91
friend class Interval
Definition interval.hpp:27
CUDA constexpr void sub(const local_type &x, const local_type &y)
Definition interval.hpp:327
CUDA constexpr bool join_lb(const A &lb)
Definition interval.hpp:199
CUDA constexpr local::B is_top() const
Definition interval.hpp:90
CUDA NI F deinterpret() const
Definition interval.hpp:271
constexpr Interval(this_type &&)=default
CUDA constexpr Interval(const Interval< A > &other)
Definition interval.hpp:62
CUDA INLINE constexpr const UB & ub() const
Definition interval.hpp:191
CUDA INLINE constexpr const LB & lb() const
Definition interval.hpp:190
CUDA constexpr Interval(Interval< A > &&other)
Definition interval.hpp:65
constexpr Interval(const this_type &)=default
CUDA constexpr void neg(const local_type &x)
Definition interval.hpp:303
CUDA constexpr this_type & operator=(const Interval< A > &other)
Definition interval.hpp:70
CUDA constexpr bool meet_lb(const A &lb)
Definition interval.hpp:221
CUDA static NI bool interpret_tell(const F &f, const Env &env, Interval< U2 > &k, IDiagnostics &diagnostics)
Definition interval.hpp:115
constexpr Interval()=default
static constexpr const bool preserve_bot
Definition interval.hpp:33
#define CALL_WITH_ERROR_CONTEXT(MSG, CALL)
Definition diagnostics.hpp:181
#define CALL_WITH_ERROR_CONTEXT_WITH_MERGE(MSG, CALL, MERGE)
Definition diagnostics.hpp:168
Definition abstract_deps.hpp:14
std::ostream & operator<<(std::ostream &s, const CartesianProduct< A, As... > &cp)
Definition cartesian_product.hpp:531
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
@ 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
@ POW
Unary arithmetic function symbols.
Definition ast.hpp:97
@ ABS
Unary arithmetic function symbols.
Definition ast.hpp:96
@ SUB
Unary arithmetic function symbols.
Definition ast.hpp:97
@ MUL
Unary arithmetic function symbols.
Definition ast.hpp:97
@ NEG
Unary arithmetic function symbols.
Definition ast.hpp:96
battery::vector< battery::tuple< F, F >, typename F::allocator_type > logic_set
Definition sort.hpp:127
CUDA Sig leq_of_constant(const TFormula< Allocator > &f)
Definition algorithm.hpp:61
CUDA constexpr bool operator<(const CartesianProduct< As... > &a, const CartesianProduct< Bs... > &b)
Definition cartesian_product.hpp:485
CUDA NI constexpr bool is_division(Sig sig)
Definition ast.hpp:234
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
CUDA Sig geq_of_constant(const TFormula< Allocator > &f)
Definition algorithm.hpp:54
CUDA NI constexpr bool is_modulo(Sig sig)
Definition ast.hpp:238
#define UNTYPED
Definition sort.hpp:21