15909488298

Committed 26 Jun 2025 06:20PM UTC coverage: 65.099% (+0.008%) from 65.091%

Build # 15909488298

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #111 from daisytuner/map-intervall-analysis

Adds intervall analysis to prove disjoint maps

Run Details

28 of 47 new or added lines in 2 files covered. (59.57%)

1 existing line in 1 file now uncovered.

8541 of 13120 relevant lines covered (65.1%)

145.28 hits per line

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

86.55

/src/symbolic/utils.cpp

#include "sdfg/symbolic/utils.h"

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

#include <regex>

#include "sdfg/codegen/language_extensions/c_language_extension.h"
#include "sdfg/symbolic/assumptions.h"
#include "sdfg/symbolic/extreme_values.h"
#include "sdfg/symbolic/polynomials.h"
#include "sdfg/symbolic/symbolic.h"

namespace sdfg {
namespace symbolic {

std::string expression_to_map_str(const MultiExpression& expr, 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 (assums.find(sym) == assums.end() && assums.at(sym).constant()) {
            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()) {
        std::sort(parameters.begin(), parameters.end());
        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 += " }";

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

    // min, max
    map = std::regex_replace(map, std::regex("__daisy_min"), "min_");
    map = std::regex_replace(map, std::regex("__daisy_max"), "max_");

    return map;
}

std::tuple<std::string, std::string, std::string> expressions_to_intersection_map_str(
    const MultiExpression& expr1, const MultiExpression& expr2, const Symbol& indvar,
    const Assumptions& assums1, const Assumptions& assums2) {
    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 (sym->get_name() != indvar->get_name() && assums1.at(sym).constant()) {
            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, assums1, 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 two maps
    std::string map_1;
    std::string map_2;
    if (!parameters.empty()) {
        map_1 += "[";
        map_1 += helpers::join(parameters, ", ");
        map_1 += "] -> ";
        map_2 += "[";
        map_2 += helpers::join(parameters, ", ");
        map_2 += "] -> ";
    }
    map_1 += "{ [";
    map_2 += "{ [";
    for (size_t i = 0; i < dimensions.size(); i++) {
        map_1 += dimensions[i] + "_1";
        map_2 += dimensions[i] + "_2";
        if (i < dimensions.size() - 1) {
            map_1 += ", ";
            map_2 += ", ";
        }
    }
    map_1 += "] -> [";
    map_2 += "] -> [";
    for (size_t i = 0; i < expr1.size(); i++) {
        auto dim = expr1[i];
        for (auto& iter : dimensions) {
            dim = symbolic::subs(dim, symbolic::symbol(iter), symbolic::symbol(iter + "_1"));
        }
        map_1 += language_extension.expression(dim);
        if (i < expr1.size() - 1) {
            map_1 += ", ";
        }
    }
    for (size_t i = 0; i < expr2.size(); i++) {
        auto dim = expr2[i];
        for (auto& iter : dimensions) {
            dim = symbolic::subs(dim, symbolic::symbol(iter), symbolic::symbol(iter + "_2"));
        }
        map_2 += language_extension.expression(dim);
        if (i < expr2.size() - 1) {
            map_2 += ", ";
        }
    }
    map_1 += "] ";
    map_2 += "] ";

    std::vector<std::string> constraints_1;
    std::vector<std::string> constraints_2;
    // Add bounds
    for (auto& con : constraints_syms) {
        auto con_1 = con;
        auto con_2 = con;
        for (auto& iter : dimensions) {
            con_1 = symbolic::subs(con_1, symbolic::symbol(iter), symbolic::symbol(iter + "_1"));
            con_2 = symbolic::subs(con_2, symbolic::symbol(iter), symbolic::symbol(iter + "_2"));
        }
        auto con_str_1 = constraint_to_isl_str(con_1);
        if (con_str_1.empty()) {
            continue;
        }
        auto con_str_2 = constraint_to_isl_str(con_2);
        if (!con_str_1.empty()) {
            constraints_1.push_back(con_str_1);
            constraints_2.push_back(con_str_2);
        }
    }
    if (!constraints_1.empty()) {
        map_1 += " : ";
        map_1 += helpers::join(constraints_1, " and ");
    }
    map_1 += " }";

    if (!constraints_2.empty()) {
        map_2 += " : ";
        map_2 += helpers::join(constraints_2, " and ");
    }
    map_2 += " }";

    std::string map_3 = "{ [";
    for (size_t i = 0; i < dimensions.size(); i++) {
        map_3 += dimensions[i] + "_2";
        if (i < dimensions.size() - 1) {
            map_3 += ", ";
        }
    }
    map_3 += "] -> [";
    for (size_t i = 0; i < dimensions.size(); i++) {
        map_3 += dimensions[i] + "_1";
        if (i < dimensions.size() - 1) {
            map_3 += ", ";
        }
    }
    map_3 += "]";
    std::vector<std::string> monotonicity_constraints;
    if (dimensions_syms.find(indvar) != dimensions_syms.end()) {
        monotonicity_constraints.push_back(indvar->get_name() + "_1 != " + indvar->get_name() +
                                           "_2");
    }
    if (!monotonicity_constraints.empty()) {
        map_3 += " : ";
        map_3 += helpers::join(monotonicity_constraints, " and ");
    }
    map_3 += " }";

    map_1 = std::regex_replace(map_1, std::regex("\\."), "_");
    map_2 = std::regex_replace(map_2, std::regex("\\."), "_");
    map_3 = std::regex_replace(map_3, std::regex("\\."), "_");

    map_1 = std::regex_replace(map_1, std::regex("__daisy_min"), "min");
    map_1 = std::regex_replace(map_1, std::regex("__daisy_max"), "max");
    map_2 = std::regex_replace(map_2, std::regex("__daisy_min"), "min");
    map_2 = std::regex_replace(map_2, std::regex("__daisy_max"), "max");
    map_3 = std::regex_replace(map_3, std::regex("__daisy_min"), "min");
    map_3 = std::regex_replace(map_3, std::regex("__daisy_max"), "max");

    return {map_1, map_2, map_3};
}

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))) {
            if (SymEngine::is_a<SymEngine::Min>(*ub)) {
                auto min = SymEngine::rcp_static_cast<const SymEngine::Min>(ub);
                auto args = min->get_args();
                for (auto& arg : args) {
                    auto con = symbolic::Le(sym, arg);
                    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());
                }
            } else {
                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))) {
            if (SymEngine::is_a<SymEngine::Max>(*lb)) {
                auto max = SymEngine::rcp_static_cast<const SymEngine::Max>(lb);
                auto args = max->get_args();
                for (auto& arg : args) {
                    auto con = symbolic::Ge(sym, arg);
                    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());
                }
            } else {
                auto con = symbolic::Ge(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();
        auto res = language_extension.expression(lhs) + " < " + language_extension.expression(rhs);
        res = std::regex_replace(res, std::regex("\\."), "_");
        res = std::regex_replace(res, std::regex("__daisy_min"), "min");
        res = std::regex_replace(res, std::regex("__daisy_max"), "max");
        return res;
    } 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();
        auto res = language_extension.expression(lhs) + " <= " + language_extension.expression(rhs);
        res = std::regex_replace(res, std::regex("\\."), "_");
        res = std::regex_replace(res, std::regex("__daisy_min"), "min");
        res = std::regex_replace(res, std::regex("__daisy_max"), "max");
        return res;
    } 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();
        auto res = language_extension.expression(lhs) + " == " + language_extension.expression(rhs);
        res = std::regex_replace(res, std::regex("\\."), "_");
        res = std::regex_replace(res, std::regex("__daisy_min"), "min");
        res = std::regex_replace(res, std::regex("__daisy_max"), "max");
        return res;
    } 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();
        auto res = language_extension.expression(lhs) + " != " + language_extension.expression(rhs);
        res = std::regex_replace(res, std::regex("\\."), "_");
        res = std::regex_replace(res, std::regex("__daisy_min"), "min");
        res = std::regex_replace(res, std::regex("__daisy_max"), "max");
        return res;
    }

    return "";
}

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

    for (int i = 0; i < n_in; ++i) {
        std::string name = in_prefix + std::to_string(i);
        map = isl_map_set_dim_name(map, isl_dim_in, i, name.c_str());
    }

    for (int i = 0; i < n_out; ++i) {
        std::string name = out_prefix + std::to_string(i);
        map = isl_map_set_dim_name(map, isl_dim_out, i, name.c_str());
    }
}

