• Home
  • Features
  • Pricing
  • Docs
  • Announcements
  • Sign In

daisytuner / sdfglib / 20026333216

08 Dec 2025 11:19AM UTC coverage: 61.756% (+0.05%) from 61.708%
20026333216

push

github

web-flow
Merge pull request #381 from daisytuner/assumptions-constants

Sets constant assumptions for read-only symbols in loop bodies

18 of 19 new or added lines in 2 files covered. (94.74%)

12 existing lines in 3 files now uncovered.

11399 of 18458 relevant lines covered (61.76%)

103.95 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

85.1
/src/symbolic/utils.cpp
1
#include "sdfg/symbolic/utils.h"
2

3
#include <isl/ctx.h>
4
#include <isl/set.h>
5
#include <isl/space.h>
6

7
#include <regex>
8

9
#include "sdfg/builder/sdfg_builder.h"
10
#include "sdfg/codegen/language_extensions/c_language_extension.h"
11
#include "sdfg/symbolic/assumptions.h"
12
#include "sdfg/symbolic/extreme_values.h"
13
#include "sdfg/symbolic/polynomials.h"
14
#include "sdfg/symbolic/symbolic.h"
15

16
namespace sdfg {
17
namespace symbolic {
18

19
std::string expression_to_map_str(const MultiExpression& expr, const Assumptions& assums) {
86✔
20
    builder::SDFGBuilder builder("sdfg", FunctionType_CPU);
86✔
21
    codegen::CLanguageExtension language_extension(builder.subject());
86✔
22

23
    // Get all symbols
24
    symbolic::SymbolSet syms;
86✔
25
    for (auto& expr : expr) {
172✔
26
        auto syms_expr = symbolic::atoms(expr);
86✔
27
        syms.insert(syms_expr.begin(), syms_expr.end());
86✔
28
    }
86✔
29

30
    // Distinguish between dimensions and parameters
31
    std::vector<std::string> dimensions;
86✔
32
    SymbolSet dimensions_syms;
86✔
33
    std::vector<std::string> parameters;
86✔
34
    SymbolSet parameters_syms;
86✔
35
    for (auto& sym : syms) {
110✔
36
        if (assums.find(sym) == assums.end() && assums.at(sym).constant()) {
24✔
37
            if (parameters_syms.find(sym) != parameters_syms.end()) {
×
38
                continue;
×
39
            }
40
            parameters.push_back(sym->get_name());
×
41
            parameters_syms.insert(sym);
×
42
        } else {
×
43
            if (dimensions_syms.find(sym) != dimensions_syms.end()) {
24✔
44
                continue;
×
45
            }
46
            dimensions.push_back(sym->get_name());
24✔
47
            dimensions_syms.insert(sym);
24✔
48
        }
49
    }
50

51
    // Generate constraints
52
    SymbolSet seen;
86✔
53
    auto constraints_syms = generate_constraints(syms, assums, seen);
86✔
54

55
    // Extend parameters with additional symbols from constraints
56
    for (auto& con : constraints_syms) {
158✔
57
        auto con_syms = symbolic::atoms(con);
72✔
58
        for (auto& con_sym : con_syms) {
170✔
59
            if (dimensions_syms.find(con_sym) == dimensions_syms.end()) {
98✔
60
                if (parameters_syms.find(con_sym) != parameters_syms.end()) {
44✔
61
                    continue;
24✔
62
                }
63
                parameters.push_back(con_sym->get_name());
20✔
64
                parameters_syms.insert(con_sym);
20✔
65
            }
20✔
66
        }
67
    }
72✔
68

69
    // Define map
70
    std::string map;
86✔
71
    if (!parameters.empty()) {
86✔
72
        std::sort(parameters.begin(), parameters.end());
12✔
73
        map += "[";
12✔
74
        map += helpers::join(parameters, ", ");
12✔
75
        map += "] -> ";
12✔
76
    }
12✔
77
    map += "{ [" + helpers::join(dimensions, ", ") + "] -> [";
86✔
78
    for (size_t i = 0; i < expr.size(); i++) {
172✔
79
        auto dim = expr[i];
86✔
80
        map += language_extension.expression(dim);
86✔
81
        if (i < expr.size() - 1) {
86✔
UNCOV
82
            map += ", ";
×
UNCOV
83
        }
×
84
    }
86✔
85
    map += "] ";
86✔
86

87
    std::vector<std::string> constraints;
86✔
88
    for (auto& con : constraints_syms) {
158✔
89
        auto con_str = constraint_to_isl_str(con);
72✔
90
        if (!con_str.empty()) {
72✔
91
            constraints.push_back(con_str);
66✔
92
        }
66✔
93
    }
72✔
94
    for (auto& dim : dimensions) {
110✔
95
        auto sym = symbolic::symbol(dim);
24✔
96
        auto map = assums.at(sym).map();
24✔
97
        if (map == SymEngine::null) {
24✔
98
            continue;
14✔
99
        }
100
        if (!SymEngine::is_a<SymEngine::Add>(*map)) {
10✔
101
            continue;
×
102
        }
103
        auto args = SymEngine::rcp_static_cast<const SymEngine::Add>(map)->get_args();
10✔
104
        if (args.size() != 2) {
10✔
105
            continue;
×
106
        }
107
        auto arg0 = args[0];
10✔
108
        auto arg1 = args[1];
10✔
109
        if (!symbolic::eq(arg0, symbolic::symbol(dim))) {
10✔
110
            arg0 = args[1];
10✔
111
            arg1 = args[0];
10✔
112
        }
10✔
113
        if (!symbolic::eq(arg0, symbolic::symbol(dim))) {
10✔
114
            continue;
×
115
        }
116
        if (!SymEngine::is_a<SymEngine::Integer>(*arg1)) {
10✔
117
            continue;
×
118
        }
119
        if (symbolic::eq(arg1, symbolic::one())) {
10✔
120
            continue;
10✔
121
        }
UNCOV
122
        auto lb = assums.at(sym).lower_bound_deprecated();
×
UNCOV
123
        if (!SymEngine::is_a<SymEngine::Integer>(*lb)) {
×
124
            continue;
×
125
        }
126

UNCOV
127
        std::string iter = "__daisy_iterator_" + dim;
×
UNCOV
128
        std::string con = "exists " + iter + " : " + dim + " = " + language_extension.expression(lb) + " + " + iter +
×
UNCOV
129
                          " * " + language_extension.expression(arg1);
×
UNCOV
130
        constraints.push_back(con);
×
131
    }
24✔
132
    if (!constraints.empty()) {
86✔
133
        map += " : ";
24✔
134
        map += helpers::join(constraints, " and ");
24✔
135
    }
24✔
136

137
    map += " }";
86✔
138

139
    // NV Symbols, e.g., threadIdx.x
140
    map = std::regex_replace(map, std::regex("\\."), "_");
86✔
141

142
    // min, max
143
    map = std::regex_replace(map, std::regex("__daisy_min"), "min_");
86✔
144
    map = std::regex_replace(map, std::regex("__daisy_max"), "max_");
86✔
145

146
    return map;
86✔
147
}
86✔
148

149
std::tuple<std::string, std::string, std::string> expressions_to_intersection_map_str(
57✔
150
    const MultiExpression& expr1,
151
    const MultiExpression& expr2,
152
    const Symbol indvar,
153
    const Assumptions& assums1,
154
    const Assumptions& assums2
155
) {
156
    builder::SDFGBuilder builder("sdfg", FunctionType_CPU);
57✔
157
    codegen::CLanguageExtension language_extension(builder.subject());
57✔
158

159
    // Get all symbols
160
    symbolic::SymbolSet syms;
57✔
161
    for (auto& expr : expr1) {
128✔
162
        auto syms_expr = symbolic::atoms(expr);
71✔
163
        syms.insert(syms_expr.begin(), syms_expr.end());
71✔
164
    }
71✔
165
    for (auto& expr : expr2) {
128✔
166
        auto syms_expr = symbolic::atoms(expr);
71✔
167
        syms.insert(syms_expr.begin(), syms_expr.end());
71✔
168
    }
71✔
169

170
    // Distinguish between dimensions and parameters
171
    std::vector<std::string> dimensions;
57✔
172
    SymbolSet dimensions_syms;
57✔
173
    std::vector<std::string> parameters;
57✔
174
    SymbolSet parameters_syms;
57✔
175
    for (auto& sym : syms) {
139✔
176
        if (sym->get_name() != indvar->get_name() && assums1.at(sym).constant() && assums2.at(sym).constant()) {
82✔
177
            if (parameters_syms.find(sym) != parameters_syms.end()) {
12✔
178
                continue;
×
179
            }
180
            parameters.push_back(sym->get_name());
12✔
181
            parameters_syms.insert(sym);
12✔
182
        } else {
12✔
183
            if (dimensions_syms.find(sym) != dimensions_syms.end()) {
70✔
184
                continue;
×
185
            }
186
            dimensions.push_back(sym->get_name());
70✔
187
            dimensions_syms.insert(sym);
70✔
188
        }
189
    }
190

191
    // Generate constraints
192
    SymbolSet seen;
57✔
193
    auto constraints_syms_1 = generate_constraints(syms, assums1, seen);
57✔
194
    seen.clear();
57✔
195
    auto constraints_syms_2 = generate_constraints(syms, assums2, seen);
57✔
196

197
    // Extend parameters with additional symbols from constraints
198
    for (auto& con : constraints_syms_1) {
397✔
199
        auto con_syms = symbolic::atoms(con);
340✔
200
        for (auto& con_sym : con_syms) {
802✔
201
            if (dimensions_syms.find(con_sym) == dimensions_syms.end()) {
462✔
202
                if (parameters_syms.find(con_sym) != parameters_syms.end()) {
266✔
203
                    continue;
200✔
204
                }
205
                parameters.push_back(con_sym->get_name());
66✔
206
                parameters_syms.insert(con_sym);
66✔
207
            }
66✔
208
        }
209
    }
340✔
210
    for (auto& con : constraints_syms_2) {
400✔
211
        auto con_syms = symbolic::atoms(con);
343✔
212
        for (auto& con_sym : con_syms) {
809✔
213
            if (dimensions_syms.find(con_sym) == dimensions_syms.end()) {
466✔
214
                if (parameters_syms.find(con_sym) != parameters_syms.end()) {
266✔
215
                    continue;
266✔
216
                }
217
                parameters.push_back(con_sym->get_name());
×
218
                parameters_syms.insert(con_sym);
×
219
            }
×
220
        }
221
    }
343✔
222

223
    // Define two maps
224
    std::string map_1;
57✔
225
    std::string map_2;
57✔
226
    if (!parameters.empty()) {
57✔
227
        map_1 += "[";
51✔
228
        map_1 += helpers::join(parameters, ", ");
51✔
229
        map_1 += "] -> ";
51✔
230
        map_2 += "[";
51✔
231
        map_2 += helpers::join(parameters, ", ");
51✔
232
        map_2 += "] -> ";
51✔
233
    }
51✔
234
    map_1 += "{ [";
57✔
235
    map_2 += "{ [";
57✔
236
    for (size_t i = 0; i < dimensions.size(); i++) {
127✔
237
        map_1 += dimensions[i] + "_1";
70✔
238
        map_2 += dimensions[i] + "_2";
70✔
239
        if (i < dimensions.size() - 1) {
70✔
240
            map_1 += ", ";
20✔
241
            map_2 += ", ";
20✔
242
        }
20✔
243
    }
70✔
244
    map_1 += "] -> [";
57✔
245
    map_2 += "] -> [";
57✔
246
    for (size_t i = 0; i < expr1.size(); i++) {
128✔
247
        auto dim = expr1[i];
71✔
248
        for (auto& iter : dimensions) {
185✔
249
            dim = symbolic::subs(dim, symbolic::symbol(iter), symbolic::symbol(iter + "_1"));
114✔
250
        }
251
        map_1 += language_extension.expression(dim);
71✔
252
        if (i < expr1.size() - 1) {
71✔
253
            map_1 += ", ";
14✔
254
        }
14✔
255
    }
71✔
256
    for (size_t i = 0; i < expr2.size(); i++) {
128✔
257
        auto dim = expr2[i];
71✔
258
        for (auto& iter : dimensions) {
185✔
259
            dim = symbolic::subs(dim, symbolic::symbol(iter), symbolic::symbol(iter + "_2"));
114✔
260
        }
261
        map_2 += language_extension.expression(dim);
71✔
262
        if (i < expr2.size() - 1) {
71✔
263
            map_2 += ", ";
14✔
264
        }
14✔
265
    }
71✔
266
    map_1 += "] ";
57✔
267
    map_2 += "] ";
57✔
268

269
    std::vector<std::string> constraints_1;
57✔
270
    // Add bounds
271
    for (auto& con : constraints_syms_1) {
397✔
272
        auto con_1 = con;
340✔
273
        for (auto& iter : dimensions) {
902✔
274
            con_1 = symbolic::subs(con_1, symbolic::symbol(iter), symbolic::symbol(iter + "_1"));
562✔
275
        }
276
        auto con_str_1 = constraint_to_isl_str(con_1);
340✔
277
        if (con_str_1.empty()) {
340✔
278
            continue;
43✔
279
        }
280
        constraints_1.push_back(con_str_1);
297✔
281
    }
340✔
282
    for (auto& dim : dimensions) {
127✔
283
        auto sym = symbolic::symbol(dim);
70✔
284
        auto map = assums1.at(sym).map();
70✔
285
        if (map == SymEngine::null) {
70✔
286
            continue;
2✔
287
        }
288
        if (!SymEngine::is_a<SymEngine::Add>(*map)) {
68✔
289
            continue;
×
290
        }
291
        auto args = SymEngine::rcp_static_cast<const SymEngine::Add>(map)->get_args();
68✔
292
        if (args.size() != 2) {
68✔
293
            continue;
×
294
        }
295
        auto arg0 = args[0];
68✔
296
        auto arg1 = args[1];
68✔
297
        if (!symbolic::eq(arg0, symbolic::symbol(dim))) {
68✔
298
            arg0 = args[1];
68✔
299
            arg1 = args[0];
68✔
300
        }
68✔
301
        if (!symbolic::eq(arg0, symbolic::symbol(dim))) {
68✔
302
            continue;
×
303
        }
304
        if (!SymEngine::is_a<SymEngine::Integer>(*arg1)) {
68✔
305
            continue;
×
306
        }
307
        if (symbolic::eq(arg1, symbolic::one())) {
68✔
308
            continue;
66✔
309
        }
310
        auto lb = assums2.at(sym).lower_bound_deprecated();
2✔
311
        if (!SymEngine::is_a<SymEngine::Integer>(*lb)) {
2✔
312
            continue;
×
313
        }
314

315
        std::string dim1 = dim + "_1";
2✔
316
        std::string iter = "__daisy_iterator_" + dim1;
2✔
317
        std::string con = "exists " + iter + " : " + dim1 + " = " + language_extension.expression(lb) + " + " + iter +
4✔
318
                          " * " + language_extension.expression(arg1);
2✔
319
        constraints_1.push_back(con);
2✔
320
    }
70✔
321
    if (!constraints_1.empty()) {
57✔
322
        map_1 += " : ";
52✔
323
        map_1 += helpers::join(constraints_1, " and ");
52✔
324
    }
52✔
325
    map_1 += " }";
57✔
326

327
    std::vector<std::string> constraints_2;
57✔
328
    for (auto& con : constraints_syms_2) {
400✔
329
        auto con_2 = con;
343✔
330
        for (auto& iter : dimensions) {
911✔
331
            con_2 = symbolic::subs(con_2, symbolic::symbol(iter), symbolic::symbol(iter + "_2"));
568✔
332
        }
333
        auto con_str_2 = constraint_to_isl_str(con_2);
343✔
334
        if (con_str_2.empty()) {
343✔
335
            continue;
45✔
336
        }
337
        constraints_2.push_back(con_str_2);
298✔
338
    }
343✔
339
    for (auto& dim : dimensions) {
127✔
340
        auto sym = symbolic::symbol(dim);
70✔
341
        auto map = assums2.at(sym).map();
70✔
342
        if (map == SymEngine::null) {
70✔
343
            continue;
1✔
344
        }
345
        if (!SymEngine::is_a<SymEngine::Add>(*map)) {
69✔
346
            continue;
×
347
        }
348
        auto args = SymEngine::rcp_static_cast<const SymEngine::Add>(map)->get_args();
69✔
349
        if (args.size() != 2) {
69✔
350
            continue;
×
351
        }
352
        auto arg0 = args[0];
69✔
353
        auto arg1 = args[1];
69✔
354
        if (!symbolic::eq(arg0, symbolic::symbol(dim))) {
69✔
355
            arg0 = args[1];
69✔
356
            arg1 = args[0];
69✔
357
        }
69✔
358
        if (!symbolic::eq(arg0, symbolic::symbol(dim))) {
69✔
359
            continue;
×
360
        }
361
        if (!SymEngine::is_a<SymEngine::Integer>(*arg1)) {
69✔
362
            continue;
×
363
        }
364
        if (symbolic::eq(arg1, symbolic::one())) {
69✔
365
            continue;
67✔
366
        }
367
        auto lb = assums2.at(sym).lower_bound_deprecated();
2✔
368
        if (!SymEngine::is_a<SymEngine::Integer>(*lb)) {
2✔
369
            continue;
×
370
        }
371

372
        std::string dim2 = dim + "_2";
2✔
373
        std::string iter = "__daisy_iterator_" + dim2;
2✔
374
        std::string con = "exists " + iter + " : " + dim2 + " = " + language_extension.expression(lb) + " + " + iter +
4✔
375
                          " * " + language_extension.expression(arg1);
2✔
376
        constraints_2.push_back(con);
2✔
377
    }
70✔
378
    if (!constraints_2.empty()) {
57✔
379
        map_2 += " : ";
52✔
380
        map_2 += helpers::join(constraints_2, " and ");
52✔
381
    }
52✔
382
    map_2 += " }";
57✔
383

384
    std::string map_3 = "{ [";
57✔
385
    for (size_t i = 0; i < dimensions.size(); i++) {
127✔
386
        map_3 += dimensions[i] + "_2";
70✔
387
        if (i < dimensions.size() - 1) {
70✔
388
            map_3 += ", ";
20✔
389
        }
20✔
390
    }
70✔
391
    map_3 += "] -> [";
57✔
392
    for (size_t i = 0; i < dimensions.size(); i++) {
127✔
393
        map_3 += dimensions[i] + "_1";
70✔
394
        if (i < dimensions.size() - 1) {
70✔
395
            map_3 += ", ";
20✔
396
        }
20✔
397
    }
70✔
398
    map_3 += "]";
57✔
399
    std::vector<std::string> monotonicity_constraints;
57✔
400
    if (dimensions_syms.find(indvar) != dimensions_syms.end()) {
57✔
401
        monotonicity_constraints.push_back(indvar->get_name() + "_1 != " + indvar->get_name() + "_2");
33✔
402
    }
33✔
403
    if (!monotonicity_constraints.empty()) {
57✔
404
        map_3 += " : ";
33✔
405
        map_3 += helpers::join(monotonicity_constraints, " and ");
33✔
406
    }
33✔
407
    map_3 += " }";
57✔
408

409
    map_1 = std::regex_replace(map_1, std::regex("\\."), "_");
57✔
410
    map_2 = std::regex_replace(map_2, std::regex("\\."), "_");
57✔
411
    map_3 = std::regex_replace(map_3, std::regex("\\."), "_");
57✔
412

413
    map_1 = std::regex_replace(map_1, std::regex("__daisy_min"), "min");
57✔
414
    map_1 = std::regex_replace(map_1, std::regex("__daisy_max"), "max");
57✔
415
    map_2 = std::regex_replace(map_2, std::regex("__daisy_min"), "min");
57✔
416
    map_2 = std::regex_replace(map_2, std::regex("__daisy_max"), "max");
57✔
417
    map_3 = std::regex_replace(map_3, std::regex("__daisy_min"), "min");
57✔
418
    map_3 = std::regex_replace(map_3, std::regex("__daisy_max"), "max");
57✔
419

420
    return {map_1, map_2, map_3};
57✔
421
}
57✔
422

423
ExpressionSet generate_constraints(SymbolSet& syms, const Assumptions& assums, SymbolSet& seen) {
961✔
424
    ExpressionSet constraints;
961✔
425
    for (auto& sym : syms) {
2,183✔
426
        if (assums.find(sym) == assums.end()) {
1,222✔
427
            continue;
8✔
428
        }
429
        if (seen.find(sym) != seen.end()) {
1,214✔
430
            continue;
880✔
431
        }
432
        seen.insert(sym);
334✔
433

434
        auto ub = assums.at(sym).upper_bound_deprecated();
334✔
435
        auto lb = assums.at(sym).lower_bound_deprecated();
334✔
436
        if (!symbolic::eq(ub, SymEngine::Inf)) {
334✔
437
            if (SymEngine::is_a<SymEngine::Min>(*ub)) {
255✔
438
                auto min = SymEngine::rcp_static_cast<const SymEngine::Min>(ub);
94✔
439
                auto args = min->get_args();
94✔
440
                for (auto& arg : args) {
294✔
441
                    auto con = symbolic::Le(sym, arg);
200✔
442
                    auto con_syms = symbolic::atoms(con);
200✔
443
                    constraints.insert(con);
200✔
444

445
                    auto con_cons = generate_constraints(con_syms, assums, seen);
200✔
446
                    constraints.insert(con_cons.begin(), con_cons.end());
200✔
447
                }
200✔
448
            } else {
94✔
449
                auto con = symbolic::Le(sym, ub);
161✔
450
                auto con_syms = symbolic::atoms(con);
161✔
451
                constraints.insert(con);
161✔
452

453
                auto con_cons = generate_constraints(con_syms, assums, seen);
161✔
454
                constraints.insert(con_cons.begin(), con_cons.end());
161✔
455
            }
161✔
456
        }
255✔
457
        if (!symbolic::eq(lb, SymEngine::NegInf)) {
334✔
458
            if (SymEngine::is_a<SymEngine::Max>(*lb)) {
330✔
459
                auto max = SymEngine::rcp_static_cast<const SymEngine::Max>(lb);
70✔
460
                auto args = max->get_args();
70✔
461
                for (auto& arg : args) {
210✔
462
                    auto con = symbolic::Ge(sym, arg);
140✔
463
                    auto con_syms = symbolic::atoms(con);
140✔
464
                    constraints.insert(con);
140✔
465

466
                    auto con_cons = generate_constraints(con_syms, assums, seen);
140✔
467
                    constraints.insert(con_cons.begin(), con_cons.end());
140✔
468
                }
140✔
469
            } else {
70✔
470
                auto con = symbolic::Ge(sym, lb);
260✔
471
                auto con_syms = symbolic::atoms(con);
260✔
472
                constraints.insert(con);
260✔
473

474
                auto con_cons = generate_constraints(con_syms, assums, seen);
260✔
475
                constraints.insert(con_cons.begin(), con_cons.end());
260✔
476
            }
260✔
477
        }
330✔
478
    }
334✔
479
    return constraints;
961✔
480
}
961✔
481

482
std::string constraint_to_isl_str(const Expression con) {
755✔
483
    builder::SDFGBuilder builder("sdfg", FunctionType_CPU);
755✔
484
    codegen::CLanguageExtension language_extension(builder.subject());
755✔
485

486
    if (SymEngine::is_a<SymEngine::StrictLessThan>(*con)) {
755✔
487
        auto le = SymEngine::rcp_static_cast<const SymEngine::StrictLessThan>(con);
×
488
        auto lhs = le->get_arg1();
×
489
        auto rhs = le->get_arg2();
×
490
        if (SymEngine::is_a<SymEngine::Infty>(*lhs) || SymEngine::is_a<SymEngine::Infty>(*rhs)) {
×
491
            return "";
×
492
        }
493
        auto res = language_extension.expression(lhs) + " < " + language_extension.expression(rhs);
×
494
        res = std::regex_replace(res, std::regex("\\."), "_");
×
495
        res = std::regex_replace(res, std::regex("__daisy_min"), "min");
×
496
        res = std::regex_replace(res, std::regex("__daisy_max"), "max");
×
497
        return res;
×
498
    } else if (SymEngine::is_a<SymEngine::LessThan>(*con)) {
755✔
499
        auto le = SymEngine::rcp_static_cast<const SymEngine::LessThan>(con);
753✔
500
        auto lhs = le->get_arg1();
753✔
501
        auto rhs = le->get_arg2();
753✔
502
        if (SymEngine::is_a<SymEngine::Infty>(*lhs) || SymEngine::is_a<SymEngine::Infty>(*rhs)) {
753✔
503
            return "";
92✔
504
        }
505
        auto res = language_extension.expression(lhs) + " <= " + language_extension.expression(rhs);
661✔
506
        res = std::regex_replace(res, std::regex("\\."), "_");
661✔
507
        res = std::regex_replace(res, std::regex("__daisy_min"), "min");
661✔
508
        res = std::regex_replace(res, std::regex("__daisy_max"), "max");
661✔
509
        return res;
661✔
510
    } else if (SymEngine::is_a<SymEngine::Equality>(*con)) {
1,416✔
511
        auto eq = SymEngine::rcp_static_cast<const SymEngine::Equality>(con);
×
512
        auto lhs = eq->get_arg1();
×
513
        auto rhs = eq->get_arg2();
×
514
        if (SymEngine::is_a<SymEngine::Infty>(*lhs) || SymEngine::is_a<SymEngine::Infty>(*rhs)) {
×
515
            return "";
×
516
        }
517
        auto res = language_extension.expression(lhs) + " == " + language_extension.expression(rhs);
×
518
        res = std::regex_replace(res, std::regex("\\."), "_");
×
519
        res = std::regex_replace(res, std::regex("__daisy_min"), "min");
×
520
        res = std::regex_replace(res, std::regex("__daisy_max"), "max");
×
521
        return res;
×
522
    } else if (SymEngine::is_a<SymEngine::Unequality>(*con)) {
2✔
523
        auto ne = SymEngine::rcp_static_cast<const SymEngine::Unequality>(con);
×
524
        auto lhs = ne->get_arg1();
×
525
        auto rhs = ne->get_arg2();
×
526
        if (SymEngine::is_a<SymEngine::Infty>(*lhs) || SymEngine::is_a<SymEngine::Infty>(*rhs)) {
×
527
            return "";
×
528
        }
529
        auto res = language_extension.expression(lhs) + " != " + language_extension.expression(rhs);
×
530
        res = std::regex_replace(res, std::regex("\\."), "_");
×
531
        res = std::regex_replace(res, std::regex("__daisy_min"), "min");
×
532
        res = std::regex_replace(res, std::regex("__daisy_max"), "max");
×
533
        return res;
×
534
    }
×
535

536
    return "";
2✔
537
}
755✔
538

539
void canonicalize_map_dims(isl_map* map, const std::string& in_prefix, const std::string& out_prefix) {
86✔
540
    int n_in = isl_map_dim(map, isl_dim_in);
86✔
541
    int n_out = isl_map_dim(map, isl_dim_out);
86✔
542

543
    for (int i = 0; i < n_in; ++i) {
110✔
544
        std::string name = in_prefix + std::to_string(i);
24✔
545
        map = isl_map_set_dim_name(map, isl_dim_in, i, name.c_str());
24✔
546
    }
24✔
547

548
    for (int i = 0; i < n_out; ++i) {
172✔
549
        std::string name = out_prefix + std::to_string(i);
86✔
550
        map = isl_map_set_dim_name(map, isl_dim_out, i, name.c_str());
86✔
551
    }
86✔
552
}
86✔
553

554
MultiExpression delinearize(const MultiExpression& expr, const Assumptions& assums) {
164✔
555
    MultiExpression delinearized;
164✔
556
    for (auto& dim : expr) {
340✔
557
        // Check if more than two symbols are involved
558
        SymbolVec symbols;
176✔
559
        for (auto& sym : atoms(dim)) {
388✔
560
            if (!assums.at(sym).constant() || !assums.at(sym).map().is_null()) {
212✔
561
                symbols.push_back(sym);
154✔
562
            }
154✔
563
        }
564
        if (symbols.size() < 1) {
176✔
565
            delinearized.push_back(dim);
72✔
566
            continue;
72✔
567
        }
568

569
        // Step 1: Get polynomial form and affine coefficients
570
        auto poly = polynomial(dim, symbols);
104✔
571
        if (poly == SymEngine::null) {
104✔
572
            delinearized.push_back(dim);
×
573
            continue;
×
574
        }
575
        auto aff_coeffs = affine_coefficients(poly, symbols);
104✔
576
        if (aff_coeffs.empty()) {
104✔
577
            delinearized.push_back(dim);
×
578
            continue;
×
579
        }
580
        auto offset = aff_coeffs.at(symbolic::symbol("__daisy_constant__"));
104✔
581
        aff_coeffs.erase(symbolic::symbol("__daisy_constant__"));
104✔
582

583
        // Step 2: Peel-off dimensions
584
        bool success = true;
104✔
585
        Expression remaining = symbolic::sub(dim, offset);
104✔
586
        std::vector<Expression> peeled_dims;
104✔
587
        while (!aff_coeffs.empty()) {
234✔
588
            // Find the symbol with largest stride (= largest atom count)
589
            Symbol new_dim = SymEngine::null;
152✔
590
            size_t max_atom_count = 0;
152✔
591
            for (const auto& [sym, coeff] : aff_coeffs) {
603✔
592
                size_t atom_count = symbolic::atoms(coeff).size();
248✔
593
                if (atom_count > max_atom_count || new_dim.is_null()) {
248✔
594
                    max_atom_count = atom_count;
203✔
595
                    new_dim = sym;
203✔
596
                }
203✔
597
            }
598
            if (new_dim.is_null()) {
152✔
599
                break;
×
600
            }
601

602
            // Symbol must be nonnegative
603
            auto sym_lb = minimum(new_dim, {}, assums);
152✔
604
            if (sym_lb.is_null()) {
152✔
605
                break;
2✔
606
            }
607
            auto sym_cond = symbolic::Ge(sym_lb, symbolic::zero());
150✔
608
            if (!symbolic::is_true(sym_cond)) {
150✔
609
                break;
17✔
610
            }
611

612
            // Stride must be positive
613
            Expression stride = aff_coeffs.at(new_dim);
133✔
614
            auto stride_lb = minimum(stride, {}, assums);
133✔
615
            if (stride_lb.is_null()) {
133✔
616
                break;
×
617
            }
618
            auto stride_cond = symbolic::Ge(stride_lb, symbolic::one());
133✔
619
            if (!symbolic::is_true(stride_cond)) {
133✔
620
                break;
3✔
621
            }
622

623
            // Peel off the dimension
624
            remaining = symbolic::sub(remaining, symbolic::mul(stride, new_dim));
130✔
625
            remaining = symbolic::expand(remaining);
130✔
626
            remaining = symbolic::simplify(remaining);
130✔
627

628
            // Check if remainder is within bounds
629

630
            // remaining must be nonnegative
631
            auto rem_lb = minimum(remaining, {}, assums);
130✔
632
            if (rem_lb.is_null()) {
130✔
633
                break;
×
634
            }
635
            auto cond_zero = symbolic::Ge(rem_lb, symbolic::zero());
130✔
636
            if (!symbolic::is_true(cond_zero)) {
130✔
UNCOV
637
                break;
×
638
            }
639

640
            // remaining must be less than stride
641
            auto ub_stride = maximum(stride, {}, assums);
130✔
642
            auto ub_remaining = maximum(remaining, {}, assums);
130✔
643
            auto cond_stride = symbolic::Ge(ub_stride, ub_remaining);
130✔
644
            if (!symbolic::is_true(cond_stride)) {
130✔
645
                break;
×
646
            }
647

648
            // Add offset contribution of peeled dimension
649
            auto [q, r] = polynomial_div(offset, stride);
260✔
650
            offset = r;
130✔
651
            auto final_dim = symbolic::add(new_dim, q);
130✔
652

653
            peeled_dims.push_back(final_dim);
130✔
654
            aff_coeffs.erase(new_dim);
130✔
655
        }
152✔
656
        // Not all dimensions could be peeled off
657
        if (!aff_coeffs.empty()) {
104✔
658
            delinearized.push_back(dim);
22✔
659
            continue;
22✔
660
        }
661
        // Offset did not reduce to zero
662
        if (!symbolic::eq(offset, symbolic::zero())) {
82✔
663
            delinearized.push_back(dim);
×
664
            continue;
×
665
        }
666

667
        // Success
668
        for (auto& peeled_dim : peeled_dims) {
212✔
669
            delinearized.push_back(peeled_dim);
130✔
670
        }
671
    }
176✔
672

673
    return delinearized;
164✔
674
}
164✔
675

676
} // namespace symbolic
677
} // namespace sdfg
STATUS · Troubleshooting · Open an Issue · Sales · Support · CAREERS · ENTERPRISE · START FREE · SCHEDULE DEMO
ANNOUNCEMENTS · TWITTER · TOS & SLA · Supported CI Services · What's a CI service? · Automated Testing

© 2026 Coveralls, Inc