15619235800

Committed 12 Jun 2025 07:29PM UTC coverage: 63.07% (+0.03%) from 63.04%

Build # 15619235800

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #74 from daisytuner/extended-expression-equivalence

adds extended check for equivalence of expressions

Run Details

142 of 225 new or added lines in 2 files covered. (63.11%)

1 existing line in 1 file now uncovered.

7487 of 11871 relevant lines covered (63.07%)

103.28 hits per line

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

62.78

/src/symbolic/sets.cpp

#include "sdfg/symbolic/sets.h"

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

#include "sdfg/codegen/language_extensions/c_language_extension.h"

namespace sdfg {
namespace symbolic {

ExpressionSet generate_constraints(SymbolSet& syms, const Assumptions& assums, SymbolSet& seen) {
    ExpressionSet constraints;
    for (auto& sym : syms) {
        if (assums.find(sym) == assums.end()) {
            continue;
        }
        if (seen.find(sym) != seen.end()) {
            continue;
        }
        seen.insert(sym);

        auto ub = assums.at(sym).upper_bound();
        auto lb = assums.at(sym).lower_bound();
        if (!symbolic::eq(ub, symbolic::infty(1))) {
            auto con = symbolic::Le(sym, ub);
            auto con_syms = symbolic::atoms(con);
            constraints.insert(con);

            auto con_cons = generate_constraints(con_syms, assums, seen);
            constraints.insert(con_cons.begin(), con_cons.end());
        }
        if (!symbolic::eq(lb, symbolic::infty(-1))) {
            auto con = symbolic::Le(sym, lb);
            auto con_syms = symbolic::atoms(con);
            constraints.insert(con);

            auto con_cons = generate_constraints(con_syms, assums, seen);
            constraints.insert(con_cons.begin(), con_cons.end());
        }
    }
    return constraints;
}

std::string constraint_to_isl_str(const Expression& con) {
    codegen::CLanguageExtension language_extension;

    if (SymEngine::is_a<SymEngine::StrictLessThan>(*con)) {
        auto le = SymEngine::rcp_static_cast<const SymEngine::StrictLessThan>(con);
        auto lhs = le->get_arg1();
        auto rhs = le->get_arg2();
        return language_extension.expression(lhs) + " < " + language_extension.expression(rhs);
    } else if (SymEngine::is_a<SymEngine::LessThan>(*con)) {
        auto le = SymEngine::rcp_static_cast<const SymEngine::LessThan>(con);
        auto lhs = le->get_arg1();
        auto rhs = le->get_arg2();
        return language_extension.expression(lhs) + " <= " + language_extension.expression(rhs);
    } else if (SymEngine::is_a<SymEngine::Equality>(*con)) {
        auto eq = SymEngine::rcp_static_cast<const SymEngine::Equality>(con);
        auto lhs = eq->get_arg1();
        auto rhs = eq->get_arg2();
        return language_extension.expression(lhs) + " == " + language_extension.expression(rhs);
    } else if (SymEngine::is_a<SymEngine::Unequality>(*con)) {
        auto ne = SymEngine::rcp_static_cast<const SymEngine::Unequality>(con);
        auto lhs = ne->get_arg1();
        auto rhs = ne->get_arg2();
        return language_extension.expression(lhs) + " != " + language_extension.expression(rhs);
    }

    return "";
}

std::string expression_to_isl_map_str(const MultiExpression& expr, const SymbolSet& params,
                                      const Assumptions& assums) {
    codegen::CLanguageExtension language_extension;

    // Get all symbols
    symbolic::SymbolSet syms;
    for (auto& expr : expr) {
        auto syms_expr = symbolic::atoms(expr);
        syms.insert(syms_expr.begin(), syms_expr.end());
    }

    // Distinguish between dimensions and parameters
    std::vector<std::string> dimensions;
    SymbolSet dimensions_syms;
    std::vector<std::string> parameters;
    SymbolSet parameters_syms;
    for (auto& sym : syms) {
        if (params.find(sym) != params.end()) {
            parameters.push_back(sym->get_name());
            parameters_syms.insert(sym);
        } else {
            dimensions.push_back(sym->get_name());
            dimensions_syms.insert(sym);
        }
    }

    // Generate constraints
    SymbolSet seen;
    auto constraints_syms = generate_constraints(syms, assums, seen);
    // Extend parameters with additional symbols from constraints
    for (auto& con : constraints_syms) {
        auto con_syms = symbolic::atoms(con);
        for (auto& con_sym : con_syms) {
            if (dimensions_syms.find(con_sym) == dimensions_syms.end()) {
                parameters.push_back(con_sym->get_name());
                parameters_syms.insert(con_sym);
            }
        }
    }

    // Define map
    std::string map;
    if (!parameters.empty()) {
        map += "[";
        map += helpers::join(parameters, ", ");
        map += "] -> ";
    }
    map += "{ [" + helpers::join(dimensions, ", ") + "] -> [";
    for (size_t i = 0; i < expr.size(); i++) {
        auto dim = expr[i];
        map += language_extension.expression(dim);
        if (i < expr.size() - 1) {
            map += ", ";
        }
    }
    map += "] ";

    std::vector<std::string> constraints;
    for (auto& con : constraints_syms) {
        auto con_str = constraint_to_isl_str(con);
        if (!con_str.empty()) {
            constraints.push_back(con_str);
        }
    }
    if (!constraints.empty()) {
        map += " : ";
        map += helpers::join(constraints, " and ");
    }
    map += " }";

    return map;
}

std::string expressions_to_isl_map_str(const MultiExpression& expr1, const MultiExpression& expr2,
                                       const SymbolSet& params, const Assumptions& assums) {
    codegen::CLanguageExtension language_extension;

    // Get all symbols
    symbolic::SymbolSet syms;
    for (auto& expr : expr1) {
        auto syms_expr = symbolic::atoms(expr);
        syms.insert(syms_expr.begin(), syms_expr.end());
    }
    for (auto& expr : expr2) {
        auto syms_expr = symbolic::atoms(expr);
        syms.insert(syms_expr.begin(), syms_expr.end());
    }

    // Distinguish between dimensions and parameters
    std::vector<std::string> dimensions;
    SymbolSet dimensions_syms;
    std::vector<std::string> parameters;
    SymbolSet parameters_syms;
    for (auto& sym : syms) {
        if (params.find(sym) != params.end()) {
            if (parameters_syms.find(sym) != parameters_syms.end()) {
                continue;
            }
            parameters.push_back(sym->get_name());
            parameters_syms.insert(sym);
        } else {
            if (dimensions_syms.find(sym) != dimensions_syms.end()) {
                continue;
            }
            dimensions.push_back(sym->get_name());
            dimensions_syms.insert(sym);
        }
    }

    // Generate constraints
    SymbolSet seen;
    auto constraints_syms = generate_constraints(syms, assums, seen);

    // Extend parameters with additional symbols from constraints
    for (auto& con : constraints_syms) {
        auto con_syms = symbolic::atoms(con);
        for (auto& con_sym : con_syms) {
            if (dimensions_syms.find(con_sym) == dimensions_syms.end()) {
                if (parameters_syms.find(con_sym) != parameters_syms.end()) {
                    continue;
                }
                parameters.push_back(con_sym->get_name());
                parameters_syms.insert(con_sym);
            }
        }
    }

    // Define map
    std::string map;
    if (!parameters.empty()) {
        map += "[";
        map += helpers::join(parameters, ", ");
        map += "] -> ";
    }
    map += "{ [" + helpers::join(dimensions, ", ") + "] -> [";
    for (size_t i = 0; i < expr1.size(); i++) {
        auto dim = expr1[i];
        map += language_extension.expression(dim);
        map += ", ";
    }
    for (size_t i = 0; i < expr2.size(); i++) {
        auto dim = expr2[i];
        map += language_extension.expression(dim);
        if (i < expr2.size() - 1) {
            map += ", ";
        }
    }
    map += "] ";

    std::vector<std::string> constraints;
    for (auto& con : constraints_syms) {
        auto con_str = constraint_to_isl_str(con);
        if (!con_str.empty()) {
            constraints.push_back(con_str);
        }
    }
    if (!constraints.empty()) {
        map += " : ";
        map += helpers::join(constraints, " and ");
    }

    map += " }";

    return map;
}

bool intersect(const MultiExpression& expr1, const SymbolSet& params1, const MultiExpression& expr2,
               const SymbolSet& params2, const Assumptions& assums) {
    return false;
}

bool is_equivalent(const MultiExpression& expr1, const MultiExpression& expr2,
                   const SymbolSet& params, const Assumptions& assums) {
    if (expr1.size() != expr2.size()) {
        return false;
    }

    // Simple check for equality
    bool equals = true;
    for (size_t i = 0; i < expr1.size(); i++) {
        if (!symbolic::eq(expr1[i], expr2[i])) {
            equals = false;
            break;
        }
    }
    if (equals) {
        return true;
    }

    // Check for set equivalence
    isl_ctx* ctx = isl_ctx_alloc();
    // Builds { [params] -> [expr1..., expr2...] : assumptions }
    std::string map_str = expressions_to_isl_map_str(expr1, expr2, params, assums);

    isl_map* pair_map = isl_map_read_from_str(ctx, map_str.c_str());
    if (!pair_map) {
        isl_ctx_free(ctx);
        return false;
    }

    isl_set* range = isl_map_range(isl_map_copy(pair_map));

    // Build diagonal set: { [x₀, ..., xₙ, y₀, ..., yₙ] : x₀ = y₀ and ... and xₙ = yₙ }
    std::string diag_str = "{ [";
    for (size_t i = 0; i < expr1.size() * 2; ++i) {
        if (i > 0) diag_str += ", ";
        diag_str += "v" + std::to_string(i);
    }
    diag_str += "] : ";
    for (size_t i = 0; i < expr1.size(); ++i) {
        if (i > 0) diag_str += " and ";
        diag_str += "v" + std::to_string(i) + " = v" + std::to_string(i + expr1.size());
    }
    diag_str += " }";

    isl_set* diagonal = isl_set_read_from_str(ctx, diag_str.c_str());

    bool equivalent = false;
    if (range && diagonal) {
        equivalent = isl_set_is_subset(range, diagonal) == 1;
    }

    isl_set_free(range);
    isl_set_free(diagonal);
    isl_map_free(pair_map);
    isl_ctx_free(ctx);

    return equivalent;
}

}  // namespace symbolic
}  // namespace sdfg