MultiExpression delinearize(const MultiExpression& expr, const Assumptions& assums) {
    MultiExpression delinearized;
    for (auto& dim : expr) {
        // Step 1: Convert expression into an affine polynomial
        SymbolVec symbols;
        for (auto& sym : atoms(dim)) {
            if (!assums.at(sym).constant()) {
                symbols.push_back(sym);
            }
        }
        if (symbols.empty() || symbols.size() <= 1) {
            delinearized.push_back(dim);
            continue;
        }

        auto poly = polynomial(dim, symbols);
        if (poly == SymEngine::null) {
            delinearized.push_back(dim);
            continue;
        }

        auto aff_coeffs = affine_coefficients(poly, symbols);
        if (aff_coeffs.empty()) {
            delinearized.push_back(dim);
            continue;
        }

        // Step 2: Peel-off dimensions
        bool success = true;
        Expression remaining = dim;
        std::vector<Expression> peeled_dims;
        while (aff_coeffs.size() > 1) {
            // Find the symbol with largest stride (= largest atom count)
            Symbol new_dim = symbolic::symbol("");
            size_t max_atom_count = 0;
            for (const auto& [sym, coeff] : aff_coeffs) {
                if (sym->get_name() == "__daisy_constant__") {
                    continue;
                }
                size_t atom_count = symbolic::atoms(coeff).size();
                if (atom_count > max_atom_count || new_dim->get_name() == "") {
                    max_atom_count = atom_count;
                    new_dim = sym;
                }
            }
            if (new_dim->get_name() == "") {
                break;
            }

            // Symbol must be nonnegative
            auto sym_lb = minimum(new_dim, {}, assums);
            if (sym_lb == SymEngine::null) {
                success = false;
                break;
            }
            auto sym_cond = symbolic::Ge(sym_lb, symbolic::zero());
            if (!symbolic::is_true(sym_cond)) {
                success = false;
                break;
            }

            // Stride must be positive
            Expression stride = aff_coeffs.at(new_dim);
            auto stride_lb = minimum(stride, {}, assums);
            if (stride_lb == SymEngine::null) {
                success = false;
                break;
            }
            auto stride_cond = symbolic::Ge(stride_lb, symbolic::one());
            if (!symbolic::is_true(stride_cond)) {
                success = false;
                break;
            }

            // Peel off the dimension
            remaining = symbolic::sub(remaining, symbolic::mul(stride, new_dim));

            // Check if remainder is within bounds

            // remaining must be nonnegative
            auto rem_lb = minimum(remaining, {}, assums);
            if (rem_lb == SymEngine::null) {
                success = false;
                break;
            }
            auto cond_zero = symbolic::Ge(rem_lb, symbolic::zero());
            if (!symbolic::is_true(cond_zero)) {
                success = false;
                break;
            }

            // remaining must be less than stride
            auto ub_stride = maximum(stride, {}, assums);
            auto ub_remaining = maximum(remaining, {}, assums);
            auto cond_stride = symbolic::Ge(ub_stride, ub_remaining);
            if (!symbolic::is_true(cond_stride)) {
                success = false;
                break;
            }

            // Add the peeled dimension to the list
            peeled_dims.push_back(new_dim);
            aff_coeffs.erase(new_dim);
        }
        if (!success) {
            delinearized.push_back(dim);
            continue;
        }

        for (auto& peeled_dim : peeled_dims) {
            delinearized.push_back(peeled_dim);
        }

        // If remaining is not zero, then add the constant term
        if (!symbolic::eq(remaining, symbolic::zero()) && success) {
            delinearized.push_back(remaining);
        }
    }

    return delinearized;
}

}  // namespace symbolic
}  // namespace sdfg

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/codegen/language_extensions/c_language_extension.h"
10	#include "sdfg/symbolic/assumptions.h"
11	#include "sdfg/symbolic/extreme_values.h"
12	#include "sdfg/symbolic/polynomials.h"
13	#include "sdfg/symbolic/symbolic.h"
14
15	namespace sdfg {
16	namespace symbolic {
17
18	std::string expression_to_map_str(const MultiExpression& expr, const Assumptions& assums) {	44✔
19	codegen::CLanguageExtension language_extension;	44✔
20
21	// Get all symbols
22	symbolic::SymbolSet syms;	44✔
23	for (auto& expr : expr) {	88✔
24	auto syms_expr = symbolic::atoms(expr);	44✔
25	syms.insert(syms_expr.begin(), syms_expr.end());	44✔
26	}	44✔
27
28	// Distinguish between dimensions and parameters
29	std::vector<std::string> dimensions;	44✔
30	SymbolSet dimensions_syms;	44✔
31	std::vector<std::string> parameters;	44✔
32	SymbolSet parameters_syms;	44✔
33	for (auto& sym : syms) {	62✔
34	if (assums.find(sym) == assums.end() && assums.at(sym).constant()) {	18✔
35	if (parameters_syms.find(sym) != parameters_syms.end()) {	×
36	continue;	×
37	}
38	parameters.push_back(sym->get_name());	×
39	parameters_syms.insert(sym);	×
40	} else {	×
41	if (dimensions_syms.find(sym) != dimensions_syms.end()) {	18✔
42	continue;	×
43	}
44	dimensions.push_back(sym->get_name());	18✔
45	dimensions_syms.insert(sym);	18✔
46	}
47	}
48
49	// Generate constraints
50	SymbolSet seen;	44✔
51	auto constraints_syms = generate_constraints(syms, assums, seen);	44✔
52
53	// Extend parameters with additional symbols from constraints
54	for (auto& con : constraints_syms) {	90✔
55	auto con_syms = symbolic::atoms(con);	46✔
56	for (auto& con_sym : con_syms) {	110✔
57	if (dimensions_syms.find(con_sym) == dimensions_syms.end()) {	64✔
58	if (parameters_syms.find(con_sym) != parameters_syms.end()) {	24✔
59	continue;	12✔
60	}
61	parameters.push_back(con_sym->get_name());	12✔
62	parameters_syms.insert(con_sym);	12✔
63	}	12✔
64	}
65	}	46✔
66
67	// Define map
68	std::string map;	44✔
69	if (!parameters.empty()) {	44✔
70	std::sort(parameters.begin(), parameters.end());	6✔
71	map += "[";	6✔
72	map += helpers::join(parameters, ", ");	6✔
73	map += "] -> ";	6✔
74	}	6✔
75	map += "{ [" + helpers::join(dimensions, ", ") + "] -> [";	44✔
76	for (size_t i = 0; i < expr.size(); i++) {	88✔
77	auto dim = expr[i];	44✔
78	map += language_extension.expression(dim);	44✔
79	if (i < expr.size() - 1) {	44✔
80	map += ", ";	×
81	}	×
82	}	44✔
83	map += "] ";	44✔
84
85	std::vector<std::string> constraints;	44✔
86	for (auto& con : constraints_syms) {	90✔
87	auto con_str = constraint_to_isl_str(con);	46✔
88	if (!con_str.empty()) {	46✔
89	constraints.push_back(con_str);	44✔
90	}	44✔
91	}	46✔
92	if (!constraints.empty()) {	44✔
93	map += " : ";	18✔
94	map += helpers::join(constraints, " and ");	18✔
95	}	18✔
96
97	map += " }";	44✔
98
99	// NV Symbols, e.g., threadIdx.x
100	map = std::regex_replace(map, std::regex("\\."), "_");	44✔
101
102	// min, max
103	map = std::regex_replace(map, std::regex("__daisy_min"), "min_");	44✔
104	map = std::regex_replace(map, std::regex("__daisy_max"), "max_");	44✔
105
106	return map;	44✔
107	}	44✔
108
109	std::tuple<std::string, std::string, std::string> expressions_to_intersection_map_str(	19✔
110	const MultiExpression& expr1, const MultiExpression& expr2, const Symbol& indvar,
111	const Assumptions& assums1, const Assumptions& assums2) {
112	codegen::CLanguageExtension language_extension;	19✔
113
114	// Get all symbols
115	symbolic::SymbolSet syms;	19✔
116	for (auto& expr : expr1) {	44✔
117	auto syms_expr = symbolic::atoms(expr);	25✔
118	syms.insert(syms_expr.begin(), syms_expr.end());	25✔
119	}	25✔
120	for (auto& expr : expr2) {	44✔
121	auto syms_expr = symbolic::atoms(expr);	25✔
122	syms.insert(syms_expr.begin(), syms_expr.end());	25✔
123	}	25✔
124
125	// Distinguish between dimensions and parameters
126	std::vector<std::string> dimensions;	19✔
127	SymbolSet dimensions_syms;	19✔
128	std::vector<std::string> parameters;	19✔
129	SymbolSet parameters_syms;	19✔
130	for (auto& sym : syms) {	42✔
131	if (sym->get_name() != indvar->get_name() && assums1.at(sym).constant()) {	23✔
132	if (parameters_syms.find(sym) != parameters_syms.end()) {	4✔
133	continue;	×
134	}
135	parameters.push_back(sym->get_name());	4✔
136	parameters_syms.insert(sym);	4✔
137	} else {	4✔
138	if (dimensions_syms.find(sym) != dimensions_syms.end()) {	19✔
139	continue;	×
140	}
141	dimensions.push_back(sym->get_name());	19✔
142	dimensions_syms.insert(sym);	19✔
143	}
144	}
145
146	// Generate constraints
147	SymbolSet seen;	19✔
148	auto constraints_syms = generate_constraints(syms, assums1, seen);	19✔
149
150	// Extend parameters with additional symbols from constraints
151	for (auto& con : constraints_syms) {	92✔
152	auto con_syms = symbolic::atoms(con);	73✔
153	for (auto& con_sym : con_syms) {	194✔
154	if (dimensions_syms.find(con_sym) == dimensions_syms.end()) {	121✔
155	if (parameters_syms.find(con_sym) != parameters_syms.end()) {	74✔
156	continue;	52✔
157	}
158	parameters.push_back(con_sym->get_name());	22✔
159	parameters_syms.insert(con_sym);	22✔
160	}	22✔
161	}
162	}	73✔
163
164	// Define two maps
165	std::string map_1;	19✔
166	std::string map_2;	19✔
167	if (!parameters.empty()) {	19✔
168	map_1 += "[";	16✔
169	map_1 += helpers::join(parameters, ", ");	16✔
170	map_1 += "] -> ";	16✔
171	map_2 += "[";	16✔
172	map_2 += helpers::join(parameters, ", ");	16✔
173	map_2 += "] -> ";	16✔
174	}	16✔
175	map_1 += "{ [";	19✔
176	map_2 += "{ [";	19✔
177	for (size_t i = 0; i < dimensions.size(); i++) {	38✔
178	map_1 += dimensions[i] + "_1";	19✔
179	map_2 += dimensions[i] + "_2";	19✔
180	if (i < dimensions.size() - 1) {	19✔
181	map_1 += ", ";	3✔
182	map_2 += ", ";	3✔
183	}	3✔
184	}	19✔
185	map_1 += "] -> [";	19✔
186	map_2 += "] -> [";	19✔
187	for (size_t i = 0; i < expr1.size(); i++) {	44✔
188	auto dim = expr1[i];	25✔
189	for (auto& iter : dimensions) {	53✔
190	dim = symbolic::subs(dim, symbolic::symbol(iter), symbolic::symbol(iter + "_1"));	28✔
191	}
192	map_1 += language_extension.expression(dim);	25✔
193	if (i < expr1.size() - 1) {	25✔
194	map_1 += ", ";	6✔
195	}	6✔
196	}	25✔
197	for (size_t i = 0; i < expr2.size(); i++) {	44✔
198	auto dim = expr2[i];	25✔
199	for (auto& iter : dimensions) {	53✔
200	dim = symbolic::subs(dim, symbolic::symbol(iter), symbolic::symbol(iter + "_2"));	28✔
201	}
202	map_2 += language_extension.expression(dim);	25✔
203	if (i < expr2.size() - 1) {	25✔
204	map_2 += ", ";	6✔
205	}	6✔
206	}	25✔
207	map_1 += "] ";	19✔
208	map_2 += "] ";	19✔
209
210	std::vector<std::string> constraints_1;	19✔
211	std::vector<std::string> constraints_2;	19✔
212	// Add bounds
213	for (auto& con : constraints_syms) {	92✔
214	auto con_1 = con;	73✔
215	auto con_2 = con;	73✔
216	for (auto& iter : dimensions) {	158✔
217	con_1 = symbolic::subs(con_1, symbolic::symbol(iter), symbolic::symbol(iter + "_1"));	85✔
218	con_2 = symbolic::subs(con_2, symbolic::symbol(iter), symbolic::symbol(iter + "_2"));	85✔
219	}
220	auto con_str_1 = constraint_to_isl_str(con_1);	73✔
221	if (con_str_1.empty()) {	73✔
222	continue;	×
223	}
224	auto con_str_2 = constraint_to_isl_str(con_2);	73✔
225	if (!con_str_1.empty()) {	73✔
226	constraints_1.push_back(con_str_1);	73✔
227	constraints_2.push_back(con_str_2);	73✔
228	}	73✔
229	}	73✔
230	if (!constraints_1.empty()) {	19✔
231	map_1 += " : ";	17✔
232	map_1 += helpers::join(constraints_1, " and ");	17✔
233	}	17✔
234	map_1 += " }";	19✔
235
236	if (!constraints_2.empty()) {	19✔
237	map_2 += " : ";	17✔
238	map_2 += helpers::join(constraints_2, " and ");	17✔
239	}	17✔
240	map_2 += " }";	19✔
241
242	std::string map_3 = "{ [";	19✔
243	for (size_t i = 0; i < dimensions.size(); i++) {	38✔
244	map_3 += dimensions[i] + "_2";	19✔
245	if (i < dimensions.size() - 1) {	19✔
246	map_3 += ", ";	3✔
247	}	3✔
248	}	19✔
249	map_3 += "] -> [";	19✔
250	for (size_t i = 0; i < dimensions.size(); i++) {	38✔
251	map_3 += dimensions[i] + "_1";	19✔
252	if (i < dimensions.size() - 1) {	19✔
253	map_3 += ", ";	3✔
254	}	3✔
255	}	19✔
256	map_3 += "]";	19✔
257	std::vector<std::string> monotonicity_constraints;	19✔
258	if (dimensions_syms.find(indvar) != dimensions_syms.end()) {	19✔
259	monotonicity_constraints.push_back(indvar->get_name() + "_1 != " + indvar->get_name() +	8✔
260	"_2");
261	}	8✔
262	if (!monotonicity_constraints.empty()) {	19✔
263	map_3 += " : ";	8✔
264	map_3 += helpers::join(monotonicity_constraints, " and ");	8✔
265	}	8✔
266	map_3 += " }";	19✔
267
268	map_1 = std::regex_replace(map_1, std::regex("\\."), "_");	19✔
269	map_2 = std::regex_replace(map_2, std::regex("\\."), "_");	19✔
270	map_3 = std::regex_replace(map_3, std::regex("\\."), "_");	19✔
271
272	map_1 = std::regex_replace(map_1, std::regex("__daisy_min"), "min");	19✔
273	map_1 = std::regex_replace(map_1, std::regex("__daisy_max"), "max");	19✔
274	map_2 = std::regex_replace(map_2, std::regex("__daisy_min"), "min");	19✔
275	map_2 = std::regex_replace(map_2, std::regex("__daisy_max"), "max");	19✔
276	map_3 = std::regex_replace(map_3, std::regex("__daisy_min"), "min");	19✔
277	map_3 = std::regex_replace(map_3, std::regex("__daisy_max"), "max");	19✔
278
279	return {map_1, map_2, map_3};	19✔
280	}	19✔
281
282	ExpressionSet generate_constraints(SymbolSet& syms, const Assumptions& assums, SymbolSet& seen) {	188✔
283	ExpressionSet constraints;	188✔
284	for (auto& sym : syms) {	422✔
285	if (assums.find(sym) == assums.end()) {	234✔
286	continue;	8✔
287	}
288	if (seen.find(sym) != seen.end()) {	226✔
289	continue;	157✔
290	}
291	seen.insert(sym);	69✔
292
293	auto ub = assums.at(sym).upper_bound();	69✔
294	auto lb = assums.at(sym).lower_bound();	69✔
295	if (!symbolic::eq(ub, symbolic::infty(1))) {	69✔
296	if (SymEngine::is_a<SymEngine::Min>(*ub)) {	46✔
297	auto min = SymEngine::rcp_static_cast<const SymEngine::Min>(ub);	8✔
298	auto args = min->get_args();	8✔
299	for (auto& arg : args) {	24✔
300	auto con = symbolic::Le(sym, arg);	16✔
301	auto con_syms = symbolic::atoms(con);	16✔
302	constraints.insert(con);	16✔
303
304	auto con_cons = generate_constraints(con_syms, assums, seen);	16✔
305	constraints.insert(con_cons.begin(), con_cons.end());	16✔
306	}	16✔
307	} else {	8✔
308	auto con = symbolic::Le(sym, ub);	38✔
309	auto con_syms = symbolic::atoms(con);	38✔
310	constraints.insert(con);	38✔
311
312	auto con_cons = generate_constraints(con_syms, assums, seen);	38✔
313	constraints.insert(con_cons.begin(), con_cons.end());	38✔
314	}	38✔
315	}	46✔
316	if (!symbolic::eq(lb, symbolic::infty(-1))) {	69✔
317	if (SymEngine::is_a<SymEngine::Max>(*lb)) {	69✔
318	auto max = SymEngine::rcp_static_cast<const SymEngine::Max>(lb);	2✔
319	auto args = max->get_args();	2✔
320	for (auto& arg : args) {	6✔
321	auto con = symbolic::Ge(sym, arg);	4✔
322	auto con_syms = symbolic::atoms(con);	4✔
323	constraints.insert(con);	4✔
324
325	auto con_cons = generate_constraints(con_syms, assums, seen);	4✔
326	constraints.insert(con_cons.begin(), con_cons.end());	4✔
327	}	4✔
328	} else {	2✔
329	auto con = symbolic::Ge(sym, lb);	67✔
330	auto con_syms = symbolic::atoms(con);	67✔
331	constraints.insert(con);	67✔
332
333	auto con_cons = generate_constraints(con_syms, assums, seen);	67✔
334	constraints.insert(con_cons.begin(), con_cons.end());	67✔
335	}	67✔
336	}	69✔
337	}	69✔
338	return constraints;	188✔
339	}	188✔
340
341	std::string constraint_to_isl_str(const Expression& con) {	192✔
342	codegen::CLanguageExtension language_extension;	192✔
343
344	if (SymEngine::is_a<SymEngine::StrictLessThan>(*con)) {	192✔
345	auto le = SymEngine::rcp_static_cast<const SymEngine::StrictLessThan>(con);	×
346	auto lhs = le->get_arg1();	×
347	auto rhs = le->get_arg2();	×
NEW 348	auto res = language_extension.expression(lhs) + " < " + language_extension.expression(rhs);	×
NEW 349	res = std::regex_replace(res, std::regex("\\."), "_");	×
NEW 350	res = std::regex_replace(res, std::regex("__daisy_min"), "min");	×
NEW 351	res = std::regex_replace(res, std::regex("__daisy_max"), "max");	×
NEW 352	return res;	×
353	} else if (SymEngine::is_a<SymEngine::LessThan>(*con)) {	192✔
354	auto le = SymEngine::rcp_static_cast<const SymEngine::LessThan>(con);	190✔
355	auto lhs = le->get_arg1();	190✔
356	auto rhs = le->get_arg2();	190✔
357	auto res = language_extension.expression(lhs) + " <= " + language_extension.expression(rhs);	190✔
358	res = std::regex_replace(res, std::regex("\\."), "_");	190✔
359	res = std::regex_replace(res, std::regex("__daisy_min"), "min");	190✔
360	res = std::regex_replace(res, std::regex("__daisy_max"), "max");	190✔
361	return res;	190✔
362	} else if (SymEngine::is_a<SymEngine::Equality>(*con)) {	192✔
363	auto eq = SymEngine::rcp_static_cast<const SymEngine::Equality>(con);	×
364	auto lhs = eq->get_arg1();	×
365	auto rhs = eq->get_arg2();	×
NEW 366	auto res = language_extension.expression(lhs) + " == " + language_extension.expression(rhs);	×
NEW 367	res = std::regex_replace(res, std::regex("\\."), "_");	×
NEW 368	res = std::regex_replace(res, std::regex("__daisy_min"), "min");	×
NEW 369	res = std::regex_replace(res, std::regex("__daisy_max"), "max");	×
NEW 370	return res;	×
371	} else if (SymEngine::is_a<SymEngine::Unequality>(*con)) {	2✔
372	auto ne = SymEngine::rcp_static_cast<const SymEngine::Unequality>(con);	×
373	auto lhs = ne->get_arg1();	×
374	auto rhs = ne->get_arg2();	×
NEW 375	auto res = language_extension.expression(lhs) + " != " + language_extension.expression(rhs);	×
NEW 376	res = std::regex_replace(res, std::regex("\\."), "_");	×
NEW 377	res = std::regex_replace(res, std::regex("__daisy_min"), "min");	×
NEW 378	res = std::regex_replace(res, std::regex("__daisy_max"), "max");	×
NEW 379	return res;	×
UNCOV 380	}	×
381
382	return "";	2✔
383	}	192✔
384
385	void canonicalize_map_dims(isl_map* map, const std::string& in_prefix,	44✔
386	const std::string& out_prefix) {
387	int n_in = isl_map_dim(map, isl_dim_in);	44✔
388	int n_out = isl_map_dim(map, isl_dim_out);	44✔
389
390	for (int i = 0; i < n_in; ++i) {	62✔
391	std::string name = in_prefix + std::to_string(i);	18✔
392	map = isl_map_set_dim_name(map, isl_dim_in, i, name.c_str());	18✔
393	}	18✔
394
395	for (int i = 0; i < n_out; ++i) {	88✔
396	std::string name = out_prefix + std::to_string(i);	44✔
397	map = isl_map_set_dim_name(map, isl_dim_out, i, name.c_str());	44✔
398	}	44✔
399	}	44✔
400
401	MultiExpression delinearize(const MultiExpression& expr, const Assumptions& assums) {	86✔
402	MultiExpression delinearized;	86✔
403	for (auto& dim : expr) {	184✔
404	// Step 1: Convert expression into an affine polynomial
405	SymbolVec symbols;	98✔
406	for (auto& sym : atoms(dim)) {	176✔
407	if (!assums.at(sym).constant()) {	78✔
408	symbols.push_back(sym);	45✔
409	}	45✔
410	}
411	if (symbols.empty() \|\| symbols.size() <= 1) {	98✔
412	delinearized.push_back(dim);	94✔
413	continue;	94✔
414	}
415
416	auto poly = polynomial(dim, symbols);	4✔
417	if (poly == SymEngine::null) {	4✔
418	delinearized.push_back(dim);	×
419	continue;	×
420	}
421
422	auto aff_coeffs = affine_coefficients(poly, symbols);	4✔
423	if (aff_coeffs.empty()) {	4✔
424	delinearized.push_back(dim);	×
425	continue;	×
426	}
427
428	// Step 2: Peel-off dimensions
429	bool success = true;	4✔
430	Expression remaining = dim;	4✔
431	std::vector<Expression> peeled_dims;	4✔
432	while (aff_coeffs.size() > 1) {	9✔
433	// Find the symbol with largest stride (= largest atom count)
434	Symbol new_dim = symbolic::symbol("");	7✔
435	size_t max_atom_count = 0;	7✔
436	for (const auto& [sym, coeff] : aff_coeffs) {	53✔
437	if (sym->get_name() == "__daisy_constant__") {	20✔
438	continue;	7✔
439	}
440	size_t atom_count = symbolic::atoms(coeff).size();	13✔
441	if (atom_count > max_atom_count \|\| new_dim->get_name() == "") {	13✔
442	max_atom_count = atom_count;	13✔
443	new_dim = sym;	13✔
444	}	13✔
445	}
446	if (new_dim->get_name() == "") {	7✔
447	break;	×
448	}
449
450	// Symbol must be nonnegative
451	auto sym_lb = minimum(new_dim, {}, assums);	7✔
452	if (sym_lb == SymEngine::null) {	7✔
453	success = false;	×
454	break;	×
455	}
456	auto sym_cond = symbolic::Ge(sym_lb, symbolic::zero());	7✔
457	if (!symbolic::is_true(sym_cond)) {	7✔
458	success = false;	1✔
459	break;	1✔
460	}
461
462	// Stride must be positive
463	Expression stride = aff_coeffs.at(new_dim);	6✔
464	auto stride_lb = minimum(stride, {}, assums);	6✔
465	if (stride_lb == SymEngine::null) {	6✔
466	success = false;	×
467	break;	×
468	}
469	auto stride_cond = symbolic::Ge(stride_lb, symbolic::one());	6✔
470	if (!symbolic::is_true(stride_cond)) {	6✔
471	success = false;	1✔
472	break;	1✔
473	}
474
475	// Peel off the dimension
476	remaining = symbolic::sub(remaining, symbolic::mul(stride, new_dim));	5✔
477
478	// Check if remainder is within bounds
479
480	// remaining must be nonnegative
481	auto rem_lb = minimum(remaining, {}, assums);	5✔
482	if (rem_lb == SymEngine::null) {	5✔
483	success = false;	×
484	break;	×
485	}
486	auto cond_zero = symbolic::Ge(rem_lb, symbolic::zero());	5✔
487	if (!symbolic::is_true(cond_zero)) {	5✔
488	success = false;	×
489	break;	×
490	}
491
492	// remaining must be less than stride
493	auto ub_stride = maximum(stride, {}, assums);	5✔
494	auto ub_remaining = maximum(remaining, {}, assums);	5✔
495	auto cond_stride = symbolic::Ge(ub_stride, ub_remaining);	5✔
496	if (!symbolic::is_true(cond_stride)) {	5✔
497	success = false;	×
498	break;	×
499	}
500
501	// Add the peeled dimension to the list
502	peeled_dims.push_back(new_dim);	5✔
503	aff_coeffs.erase(new_dim);	5✔
504	}	7✔
505	if (!success) {	4✔
506	delinearized.push_back(dim);	2✔
507	continue;	2✔
508	}
509
510	for (auto& peeled_dim : peeled_dims) {	7✔
511	delinearized.push_back(peeled_dim);	5✔
512	}
513
514	// If remaining is not zero, then add the constant term
515	if (!symbolic::eq(remaining, symbolic::zero()) && success) {	2✔
516	delinearized.push_back(remaining);	×
517	}	×
518	}	98✔
519
520	return delinearized;	86✔
521	}	86✔
522
523	} // namespace symbolic
524	} // namespace sdfg

daisytuner / sdfglib / 15909488298

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