20026333216

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

Build # 20026333216

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #381 from daisytuner/assumptions-constants

Sets constant assumptions for read-only symbols in loop bodies

Run Details

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

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) {	60✔
17	SymbolVec symbols = {sym};	60✔
18	auto poly = polynomial(expr, symbols);	60✔
19	if (poly == SymEngine::null) {	60✔
20	return false;	×
21	}
22	auto coeffs = affine_coefficients(poly, symbols);	60✔
23	if (coeffs.empty()) {	60✔
24	return false;	1✔
25	}
26	auto mul = minimum(coeffs[sym], {}, assums);	59✔
27	if (mul == SymEngine::null) {	59✔
28	return false;	×
29	}
30	if (!SymEngine::is_a<SymEngine::Integer>(*mul)) {	59✔
31	return false;	1✔
32	}
33	auto mul_int = SymEngine::rcp_dynamic_cast<const SymEngine::Integer>(mul);	58✔
34	if (mul_int->as_int() <= 0) {	58✔
35	return false;	9✔
36	}
37
38	return true;	49✔
39	}	60✔
40
41	bool is_monotonic_pow(const Expression expr, const Symbol sym, const Assumptions& assums) {	11✔
42	if (SymEngine::is_a<SymEngine::Pow>(*expr)) {	11✔
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;	10✔
62	}	11✔
63
64	bool is_monotonic(const Expression expr, const Symbol sym, const Assumptions& assums) {	60✔
65	if (is_monotonic_affine(expr, sym, assums)) {	60✔
66	return true;	49✔
67	}
68	return is_monotonic_pow(expr, sym, assums);	11✔
69	}	60✔
70
71	bool is_disjoint_isl(	35✔
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()) {	35✔
79	return false;	×
80	}
81	if (expr1.empty()) {	35✔
82	return false;	×
83	}
84
85	// Transform both expressions into two maps with separate dimensions
86	auto expr1_delinearized = delinearize(expr1, assums1);	35✔
87	auto expr2_delinearized = delinearize(expr2, assums2);	35✔
88	if (expr1_delinearized.size() != expr2_delinearized.size()) {	35✔
UNCOV 89	return false;	×
90	}
91
92	// Cheap per-dimension check
93	for (size_t i = 0; i < expr1_delinearized.size(); i++) {	70✔
94	auto& dim1 = expr1_delinearized[i];	49✔
95	auto& dim2 = expr2_delinearized[i];	49✔
96	auto maps = expressions_to_intersection_map_str({dim1}, {dim2}, indvar, assums1, assums2);	49✔
97
98	isl_ctx* ctx = isl_ctx_alloc();	49✔
99	isl_options_set_on_error(ctx, ISL_ON_ERROR_CONTINUE);	49✔
100
101	isl_map* map_1 = isl_map_read_from_str(ctx, std::get<0>(maps).c_str());	49✔
102	isl_map* map_2 = isl_map_read_from_str(ctx, std::get<1>(maps).c_str());	49✔
103	isl_map* map_3 = isl_map_read_from_str(ctx, std::get<2>(maps).c_str());	49✔
104	if (!map_1 \|\| !map_2 \|\| !map_3) {	49✔
105	if (map_1) {	1✔
106	isl_map_free(map_1);	×
107	}	×
108	if (map_2) {	1✔
109	isl_map_free(map_2);	×
110	}	×
111	if (map_3) {	1✔
112	isl_map_free(map_3);	1✔
113	}	1✔
114	isl_ctx_free(ctx);	1✔
115	return false;	1✔
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);	48✔
121	if (!composed) {	48✔
122	isl_map_free(map_1);	×
123	if (map_2) {	×
124	isl_map_free(map_2);	×
125	}	×
126	if (map_3) {	×
127	isl_map_free(map_3);	×
128	}	×
129	isl_ctx_free(ctx);	×
130	return false;	×
131	}
132	isl_map* alias_pairs = isl_map_intersect(composed, map_1);	48✔
133	if (!alias_pairs) {	48✔
134	if (composed) {	×
135	isl_map_free(composed);	×
136	}	×
137	if (map_1) {	×
138	isl_map_free(map_1);	×
139	}	×
140	isl_ctx_free(ctx);	×
141	return false;	×
142	}
143
144	bool disjoint = isl_map_is_empty(alias_pairs);	48✔
145	isl_map_free(alias_pairs);	48✔
146	isl_ctx_free(ctx);	48✔
147	if (disjoint) {	48✔
148	return true;	13✔
149	}
150	}	49✔
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✔
165	if (map_1) {	×
166	isl_map_free(map_1);	×
167	}	×
168	if (map_2) {	×
169	isl_map_free(map_2);	×
170	}	×
171	if (map_3) {	×
172	isl_map_free(map_3);	×
173	}	×
174	isl_ctx_free(ctx);	×
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	}	35✔
210
211	bool is_disjoint_monotonic(	85✔
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++) {	131✔
221	auto& dim1 = expr1[i];	96✔
222	if (expr2.size() <= i) {	96✔
223	continue;	×
224	}
225	auto& dim2 = expr2[i];	96✔
226	if (!symbolic::eq(dim1, dim2)) {	96✔
227	continue;	25✔
228	}
229
230	// Collect all symbols
231	symbolic::SymbolSet syms;	71✔
232	for (auto& sym : symbolic::atoms(dim1)) {	139✔
233	syms.insert(sym);	68✔
234	}
235
236	// Collect all non-constant symbols
237	bool can_analyze = true;	71✔
238	for (auto& sym : syms) {	128✔
239	if (!assums1.at(sym).constant()) {	68✔
240	if (sym->get_name() != indvar->get_name()) {	11✔
241	can_analyze = false;	11✔
242	break;	11✔
243	}
244	}	×
245	}
246	if (!can_analyze) {	71✔
247	continue;	11✔
248	}
249
250	// Check if both dimensions are monotonic in non-constant symbols
251	if (is_monotonic(dim1, indvar, assums1)) {	60✔
252	return true;	50✔
253	}
254	}	71✔
255
256	return false;	35✔
257	}	85✔
258
259	bool is_disjoint_interval(	88✔
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++) {	190✔
267	auto& dim1 = expr1[i];	105✔
268	if (expr2.size() <= i) {	105✔
269	continue;	×
270	}
271	auto& dim2 = expr2[i];	105✔
272
273	auto lb1 = minimum(dim1, {}, assums1);	105✔
274	if (lb1 == SymEngine::null \|\| SymEngine::is_a<SymEngine::NaN>(*lb1)) {	105✔
275	continue;	1✔
276	}
277	auto ub1 = maximum(dim1, {}, assums1);	104✔
278	if (ub1 == SymEngine::null \|\| SymEngine::is_a<SymEngine::NaN>(*ub1)) {	104✔
279	continue;	×
280	}
281	auto lb2 = minimum(dim2, {}, assums2);	104✔
282	if (lb2 == SymEngine::null \|\| SymEngine::is_a<SymEngine::NaN>(*lb2)) {	104✔
283	continue;	×
284	}
285	auto ub2 = maximum(dim2, {}, assums2);	104✔
286	if (ub2 == SymEngine::null \|\| SymEngine::is_a<SymEngine::NaN>(*ub2)) {	104✔
287	continue;	×
288	}
289
290	auto dis1 = symbolic::Gt(lb1, ub2);	104✔
291	auto dis2 = symbolic::Gt(lb2, ub1);	104✔
292	if (symbolic::is_true(dis1) \|\| symbolic::is_true(dis2)) {	104✔
293	return true;	3✔
294	}
295	}	105✔
296
297	return false;	85✔
298	}	88✔
299
300	bool intersects(	88✔
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)) {	88✔
308	return false;	3✔
309	}
310	if (is_disjoint_monotonic(expr1, expr2, indvar, assums1, assums2)) {	85✔
311	return false;	50✔
312	}
313	if (is_disjoint_isl(expr1, expr2, indvar, assums1, assums2)) {	35✔
314	return false;	17✔
315	}
316	return true;	18✔
317	}	88✔
318
319	} // namespace maps
320	} // namespace symbolic
321	} // namespace sdfg

daisytuner / sdfglib / 20026333216

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