Lattice Land Core Library
Loading...
Searching...
No Matches
interval.hpp
Go to the documentation of this file.
1// Copyright 2021 Pierre Talbot
2
3#ifndef LALA_CORE_INTERVAL_HPP
4#define LALA_CORE_INTERVAL_HPP
5
8
9namespace lala {
10
11template <class U>
12class Interval;
13
14/** An interval is a Cartesian product of a lower and upper bounds, themselves represented as lattices.
15 One difference, is that the \f$ \top \f$ can be represented by multiple interval elements, whenever \f$ l > u \f$, therefore some operations are different than on the Cartesian product, e.g., \f$ [3..2] \equiv [4..1] \f$ in the interval lattice. */
16template <class U>
17class Interval {
18public:
19 using LB = U;
20 using UB = typename LB::dual_type;
23 using value_type = battery::tuple<typename LB::value_type, typename UB::value_type>;
24 using memory_type = typename LB::memory_type;
25
26 template <class A>
27 friend class Interval;
28
29 constexpr static const bool is_abstract_universe = true;
30 constexpr static const bool sequential = LB::sequential;
31 constexpr static const bool is_totally_ordered = false;
32 constexpr static const bool preserve_top = LB::preserve_top && UB::preserve_top;
33 constexpr static const bool preserve_bot = true;
34 constexpr static const bool preserve_meet = true;
35 constexpr static const bool preserve_join = false;
36 constexpr static const bool injective_concretization = LB::injective_concretization && UB::injective_concretization;
37 constexpr static const bool preserve_concrete_covers = LB::preserve_concrete_covers && UB::preserve_concrete_covers;
38 constexpr static const bool complemented = false;
39 constexpr static const bool is_arithmetic = LB::is_arithmetic && UB::is_arithmetic;
40 constexpr static const char* name = "Interval";
41
42private:
43 using LB2 = typename LB::local_type;
44 using UB2 = typename UB::local_type;
45 LB l;
46 UB u;
47
48 CUDA constexpr local_type lb2() const { return local_type(lb(), dual_bound<UB2>(lb())); }
49 CUDA constexpr local_type ub2() const { return local_type(dual_bound<LB2>(ub()), ub()); }
50
51public:
52 /** Initialize the interval to top using the default constructor of the bounds. */
53 constexpr Interval() = default;
54 constexpr Interval(const this_type&) = default;
55 constexpr Interval(this_type&&) = default;
56
57 /** Given a value \f$ x \in U \f$ where \f$ U \f$ is the universe of discourse, we initialize a singleton interval \f$ [x..x] \f$. */
58 CUDA constexpr Interval(const typename U::value_type& x): l(x), u(x) {}
59 CUDA constexpr Interval(const LB& lb, const UB& ub): l(lb), u(ub) {}
60
61 template<class A>
62 CUDA constexpr Interval(const Interval<A>& other): l(other.l), u(other.u) {}
63
64 template<class A>
65 CUDA constexpr Interval(Interval<A>&& other): l(std::move(other.l)), u(std::move(other.u)) {}
66
67 /** The assignment operator can only be used in a sequential context.
68 * It is monotone but not extensive. */
69 template <class A>
70 CUDA constexpr this_type& operator=(const Interval<A>& other) {
71 l = other.l;
72 u = other.u;
73 return *this;
74 }
75
76 constexpr this_type& operator=(const this_type&) = default;
77 constexpr this_type& operator=(this_type&&) = default;
78
79 /** Pre-interpreted formula `x == 0`. */
80 CUDA constexpr static local_type eq_zero() { return local_type(LB::geq_k(LB::pre_universe::zero()), UB::leq_k(UB::pre_universe::zero())); }
81 /** Pre-interpreted formula `x == 1`. */
82 CUDA constexpr static local_type eq_one() { return local_type(LB::geq_k(LB::pre_universe::one()), UB::leq_k(UB::pre_universe::one())); }
83
84 CUDA constexpr static local_type bot() { return Interval(LB::bot(), UB::bot()); }
85 CUDA constexpr static local_type top() { return Interval(LB::top(), UB::top()); }
86 CUDA constexpr local::B is_bot() const {
87 // The conversion to UB2 is possible because we have verified that lb() is different from bot and top.
88 return l.is_bot() || u.is_bot() || (!is_top() && UB2(lb().value()) > ub());
89 }
90 CUDA constexpr local::B is_top() const { return l.is_top() && u.is_top(); }
91 CUDA constexpr value_type value() const { return battery::make_tuple(l.value(), u.value()); }
92
93private:
94 template<class A, class B>
95 CUDA constexpr void flat_fun(Sig fun, const Interval<A>& a, const Interval<B>& b) {
96 lb().project(fun,
97 typename A::template flat_type<battery::local_memory>(a.lb()),
98 typename B::template flat_type<battery::local_memory>(b.lb()));
99 ub().project(fun,
100 typename A::template flat_type<battery::local_memory>(a.ub()),
101 typename B::template flat_type<battery::local_memory>(b.ub()));
102 }
103
104 template<class A>
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()));
108 }
109
110public:
111 /** Support the same language than the Cartesian product, and more:
112 * * `var x:B` when the underlying universe is arithmetic and preserve concrete covers.
113 * Therefore, the element `k` is always in \f$ \gamma(lb) \cap \gamma(ub) \f$. */
114 template<bool diagnose = false, class F, class Env, class U2>
115 CUDA NI static bool interpret_tell(const F& f, const Env& env, Interval<U2>& k, IDiagnostics& diagnostics) {
116 if constexpr(LB::preserve_concrete_covers && LB::is_arithmetic) {
117 if(f.is(F::E)) {
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())));
121 return true;
122 }
123 }
124 }
125 bool r;
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),
130 r));
131 }
132
133 /** Support the same language than the Cartesian product, and more:
134 * * `x != k` is under-approximated by interpreting `x != k` in the lower bound.
135 * * `x == k` is interpreted by over-approximating `x == k` in both bounds and then verifying both bounds are the same.
136 * * `x in {[l..u]} is interpreted by under-approximating `x >= l` and `x <= u`. */
137 template<bool diagnose = false, class F, class Env, class U2>
138 CUDA NI static bool interpret_ask(const F& f, const Env& env, Interval<U2>& k, IDiagnostics& diagnostics) {
140 if(f.is_binary() && f.sig() == NEQ) {
141 return LB::template interpret_ask<diagnose>(f, env, k.lb(), diagnostics);
142 }
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()),
149 (k.meet(itv)));
150 }
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)
153 {
154 const auto& lb = battery::get<0>(f.seq(1).s()[0]);
155 const auto& ub = battery::get<1>(f.seq(1).s()[0]);
156 if(lb == ub) {
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)));
160 }
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)),
165 (k.meet(itv))
166 );
167 }
168 bool r;
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),
173 r));
174 }
175
176 template<IKind kind, bool diagnose = false, class F, class Env, class U2>
177 CUDA NI static bool interpret(const F& f, const Env& env, Interval<U2>& k, IDiagnostics& diagnostics) {
178 if constexpr(kind == IKind::ASK) {
179 return interpret_ask<diagnose>(f, env, k, diagnostics);
180 }
181 else {
182 return interpret_tell<diagnose>(f, env, k, diagnostics);
183 }
184 }
185
186 /** You must use the lattice interface (join/meet methods) to modify the lower and upper bounds, if you use assignment you violate the PCCP model. */
187 CUDA INLINE constexpr LB& lb() { return l; }
188 CUDA INLINE constexpr UB& ub() { return u; }
189
190 CUDA INLINE constexpr const LB& lb() const { return l; }
191 CUDA INLINE constexpr const UB& ub() const { return u; }
192
193 CUDA constexpr void join_top() {
194 l.join_top();
195 u.join_top();
196 }
197
198 template<class A>
199 CUDA constexpr bool join_lb(const A& lb) {
200 return l.join(lb);
201 }
202
203 template<class A>
204 CUDA constexpr bool join_ub(const A& ub) {
205 return u.join(ub);
206 }
207
208 template<class A>
209 CUDA constexpr bool join(const Interval<A>& other) {
210 bool r = l.join(other.l);
211 r |= u.join(other.u);
212 return r;
213 }
214
215 CUDA constexpr void meet_bot() {
216 l.meet_bot();
217 u.meet_bot();
218 }
219
220 template<class A>
221 CUDA constexpr bool meet_lb(const A& lb) {
222 return l.meet(lb);
223 }
224
225 template<class A>
226 CUDA constexpr bool meet_ub(const A& ub) {
227 return u.meet(ub);
228 }
229
230 template<class A>
231 CUDA constexpr bool meet(const Interval<A>& other) {
232 bool r = l.meet(other.l);
233 r |= u.meet(other.u);
234 return r;
235 }
236
237 template <class A>
238 CUDA constexpr bool extract(Interval<A>& ua) const {
239 return l.extract(ua.l) && u.extract(ua.u);
240 }
241
242 template<class Env, class Allocator = typename Env::allocator_type>
243 CUDA TFormula<Allocator> deinterpret(AVar x, const Env& env, const Allocator& allocator = Allocator()) const {
244 using F = TFormula<Allocator>;
245 if(is_bot()) {
246 return F::make_false();
247 }
248 if(is_top()) {
249 return F::make_true();
250 }
251 if(lb().is_top()) {
252 return ub().deinterpret(x, env, allocator);
253 }
254 else if(ub().is_top()) {
255 return lb().deinterpret(x, env, allocator);
256 }
257 F logical_lb = lb().template deinterpret<F>();
258 F logical_ub = ub().template deinterpret<F>();
259 logic_set<F> logical_set(1, allocator);
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);
264 }
265
266 /** Deinterpret the current value to a logical constant.
267 * The lower bound is deinterpreted, and it is up to the user to check that interval is a singleton.
268 * A special case is made for real numbers where the both bounds are used, since the logical interpretation uses interval.
269 */
270 template<class F>
271 CUDA NI F deinterpret() const {
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());
276 }
277 else {
278 assert(lb().value() == ub().value());
279 }
280 return logical_lb;
281 }
282
283 CUDA NI void print() const {
284 printf("[");
285 lb().print();
286 printf("..");
287 ub().print();
288 printf("]");
289 }
290
291 /** The additive inverse is obtained by pairwise negation of the components.
292 * Equivalent to `neg(reverse(x))`.
293 * Note that the inverse of `bot` is `bot`, simply because `bot` has no mathematical inverse. */
294 CUDA constexpr void additive_inverse(const this_type& x) {
295 flat_fun(NEG, x);
296 }
297
298 template<class L>
299 CUDA constexpr static local_type reverse(const Interval<L>& x) {
300 return local_type(dual_bound<LB2>(x.ub()), dual_bound<UB2>(x.lb()));
301 }
302
303 CUDA constexpr void neg(const local_type& x) {
304 flat_fun(NEG, reverse(x));
305 }
306
307 // This operation preserves top, i.e., \f$ abs(x) \in [\top] \f$ if \f$ x \in [\top] \f$, \f$ [\top] \f$ being the equivalence class of top elements.
308 CUDA constexpr void abs(const local_type& x) {
309 local_type nx{};
310 nx.neg(x);
311 nx.meet_lb(LB2::geq_k(LB2::pre_universe::zero()));
312 meet_lb(fmeet(x.lb(), nx.lb()));
313 meet_ub(fjoin(x.ub(), nx.ub()));
314 }
315
316 CUDA constexpr void project(Sig fun, const local_type& x) {
317 switch(fun) {
318 case NEG: neg(x); break;
319 case ABS: abs(x); break;
320 }
321 }
322
323 CUDA constexpr void add(const local_type& x, const local_type& y) {
324 flat_fun(ADD, x, y);
325 }
326
327 CUDA constexpr void sub(const local_type& x, const local_type& y) {
328 local_type ny{};
329 ny.neg(y);
330 add(x, ny);
331 }
332
333private:
334 /** Characterization of the sign of the bounds (e.g., NP = lower bound is negative, upper bound is positive).
335 * It can viewed as a lattice with the order NP < PP < PN and NP < NN < PN. */
336 enum bounds_sign {
337 PP, NN, NP, PN
338 };
339
340 /** The sign function is monotone w.r.t. the order of `Interval<A>` and `bounds_sign`. */
341 template<class A>
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())) {
345 return PN;
346 }
347 else {
348 return PP;
349 }
350 }
351 else {
352 if(a.ub() >= UB2::leq_k(UB2::pre_universe::zero())) {
353 return NN;
354 }
355 else {
356 return NP;
357 }
358 }
359 }
360
361 /** This is a generic implementation of interval piecewise monotone function, where the function is monotone for each pair of bounds.
362 * Let `fun` be a monotone binary operation such as multiplication: [rl..ru] = [al..au] * [bl..bu]
363 where:
364 (1) rl = min(al*bl, al*bu, au*bl, au*bu)
365 (2) ru = max(al*bl, al*bu, au*bl, au*bu)
366 In the discrete case, we can precompute the products in `l` and `u`.
367 Otherwise, due to rounding, al*bl can be rounded downwards or upwards, and therefore must be computed differently for (1) and (2).
368
369 We do not check if a and b are bot. This is the responsibility of the caller depending if it could pose issues with the function `fun`.
370 */
371 CUDA constexpr void piecewise_monotone_fun(Sig fun, const local_type& a, const local_type& b) {
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))));
382 }
383 else {
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))));
389
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))));
395 }
396 }
397
398public:
399 CUDA constexpr void mul(const local_type& a, const local_type& b) {
400 if(a.is_bot() || b.is_bot()) { meet_bot(); return; } // Perhaps not necessary?
401 piecewise_monotone_fun(MUL, a, b);
402 }
403
404 // Interval division, [al..au] / [bl..bu]
405 CUDA constexpr void div(Sig divfun, const local_type& a, const local_type& 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);
409 if(a.is_bot() || b.is_bot() || (b.lb().value() == zero && b.ub().value() == zero)) { meet_bot(); return; }
410 // Interval division, [rl..ru] = [al..au] / [bl..bu]
411 if constexpr(preserve_concrete_covers) {
412 if(b.lb().value() < 0 && b.ub().value() > 0) {
413 meet_lb(LB(battery::min(a.lb().value(), -a.ub().value())));
414 meet_ub(UB(battery::max(-a.lb().value(), a.ub().value())));
415 }
416 else {
417 // Remove 0 from the bounds of b if any is equal to it.
418 piecewise_monotone_fun(divfun, a,
419 local_type((b.lb().value() == zero) ? LB2(1) : b.lb(),
420 (b.ub().value() == zero) ? UB2(-1) : b.ub()));
421 }
422 }
423 else {
424 flat_type al(a.lb());
425 flat_type au(a.ub());
426 flat_type bl(b.lb());
427 flat_type bu(b.ub());
428
429 // The case where 0 in [bl, bu].
430 if(bl <= fzero && bu >= fzero) {
431 if(bl == fzero && bu == fzero) { meet_bot(); return; } // b is a singleton equal to zero.
432 if(al == fzero && au == fzero) { meet_lb(LB2::geq_k(zero)); meet_ub(UB2::leq_k(zero)); return; } // 0 / b = 0 (b != 0)
433 if(bl == fzero) { lb().project(divfun, al, bu); return; } // If bl is 0, then the upper bound is infinite.
434 ub().project(divfun, al, bl); // if bu is 0, then the lower bound is infinite.
435 return;
436 }
437 else {
438 piecewise_monotone_fun(divfun, a, b);
439 }
440 }
441 }
442
443 CUDA constexpr void mod(Sig modfun, const local_type& a, const local_type& b) {
444 if(a.is_bot() || b.is_bot()) { meet_bot(); return; }
445 if(a.lb().value() == a.ub().value() && b.lb().value() == b.ub().value()) {
446 flat_fun(modfun, a, b);
447 }
448 }
449
450 CUDA constexpr void pow(const local_type& a, const local_type& b) {
451 if(a.is_bot() || b.is_bot()) { meet_bot(); return; }
452 if(a.lb().value() == a.ub().value() && b.lb().value() == b.ub().value()) {
453 flat_fun(POW, a, b);
454 }
455 }
456
457 CUDA static constexpr bool is_trivial_fun(Sig fun) {
458 return LB2::is_trivial_fun(fun) && UB2::is_trivial_fun(fun)
459 && fun != MUL && !is_division(fun) && fun != ABS && fun != SUB && fun != POW && !is_modulo(fun);
460 }
461
462 CUDA constexpr void project(Sig fun, const local_type& x, const local_type& y) {
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());
466 }
467 else if constexpr(LB::is_arithmetic) {
468 if (fun == SUB) { sub(x, y); }
469 else if (fun == MUL) { mul(x, y); }
470 else if (is_division(fun)) { div(fun, x, y); }
471 else if (is_modulo(fun)) { mod(fun, x, y); }
472 else if (fun == POW) { pow(x, y); }
473 }
474 }
475
476 CUDA constexpr local_type width() const {
477 static_assert(LB::is_totally_ordered && LB::is_arithmetic,
478 "Width is only defined for totally ordered arithmetic intervals.");
480 width.sub(ub2(), lb2());
481 return width;
482 }
483
484 /** \return The median value of the interval, which is computed by `lb() + ((ub() - lb()) / 2)`. */
485 CUDA constexpr local_type median() const {
486 static_assert(LB::is_totally_ordered && LB::is_arithmetic,
487 "Median function is only defined for totally ordered arithmetic intervals.");
488 if(is_bot()) { return local_type::bot(); }
489 if(lb().is_top() || ub().is_top()) { return local_type::top(); }
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));
494 }
495};
496
497// Lattice operations
498
499template<class L, class K>
501{
502 if(a.is_bot()) { return b; }
503 if(b.is_bot()) { return a; }
504 return Interval<typename L::local_type>(fjoin(a.lb(), b.lb()), fjoin(a.ub(), b.ub()));
505}
506
507template<class L, class K>
509{
510 return Interval<typename L::local_type>(fmeet(a.lb(), b.lb()), fmeet(a.ub(), b.ub()));
511}
512
513template<class L, class K>
514CUDA constexpr bool operator<=(const Interval<L>& a, const Interval<K>& b)
515{
516 return a.is_bot() || (a.lb() <= b.lb() && a.ub() <= b.ub());
517}
518
519template<class L, class K>
520CUDA constexpr bool operator<(const Interval<L>& a, const Interval<K>& b)
521{
522 return a <= b && a != b;
523}
524
525template<class L, class K>
526CUDA constexpr bool operator>=(const Interval<L>& a, const Interval<K>& b)
527{
528 return b <= a;
529}
530
531template<class L, class K>
532CUDA constexpr bool operator>(const Interval<L>& a, const Interval<K>& b)
533{
534 return b < a;
535}
536
537template<class L, class K>
538CUDA constexpr bool operator==(const Interval<L>& a, const Interval<K>& b)
539{
540 return (a.is_bot() && b.is_bot()) || (a.lb() == b.lb() && a.ub() == b.ub());
541}
542
543template<class L>
544CUDA constexpr bool operator==(const Interval<L>& a, typename L::value_type k)
545{
546 return a.lb().value() == k && a.ub().value() == k;
547}
548
549template<class L, class K>
550CUDA constexpr bool operator!=(const Interval<L>& a, const Interval<K>& b)
551{
552 return !(a == b);
553}
554
555template<class L>
556std::ostream& operator<<(std::ostream &s, const Interval<L> &itv) {
557 return s << "[" << itv.lb() << ".." << itv.ub() << "]";
558}
559
560} // namespace lala
561
562#endif
Definition ast.hpp:38
Definition b.hpp:10
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
Definition ast.hpp:290
#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
Sig
Definition ast.hpp:94
@ 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