20009964405

Committed 07 Dec 2025 08:34PM UTC coverage: 61.622% (-0.02%) from 61.641%

Build # 20009964405

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #377 from daisytuner/delinearization

improves delinearization utils

Run Details

45 of 66 new or added lines in 2 files covered. (68.18%)

7 existing lines in 1 file now uncovered.

11299 of 18336 relevant lines covered (61.62%)

117.38 hits per line

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

69.61

/src/symbolic/maps.cpp

#include "sdfg/symbolic/maps.h"

#include <isl/ctx.h>
#include <isl/options.h>
#include <isl/set.h>
#include <isl/space.h>

#include "sdfg/symbolic/extreme_values.h"
#include "sdfg/symbolic/polynomials.h"
#include "sdfg/symbolic/utils.h"

namespace sdfg {
namespace symbolic {
namespace maps {

bool is_monotonic_affine(const Expression expr, const Symbol sym, const Assumptions& assums) {
    SymbolVec symbols = {sym};
    auto poly = polynomial(expr, symbols);
    if (poly == SymEngine::null) {
        return false;
    }
    auto coeffs = affine_coefficients(poly, symbols);
    if (coeffs.empty()) {
        return false;
    }
    auto mul = minimum(coeffs[sym], {}, assums);
    if (mul == SymEngine::null) {
        return false;
    }
    if (!SymEngine::is_a<SymEngine::Integer>(*mul)) {
        return false;
    }
    auto mul_int = SymEngine::rcp_dynamic_cast<const SymEngine::Integer>(mul);
    if (mul_int->as_int() <= 0) {
        return false;
    }

    return true;
}

bool is_monotonic_pow(const Expression expr, const Symbol sym, const Assumptions& assums) {
    if (SymEngine::is_a<SymEngine::Pow>(*expr)) {
        auto pow = SymEngine::rcp_dynamic_cast<const SymEngine::Pow>(expr);
        auto base = pow->get_base();
        auto exp = pow->get_exp();
        if (SymEngine::is_a<SymEngine::Integer>(*exp) && SymEngine::is_a<SymEngine::Symbol>(*base)) {
            auto exp_int = SymEngine::rcp_dynamic_cast<const SymEngine::Integer>(exp);
            if (exp_int->as_int() <= 0) {
                return false;
            }
            auto base_sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(base);
            auto ub_sym = minimum(base_sym, {}, assums);
            if (ub_sym == SymEngine::null) {
                return false;
            }
            auto positive = symbolic::Ge(ub_sym, symbolic::integer(0));
            return symbolic::is_true(positive);
        }
    }

    return false;
}

bool is_monotonic(const Expression expr, const Symbol sym, const Assumptions& assums) {
    if (is_monotonic_affine(expr, sym, assums)) {
        return true;
    }
    return is_monotonic_pow(expr, sym, assums);
}

bool is_disjoint_isl(
    const MultiExpression& expr1,
    const MultiExpression& expr2,
    const Symbol indvar,
    const Assumptions& assums1,
    const Assumptions& assums2
) {
    if (expr1.size() != expr2.size()) {
        return false;
    }
    if (expr1.empty()) {
        return false;
    }

    // Transform both expressions into two maps with separate dimensions
    auto expr1_delinearized = delinearize(expr1, assums1);
    auto expr2_delinearized = delinearize(expr2, assums2);
    if (expr1_delinearized.size() != expr2_delinearized.size()) {
        return false;
    }

    // Cheap per-dimension check
    for (size_t i = 0; i < expr1_delinearized.size(); i++) {
        auto& dim1 = expr1_delinearized[i];
        auto& dim2 = expr2_delinearized[i];
        auto maps = expressions_to_intersection_map_str({dim1}, {dim2}, indvar, assums1, assums2);

        isl_ctx* ctx = isl_ctx_alloc();
        isl_options_set_on_error(ctx, ISL_ON_ERROR_CONTINUE);

        isl_map* map_1 = isl_map_read_from_str(ctx, std::get<0>(maps).c_str());
        isl_map* map_2 = isl_map_read_from_str(ctx, std::get<1>(maps).c_str());
        isl_map* map_3 = isl_map_read_from_str(ctx, std::get<2>(maps).c_str());
        if (!map_1 || !map_2 || !map_3) {
            if (map_1) {
                isl_map_free(map_1);
            }
            if (map_2) {
                isl_map_free(map_2);
            }
            if (map_3) {
                isl_map_free(map_3);
            }
            isl_ctx_free(ctx);
            return false;
        }

        // Find aliasing pairs under the constraint that dimensions are different

        isl_map* composed = isl_map_apply_domain(map_2, map_3);
        if (!composed) {
            isl_map_free(map_1);
            if (map_2) {
                isl_map_free(map_2);
            }
            if (map_3) {
                isl_map_free(map_3);
            }
            isl_ctx_free(ctx);
            return false;
        }
        isl_map* alias_pairs = isl_map_intersect(composed, map_1);
        if (!alias_pairs) {
            if (composed) {
                isl_map_free(composed);
            }
            if (map_1) {
                isl_map_free(map_1);
            }
            isl_ctx_free(ctx);
            return false;
        }

        bool disjoint = isl_map_is_empty(alias_pairs);
        isl_map_free(alias_pairs);
        isl_ctx_free(ctx);
        if (disjoint) {
            return true;
        }
    }
    if (expr1_delinearized.size() == 1) {
        return false;
    }

    // Now check on all dimensions together
    auto maps = expressions_to_intersection_map_str(expr1_delinearized, expr2_delinearized, indvar, assums1, assums2);

    isl_ctx* ctx = isl_ctx_alloc();
    isl_options_set_on_error(ctx, ISL_ON_ERROR_CONTINUE);

    isl_map* map_1 = isl_map_read_from_str(ctx, std::get<0>(maps).c_str());
    isl_map* map_2 = isl_map_read_from_str(ctx, std::get<1>(maps).c_str());
    isl_map* map_3 = isl_map_read_from_str(ctx, std::get<2>(maps).c_str());
    if (!map_1 || !map_2 || !map_3) {
        if (map_1) {
            isl_map_free(map_1);
        }
        if (map_2) {
            isl_map_free(map_2);
        }
        if (map_3) {
            isl_map_free(map_3);
        }
        isl_ctx_free(ctx);
        return false;
    }

    // Find aliasing pairs under the constraint that dimensions are different

    isl_map* composed = isl_map_apply_domain(map_2, map_3);
    if (!composed) {
        isl_map_free(map_1);
        if (map_2) {
            isl_map_free(map_2);
        }
        if (map_3) {
            isl_map_free(map_3);
        }
        isl_ctx_free(ctx);
        return false;
    }
    isl_map* alias_pairs = isl_map_intersect(composed, map_1);
    if (!alias_pairs) {
        if (composed) {
            isl_map_free(composed);
        }
        if (map_1) {
            isl_map_free(map_1);
        }
        isl_ctx_free(ctx);
        return false;
    }

    bool disjoint = isl_map_is_empty(alias_pairs);
    isl_map_free(alias_pairs);
    isl_ctx_free(ctx);

    return disjoint;
}

bool is_disjoint_monotonic(
    const MultiExpression& expr1,
    const MultiExpression& expr2,
    const Symbol indvar,
    const Assumptions& assums1,
    const Assumptions& assums2
) {
    // TODO: Handle assumptions1 and assumptions2

    for (size_t i = 0; i < expr1.size(); i++) {
        auto& dim1 = expr1[i];
        if (expr2.size() <= i) {
            continue;
        }
        auto& dim2 = expr2[i];
        if (!symbolic::eq(dim1, dim2)) {
            continue;
        }

        // Collect all symbols
        symbolic::SymbolSet syms;
        for (auto& sym : symbolic::atoms(dim1)) {
            syms.insert(sym);
        }

        // Collect all non-constant symbols
        bool can_analyze = true;
        for (auto& sym : syms) {
            if (!assums1.at(sym).constant()) {
                if (sym->get_name() != indvar->get_name()) {
                    can_analyze = false;
                    break;
                }
            }
        }
        if (!can_analyze) {
            continue;
        }

        // Check if both dimensions are monotonic in non-constant symbols
        if (is_monotonic(dim1, indvar, assums1)) {
            return true;
        }
    }

    return false;
}

bool is_disjoint_interval(
    const MultiExpression& expr1,
    const MultiExpression& expr2,
    const Symbol indvar,
    const Assumptions& assums1,
    const Assumptions& assums2
) {
    for (size_t i = 0; i < expr1.size(); i++) {
        auto& dim1 = expr1[i];
        if (expr2.size() <= i) {
            continue;
        }
        auto& dim2 = expr2[i];

        auto lb1 = minimum(dim1, {}, assums1);
        if (lb1 == SymEngine::null || SymEngine::is_a<SymEngine::NaN>(*lb1)) {
            continue;
        }
        auto ub1 = maximum(dim1, {}, assums1);
        if (ub1 == SymEngine::null || SymEngine::is_a<SymEngine::NaN>(*ub1)) {
            continue;
        }
        auto lb2 = minimum(dim2, {}, assums2);
        if (lb2 == SymEngine::null || SymEngine::is_a<SymEngine::NaN>(*lb2)) {
            continue;
        }
        auto ub2 = maximum(dim2, {}, assums2);
        if (ub2 == SymEngine::null || SymEngine::is_a<SymEngine::NaN>(*ub2)) {
            continue;
        }

        auto dis1 = symbolic::Gt(lb1, ub2);
        auto dis2 = symbolic::Gt(lb2, ub1);
        if (symbolic::is_true(dis1) || symbolic::is_true(dis2)) {
            return true;
        }
    }

    return false;
}

bool intersects(
    const MultiExpression& expr1,
    const MultiExpression& expr2,
    const Symbol indvar,
    const Assumptions& assums1,
    const Assumptions& assums2
) {
    if (is_disjoint_interval(expr1, expr2, indvar, assums1, assums2)) {
        return false;
    }
    if (is_disjoint_monotonic(expr1, expr2, indvar, assums1, assums2)) {
        return false;
    }
    if (is_disjoint_isl(expr1, expr2, indvar, assums1, assums2)) {
        return false;
    }
    return true;
}

} // namespace maps
} // namespace symbolic
} // namespace sdfg

