Lattice Land Core Library
Loading...
Searching...
No Matches
simplifier.hpp
Go to the documentation of this file.
1// Copyright 2023 Pierre Talbot
2
3#ifndef LALA_CORE_SIMPLIFIER_HPP
4#define LALA_CORE_SIMPLIFIER_HPP
5
6#include "logic/logic.hpp"
8#include "abstract_deps.hpp"
9#include "battery/dynamic_bitset.hpp"
10
11namespace lala {
12
19
20 template <class StatPrinter>
21 CUDA void print(StatPrinter& stats, size_t fp_iter) {
22 stats.print_stat_fp_iter("eliminated_entailed_constraints", fp_iter, eliminated_entailed_constraints);
23 stats.print_stat_fp_iter("eliminated_equality_constraints", fp_iter, eliminated_equality_constraints);
24 stats.print_stat_fp_iter("eliminated_constraints_by_icse", fp_iter, eliminated_constraints_by_icse);
25 stats.print_stat_fp_iter("eliminated_constraints_by_as", fp_iter, eliminated_constraints_by_as);
26 stats.print_stat_fp_iter("icse_fixpoint_iterations", fp_iter, icse_fixpoint_iterations);
27 }
28
29 template <class StatPrinter>
30 CUDA void print(StatPrinter& stats) {
31 stats.print_stat("eliminated_entailed_constraints", eliminated_entailed_constraints);
32 stats.print_stat("eliminated_equality_constraints", eliminated_equality_constraints);
33 stats.print_stat("eliminated_constraints_by_icse", eliminated_constraints_by_icse);
34 stats.print_stat("eliminated_constraints_by_as", eliminated_constraints_by_as);
35 stats.print_stat("icse_fixpoint_iterations", icse_fixpoint_iterations);
36 }
37
45};
46
47/** This abstract domain works at the level of logical formulas.
48 * It deduces the formula by performing a number of simplifications w.r.t. an underlying abstract domain including:
49 * 1. Removing assigned variables.
50 * 2. Removing unused variables.
51 * 3. Removing entailed formulas.
52 * 4. Removing variable equality by tracking equivalence classes.
53 *
54 * The simplified formula can be obtained by calling `deinterpret()`.
55 * Given a solution to the simplified formula, the value of the variables deleted can be obtained by calling `print_variable()`.
56 */
57template<class A, class Allocator>
59public:
60 using allocator_type = Allocator;
61 using sub_type = A;
62 using sub_allocator_type = typename sub_type::allocator_type;
63 using universe_type = typename sub_type::universe_type;
64 using memory_type = typename universe_type::memory_type;
66
67 constexpr static const bool is_abstract_universe = false;
68 constexpr static const bool sequential = universe_type::sequential;
69 constexpr static const bool is_totally_ordered = false;
70 // Note that I did not define the concretization function formally yet... This is not yet an fully fledged abstract domain, we need to work more on it!
71 constexpr static const bool preserve_bot = true;
72 constexpr static const bool preserve_top = true;
73 constexpr static const bool preserve_join = true;
74 constexpr static const bool preserve_meet = true;
75 constexpr static const bool injective_concretization = true;
76 constexpr static const bool preserve_concrete_covers = true;
77 constexpr static const char* name = "Simplifier";
78
79 template<class A2, class Alloc2>
80 friend class Simplifier;
81
82 using formula_sequence = battery::vector<TFormula<allocator_type>, allocator_type>;
83
84private:
85 AType atype;
86 AType store_aty;
88 // We keep a copy of the variable environment in which the formula has been initially interpreted.
89 // This is necessary to project the variables and ask constraints in the subdomain during deduction.
91 // Read-only conjunctive formula, where each is treated independently.
92 formula_sequence formulas;
93 // Write-only (accessed in only 1 thread because this is not a parallel lattice entity) conjunctive formula, the main operation is a map between formulas and simplified_formulas.
94 formula_sequence simplified_formulas;
95 // eliminated_variables[i] is `true` when the variable `i` can be removed because it is assigned to a constant.
96 battery::dynamic_bitset<memory_type, allocator_type> eliminated_variables;
97 // eliminated_formulas[i] is `true` when the formula `i` is entailed.
98 battery::dynamic_bitset<memory_type, allocator_type> eliminated_formulas;
99 // `equivalence_classes[i]` contains the index of the representative variable in the equivalence class of the variable `i`.
100 battery::vector<ZUB<int, memory_type>, allocator_type> equivalence_classes;
101 // `constants[i]` contains the universe value of the representative variables `i`, aggregated by meet on the values of all variables in the equivalence class.
102 battery::vector<universe_type, allocator_type> constants;
103
104public:
105 CUDA Simplifier(AType atype
106 , AType store_aty
108 , const allocator_type& alloc = allocator_type())
109 : atype(atype), store_aty(store_aty), sub(sub), env(alloc)
110 , formulas(alloc), simplified_formulas(alloc)
111 , eliminated_variables(alloc), eliminated_formulas(alloc)
112 , equivalence_classes(alloc), constants(alloc)
113 {}
114
115 CUDA Simplifier(this_type&& other)
116 : atype(other.atype), store_aty(other.store_aty), sub(std::move(other.sub)), env(other.env)
117 , formulas(std::move(other.formulas)), simplified_formulas(std::move(other.simplified_formulas))
118 , eliminated_variables(std::move(other.eliminated_variables)), eliminated_formulas(std::move(other.eliminated_formulas))
119 , equivalence_classes(std::move(other.equivalence_classes)), constants(std::move(other.constants))
120 {}
121
122 struct light_copy_tag {};
123
124 // This return a light copy of `other`, basically just keeping the equivalence classes and the environment to be able to print solutions and call `representative`.
125 template<class A2, class Alloc2>
127 : atype(other.atype)
128 , store_aty(other.store_aty)
129 , sub(sub)
130 , env(other.env, alloc)
131 , equivalence_classes(other.equivalence_classes, alloc)
132 , constants(other.constants, alloc)
133 {}
134
136 return formulas.get_allocator();
137 }
138
139 CUDA AType aty() const {
140 return atype;
141 }
142
143 /** @parallel @order-preserving @increasing */
144 CUDA local::B is_bot() const {
145 return sub->is_bot();
146 }
147
148 /** Returns the number of variables currently represented by this abstract element. */
149 CUDA size_t vars() const {
150 return equivalence_classes.size();
151 }
152
153 template <class Alloc>
154 struct tell_type {
158 tell_type(const Alloc& alloc = Alloc())
159 : num_vars(0), formulas(alloc), env(nullptr)
160 {}
161 };
162
163public:
164 template <bool diagnose = false, class F, class Env, class Alloc2>
165 CUDA NI bool interpret_tell(const F& f, Env& env, tell_type<Alloc2>& tell, IDiagnostics& diagnostics) const {
166 if(f.is(F::E)) {
167 tell.num_vars++;
168 tell.env = &env;
169 }
170 else {
171 tell.formulas.push_back(f);
172 tell.env = &env;
173 }
174 return true;
175 }
176
177 template <IKind kind, bool diagnose = false, class F, class Env, class Alloc2>
178 CUDA bool interpret(const F& f, Env& env, tell_type<Alloc2>& tell, IDiagnostics& diagnostics) const {
179 return interpret_tell<diagnose>(f, env, tell, diagnostics);
180 }
181
182 CUDA void initialize(int num_vars, int num_cons) {
183 eliminated_variables.resize(num_vars);
184 eliminated_variables.reset();
185 eliminated_formulas.resize(num_cons);
186 eliminated_formulas.reset();
187 constants.resize(num_vars);
188 for(int i = 0; i < constants.size(); ++i) {
189 constants[i].join_top();
190 }
191 equivalence_classes.resize(num_vars);
192 for(int i = 0; i < equivalence_classes.size(); ++i) {
193 equivalence_classes[i] = i;
194 }
195 }
196
197 /** We initialize the equivalence classes and var/cons elimination masks.
198 * Further, we eliminate all constraints in `tnf` that are not in TNF.
199 * (It is the existential quantifiers and unary constraints that are re-generated from the underlying store later.)
200 */
201 template <class Seq>
202 CUDA void initialize_tnf(int num_vars, const Seq& tnf) {
203 initialize(num_vars, tnf.size());
204 int z = 0;
205 for(int i = 0; i < tnf.size(); ++i) {
206 if(!is_tnf(tnf[i])) {
207 ++z;
208 eliminate(eliminated_formulas, i);
209 }
210 }
211 }
212
213public:
214 /** @sequential */
215 template <class Alloc2>
216 CUDA bool deduce(tell_type<Alloc2>&& t) {
217 if(t.env != nullptr) { // could be nullptr if the interpreted formula is true.
218 env = *(t.env);
219 initialize(t.num_vars, t.formulas.size());
220 formulas = std::move(t.formulas);
221 simplified_formulas.resize(formulas.size());
222 return true;
223 }
224 return false;
225 }
226
227 // `f` must be a formula from `formulas`.
228 CUDA AVar var_of(const TFormula<allocator_type>& f) const {
229 using F = TFormula<allocator_type>;
230 if(f.is(F::LV)) {
231 assert(env.variable_of(f.lv()).has_value());
232 assert(env.variable_of(f.lv())->get().avar_of(store_aty).has_value());
233 return env.variable_of(f.lv())->get().avar_of(store_aty).value();
234 }
235 else {
236 assert(f.is(F::V));
237 assert(env[f.v()].avar_of(store_aty).has_value());
238 return env[f.v()].avar_of(store_aty).value();
239 }
240 }
241
242public:
243 /** Print the abstract universe of `vname` taking into account simplifications (representative variable and constant).
244 */
245 template <class Alloc, class Abs, class Env>
246 CUDA void print_variable(const LVar<Alloc>& vname, const Env& benv, const Abs& b) const {
247 assert(env.variable_of(vname).has_value());
248 const auto& local_var = env.variable_of(vname)->get();
249 assert(local_var.avar_of(store_aty).has_value());
250 int rep = equivalence_classes[local_var.avar_of(store_aty)->vid()];
251 const auto& rep_name = env.name_of(AVar{store_aty, rep});
252 auto benv_variable = benv.variable_of(rep_name);
253 if(benv_variable.has_value()) {
254 benv_variable->get().sort.print_value(b.project(benv_variable->get().avars[0]));
255 }
256 else {
257 local_var.sort.print_value(constants[rep]);
258 }
259 }
260
261private:
262 /** \return `true` if mask[i] was changed. */
263 CUDA local::B eliminate(battery::dynamic_bitset<memory_type, allocator_type>& mask, size_t i) {
264 if(!mask.test(i)) {
265 mask.set(i, true);
266 return true;
267 }
268 return false;
269 }
270
271 CUDA local::B eliminate(battery::dynamic_bitset<memory_type, allocator_type>& mask, size_t i, size_t& eliminated_constraints) {
272 if(eliminate(mask, i)) {
273 ++eliminated_constraints;
274 return true;
275 }
276 return false;
277 }
278
279 // We eliminate the representative of the variable `i` if it is a singleton.
280 CUDA local::B vdeduce(int i) {
281 const auto& u = sub->project(AVar{store_aty, i});
282 size_t j = find(i);
283 local::B has_changed = constants[j].meet(u);
284 if(!constants[j].is_bot() && constants[j].lb().value() == constants[j].ub().value()) {
285 has_changed |= eliminate(eliminated_variables, j);
286 }
287 return has_changed;
288 }
289
290public:
291 CUDA local::B cons_deduce(int i) {
292 using F = TFormula<allocator_type>;
293 local::B has_changed = false;
294 // Eliminate constraint of the form x = y, and add x,y in the same equivalence class.
295 if(is_var_equality(formulas[i])) {
296 size_t s = 0;
297 return replace_by_equivalence(var_of(formulas[i].seq(0)), var_of(formulas[i].seq(1)), i, s);
298 }
299 else {
300 // Eliminate entailed formulas.
301 IDiagnostics diagnostics;
302 typename sub_type::template ask_type<allocator_type> ask;
303#ifdef _MSC_VER // Avoid MSVC compiler bug. See https://stackoverflow.com/questions/77144003/use-of-template-keyword-before-dependent-template-name
304 if(sub->interpret_ask(formulas[i], env, ask, diagnostics))
305#else
306 if(sub->template interpret_ask(formulas[i], env, ask, diagnostics))
307#endif
308 {
309 if(sub->ask(ask)) {
310 return eliminate(eliminated_formulas, i);
311 }
312 }
313 // Replace assigned variables by constants.
314 // Note that since everything is in a fixed point loop, both the constant and the equivalence class might be updated later on.
315 // This is one of the reasons we cannot update `formulas` in-place: we would not be able to update the constant a second time (since the variable would be eliminated).
316 auto f = formulas[i].map([&](const F& f, const F& parent) {
317 if(f.is_variable()) {
318 AVar x = var_of(f);
319 if(eliminated_variables.test(x.vid())) {
320 auto k = constants[x.vid()].template deinterpret<F>();
321 if(env[x].sort.is_bool() && k.is(F::Z) && parent.is_logical()) {
322 return k.z() == 0 ? F::make_false() : F::make_true();
323 }
324 return std::move(k);
325 }
326 else if(equivalence_classes[x.vid()] != x.vid()) {
327 return F::make_lvar(UNTYPED, env.name_of(AVar{store_aty, equivalence_classes[x.vid()]}));
328 }
329 return f.map_atype(UNTYPED);
330 }
331 return f;
332 });
333 f = eval(f);
334 if(f.is_true()) {
335 return eliminate(eliminated_formulas, i);
336 }
337 if(f != simplified_formulas[i]) {
338 simplified_formulas[i] = f;
339 return true;
340 }
341 return false;
342 }
343 }
344
345 /** We have one deduction operator per variable and one per constraint in the interpreted formula. */
346 CUDA size_t num_deductions() const {
347 return constants.size() + formulas.size();
348 }
349
350 CUDA local::B deduce(size_t i) {
351 assert(i < num_deductions());
352 if(i < constants.size()) {
353 return vdeduce(i);
354 }
355 else {
356 return cons_deduce(i - constants.size());
357 }
358 }
359
360 template <class Env>
361 CUDA void init_env(const Env& env) {
362 this->env = env;
363 }
364
365private:
366 CUDA local::B replace_by_equivalence(AVar x, AVar y, int i, size_t& eliminated_constraints) {
367 return replace_by_equivalence(x.vid(), y.vid(), i, eliminated_constraints);
368 }
369
370 CUDA local::B replace_by_equivalence(int x, int y, int i, size_t& eliminated_constraints) {
371 merge(x, y);
372 return eliminate(eliminated_formulas, i, eliminated_constraints);
373 }
374
375public:
376 /** I-CSE algorithm.
377 * For each pair of TNF constraints `x <=> y op z` and `x' <=> y' op' z'`, whenever `[y'] = [y]`, `op = op'` and `[z] = [z']`, we add the equivalence `x = x'` and eliminate the second constraint.
378 * Note that [x] represents the equivalence class of `x`.
379 * To avoid an algorithm running in O(n^2), we use a hash map to detect syntactical equivalence between `y op z` and `y' op z'`.
380 * Further, for commutative operators, we redefine the equality function.
381 *
382 * This algorithm is applied until a fixpoint is reached.
383 * \return The number of formulas eliminated.
384 */
385 template <class Seq>
386 CUDA bool i_cse(const Seq& tnf, SimplifierStats& stats) {
387 auto hash = [](const std::tuple<int,Sig,int> &right_tnf) {
388 return static_cast<size_t>(std::get<0>(right_tnf))
389 * static_cast<size_t>(std::get<1>(right_tnf))
390 * static_cast<size_t>(std::get<2>(right_tnf));
391 };
392 // This equality function also checks for commutative operators (in which case the hash will also be the same).
393 auto equal = [](const std::tuple<int,Sig,int> &l, const std::tuple<int,Sig,int> &r){
394 return std::get<1>(l) == std::get<1>(r)
395 && ((std::get<0>(l) == std::get<0>(r) && std::get<2>(l) == std::get<2>(r)));
396 // || (is_commutative(std::get<1>(l)) && std::get<0>(l) == std::get<2>(r) && std::get<2>(l) == std::get<0>(r)));
397 };
398 std::unordered_map<std::tuple<int,Sig,int>, int, decltype(hash), decltype(equal)> cs(tnf.size(), hash, equal);
399 bool has_changed = false;
400 bool local_has_changed = true;
401 while(local_has_changed) {
403 local_has_changed = false;
404 cs.clear();
405 for(int i = 0; i < tnf.size(); ++i) {
406 if(!eliminated_formulas.test(i)) {
407 int x = find(var_of(tnf[i].seq(0)).vid());
408 int y = find(var_of(tnf[i].seq(1).seq(0)).vid());
409 int z = find(var_of(tnf[i].seq(1).seq(1)).vid());
410 Sig op = tnf[i].seq(1).sig();
411 auto p = cs.insert(std::make_pair(std::make_tuple(y, op, z), x));
412 if(!p.second) { // `p.second` is false if we detect a collision.
413 local_has_changed |= replace_by_equivalence(x, p.first->second, i, stats.eliminated_constraints_by_icse);
414 if(local_has_changed) {
415 has_changed = true;
416 }
417 }
418 }
419 }
420 }
421 return has_changed;
422 }
423
424 /** Perform algebraic simplification on the TNF.
425 * The non-eliminated constraints are assumed to be in TNF.
426 */
427 template <class Seq>
428 CUDA bool algebraic_simplify(Seq& tnf, SimplifierStats& stats) {
429 using F = typename Seq::value_type;
430 constexpr universe_type ZERO(0,0);
431 constexpr universe_type ONE(1,1);
432 auto& vstore = *sub;
433 size_t elim_cons = stats.eliminated_constraints_by_as;
434 size_t elim_eq = stats.eliminated_equality_constraints;
435 bool has_changed = false;
436 for(int i = 0; i < tnf.size(); ++i) {
437 if(!eliminated_formulas.test(i)) {
438 int x = find(var_of(tnf[i].seq(0)).vid());
439 int y = find(var_of(tnf[i].seq(1).seq(0)).vid());
440 int z = find(var_of(tnf[i].seq(1).seq(1)).vid());
441 Sig sig = tnf[i].seq(1).sig();
442 bool x_is_c = vstore[x].lb() == vstore[x].ub();
443 bool y_is_c = vstore[y].lb() == vstore[y].ub();
444 bool z_is_c = vstore[z].lb() == vstore[z].ub();
445 /** Put constants on the right side of the operator. */
446 if(is_commutative(sig) && y_is_c) {
447 std::swap(y, z);
448 }
449 switch(sig) {
450 case ADD: {
451 /** x = x + z -> z = 0 and x = y + x -> y = 0 */
452 if(x == y || x == z) {
453 int y2 = x == y ? z : y;
454 vstore[y2].meet(ZERO);
455 eliminate(eliminated_formulas, i, stats.eliminated_constraints_by_as);
456 }
457 /** x = y + 0 -> x = y */
458 else if(vstore[z] == ZERO) {
459 replace_by_equivalence(x, y, i, stats.eliminated_constraints_by_as);
460 }
461 /** x = y + y -> x = y * 2 */
462 else if(y == z) {
463 tnf[i].seq(1) = F::make_binary(
464 F::make_lvar(UNTYPED, env.name_of(AVar{store_aty, y})),
465 MUL,
466 F::make_lvar(UNTYPED, LVar<allocator_type>("__CONSTANT_2")));
467 }
468 break;
469 }
470 case MUL: {
471 /** x = x * k -> x = 0 (if k != 1), true otherwise. */
472 if(x == y && z_is_c) {
473 if(vstore[z] != ONE) {
474 has_changed |= vstore[x].meet(ZERO);
475 }
476 else { /* true */ }
477 eliminate(eliminated_formulas, i, stats.eliminated_constraints_by_as);
478 }
479 /** k = y * y -> y \in [-n,n] (if n * n = k), false (otherwise).
480 * This is an over-approximation, thus we cannot eliminate the constraint. */
481 else if(x_is_c && y == z) {
482 auto n = battery::iroots_up(vstore[x].lb().value(), 2);
483 if(n * n == vstore[x].lb()) {
484 has_changed |= vstore[y].meet(universe_type(-n, n));
485 }
486 else {
487 vstore[y].meet_bot(); // false because k is not a perfect square.
488 }
489 }
490 /** x = y * 1 */
491 else if(vstore[z] == ONE) {
492 replace_by_equivalence(x, y, i, stats.eliminated_constraints_by_as);
493 }
494 /** x = x * x */
495 else if(x == y && y == z) {
496 vstore[x].meet(universe_type(0,1));
497 eliminate(eliminated_formulas, i, stats.eliminated_constraints_by_as);
498 }
499 break;
500 }
501 case EDIV: {
502 /** x = 1/x -> x \in {-1,1} (over-approximated so the constraint cannot not eliminated) */
503 if(vstore[y] == ONE && x == z) {
504 has_changed |= vstore[x].meet(universe_type(-1,1));
505 }
506 else if(vstore[y] == ZERO && x == z) {
507 vstore[x].meet_bot();
508 }
509 else if(x_is_c && y == z) {
510 if(vstore[x] != ONE) {
511 vstore[y].meet_bot();
512 }
513 // Cannot eliminate the constraint as we must take into account that y != 0.
514 }
515 else if(vstore[z] == ONE) {
516 replace_by_equivalence(x, y, i, stats.eliminated_constraints_by_as);
517 }
518 else if(x == y && y == z) {
519 vstore[x].meet(ONE);
520 eliminate(eliminated_formulas, i, stats.eliminated_constraints_by_as);
521 }
522 break;
523 }
524 case EMOD: {
525 /** x = x mod x -> x = 0 */
526 if(x == y && y == z) {
527 vstore[x].meet(ZERO);
528 eliminate(eliminated_formulas, i, stats.eliminated_constraints_by_as);
529 }
530 /** x = x mod k -> x in [0, abs(k) - 1] */
531 else if(x == y && z_is_c) {
532 vstore[x].meet(universe_type(0, std::abs(vstore[z].lb()) - 1));
533 eliminate(eliminated_formulas, i, stats.eliminated_constraints_by_as);
534 }
535 /** x = k mod x is always false. */
536 else if(x == z && y_is_c) {
537 vstore[x].meet_bot();
538 }
539 /** 0 = x mod x is always true. */
540 else if(y == z && vstore[x] == ZERO) {
541 eliminate(eliminated_formulas, i, stats.eliminated_constraints_by_as);
542 }
543 break;
544 }
545 case MIN:
546 case MAX: {
547 /** x = min/max(y, y) -> x = y */
548 if(y == z) {
549 replace_by_equivalence(x, y, i, stats.eliminated_constraints_by_as);
550 }
551 /** x = min(x, y) -> 1 = (x <= y) */
552 /** x = max(x, y) -> 1 = (y <= x) */
553 else if(x == y || x == z) {
554 int y2 = x == y ? z : y;
555 int x2 = x;
556 if(sig == MAX) {
557 std::swap(x2, y2);
558 }
559 tnf[i].seq(0) = F::make_lvar(UNTYPED, LVar<allocator_type>("__CONSTANT_1"));
560 tnf[i].seq(1) = F::make_binary(
561 F::make_lvar(UNTYPED, env.name_of(AVar{store_aty, x2})),
562 LEQ,
563 F::make_lvar(UNTYPED, env.name_of(AVar{store_aty, y2})));
564 }
565 break;
566 }
567 case EQUIV:
568 case EQ: {
569 if(vstore[x] == ONE) {
570 replace_by_equivalence(y, z, i, stats.eliminated_equality_constraints);
571 }
572 /** x = (x = k) -> false (k = 0), x = 1 (k = 1) or x = 0 */
573 else if(x == y && z_is_c) {
574 if(vstore[z] == ZERO) {
575 vstore[x].meet_bot();
576 }
577 else if(vstore[z] == ONE) {
578 vstore[x].meet(ONE);
579 }
580 else {
581 vstore[x].meet(ZERO);
582 }
583 eliminate(eliminated_formulas, i, stats.eliminated_constraints_by_as);
584 }
585 else if(y == z) {
586 vstore[x].meet(ONE);
587 eliminate(eliminated_formulas, i, stats.eliminated_constraints_by_as);
588 }
589 break;
590 }
591 case LEQ: {
592 /** x = (x <= k) -> x = 0 (k < 0), x = 1 (k > 0), false (k = 0) */
593 if(x == y && z_is_c) {
594 int k = vstore[z].lb();
595 if(k < 0) {
596 vstore[x].meet(ZERO);
597 }
598 else if(k > 0) {
599 vstore[x].meet(ONE);
600 }
601 else { /** no solution with k == 0 */
602 vstore[x].meet_bot();
603 }
604 eliminate(eliminated_formulas, i, stats.eliminated_constraints_by_as);
605 }
606 /** x = (k <= x) -> x = 0 (k > 1), x = 1 (k <= 1), true (k = 1). */
607 else if(x == z && y_is_c) {
608 int k = vstore[y].lb();
609 if(k > 1) {
610 vstore[x].meet(ZERO);
611 }
612 else if(k < 1) {
613 vstore[x].meet(ONE);
614 }
615 else { /** true whenever k = 1 */ }
616 eliminate(eliminated_formulas, i, stats.eliminated_constraints_by_as);
617 }
618 else if(y == z) {
619 vstore[x].meet(ONE);
620 eliminate(eliminated_formulas, i, stats.eliminated_constraints_by_as);
621 }
622 break;
623 }
624 default:
625 printf("Unsupported operator %s in TNF algebraic simplification.\n", string_of_sig(sig));
626 }
627 }
628 }
629 return has_changed || elim_cons != stats.eliminated_constraints_by_as || elim_eq != stats.eliminated_equality_constraints;
630 }
631
632private:
633 /** Find operation in union-find algorithm.
634 * An additional invariant is that:
635 * forall x. store[x] >= store[find(x)]
636 * That is, the root node contains the meet of all domains in the equivalence class.
637 */
638 CUDA int find(int x) {
639 int root = x;
640 while(equivalence_classes[root] != root) {
641 root = equivalence_classes[root];
642 }
643 while(equivalence_classes[x] != root) {
644 int parent = equivalence_classes[x];
645 sub->embed(AVar{store_aty, parent}, (*sub)[x]);
646 equivalence_classes[x] = root;
647 x = parent;
648 }
649 return root;
650 }
651
652 /** A simple merge operation in union-find algorithm. */
653 CUDA void merge(int x, int y) {
654 int rx = find(x);
655 int ry = find(y);
656 if(rx != ry) {
657 // Easier to debug and more robust for testing: use the root with the smallest index.
658 if(rx < ry) battery::swap(rx, ry);
659 equivalence_classes[rx] = ry;
660 sub->embed(AVar{store_aty, ry}, (*sub)[rx]);
661 }
662 }
663
664public:
666 for(int i = 0; i < equivalence_classes.size(); ++i) {
667 int root = find(i);
668 sub->embed(AVar{store_aty, root}, (*sub)[i]);
669 }
670 for(int i = 0; i < equivalence_classes.size(); ++i) {
671 int root = find(i);
672 sub->embed(AVar{store_aty, i}, (*sub)[root]);
673 }
674 }
675
676 template <class B, class Seq>
677 CUDA void eliminate_entailed_constraints(const B& b, const Seq& tnf, SimplifierStats& stats) {
678 for(int i = 0; i < tnf.size(); ++i) {
679 if(!is_tnf(tnf[i]) || eliminated_formulas.test(i)) {
680 continue;
681 }
682 IDiagnostics diagnostics;
683 typename sub_type::template ask_type<allocator_type> ask_value;
684 bool ask_success = b.interpret_ask(tnf[i], env, ask_value, diagnostics);
685 assert(ask_success);
686 if(b.ask(ask_value)) {
687 eliminate(eliminated_formulas, i, stats.eliminated_entailed_constraints);
688 }
689 }
690 }
691
692 template <class Seq>
693 CUDA void eliminate_useless_variables(const Seq& tnf, size_t& num_eliminated_variables) {
694 /** Keep only the variables that are representative and occur in at least one TNF constraint. */
695 eliminated_variables.set();
696 for(int i = 0; i < tnf.size(); ++i) {
697 if(!eliminated_formulas.test(i)) {
698 eliminated_variables.set(find(var_of(tnf[i].seq(0)).vid()), false);
699 eliminated_variables.set(find(var_of(tnf[i].seq(1).seq(0)).vid()), false);
700 eliminated_variables.set(find(var_of(tnf[i].seq(1).seq(1)).vid()), false);
701 }
702 }
703 num_eliminated_variables = eliminated_variables.count();
704 /** Eliminated variables might still occur in the variables we need to print.
705 * Therefore, we save them in `constants`. */
706 for(int i = 0; i < sub->vars(); ++i) {
707 int root = find(i);
708 constants[i] = sub->project(AVar{store_aty, root});
709 }
710 }
711
712private:
713 template <class F>
714 void substitute_var(F& f) const {
715 if(f.is_variable()) {
716 AVar x = var_of(f);
717 // Note: `find` is non-const, and anyways, `eliminate_useless_variables` is called before, hence find(x) = equivalence_classes[x].
718 int root = equivalence_classes[x.vid()];
719 if(x.vid() != root) {
720 x = AVar{store_aty, root};
721 f = F::make_lvar(store_aty, env.name_of(x));
722 }
723 /** If the variable is eliminated, but still appear in a constraint at this stage, it means it's an "extra" constraint not in TNF, and therefore substitute the variable by its constant. */
724 if(eliminated_variables.test(x.vid())) {
725 auto k = (*sub)[x.vid()].template deinterpret<F>();
726 if(env[x].sort.is_bool() && k.is(F::Z)) {
727 f = k.z() == 0 ? F::make_false() : F::make_true();
728 }
729 else {
730 f = std::move(k);
731 }
732 }
733 }
734 }
735
736public:
737 /** Given any formula (not necessarily in TNF), we substitute each variable with its representative variable or a constant if it got eliminated. */
738 template <class F>
739 CUDA void substitute(F& f) const {
740 f.inplace_map([this](F& leaf, const F&) { substitute_var(leaf); });
741 }
742
743 CUDA size_t num_vars_after_elimination() const {
744 size_t keep = 0;
745 for(int i = 0; i < equivalence_classes.size(); ++i) {
746 if(equivalence_classes[i] == i && !eliminated_variables.test(i)) {
747 ++keep;
748 }
749 }
750 return keep;
751 }
752
753private:
754 // Deinterpret the existential quantifiers (only one per equivalence classes), and the domain of each variable.
755 template <class Seq>
756 CUDA void deinterpret_vars(Seq& seq) {
757 using F = TFormula<allocator_type>;
758 for(int i = 0; i < equivalence_classes.size(); ++i) {
759 if(equivalence_classes[i] == i && !eliminated_variables.test(i)) {
760 const auto& x = env[AVar{store_aty, i}];
761 seq.push_back(F::make_exists(UNTYPED, x.name, x.sort));
762 auto domain_constraint = constants[i].deinterpret(AVar{store_aty, i}, env, get_allocator());
763 map_avar_to_lvar(domain_constraint, env, true);
764 seq.push_back(domain_constraint);
765 }
766 }
767 }
768
769 template <class Seq1, class Seq2>
770 CUDA void deinterpret_constraints(Seq1& seq, const Seq2& formulas, bool enable_substitute = false) {
771 // Deinterpret the simplified formulas.
772 for(int i = 0; i < formulas.size(); ++i) {
773 if(!eliminated_formulas.test(i)) {
774 seq.push_back(formulas[i]);
775 if(enable_substitute) {
776 substitute(seq.back());
777 }
778 }
779 }
780 }
781
782public:
783 template <class Seq>
784 CUDA NI TFormula<allocator_type> deinterpret(const Seq& source, bool substitute) {
785 using F = TFormula<allocator_type>;
786 typename F::Sequence seq(get_allocator());
787 if(is_bot()) {
788 return F::make_false();
789 }
790 if(eliminated_variables.all() || eliminated_formulas.all()) {
791 return F::make_true();
792 }
793 deinterpret_vars(seq);
794 deinterpret_constraints(seq, source, substitute);
795 return seq.size() == 0 ? F::make_true() : F::make_nary(AND, std::move(seq));
796 }
797
799 return deinterpret(simplified_formulas, false);
800 }
801};
802
803} // namespace lala
804
805#endif
Definition ast.hpp:38
CUDA constexpr int vid() const
Definition ast.hpp:69
Definition b.hpp:10
Definition diagnostics.hpp:19
Definition simplifier.hpp:58
CUDA allocator_type get_allocator() const
Definition simplifier.hpp:135
static constexpr const bool preserve_bot
Definition simplifier.hpp:71
CUDA local::B deduce(size_t i)
Definition simplifier.hpp:350
CUDA Simplifier(this_type &&other)
Definition simplifier.hpp:115
CUDA bool deduce(tell_type< Alloc2 > &&t)
Definition simplifier.hpp:216
Allocator allocator_type
Definition simplifier.hpp:60
A sub_type
Definition simplifier.hpp:61
CUDA size_t vars() const
Definition simplifier.hpp:149
static constexpr const bool preserve_join
Definition simplifier.hpp:73
CUDA void init_env(const Env &env)
Definition simplifier.hpp:361
CUDA local::B is_bot() const
Definition simplifier.hpp:144
static constexpr const bool injective_concretization
Definition simplifier.hpp:75
CUDA local::B cons_deduce(int i)
Definition simplifier.hpp:291
CUDA void eliminate_entailed_constraints(const B &b, const Seq &tnf, SimplifierStats &stats)
Definition simplifier.hpp:677
CUDA AVar var_of(const TFormula< allocator_type > &f) const
Definition simplifier.hpp:228
CUDA NI bool interpret_tell(const F &f, Env &env, tell_type< Alloc2 > &tell, IDiagnostics &diagnostics) const
Definition simplifier.hpp:165
CUDA NI TFormula< allocator_type > deinterpret(const Seq &source, bool substitute)
Definition simplifier.hpp:784
battery::vector< TFormula< allocator_type >, allocator_type > formula_sequence
Definition simplifier.hpp:82
CUDA bool interpret(const F &f, Env &env, tell_type< Alloc2 > &tell, IDiagnostics &diagnostics) const
Definition simplifier.hpp:178
CUDA bool algebraic_simplify(Seq &tnf, SimplifierStats &stats)
Definition simplifier.hpp:428
CUDA bool i_cse(const Seq &tnf, SimplifierStats &stats)
Definition simplifier.hpp:386
CUDA size_t num_vars_after_elimination() const
Definition simplifier.hpp:743
CUDA AType aty() const
Definition simplifier.hpp:139
static constexpr const bool preserve_top
Definition simplifier.hpp:72
CUDA void eliminate_useless_variables(const Seq &tnf, size_t &num_eliminated_variables)
Definition simplifier.hpp:693
static constexpr const char * name
Definition simplifier.hpp:77
static constexpr const bool is_abstract_universe
Definition simplifier.hpp:67
static constexpr const bool is_totally_ordered
Definition simplifier.hpp:69
CUDA Simplifier(AType atype, AType store_aty, abstract_ptr< sub_type > sub, const allocator_type &alloc=allocator_type())
Definition simplifier.hpp:105
CUDA size_t num_deductions() const
Definition simplifier.hpp:346
typename sub_type::allocator_type sub_allocator_type
Definition simplifier.hpp:62
typename universe_type::memory_type memory_type
Definition simplifier.hpp:64
CUDA void substitute(F &f) const
Definition simplifier.hpp:739
CUDA NI TFormula< allocator_type > deinterpret()
Definition simplifier.hpp:798
CUDA void initialize(int num_vars, int num_cons)
Definition simplifier.hpp:182
CUDA void initialize_tnf(int num_vars, const Seq &tnf)
Definition simplifier.hpp:202
CUDA void print_variable(const LVar< Alloc > &vname, const Env &benv, const Abs &b) const
Definition simplifier.hpp:246
CUDA Simplifier(const Simplifier< A2, Alloc2 > &other, light_copy_tag tag, abstract_ptr< sub_type > sub, const allocator_type &alloc=allocator_type())
Definition simplifier.hpp:126
static constexpr const bool sequential
Definition simplifier.hpp:68
typename sub_type::universe_type universe_type
Definition simplifier.hpp:63
CUDA void meet_equivalence_classes()
Definition simplifier.hpp:665
static constexpr const bool preserve_concrete_covers
Definition simplifier.hpp:76
static constexpr const bool preserve_meet
Definition simplifier.hpp:74
Definition ast.hpp:286
CUDA bool is(size_t kind) const
Definition ast.hpp:526
CUDA const LVar< Allocator > & lv() const
Definition ast.hpp:579
CUDA AVar v() const
Definition ast.hpp:575
Definition env.hpp:264
CUDA NI std::optional< std::reference_wrapper< const variable_type > > variable_of(const char *lv) const
Definition env.hpp:478
CUDA const bstring & name_of(AVar av) const
Definition env.hpp:517
::lala::B<::battery::local_memory > B
Definition b.hpp:12
Definition abstract_deps.hpp:14
CUDA NI constexpr bool is_commutative(Sig sig)
Definition ast.hpp:243
CUDA NI void map_avar_to_lvar(F &f, const Env &env, bool erase_type=false)
Definition algorithm.hpp:438
Sig
Definition ast.hpp:94
@ LEQ
Unary arithmetic function symbols.
Definition ast.hpp:113
@ EQ
Unary arithmetic function symbols.
Definition ast.hpp:112
@ ADD
Unary arithmetic function symbols.
Definition ast.hpp:97
@ MIN
Unary arithmetic function symbols.
Definition ast.hpp:97
@ EDIV
Unary arithmetic function symbols.
Definition ast.hpp:105
@ MAX
Binary arithmetic function symbols.
Definition ast.hpp:97
@ AND
Unary arithmetic function symbols.
Definition ast.hpp:114
@ EQUIV
Unary arithmetic function symbols.
Definition ast.hpp:114
@ MUL
Unary arithmetic function symbols.
Definition ast.hpp:97
@ EMOD
Euclidean division (Boute T. R. (1992). The Euclidean definition of the functions div and mod)....
Definition ast.hpp:105
battery::shared_ptr< A, typename A::allocator_type > abstract_ptr
Definition abstract_deps.hpp:17
int AType
Definition sort.hpp:18
CUDA NI bool is_var_equality(const TFormula< Allocator, ExtendedSig > &f)
Definition algorithm.hpp:33
CUDA NI const char * string_of_sig(Sig sig)
Definition ast.hpp:121
CUDA NI int num_vars(const F &f)
Definition algorithm.hpp:154
battery::string< Allocator > LVar
Definition ast.hpp:25
CUDA NI F eval(const F &f)
Definition algorithm.hpp:814
CUDA bool is_tnf(const F &f)
Definition ternarize.hpp:28
#define UNTYPED
Definition sort.hpp:21
Definition simplifier.hpp:122
Definition simplifier.hpp:154
tell_type(const Alloc &alloc=Alloc())
Definition simplifier.hpp:158
int num_vars
Definition simplifier.hpp:155
VarEnv< Alloc > * env
Definition simplifier.hpp:157
formula_sequence formulas
Definition simplifier.hpp:156
Definition simplifier.hpp:13
size_t eliminated_equality_constraints
Definition simplifier.hpp:15
size_t eliminated_constraints_by_as
Definition simplifier.hpp:16
CUDA void merge(SimplifierStats &other)
Definition simplifier.hpp:38
size_t icse_fixpoint_iterations
Definition simplifier.hpp:18
CUDA void print(StatPrinter &stats)
Definition simplifier.hpp:30
size_t eliminated_constraints_by_icse
Definition simplifier.hpp:14
CUDA void print(StatPrinter &stats, size_t fp_iter)
Definition simplifier.hpp:21
size_t eliminated_entailed_constraints
Definition simplifier.hpp:17