1	#include "sdfg/symbolic/sets.h"
2
3	#include <isl/ctx.h>
4	#include <isl/map.h>
5	#include <isl/set.h>
6	#include <isl/space.h>
7
8	#include "sdfg/codegen/language_extensions/c_language_extension.h"
9
10	namespace sdfg {
11	namespace symbolic {
12
13	ExpressionSet generate_constraints(SymbolSet& syms, const Assumptions& assums, SymbolSet& seen) {	21✔
14	ExpressionSet constraints;	21✔
15	for (auto& sym : syms) {	55✔
16	if (assums.find(sym) == assums.end()) {	34✔
17	continue;	1✔
18	}
19	if (seen.find(sym) != seen.end()) {	33✔
20	continue;	25✔
21	}
22	seen.insert(sym);	8✔
23
24	auto ub = assums.at(sym).upper_bound();	8✔
25	auto lb = assums.at(sym).lower_bound();	8✔
26	if (!symbolic::eq(ub, symbolic::infty(1))) {	8✔
27	auto con = symbolic::Le(sym, ub);	8✔
28	auto con_syms = symbolic::atoms(con);	8✔
29	constraints.insert(con);	8✔
30
31	auto con_cons = generate_constraints(con_syms, assums, seen);	8✔
32	constraints.insert(con_cons.begin(), con_cons.end());	8✔
33	}	8✔
34	if (!symbolic::eq(lb, symbolic::infty(-1))) {	8✔
35	auto con = symbolic::Le(sym, lb);	8✔
36	auto con_syms = symbolic::atoms(con);	8✔
37	constraints.insert(con);	8✔
38
39	auto con_cons = generate_constraints(con_syms, assums, seen);	8✔
40	constraints.insert(con_cons.begin(), con_cons.end());	8✔
41	}	8✔
42	}	8✔
43	return constraints;	21✔
44	}	21✔
45
46	std::string constraint_to_isl_str(const Expression& con) {	11✔
47	codegen::CLanguageExtension language_extension;	11✔
48
49	if (SymEngine::is_a<SymEngine::StrictLessThan>(*con)) {	11✔
NEW 50	auto le = SymEngine::rcp_static_cast<const SymEngine::StrictLessThan>(con);	×
NEW 51	auto lhs = le->get_arg1();	×
NEW 52	auto rhs = le->get_arg2();	×
NEW 53	return language_extension.expression(lhs) + " < " + language_extension.expression(rhs);	×
54	} else if (SymEngine::is_a<SymEngine::LessThan>(*con)) {	11✔
55	auto le = SymEngine::rcp_static_cast<const SymEngine::LessThan>(con);	10✔
56	auto lhs = le->get_arg1();	10✔
57	auto rhs = le->get_arg2();	10✔
58	return language_extension.expression(lhs) + " <= " + language_extension.expression(rhs);	10✔
59	} else if (SymEngine::is_a<SymEngine::Equality>(*con)) {	11✔
NEW 60	auto eq = SymEngine::rcp_static_cast<const SymEngine::Equality>(con);	×
NEW 61	auto lhs = eq->get_arg1();	×
NEW 62	auto rhs = eq->get_arg2();	×
NEW 63	return language_extension.expression(lhs) + " == " + language_extension.expression(rhs);	×
64	} else if (SymEngine::is_a<SymEngine::Unequality>(*con)) {	1✔
NEW 65	auto ne = SymEngine::rcp_static_cast<const SymEngine::Unequality>(con);	×
NEW 66	auto lhs = ne->get_arg1();	×
NEW 67	auto rhs = ne->get_arg2();	×
NEW 68	return language_extension.expression(lhs) + " != " + language_extension.expression(rhs);	×
NEW 69	}	×
70
71	return "";	1✔
72	}	11✔
73
NEW 74	std::string expression_to_isl_map_str(const MultiExpression& expr, const SymbolSet& params,	×
75	const Assumptions& assums) {
NEW 76	codegen::CLanguageExtension language_extension;	×
77
78	// Get all symbols
NEW 79	symbolic::SymbolSet syms;	×
NEW 80	for (auto& expr : expr) {	×
NEW 81	auto syms_expr = symbolic::atoms(expr);	×
NEW 82	syms.insert(syms_expr.begin(), syms_expr.end());	×
NEW 83	}	×
84
85	// Distinguish between dimensions and parameters
NEW 86	std::vector<std::string> dimensions;	×
NEW 87	SymbolSet dimensions_syms;	×
NEW 88	std::vector<std::string> parameters;	×
NEW 89	SymbolSet parameters_syms;	×
NEW 90	for (auto& sym : syms) {	×
NEW 91	if (params.find(sym) != params.end()) {	×
NEW 92	parameters.push_back(sym->get_name());	×
NEW 93	parameters_syms.insert(sym);	×
NEW 94	} else {	×
NEW 95	dimensions.push_back(sym->get_name());	×
NEW 96	dimensions_syms.insert(sym);	×
97	}
98	}
99
100	// Generate constraints
NEW 101	SymbolSet seen;	×
NEW 102	auto constraints_syms = generate_constraints(syms, assums, seen);	×
103	// Extend parameters with additional symbols from constraints
NEW 104	for (auto& con : constraints_syms) {	×
NEW 105	auto con_syms = symbolic::atoms(con);	×
NEW 106	for (auto& con_sym : con_syms) {	×
NEW 107	if (dimensions_syms.find(con_sym) == dimensions_syms.end()) {	×
NEW 108	parameters.push_back(con_sym->get_name());	×
NEW 109	parameters_syms.insert(con_sym);	×
NEW 110	}	×
111	}
NEW 112	}	×
113
114	// Define map
NEW 115	std::string map;	×
NEW 116	if (!parameters.empty()) {	×
NEW 117	map += "[";	×
NEW 118	map += helpers::join(parameters, ", ");	×
NEW 119	map += "] -> ";	×
NEW 120	}	×
NEW 121	map += "{ [" + helpers::join(dimensions, ", ") + "] -> [";	×
NEW 122	for (size_t i = 0; i < expr.size(); i++) {	×
NEW 123	auto dim = expr[i];	×
NEW 124	map += language_extension.expression(dim);	×
NEW 125	if (i < expr.size() - 1) {	×
NEW 126	map += ", ";	×
NEW 127	}	×
NEW 128	}	×
NEW 129	map += "] ";	×
130
NEW 131	std::vector<std::string> constraints;	×
NEW 132	for (auto& con : constraints_syms) {	×
NEW 133	auto con_str = constraint_to_isl_str(con);	×
NEW 134	if (!con_str.empty()) {	×
NEW 135	constraints.push_back(con_str);	×
NEW 136	}	×
NEW 137	}	×
NEW 138	if (!constraints.empty()) {	×
NEW 139	map += " : ";	×
NEW 140	map += helpers::join(constraints, " and ");	×
NEW 141	}	×
NEW 142	map += " }";	×
143
NEW 144	return map;	×
NEW 145	}	×
146
147	std::string expressions_to_isl_map_str(const MultiExpression& expr1, const MultiExpression& expr2,	5✔
148	const SymbolSet& params, const Assumptions& assums) {
149	codegen::CLanguageExtension language_extension;	5✔
150
151	// Get all symbols
152	symbolic::SymbolSet syms;	5✔
153	for (auto& expr : expr1) {	10✔
154	auto syms_expr = symbolic::atoms(expr);	5✔
155	syms.insert(syms_expr.begin(), syms_expr.end());	5✔
156	}	5✔
157	for (auto& expr : expr2) {	10✔
158	auto syms_expr = symbolic::atoms(expr);	5✔
159	syms.insert(syms_expr.begin(), syms_expr.end());	5✔
160	}	5✔
161
162	// Distinguish between dimensions and parameters
163	std::vector<std::string> dimensions;	5✔
164	SymbolSet dimensions_syms;	5✔
165	std::vector<std::string> parameters;	5✔
166	SymbolSet parameters_syms;	5✔
167	for (auto& sym : syms) {	13✔
168	if (params.find(sym) != params.end()) {	8✔
NEW 169	if (parameters_syms.find(sym) != parameters_syms.end()) {	×
NEW 170	continue;	×
171	}
NEW 172	parameters.push_back(sym->get_name());	×
NEW 173	parameters_syms.insert(sym);	×
NEW 174	} else {	×
175	if (dimensions_syms.find(sym) != dimensions_syms.end()) {	8✔
NEW 176	continue;	×
177	}
178	dimensions.push_back(sym->get_name());	8✔
179	dimensions_syms.insert(sym);	8✔
180	}
181	}
182
183	// Generate constraints
184	SymbolSet seen;	5✔
185	auto constraints_syms = generate_constraints(syms, assums, seen);	5✔
186
187	// Extend parameters with additional symbols from constraints
188	for (auto& con : constraints_syms) {	16✔
189	auto con_syms = symbolic::atoms(con);	11✔
190	for (auto& con_sym : con_syms) {	29✔
191	if (dimensions_syms.find(con_sym) == dimensions_syms.end()) {	18✔
192	if (parameters_syms.find(con_sym) != parameters_syms.end()) {	4✔
193	continue;	3✔
194	}
195	parameters.push_back(con_sym->get_name());	1✔
196	parameters_syms.insert(con_sym);	1✔
197	}	1✔
198	}
199	}	11✔
200
201	// Define map
202	std::string map;	5✔
203	if (!parameters.empty()) {	5✔
204	map += "[";	1✔
205	map += helpers::join(parameters, ", ");	1✔
206	map += "] -> ";	1✔
207	}	1✔
208	map += "{ [" + helpers::join(dimensions, ", ") + "] -> [";	5✔
209	for (size_t i = 0; i < expr1.size(); i++) {	10✔
210	auto dim = expr1[i];	5✔
211	map += language_extension.expression(dim);	5✔
212	map += ", ";	5✔
213	}	5✔
214	for (size_t i = 0; i < expr2.size(); i++) {	10✔
215	auto dim = expr2[i];	5✔
216	map += language_extension.expression(dim);	5✔
217	if (i < expr2.size() - 1) {	5✔
NEW 218	map += ", ";	×
NEW 219	}	×
220	}	5✔
221	map += "] ";	5✔
222
223	std::vector<std::string> constraints;	5✔
224	for (auto& con : constraints_syms) {	16✔
225	auto con_str = constraint_to_isl_str(con);	11✔
226	if (!con_str.empty()) {	11✔
227	constraints.push_back(con_str);	10✔
228	}	10✔
229	}	11✔
230	if (!constraints.empty()) {	5✔
231	map += " : ";	4✔
232	map += helpers::join(constraints, " and ");	4✔
233	}	4✔
234
235	map += " }";	5✔
236
237	return map;	5✔
238	}	5✔
239
UNCOV 240	bool intersect(const MultiExpression& expr1, const SymbolSet& params1, const MultiExpression& expr2,	×
241	const SymbolSet& params2, const Assumptions& assums) {
242	return false;	×
243	}
244
245	bool is_equivalent(const MultiExpression& expr1, const MultiExpression& expr2,	13✔
246	const SymbolSet& params, const Assumptions& assums) {
247	if (expr1.size() != expr2.size()) {	13✔
NEW 248	return false;	×
249	}
250
251	// Simple check for equality
252	bool equals = true;	13✔
253	for (size_t i = 0; i < expr1.size(); i++) {	15✔
254	if (!symbolic::eq(expr1[i], expr2[i])) {	7✔
255	equals = false;	5✔
256	break;	5✔
257	}
258	}	2✔
259	if (equals) {	13✔
260	return true;	8✔
261	}
262
263	// Check for set equivalence
264	isl_ctx* ctx = isl_ctx_alloc();	5✔
265	// Builds { [params] -> [expr1..., expr2...] : assumptions }
266	std::string map_str = expressions_to_isl_map_str(expr1, expr2, params, assums);	5✔
267
268	isl_map* pair_map = isl_map_read_from_str(ctx, map_str.c_str());	5✔
269	if (!pair_map) {	5✔
NEW 270	isl_ctx_free(ctx);	×
NEW 271	return false;	×
272	}
273
274	isl_set* range = isl_map_range(isl_map_copy(pair_map));	5✔
275
276	// Build diagonal set: { [x₀, ..., xₙ, y₀, ..., yₙ] : x₀ = y₀ and ... and xₙ = yₙ }
277	std::string diag_str = "{ [";	5✔
278	for (size_t i = 0; i < expr1.size() * 2; ++i) {	15✔
279	if (i > 0) diag_str += ", ";	10✔
280	diag_str += "v" + std::to_string(i);	10✔
281	}	10✔
282	diag_str += "] : ";	5✔
283	for (size_t i = 0; i < expr1.size(); ++i) {	10✔
284	if (i > 0) diag_str += " and ";	5✔
285	diag_str += "v" + std::to_string(i) + " = v" + std::to_string(i + expr1.size());	5✔
286	}	5✔
287	diag_str += " }";	5✔
288
289	isl_set* diagonal = isl_set_read_from_str(ctx, diag_str.c_str());	5✔
290
291	bool equivalent = false;	5✔
292	if (range && diagonal) {	5✔
293	equivalent = isl_set_is_subset(range, diagonal) == 1;	5✔
294	}	5✔
295
296	isl_set_free(range);	5✔
297	isl_set_free(diagonal);	5✔
298	isl_map_free(pair_map);	5✔
299	isl_ctx_free(ctx);	5✔
300
301	return equivalent;	5✔
302	}	13✔
303
304	} // namespace symbolic
305	} // namespace sdfg

daisytuner / sdfglib / 15619235800

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