1	#include "sdfg/symbolic/maps.h"
2
3	#include <isl/ctx.h>
4	#include <isl/options.h>
5	#include <isl/set.h>
6	#include <isl/space.h>
7
8	#include "sdfg/symbolic/extreme_values.h"
9	#include "sdfg/symbolic/polynomials.h"
10	#include "sdfg/symbolic/utils.h"
11
12	namespace sdfg {
13	namespace symbolic {
14	namespace maps {
15
16	bool is_monotonic_affine(const Expression expr, const Symbol sym, const Assumptions& assums) {	65✔
17	SymbolVec symbols = {sym};	65✔
18	auto poly = polynomial(expr, symbols);	65✔
19	if (poly == SymEngine::null) {	65✔
20	return false;	×
21	}
22	auto coeffs = affine_coefficients(poly, symbols);	65✔
23	if (coeffs.empty()) {	65✔
24	return false;	1✔
25	}
26	auto mul = minimum(coeffs[sym], {}, assums);	64✔
27	if (mul == SymEngine::null) {	64✔
28	return false;	×
29	}
30	if (!SymEngine::is_a<SymEngine::Integer>(*mul)) {	64✔
31	return false;	×
32	}
33	auto mul_int = SymEngine::rcp_dynamic_cast<const SymEngine::Integer>(mul);	64✔
34	if (mul_int->as_int() <= 0) {	64✔
35	return false;	11✔
36	}
37
38	return true;	53✔
39	}	65✔
40
41	bool is_monotonic_pow(const Expression expr, const Symbol sym, const Assumptions& assums) {	12✔
42	if (SymEngine::is_a<SymEngine::Pow>(*expr)) {	12✔
43	auto pow = SymEngine::rcp_dynamic_cast<const SymEngine::Pow>(expr);	1✔
44	auto base = pow->get_base();	1✔
45	auto exp = pow->get_exp();	1✔
46	if (SymEngine::is_a<SymEngine::Integer>(exp) && SymEngine::is_a<SymEngine::Symbol>(base)) {	1✔
47	auto exp_int = SymEngine::rcp_dynamic_cast<const SymEngine::Integer>(exp);	1✔
48	if (exp_int->as_int() <= 0) {	1✔
49	return false;	×
50	}
51	auto base_sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(base);	1✔
52	auto ub_sym = minimum(base_sym, {}, assums);	1✔
53	if (ub_sym == SymEngine::null) {	1✔
54	return false;	×
55	}
56	auto positive = symbolic::Ge(ub_sym, symbolic::integer(0));	1✔
57	return symbolic::is_true(positive);	1✔
58	}	1✔
59	}	1✔
60
61	return false;	11✔
62	}	12✔
63
64	bool is_monotonic(const Expression expr, const Symbol sym, const Assumptions& assums) {	65✔
65	if (is_monotonic_affine(expr, sym, assums)) {	65✔
66	return true;	53✔
67	}
68	return is_monotonic_pow(expr, sym, assums);	12✔
69	}	65✔
70
71	bool is_disjoint_isl(	69✔
72	const MultiExpression& expr1,
73	const MultiExpression& expr2,
74	const Symbol indvar,
75	const Assumptions& assums1,
76	const Assumptions& assums2
77	) {
78	if (expr1.size() != expr2.size()) {	69✔
79	return false;	×
80	}
81	if (expr1.empty()) {	69✔
82	return false;	×
83	}
84
85	// Transform both expressions into two maps with separate dimensions
86	auto expr1_delinearized = delinearize(expr1, assums1);	69✔
87	auto expr2_delinearized = delinearize(expr2, assums2);	69✔
88	if (expr1_delinearized.size() != expr2_delinearized.size()) {	69✔
89	return false;	12✔
90	}
91
92	// Cheap per-dimension check
93	for (size_t i = 0; i < expr1_delinearized.size(); i++) {	97✔
94	auto& dim1 = expr1_delinearized[i];	76✔
95	auto& dim2 = expr2_delinearized[i];	76✔
96	auto maps = expressions_to_intersection_map_str({dim1}, {dim2}, indvar, assums1, assums2);	76✔
97
98	isl_ctx* ctx = isl_ctx_alloc();	76✔
99	isl_options_set_on_error(ctx, ISL_ON_ERROR_CONTINUE);	76✔
100
101	isl_map* map_1 = isl_map_read_from_str(ctx, std::get<0>(maps).c_str());	76✔
102	isl_map* map_2 = isl_map_read_from_str(ctx, std::get<1>(maps).c_str());	76✔
103	isl_map* map_3 = isl_map_read_from_str(ctx, std::get<2>(maps).c_str());	76✔
104	if (!map_1 \|\| !map_2 \|\| !map_3) {	76✔
105	if (map_1) {	16✔
NEW 106	isl_map_free(map_1);	×
NEW 107	}	×
108	if (map_2) {	16✔
NEW 109	isl_map_free(map_2);	×
NEW 110	}	×
111	if (map_3) {	16✔
112	isl_map_free(map_3);	16✔
113	}	16✔
114	isl_ctx_free(ctx);	16✔
115	return false;	16✔
116	}
117
118	// Find aliasing pairs under the constraint that dimensions are different
119
120	isl_map* composed = isl_map_apply_domain(map_2, map_3);	60✔
121	if (!composed) {	60✔
NEW 122	isl_map_free(map_1);	×
NEW 123	if (map_2) {	×
NEW 124	isl_map_free(map_2);	×
NEW 125	}	×
NEW 126	if (map_3) {	×
NEW 127	isl_map_free(map_3);	×
NEW 128	}	×
NEW 129	isl_ctx_free(ctx);	×
NEW 130	return false;	×
131	}
132	isl_map* alias_pairs = isl_map_intersect(composed, map_1);	60✔
133	if (!alias_pairs) {	60✔
NEW 134	if (composed) {	×
NEW 135	isl_map_free(composed);	×
NEW 136	}	×
NEW 137	if (map_1) {	×
NEW 138	isl_map_free(map_1);	×
NEW 139	}	×
NEW 140	isl_ctx_free(ctx);	×
NEW 141	return false;	×
142	}
143
144	bool disjoint = isl_map_is_empty(alias_pairs);	60✔
145	isl_map_free(alias_pairs);	60✔
146	isl_ctx_free(ctx);	60✔
147	if (disjoint) {	60✔
148	return true;	20✔
149	}
150	}	76✔
151	if (expr1_delinearized.size() == 1) {	21✔
152	return false;	13✔
153	}
154
155	// Now check on all dimensions together
156	auto maps = expressions_to_intersection_map_str(expr1_delinearized, expr2_delinearized, indvar, assums1, assums2);	8✔
157
158	isl_ctx* ctx = isl_ctx_alloc();	8✔
159	isl_options_set_on_error(ctx, ISL_ON_ERROR_CONTINUE);	8✔
160
161	isl_map* map_1 = isl_map_read_from_str(ctx, std::get<0>(maps).c_str());	8✔
162	isl_map* map_2 = isl_map_read_from_str(ctx, std::get<1>(maps).c_str());	8✔
163	isl_map* map_3 = isl_map_read_from_str(ctx, std::get<2>(maps).c_str());	8✔
164	if (!map_1 \|\| !map_2 \|\| !map_3) {	8✔
UNCOV 165	if (map_1) {	×
166	isl_map_free(map_1);	×
167	}	×
UNCOV 168	if (map_2) {	×
169	isl_map_free(map_2);	×
170	}	×
UNCOV 171	if (map_3) {	×
UNCOV 172	isl_map_free(map_3);	×
UNCOV 173	}	×
UNCOV 174	isl_ctx_free(ctx);	×
UNCOV 175	return false;	×
176	}
177
178	// Find aliasing pairs under the constraint that dimensions are different
179
180	isl_map* composed = isl_map_apply_domain(map_2, map_3);	8✔
181	if (!composed) {	8✔
182	isl_map_free(map_1);	×
183	if (map_2) {	×
184	isl_map_free(map_2);	×
185	}	×
186	if (map_3) {	×
187	isl_map_free(map_3);	×
188	}	×
189	isl_ctx_free(ctx);	×
190	return false;	×
191	}
192	isl_map* alias_pairs = isl_map_intersect(composed, map_1);	8✔
193	if (!alias_pairs) {	8✔
194	if (composed) {	×
195	isl_map_free(composed);	×
196	}	×
197	if (map_1) {	×
198	isl_map_free(map_1);	×
199	}	×
200	isl_ctx_free(ctx);	×
201	return false;	×
202	}
203
204	bool disjoint = isl_map_is_empty(alias_pairs);	8✔
205	isl_map_free(alias_pairs);	8✔
206	isl_ctx_free(ctx);	8✔
207
208	return disjoint;	8✔
209	}	69✔
210
211	bool is_disjoint_monotonic(	123✔
212	const MultiExpression& expr1,
213	const MultiExpression& expr2,
214	const Symbol indvar,
215	const Assumptions& assums1,
216	const Assumptions& assums2
217	) {
218	// TODO: Handle assumptions1 and assumptions2
219
220	for (size_t i = 0; i < expr1.size(); i++) {	203✔
221	auto& dim1 = expr1[i];	134✔
222	if (expr2.size() <= i) {	134✔
223	continue;	×
224	}
225	auto& dim2 = expr2[i];	134✔
226	if (!symbolic::eq(dim1, dim2)) {	134✔
227	continue;	54✔
228	}
229
230	// Collect all symbols
231	symbolic::SymbolSet syms;	80✔
232	for (auto& sym : symbolic::atoms(dim1)) {	189✔
233	syms.insert(sym);	109✔
234	}
235
236	// Collect all non-constant symbols
237	bool can_analyze = true;	80✔
238	for (auto& sym : syms) {	170✔
239	if (!assums1.at(sym).constant()) {	105✔
240	if (sym->get_name() != indvar->get_name()) {	15✔
241	can_analyze = false;	15✔
242	break;	15✔
243	}
244	}	×
245	}
246	if (!can_analyze) {	80✔
247	continue;	15✔
248	}
249
250	// Check if both dimensions are monotonic in non-constant symbols
251	if (is_monotonic(dim1, indvar, assums1)) {	65✔
252	return true;	54✔
253	}
254	}	80✔
255
256	return false;	69✔
257	}	123✔
258
259	bool is_disjoint_interval(	126✔
260	const MultiExpression& expr1,
261	const MultiExpression& expr2,
262	const Symbol indvar,
263	const Assumptions& assums1,
264	const Assumptions& assums2
265	) {
266	for (size_t i = 0; i < expr1.size(); i++) {	266✔
267	auto& dim1 = expr1[i];	143✔
268	if (expr2.size() <= i) {	143✔
269	continue;	×
270	}
271	auto& dim2 = expr2[i];	143✔
272
273	auto lb1 = minimum(dim1, {}, assums1);	143✔
274	if (lb1 == SymEngine::null \|\| SymEngine::is_a<SymEngine::NaN>(*lb1)) {	143✔
275	continue;	1✔
276	}
277	auto ub1 = maximum(dim1, {}, assums1);	142✔
278	if (ub1 == SymEngine::null \|\| SymEngine::is_a<SymEngine::NaN>(*ub1)) {	142✔
279	continue;	×
280	}
281	auto lb2 = minimum(dim2, {}, assums2);	142✔
282	if (lb2 == SymEngine::null \|\| SymEngine::is_a<SymEngine::NaN>(*lb2)) {	142✔
283	continue;	×
284	}
285	auto ub2 = maximum(dim2, {}, assums2);	142✔
286	if (ub2 == SymEngine::null \|\| SymEngine::is_a<SymEngine::NaN>(*ub2)) {	142✔
287	continue;	×
288	}
289
290	auto dis1 = symbolic::Gt(lb1, ub2);	142✔
291	auto dis2 = symbolic::Gt(lb2, ub1);	142✔
292	if (symbolic::is_true(dis1) \|\| symbolic::is_true(dis2)) {	142✔
293	return true;	3✔
294	}
295	}	143✔
296
297	return false;	123✔
298	}	126✔
299
300	bool intersects(	126✔
301	const MultiExpression& expr1,
302	const MultiExpression& expr2,
303	const Symbol indvar,
304	const Assumptions& assums1,
305	const Assumptions& assums2
306	) {
307	if (is_disjoint_interval(expr1, expr2, indvar, assums1, assums2)) {	126✔
308	return false;	3✔
309	}
310	if (is_disjoint_monotonic(expr1, expr2, indvar, assums1, assums2)) {	123✔
311	return false;	54✔
312	}
313	if (is_disjoint_isl(expr1, expr2, indvar, assums1, assums2)) {	69✔
314	return false;	25✔
315	}
316	return true;	44✔
317	}	126✔
318
319	} // namespace maps
320	} // namespace symbolic
321	} // namespace sdfg

daisytuner / sdfglib / 20009964405

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

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