Lattice Land Core Library
Loading...
Searching...
No Matches
arith_bound.hpp
Go to the documentation of this file.
1// Copyright 2022 Pierre Talbot
2
3#ifndef LALA_CORE_ARITH_BOUND_HPP
4#define LALA_CORE_ARITH_BOUND_HPP
5
6#include <type_traits>
7#include <utility>
8#include <cmath>
9#include <iostream>
10#include "../logic/logic.hpp"
11#include "pre_flb.hpp"
12#include "pre_fub.hpp"
13#include "pre_zlb.hpp"
14#include "pre_zub.hpp"
15#include "../b.hpp"
16#include "battery/memory.hpp"
17
18/** A pre-abstract universe is a lattice (with usual operations join, order, ...) equipped with a simple logical interpretation function and a next/prev functions.
19 We consider totally ordered pre-abstract universes with a downset semantics.
20 For any lattice \f$ L \f$, we consider an element \f$ a \in L \f$ to represent all the concrete elements equal to or below it.
21 This set is called the downset of \f$ a \f$ and is denoted \f$ \mathord{\downarrow}{a} \f$.
22 The concretization function \f$ \gamma \f$ formalizes this idea: \f$ \gamma(a) = \{x \mapsto b \;|\; b \in \mathord{\downarrow}{a} \cap U \} \f$ where \f$ U \f$ is the universe of discourse.
23 The intersection with \f$ U \f$ is necessary to remove potential elements in the abstract universe that are not in the concrete universe of discourse (e.g., \f$ -\infty, \infty \f$ below).
24
25 The downset semantics associates each element of a lattice to its concrete downset.
26 It is possible to decide that each element is associated to the concrete upset instead.
27 Doing so will reverse our usage of the lattice-theoretic operations (join instead of meet, <= instead of >=, etc.).
28 Instead of considering the upset semantics, it is more convenient to consider the downset semantics of the dual lattice.
29
30 Example:
31 * The lattice of increasing integer \f$ \mathit{ZUB} = \langle \{-\infty, \ldots, -2, -1, 0, 1, 2, \ldots, \infty\}, \leq \rangle \f$ is ordered by the natural arithmetic comparison operator, it represents an upper bound on the set of integers represented.
32 Using the downset semantics, we can represent simple constraints such as \f$ x \leq 3 \f$, in which case the downset \f$ \mathord{\downarrow}{3} = \{\ldots, 1, 2, 3\} \f$ represents all the values of \f$ x \f$ satisfying the constraints \f$ x \leq 3 \f$, that is, the solutions of the constraints.
33 * By taking the upset semantics of \f$ \mathit{ZUB} \f$, we can represent constraints such as \f$ x \geq 3 \f$.
34 * Alternatively, we can take the dual lattice of decreasing integers \f$ \mathit{ZLB} = \langle \{\infty, \ldots, 2, 1, 0, -1, -2, \ldots, -\infty\}, \geq \rangle \f$.
35 The downset semantics of \f$ \mathit{ZLB} \f$ corresponds to the upset semantics of \f$ \mathit{ZUB} \f$.
36
37 From a pre-abstract universe, we obtain an abstract universe using the `Universe` class below.
38 We also define various aliases to abstract universes such as `ZLB`, `ZUB`, etc.
39*/
40
41namespace lala {
42
43template<class PreUniverse, class Mem>
44class FlatUniverse;
45
46template<class PreUniverse, class Mem>
47class ArithBound;
48
49/** Lattice of integer lower bounds. */
50template<class VT, class Mem>
52
53/** Lattice of integer upper bounds. */
54template<class VT, class Mem>
56
57/** Lattice of floating-point lower bounds. */
58template<class VT, class Mem>
60
61/** Lattice of floating-point upper bounds. */
62template<class VT, class Mem>
64
65/** Aliases for lattice allocated on the stack (as local variable) and accessed by only one thread.
66 * To make things simpler, the underlying type is also chosen (when required). */
67namespace local {
72}
73
74namespace impl {
75 template<class T>
76 struct is_arith_bound {
77 static constexpr bool value = false;
78 };
79
80 template<class PreUniverse, class Mem>
81 struct is_arith_bound<ArithBound<PreUniverse, Mem>> {
82 static constexpr bool value = true;
83 };
84
85 template <class T>
86 inline constexpr bool is_arith_bound_v = is_arith_bound<T>::value;
87}
88
89
90template <class A, class R = A>
91R project_fun(Sig fun, const A& a, const A& b) {
92 R r{};
93 r.project(fun, a, b);
94 return r;
95}
96
97template <class A, class R = A>
98R project_fun(Sig fun, const A& a) {
99 R r{};
100 r.project(fun, a);
101 return r;
102}
103
104/** This function is useful when we need to convert a value to its dual.
105 The dual is the upset of the current element, therefore, if we have \f$ x <= 10 \f$, the dual is given by the formula \f$ x >= 10 \f$ interpreted in the dual lattice.
106 In that case, it just changes the type of the lattice without changing the value.
107 A difference occurs on the bottom and top element.
108 Indeed, by our representation of bot and top, the bottom value in a lattice L equals the top value in its dual, but we need them to remain the same, so the dual of `L::bot()` is `LDual::bot()`.*/
109template <class LDual, class L>
110CUDA constexpr LDual dual_bound(const L& x) {
111 if(x.is_bot()) return LDual::bot();
112 if(x.is_top()) return LDual::top();
113 return LDual(x.value());
114}
115
116template<class PreUniverse, class Mem>
118{
119 using U = PreUniverse;
120public:
121 using pre_universe = PreUniverse;
122 using value_type = typename pre_universe::value_type;
123 using memory_type = Mem;
126
127 template<class M>
129
131
132 template<class M>
135
136 constexpr static const bool is_abstract_universe = true;
137 constexpr static const bool sequential = Mem::sequential;
138 constexpr static const bool is_totally_ordered = pre_universe::is_totally_ordered;
139 constexpr static const bool preserve_bot = pre_universe::preserve_bot;
140 constexpr static const bool preserve_top = pre_universe::preserve_top;
141 constexpr static const bool preserve_join = pre_universe::preserve_join;
142 constexpr static const bool preserve_meet = pre_universe::preserve_meet;
143 constexpr static const bool injective_concretization = pre_universe::injective_concretization;
144 constexpr static const bool preserve_concrete_covers = pre_universe::preserve_concrete_covers;
145 constexpr static const bool is_lower_bound = pre_universe::is_lower_bound;
146 constexpr static const bool is_upper_bound = pre_universe::is_upper_bound;
147 constexpr static const char* name = pre_universe::name;
148
149 constexpr static const bool is_arithmetic = pre_universe::is_arithmetic;
150
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).");
153
154 /** A pre-interpreted formula `x >= value` ready to use.
155 * This is mainly for optimization purpose to avoid calling `interpret` each time we need it. */
156 CUDA static constexpr this_type geq_k(value_type k) {
157 if constexpr(is_lower_bound) {
158 return this_type(k);
159 }
160 else {
161 static_assert(is_lower_bound,
162 "The pre-interpreted formula x >= k is only available over abstract universe modelling lower bounds.");
163 }
164 }
165
166 CUDA static constexpr this_type leq_k(value_type k) {
167 if constexpr(is_upper_bound) {
168 return this_type(k);
169 }
170 else {
171 static_assert(is_upper_bound,
172 "The pre-interpreted formula x <= k is only available over abstract universe modelling upper bounds.");
173 }
174 }
175
176 using atomic_type = memory_type::template atomic_type<value_type>;
177private:
178 atomic_type val;
179
180public:
181 /** Similar to \f$[\![\mathit{false}]\!]\f$ if `preserve_bot` is true. */
182 CUDA static constexpr local_type bot() { return local_type(U::bot()); }
183
184 /** Similar to \f$[\![\mathit{true}]\!]\f$ if `preserve_top` is true. */
185 CUDA static constexpr local_type top() { return local_type(U::top()); }
186 /** Initialize an upset universe to top. */
187 CUDA constexpr ArithBound(): val(U::top()) {}
188 /** Similar to \f$[\![x \leq_A i]\!]\f$ for any name `x` where \f$ \leq_A \f$ is the lattice order. */
189 CUDA constexpr ArithBound(value_type x): val(x) {}
190 constexpr ArithBound(const this_type& other) = default;
191 constexpr ArithBound(this_type&& other) = default;
192
193 template <class M>
194 CUDA constexpr ArithBound(const this_type2<M>& other): ArithBound(other.value()) {}
195
196 /** The assignment operator can only be used in a sequential context.
197 * It is monotone but not extensive. */
198 template <class M>
199 CUDA constexpr this_type& operator=(const this_type2<M>& other) {
200 memory_type::store(val, other.value());
201 return *this;
202 }
203
204 constexpr this_type& operator=(const this_type& other) = default;
205
206 CUDA constexpr value_type value() const { return memory_type::load(val); }
207
208 CUDA constexpr atomic_type& atomic() { return val; }
209
210 // This is dangerous because a conversion to `value_type` can be done implicitly, and overloaded operators <, >, ... can be used on the underlying value_type instead of the abstract universe.
211 CUDA constexpr operator value_type() const { return value(); }
212
213 /** \return `true` whenever \f$ a = \top \f$, `false` otherwise.
214 * @parallel @order-preserving @increasing
215 */
216 CUDA constexpr local::B is_top() const {
217 return value() == U::top();
218 }
219
220 /** \return `true` whenever \f$ a = \bot \f$, `false` otherwise.
221 * @parallel @order-preserving @decreasing
222 */
223 CUDA constexpr local::B is_bot() const {
224 return value() == U::bot();
225 }
226
227 CUDA constexpr void join_top() {
228 memory_type::store(val, U::top());
229 }
230
231 template<class M1>
232 CUDA constexpr bool join(const this_type2<M1>& other) {
233 value_type r1 = value();
234 value_type r2 = other.value();
235 if(U::strict_order(r1, r2)) {
236 memory_type::store(val, r2);
237 return true;
238 }
239 return false;
240 }
241
242 CUDA constexpr void meet_bot() {
243 memory_type::store(val, U::bot());
244 }
245
246 template<class M1>
247 CUDA constexpr bool meet(const this_type2<M1>& other) {
248 value_type r1 = value();
249 value_type r2 = other.value();
250 if(U::strict_order(r2, r1)) {
251 memory_type::store(val, r2);
252 return true;
253 }
254 return false;
255 }
256
257 /** \return \f$ x <op> i \f$ where `x` is a variable's name, `i` the current value and `<op>` depends on the underlying universe.
258 If `U` preserves top, `true` is returned whenever \f$ a = \top \f$, if it preserves bottom `false` is returned whenever \f$ a = \bot \f$.
259 We always return an exact approximation, hence for any formula \f$ \llbracket \varphi \rrbracket = a \f$, we must have \f$ a = \llbracket \rrbracket a \llbracket \rrbracket \f$ where \f$ \rrbracket a \llbracket \f$ is the deinterpretation function.
260 */
261 template<class Env, class Allocator = typename Env::allocator_type>
262 CUDA NI TFormula<Allocator> deinterpret(AVar avar, const Env& env, const Allocator& allocator = Allocator()) const {
263 using F = TFormula<Allocator>;
264 if(preserve_top && is_top()) {
265 return F::make_true();
266 }
267 else if(preserve_bot && is_bot()) {
268 return F::make_false();
269 }
270 return F::make_binary(
271 F::make_avar(avar),
272 U::sig_order(),
273 deinterpret<F>(),
274 UNTYPED, allocator);
275 }
276
277 /** Deinterpret the current value to a logical constant. */
278 template<class F>
279 CUDA NI F deinterpret() const {
280 return pre_universe::template deinterpret<F>(value());
281 }
282
283 /** Under-approximates the current element \f$ a \f$ w.r.t. \f$ \rrbracket a \llbracket \f$ into `ua`.
284 * For this abstract universe, it always returns `true` since the current element \f$ a \f$ is an exact representation of \f$ \rrbracket a \llbracket \f$. */
285 CUDA constexpr bool extract(local_type& ua) const {
286 ua.val = value();
287 return true;
288 }
289
290 /** Print the current element. */
291 CUDA NI void print() const {
292 if(is_bot()) {
293 printf("\u22A5");
294 }
295 else if(is_top()) {
296 printf("\u22A4");
297 }
298 else {
300 }
301 }
302
303private:
304 /** Interpret a formula of the form `x <sig> k`. */
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) {
307 value_type value = pre_universe::top();
308 bool res = pre_universe::template interpret_tell<diagnose>(f.seq(1), value, diagnostics);
309 if(res) {
310 if(f.sig() == EQ || f.sig() == U::sig_order()) { // e.g., x <= 4 or x >= 4.24
311 tell.meet(local_type(value));
312 }
313 else if(f.sig() == U::sig_strict_order()) { // e.g., x < 4 or x > 4.24
314 if constexpr(preserve_concrete_covers) {
315 tell.meet(local_type(pre_universe::prev(value)));
316 }
317 else {
318 tell.meet(local_type(value));
319 }
320 }
321 else {
322 RETURN_INTERPRETATION_ERROR("The symbol `" + LVar<typename F::allocator_type>(string_of_sig(f.sig())) + "` is not supported in the tell language of this universe.");
323 }
324 }
325 return res;
326 }
327
328 /** Interpret a formula of the form `x <sig> k`. */
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) {
331 value_type value = pre_universe::top();
332 bool res = pre_universe::template interpret_ask<diagnose>(f.seq(1), value, diagnostics);
333 if(res) {
334 if(f.sig() == U::sig_order()) {
335 tell.meet(local_type(value));
336 }
337 else if(f.sig() == NEQ || f.sig() == U::sig_strict_order()) {
338 // We could actually do a little bit better in the case of FLB/FUB.
339 // If the real number `k` is approximated by `[f, g]`, it actually means `]f, g[` so we could safely choose `r` since it already under-approximates `k`.
340 tell.meet(local_type(pre_universe::prev(value)));
341 }
342 else {
343 RETURN_INTERPRETATION_ERROR("The symbol `" + LVar<typename F::allocator_type>(string_of_sig(f.sig())) + "` is not supported in the ask language of this universe.");
344 }
345 }
346 return res;
347 }
348
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)) {
352 RETURN_INTERPRETATION_ERROR("The constant `S` in a constraint `x in S` must be a set.");
353 }
354 const auto& set = f.seq(1).s();
355 if(set.size() == 0) {
356 tell.meet_bot();
357 return true;
358 }
359 value_type join_s = pre_universe::bot();
360 constexpr int bound_index = is_lower_bound ? 0 : 1;
361 // We interpret each component of the set and take the meet of all the results.
362 for(int i = 0; i < set.size(); ++i) {
363 auto bound = battery::get<bound_index>(set[i]);
364 value_type set_element = pre_universe::top();
365 bool res = pre_universe::template interpret_tell<diagnose>(bound, set_element, diagnostics);
366 if(!res) {
367 return false;
368 }
369 join_s = pre_universe::join(join_s, set_element);
370 }
371 tell.meet(local_type(join_s));
372 return true;
373 }
374
375public:
376 /** Expects a predicate of the form `x <op> k` where `x` is any variable's name, and `k` a constant.
377 * The symbol `<op>` is expected to be `U::sig_order()`, `U::sig_strict_order()`, `=` or `in`.
378 * Existential formula \f$ \exists{x:T} \f$ can also be interpreted (only to top) depending on the underlying pre-universe.
379 */
380 template<bool diagnose = false, class F, class Env, class M2>
381 CUDA NI static bool interpret_tell(const F& f, const Env&, this_type2<M2>& tell, IDiagnostics& diagnostics) {
382 if(f.is(F::E)) {
383 typename U::value_type val;
384 bool res = pre_universe::template interpret_type<diagnose>(f, val, diagnostics);
385 if(res) {
386 tell.meet(local_type(val));
387 }
388 return res;
389 }
390 else {
391 if(f.is_binary() && f.seq(0).is_variable() && f.seq(1).is_constant()) {
392 // `x in k` is equivalent to `x >= meet k` where `>=` is the lattice order `U::sig_order()`.
393 if(f.sig() == IN) {
394 return interpret_tell_set<diagnose>(f, tell, diagnostics);
395 }
396 else {
397 return interpret_tell_x_op_k<diagnose>(f, tell, diagnostics);
398 }
399 }
400 else {
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.");
402 }
403 }
404 }
405
406 /** Expects a predicate of the form `x <op> k` where `x` is any variable's name, and `k` a constant.
407 * The symbol `<op>` is expected to be `U::sig_order()`, `U::sig_strict_order()` or `!=`.
408 */
409 template<bool diagnose = false, class F, class Env, class M2>
410 CUDA NI static bool interpret_ask(const F& f, const Env&, this_type2<M2>& ask, IDiagnostics& diagnostics) {
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);
413 }
414 else {
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.");
416 }
417 }
418
419 template<IKind kind, bool diagnose = false, class F, class Env, class M2>
420 CUDA NI static bool interpret(const F& f, const Env& env, this_type2<M2>& value, IDiagnostics& diagnostics) {
421 if constexpr(kind == IKind::TELL) {
422 return interpret_tell<diagnose>(f, env, value, diagnostics);
423 }
424 else {
425 return interpret_ask<diagnose>(f, env, value, diagnostics);
426 }
427 }
428
429public:
430 CUDA static constexpr local_type next(const this_type2<Mem>& a) {
431 return local_type(pre_universe::next(a.value()));
432 }
433
434 CUDA static constexpr local_type prev(const this_type2<Mem>& a) {
435 return local_type(pre_universe::prev(a.value()));
436 }
437
438 /** Unary function of type `fun: FlatUniverse -> ArithBound`.
439 * If `a` is `bot`, we meet with bottom in-place.
440 * Otherwise, we apply the function `fun` to `a` and meet the result.
441 * \remark The result of the function is always over-approximated (or exact when possible).
442 */
443 CUDA constexpr void project(Sig fun, const local_flat_type& a) {
444 if(a.is_bot()) { meet_bot(); }
445 else if(!a.is_top()) {
446 meet(local_type(pre_universe::project(fun, a)));
447 }
448 }
449
450 /** Binary functions of type `project: FlatUniverse x FlatUniverse -> ArithBound`.
451 * If `a` or `b` is `bot`, we meet bottom in-place.
452 * Otherwise, we meet `fun(a,b)` in-place.
453 * \remark The result of the function is always over-approximated (or exact when possible).
454 * \remark If the function `fun` is partial (e.g. division), we expect the arguments `a` and `b` to be in the domain of `fun` (e.g. not equal to 0).
455 */
456 CUDA constexpr void project(Sig fun, const local_flat_type& a, const local_flat_type& b) {
457 if(a.is_bot() || b.is_bot()) { meet_bot(); }
458 else if(!a.is_top() && !b.is_top()) {
459 meet(local_type(pre_universe::project(fun, a.value(), b.value())));
460 }
461 }
462
463 /** In this universe, the non-trivial order-preserving functions are {min, max, +}. */
464 CUDA static constexpr bool is_trivial_fun(Sig fun) {
465 return fun != MIN && fun != MAX && fun != ADD && (is_upper_bound || fun != ABS);
466 }
467
468 /** The functions that are order-preserving on the natural order of the universe of discourse, and its dual. */
469 CUDA static constexpr bool is_order_preserving_fun(Sig fun) {
470 return fun == ADD || fun == MIN || fun == MAX || (is_lower_bound && fun == ABS);
471 }
472
473 CUDA constexpr void project(Sig fun, const local_type &a, const local_type &b) {
474 if (a.is_bot() || b.is_bot()) { meet_bot(); return; }
475 if(fun == MIN || fun == MAX || fun == ADD) {
476 meet(local_type(pre_universe::project(fun, a.value(), b.value())));
477 }
478 }
479
480 CUDA constexpr void project(Sig fun, const local_type &a) {
481 if (a.is_bot()) { meet_bot(); return; }
482 if (!a.is_top()) {
483 meet(project(fun, a.value()));
484 }
485 }
486
487 template<class Pre2, class Mem2>
488 friend class ArithBound;
489};
490
491// Lattice operators
492
493template<class Pre, class M1, class M2>
495 return Pre::join(a.value(), b.value());
496}
497
498template<class Pre, class M1, class M2>
500 return Pre::meet(a.value(), b.value());
501}
502
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());
506}
507
508template<class Pre, class M1, class M2>
509CUDA constexpr bool operator<(const ArithBound<Pre, M1>& a, const ArithBound<Pre, M2>& b) {
510 return Pre::strict_order(a.value(), b.value());
511}
512
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());
516}
517
518template<class Pre, class M1, class M2>
519CUDA constexpr bool operator>(const ArithBound<Pre, M1>& a, const ArithBound<Pre, M2>& b) {
520 return Pre::strict_order(b.value(), a.value());
521}
522
523template<class Pre, class M1, class M2>
524CUDA constexpr bool operator==(const ArithBound<Pre, M1>& a, const ArithBound<Pre, M2>& b) {
525 return a.value() == b.value();
526}
527
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();
531}
532
533template<class Pre, class M>
534std::ostream& operator<<(std::ostream &s, const ArithBound<Pre, M> &a) {
535 if(a.is_bot()) {
536 s << "\u22A5";
537 }
538 else if(a.is_top()) {
539 s << "\u22A4";
540 }
541 else {
542 s << a.value();
543 }
544 return s;
545}
546
547} // namespace lala
548
549#endif
Definition ast.hpp:38
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 b.hpp:10
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
Definition ast.hpp:286
#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
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
@ 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