20320588678

Committed 17 Dec 2025 11:30PM UTC coverage: 39.849% (-0.2%) from 40.001%

Build # 20320588678

Build Type

Pull #397

github

Committed by

web-flow

Commit Message

Merge e0882eafd into ea9155d89

Pull Request Pull Request #397: adds zext_i64 symbolic function

Run Details

13477 of 43870 branches covered (30.72%)

Branch coverage included in aggregate %.

39 of 125 new or added lines in 8 files covered. (31.2%)

3 existing lines in 2 files now uncovered.

11603 of 19068 relevant lines covered (60.85%)

86.64 hits per line

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

38.16

/src/symbolic/extreme_values.cpp

#include "sdfg/symbolic/extreme_values.h"

#include "sdfg/symbolic/polynomials.h"

namespace sdfg {
namespace symbolic {

size_t MAX_DEPTH = 100;
Expression minimum(const Expression expr, const SymbolSet& parameters, const Assumptions& assumptions, const size_t depth);
Expression maximum(const Expression expr, const SymbolSet& parameters, const Assumptions& assumptions, const size_t depth);

Expression minimum(const Expression expr, const SymbolSet& parameters, const Assumptions& assumptions, const size_t depth) {
    // Base Cases
    if (depth > MAX_DEPTH) {
        return SymEngine::null;
    }

    if (SymEngine::is_a<SymEngine::NaN>(*expr)) {
        return SymEngine::null;
    }

    if (SymEngine::is_a<SymEngine::Integer>(*expr)) {
        return expr;
    } else if (SymEngine::is_a<SymEngine::Infty>(*expr)) {
        return expr;
    } else if (SymEngine::is_a<symbolic::ZExtI64Function>(*expr)) {
        auto zext = SymEngine::rcp_static_cast<const symbolic::ZExtI64Function>(expr);
        auto min_arg = minimum(zext->get_args()[0], parameters, assumptions, depth + 1);
        if (min_arg == SymEngine::null) {
            return SymEngine::null;
        } else {
            return symbolic::zext_i64(min_arg);
        }
    }

    // Symbol
    if (SymEngine::is_a<SymEngine::Symbol>(*expr)) {
        auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(expr);
        if (parameters.find(sym) != parameters.end()) {
            return sym;
        }
        if (assumptions.find(sym) != assumptions.end()) {
            return minimum(assumptions.at(sym).lower_bound_deprecated(), parameters, assumptions, depth + 1);
        }
        return SymEngine::null;
    }

    // Mul
    if (SymEngine::is_a<SymEngine::Mul>(*expr)) {
        auto mul = SymEngine::rcp_static_cast<const SymEngine::Mul>(expr);
        const auto& args = mul->get_args();
        size_t n = args.size();

        std::vector<std::pair<Expression, Expression>> bounds;
        bounds.reserve(n);

        for (const auto& arg : args) {
            Expression min_val = minimum(arg, parameters, assumptions, depth + 1);
            Expression max_val = maximum(arg, parameters, assumptions, depth + 1);

            if (min_val == SymEngine::null || max_val == SymEngine::null) {
                return SymEngine::null;
            }
            bounds.emplace_back(min_val, max_val);
        }

        // Iterate over 2^n combinations
        Expression min_product = SymEngine::null;
        const size_t total_combinations = 1ULL << n;

        for (size_t mask = 0; mask < total_combinations; ++mask) {
            Expression product = SymEngine::integer(1);
            for (size_t i = 0; i < n; ++i) {
                const auto& bound = bounds[i];
                Expression val = (mask & (1ULL << i)) ? bound.second : bound.first;
                product = symbolic::mul(product, val);
            }
            if (min_product == SymEngine::null) {
                min_product = product;
            } else {
                min_product = symbolic::min(min_product, product);
            }
        }

        return min_product;
    }

    // Add
    if (SymEngine::is_a<SymEngine::Add>(*expr)) {
        auto add = SymEngine::rcp_static_cast<const SymEngine::Add>(expr);
        const auto& args = add->get_args();
        Expression lbs = SymEngine::null;
        for (const auto& arg : args) {
            auto lb = minimum(arg, parameters, assumptions, depth + 1);
            if (lb == SymEngine::null) {
                return SymEngine::null;
            }
            if (lbs == SymEngine::null) {
                lbs = lb;
            } else {
                lbs = symbolic::add(lbs, lb);
            }
        }
        return lbs;
    }

    // Max
    if (SymEngine::is_a<SymEngine::Max>(*expr)) {
        auto args = SymEngine::rcp_dynamic_cast<const SymEngine::Max>(expr)->get_args();
        Expression lbs = SymEngine::null;
        for (const auto& arg : args) {
            auto lb = minimum(arg, parameters, assumptions, depth + 1);
            if (lb == SymEngine::null) {
                return SymEngine::null;
            }
            if (lbs == SymEngine::null) {
                lbs = lb;
            } else {
                lbs = symbolic::min(lbs, lb);
            }
        }
        return lbs;
    }

    // Min
    if (SymEngine::is_a<SymEngine::Min>(*expr)) {
        auto args = SymEngine::rcp_dynamic_cast<const SymEngine::Min>(expr)->get_args();
        Expression lbs = SymEngine::null;
        for (const auto& arg : args) {
            auto lb = minimum(arg, parameters, assumptions, depth + 1);
            if (lb == SymEngine::null) {
                return SymEngine::null;
            }
            if (lbs == SymEngine::null) {
                lbs = lb;
            } else {
                lbs = symbolic::min(lbs, lb);
            }
        }
        return lbs;
    }

    return SymEngine::null;
}

Expression maximum(const Expression expr, const SymbolSet& parameters, const Assumptions& assumptions, const size_t depth) {
    if (depth > MAX_DEPTH) {
        return SymEngine::null;
    }

    if (SymEngine::is_a<SymEngine::NaN>(*expr)) {
        return SymEngine::null;
    }

    // Base Cases
    if (SymEngine::is_a<SymEngine::Integer>(*expr)) {
        return expr;
    } else if (SymEngine::is_a<SymEngine::Infty>(*expr)) {
        return expr;
    }

    // Symbol
    if (SymEngine::is_a<SymEngine::Symbol>(*expr)) {
        auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(expr);
        if (parameters.find(sym) != parameters.end()) {
            return sym;
        }
        if (assumptions.find(sym) != assumptions.end()) {
            return maximum(assumptions.at(sym).upper_bound_deprecated(), parameters, assumptions, depth + 1);
        }
        return SymEngine::null;
    }

    if (SymEngine::is_a<symbolic::ZExtI64Function>(*expr)) {
        auto zext = SymEngine::rcp_static_cast<const symbolic::ZExtI64Function>(expr);
        auto max_arg = maximum(zext->get_args()[0], parameters, assumptions, depth + 1);
        if (max_arg == SymEngine::null) {
            return SymEngine::null;
        } else {
            return symbolic::zext_i64(max_arg);
        }
    }

    // Mul
    if (SymEngine::is_a<SymEngine::Mul>(*expr)) {
        auto mul = SymEngine::rcp_static_cast<const SymEngine::Mul>(expr);
        const auto& args = mul->get_args();
        size_t n = args.size();

        std::vector<std::pair<Expression, Expression>> bounds;
        bounds.reserve(n);

        for (const auto& arg : args) {
            Expression min_val = minimum(arg, parameters, assumptions, depth + 1);
            Expression max_val = maximum(arg, parameters, assumptions, depth + 1);

            if (min_val == SymEngine::null || max_val == SymEngine::null) {
                return SymEngine::null;
            }
            bounds.emplace_back(min_val, max_val);
        }

        // Iterate over 2^n combinations
        Expression max_product = SymEngine::null;
        const size_t total_combinations = 1ULL << n;

        for (size_t mask = 0; mask < total_combinations; ++mask) {
            Expression product = SymEngine::integer(1);
            for (size_t i = 0; i < n; ++i) {
                const auto& bound = bounds[i];
                Expression val = (mask & (1ULL << i)) ? bound.second : bound.first;
                product = symbolic::mul(product, val);
            }
            if (max_product == SymEngine::null) {
                max_product = product;
            } else {
                max_product = symbolic::max(max_product, product);
            }
        }

        return max_product;
    }

    // Add
    if (SymEngine::is_a<SymEngine::Add>(*expr)) {
        auto add = SymEngine::rcp_static_cast<const SymEngine::Add>(expr);
        const auto& args = add->get_args();
        Expression ubs = SymEngine::null;
        for (const auto& arg : args) {
            auto ub = maximum(arg, parameters, assumptions, depth + 1);
            if (ub == SymEngine::null) {
                return SymEngine::null;
            }
            if (ubs == SymEngine::null) {
                ubs = ub;
            } else {
                ubs = symbolic::add(ubs, ub);
            }
        }
        return ubs;
    }

    // Max
    if (SymEngine::is_a<SymEngine::Max>(*expr)) {
        auto args = SymEngine::rcp_dynamic_cast<const SymEngine::Max>(expr)->get_args();
        Expression ubs = SymEngine::null;
        for (const auto& arg : args) {
            auto ub = maximum(arg, parameters, assumptions, depth + 1);
            if (ub == SymEngine::null) {
                return SymEngine::null;
            }
            if (ubs == SymEngine::null) {
                ubs = ub;
            } else {
                ubs = symbolic::max(ubs, ub);
            }
        }
        return ubs;
    }

    // Min
    if (SymEngine::is_a<SymEngine::Min>(*expr)) {
        auto args = SymEngine::rcp_dynamic_cast<const SymEngine::Min>(expr)->get_args();
        Expression ubs = SymEngine::null;
        for (const auto& arg : args) {
            auto ub = maximum(arg, parameters, assumptions, depth + 1);
            if (ub == SymEngine::null) {
                return SymEngine::null;
            }
            if (ubs == SymEngine::null) {
                ubs = ub;
            } else {
                ubs = symbolic::max(ubs, ub);
            }
        }
        return ubs;
    }

    return SymEngine::null;
}

Expression minimum(const Expression expr, const SymbolSet& parameters, const Assumptions& assumptions) {
    return minimum(expr, parameters, assumptions, 0);
}

Expression maximum(const Expression expr, const SymbolSet& parameters, const Assumptions& assumptions) {
    return maximum(expr, parameters, assumptions, 0);
}

Expression minimum_new(
    const Expression expr, const SymbolSet& parameters, const Assumptions& assumptions, const size_t depth, bool tight
);
Expression maximum_new(
    const Expression expr, const SymbolSet& parameters, const Assumptions& assumptions, const size_t depth, bool tight
);

Expression minimum_new(
    const Expression expr, const SymbolSet& parameters, const Assumptions& assumptions, const size_t depth, bool tight
) {
    // End of recursion: fail
    if (depth > MAX_DEPTH) {
        return SymEngine::null;
    }
    if (SymEngine::is_a<SymEngine::NaN>(*expr)) {
        return SymEngine::null;
    }
    if (SymEngine::is_a<SymEngine::Infty>(*expr)) {
        return SymEngine::null;
    }
    // End of recursion: success
    if (SymEngine::is_a<SymEngine::Integer>(*expr)) {
        return expr;
    }
    if (SymEngine::is_a<SymEngine::Symbol>(*expr)) {
        auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(expr);
        if (parameters.find(sym) != parameters.end()) {
            return sym;
        }
    }

    if (SymEngine::is_a<symbolic::ZExtI64Function>(*expr)) {
        auto zext = SymEngine::rcp_static_cast<const symbolic::ZExtI64Function>(expr);
        auto min_arg = minimum_new(zext->get_args()[0], parameters, assumptions, depth + 1, tight);
        if (min_arg == SymEngine::null) {
            return SymEngine::null;
        } else {
            return symbolic::zext_i64(min_arg);
        }
    }

    // Symbol
    if (SymEngine::is_a<SymEngine::Symbol>(*expr)) {
        auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(expr);
        if (assumptions.find(sym) != assumptions.end()) {
            if (tight) {
                if (assumptions.at(sym).tight_lower_bound().is_null()) {
                    return SymEngine::null;
                }
                return minimum_new(assumptions.at(sym).tight_lower_bound(), parameters, assumptions, depth + 1, tight);
            }
            symbolic::Expression new_lb = SymEngine::null;
            for (auto& lb : assumptions.at(sym).lower_bounds()) {
                auto new_min = minimum_new(lb, parameters, assumptions, depth + 1, tight);
                if (new_min.is_null()) {
                    continue;
                }
                if (new_lb.is_null()) {
                    new_lb = new_min;
                    continue;
                }
                new_lb = symbolic::max(new_lb, new_min);
            }
            return new_lb;
        }
        return SymEngine::null;
    }

    // Mul
    if (SymEngine::is_a<SymEngine::Mul>(*expr)) {
        auto mul = SymEngine::rcp_static_cast<const SymEngine::Mul>(expr);
        const auto& args = mul->get_args();
        size_t n = args.size();

        std::vector<std::pair<Expression, Expression>> bounds;
        bounds.reserve(n);

        for (const auto& arg : args) {
            Expression min_val = minimum_new(arg, parameters, assumptions, depth + 1, tight);
            Expression max_val = maximum_new(arg, parameters, assumptions, depth + 1, tight);

            if (min_val == SymEngine::null || max_val == SymEngine::null) {
                return SymEngine::null;
            }
            bounds.emplace_back(min_val, max_val);
        }

        // Iterate over 2^n combinations
        Expression min_product = SymEngine::null;
        const size_t total_combinations = 1ULL << n;

        for (size_t mask = 0; mask < total_combinations; ++mask) {
            Expression product = SymEngine::integer(1);
            for (size_t i = 0; i < n; ++i) {
                const auto& bound = bounds[i];
                Expression val = (mask & (1ULL << i)) ? bound.second : bound.first;
                product = symbolic::mul(product, val);
            }
            if (min_product == SymEngine::null) {
                min_product = product;
            } else {
                min_product = symbolic::min(min_product, product);
            }
        }

        return min_product;
    }

    // Add
    if (SymEngine::is_a<SymEngine::Add>(*expr)) {
        auto add = SymEngine::rcp_static_cast<const SymEngine::Add>(expr);
        const auto& args = add->get_args();
        Expression lbs = SymEngine::null;
        for (const auto& arg : args) {
            auto lb = minimum_new(arg, parameters, assumptions, depth + 1, tight);
            if (lb == SymEngine::null) {
                return SymEngine::null;
            }
            if (lbs == SymEngine::null) {
                lbs = lb;
            } else {
                lbs = symbolic::add(lbs, lb);
            }
        }
        return lbs;
    }

    // Max
    if (SymEngine::is_a<SymEngine::Max>(*expr)) {
        auto args = SymEngine::rcp_dynamic_cast<const SymEngine::Max>(expr)->get_args();
        Expression lbs = SymEngine::null;
        for (const auto& arg : args) {
            auto lb = minimum_new(arg, parameters, assumptions, depth + 1, tight);
            if (lb == SymEngine::null) {
                return SymEngine::null;
            }
            if (lbs == SymEngine::null) {
                lbs = lb;
            } else {
                lbs = symbolic::min(lbs, lb);
            }
        }
        return lbs;
    }

    // Min
    if (SymEngine::is_a<SymEngine::Min>(*expr)) {
        auto args = SymEngine::rcp_dynamic_cast<const SymEngine::Min>(expr)->get_args();
        Expression lbs = SymEngine::null;
        for (const auto& arg : args) {
            auto lb = minimum_new(arg, parameters, assumptions, depth + 1, tight);
            if (lb == SymEngine::null) {
                return SymEngine::null;
            }
            if (lbs == SymEngine::null) {
                lbs = lb;
            } else {
                lbs = symbolic::min(lbs, lb);
            }
        }
        return lbs;
    }

    return SymEngine::null;
}

Expression maximum_new(
    const Expression expr, const SymbolSet& parameters, const Assumptions& assumptions, const size_t depth, bool tight
) {
    // End of recursion: fail
    if (depth > MAX_DEPTH) {
        return SymEngine::null;
    }
    if (SymEngine::is_a<SymEngine::NaN>(*expr)) {
        return SymEngine::null;
    }
    if (SymEngine::is_a<SymEngine::Infty>(*expr)) {
        return SymEngine::null;
    }
    // End of recursion: success
    if (SymEngine::is_a<SymEngine::Integer>(*expr)) {
        return expr;
    }
    if (SymEngine::is_a<SymEngine::Symbol>(*expr)) {
        auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(expr);
        if (parameters.find(sym) != parameters.end()) {
            return sym;
        }
    }

    if (SymEngine::is_a<symbolic::ZExtI64Function>(*expr)) {
        auto zext = SymEngine::rcp_static_cast<const symbolic::ZExtI64Function>(expr);
        auto max_arg = maximum_new(zext->get_args()[0], parameters, assumptions, depth + 1, tight);
        if (max_arg == SymEngine::null) {
            return SymEngine::null;
        } else {
            return symbolic::zext_i64(max_arg);
        }
    }

    // Symbol
    if (SymEngine::is_a<SymEngine::Symbol>(*expr)) {
        auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(expr);
        if (assumptions.find(sym) != assumptions.end()) {
            if (tight) {
                if (assumptions.at(sym).tight_upper_bound().is_null()) {
                    return SymEngine::null;
                }
                return maximum_new(assumptions.at(sym).tight_upper_bound(), parameters, assumptions, depth + 1, tight);
            }
            symbolic::Expression new_ub = SymEngine::null;
            for (auto& ub : assumptions.at(sym).upper_bounds()) {
                auto new_max = maximum_new(ub, parameters, assumptions, depth + 1, tight);
                if (new_max.is_null()) {
                    continue;
                }
                if (new_ub.is_null()) {
                    new_ub = new_max;
                    continue;
                }
                new_ub = symbolic::min(new_ub, new_max);
            }
            return new_ub;
        }
        return SymEngine::null;
    }

    // Mul
    if (SymEngine::is_a<SymEngine::Mul>(*expr)) {
        auto mul = SymEngine::rcp_static_cast<const SymEngine::Mul>(expr);
        const auto& args = mul->get_args();
        size_t n = args.size();

        std::vector<std::pair<Expression, Expression>> bounds;
        bounds.reserve(n);

        for (const auto& arg : args) {
            Expression min_val = minimum_new(arg, parameters, assumptions, depth + 1, tight);
            Expression max_val = maximum_new(arg, parameters, assumptions, depth + 1, tight);

            if (min_val == SymEngine::null || max_val == SymEngine::null) {
                return SymEngine::null;
            }
            bounds.emplace_back(min_val, max_val);
        }

        // Iterate over 2^n combinations
        Expression max_product = SymEngine::null;
        const size_t total_combinations = 1ULL << n;

        for (size_t mask = 0; mask < total_combinations; ++mask) {
            Expression product = SymEngine::integer(1);
            for (size_t i = 0; i < n; ++i) {
                const auto& bound = bounds[i];
                Expression val = (mask & (1ULL << i)) ? bound.second : bound.first;
                product = symbolic::mul(product, val);
            }
            if (max_product == SymEngine::null) {
                max_product = product;
            } else {
                max_product = symbolic::max(max_product, product);
            }
        }

        return max_product;
    }

    // Add
    if (SymEngine::is_a<SymEngine::Add>(*expr)) {
        auto add = SymEngine::rcp_static_cast<const SymEngine::Add>(expr);
        const auto& args = add->get_args();
        Expression ubs = SymEngine::null;
        for (const auto& arg : args) {
            auto ub = maximum_new(arg, parameters, assumptions, depth + 1, tight);
            if (ub == SymEngine::null) {
                return SymEngine::null;
            }
            if (ubs == SymEngine::null) {
                ubs = ub;
            } else {
                ubs = symbolic::add(ubs, ub);
            }
        }
        return ubs;
    }

    // Max
    if (SymEngine::is_a<SymEngine::Max>(*expr)) {
        auto args = SymEngine::rcp_dynamic_cast<const SymEngine::Max>(expr)->get_args();
        Expression ubs = SymEngine::null;
        for (const auto& arg : args) {
            auto ub = maximum_new(arg, parameters, assumptions, depth + 1, tight);
            if (ub == SymEngine::null) {
                return SymEngine::null;
            }
            if (ubs == SymEngine::null) {
                ubs = ub;
            } else {
                ubs = symbolic::max(ubs, ub);
            }
        }
        return ubs;
    }

    // Min
    if (SymEngine::is_a<SymEngine::Min>(*expr)) {
        auto args = SymEngine::rcp_dynamic_cast<const SymEngine::Min>(expr)->get_args();
        Expression ubs = SymEngine::null;
        for (const auto& arg : args) {
            auto ub = maximum_new(arg, parameters, assumptions, depth + 1, tight);
            if (ub == SymEngine::null) {
                return SymEngine::null;
            }
            if (ubs == SymEngine::null) {
                ubs = ub;
            } else {
                ubs = symbolic::max(ubs, ub);
            }
        }
        return ubs;
    }

    return SymEngine::null;
}

Expression minimum_new(const Expression expr, const SymbolSet& parameters, const Assumptions& assumptions, bool tight) {
    return minimum_new(expr, parameters, assumptions, 0, tight);
}

Expression maximum_new(const Expression expr, const SymbolSet& parameters, const Assumptions& assumptions, bool tight) {
    return maximum_new(expr, parameters, assumptions, 0, tight);
}

} // namespace symbolic
} // namespace sdfg

1	#include "sdfg/symbolic/extreme_values.h"
2
3	#include "sdfg/symbolic/polynomials.h"
4
5	namespace sdfg {
6	namespace symbolic {
7
8	size_t MAX_DEPTH = 100;
9	Expression minimum(const Expression expr, const SymbolSet& parameters, const Assumptions& assumptions, const size_t depth);
10	Expression maximum(const Expression expr, const SymbolSet& parameters, const Assumptions& assumptions, const size_t depth);
11
12	Expression minimum(const Expression expr, const SymbolSet& parameters, const Assumptions& assumptions, const size_t depth) {	4,883✔
13	// Base Cases
14	if (depth > MAX_DEPTH) {	4,883✔
15	return SymEngine::null;	12✔
16	}
17
18	if (SymEngine::is_a<SymEngine::NaN>(*expr)) {	4,871!
19	return SymEngine::null;	×
20	}
21
22	if (SymEngine::is_a<SymEngine::Integer>(*expr)) {	4,871✔
23	return expr;	2,488✔
24	} else if (SymEngine::is_a<SymEngine::Infty>(*expr)) {	2,383!
25	return expr;	×
26	} else if (SymEngine::is_a<symbolic::ZExtI64Function>(*expr)) {	2,383!
NEW 27	auto zext = SymEngine::rcp_static_cast<const symbolic::ZExtI64Function>(expr);	×
NEW 28	auto min_arg = minimum(zext->get_args()[0], parameters, assumptions, depth + 1);	×
NEW 29	if (min_arg == SymEngine::null) {	×
NEW 30	return SymEngine::null;	×
31	} else {
NEW 32	return symbolic::zext_i64(min_arg);	×
33	}
UNCOV 34	}	×
35
36	// Symbol
37	if (SymEngine::is_a<SymEngine::Symbol>(*expr)) {	2,383✔
38	auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(expr);	1,488✔
39	if (parameters.find(sym) != parameters.end()) {	1,488!
40	return sym;	7✔
41	}
42	if (assumptions.find(sym) != assumptions.end()) {	1,481!
43	return minimum(assumptions.at(sym).lower_bound_deprecated(), parameters, assumptions, depth + 1);	1,478!
44	}
45	return SymEngine::null;	3!
46	}	1,488✔
47
48	// Mul
49	if (SymEngine::is_a<SymEngine::Mul>(*expr)) {	895✔
50	auto mul = SymEngine::rcp_static_cast<const SymEngine::Mul>(expr);	150✔
51	const auto& args = mul->get_args();	150!
52	size_t n = args.size();	150✔
53
54	std::vector<std::pair<Expression, Expression>> bounds;	150✔
55	bounds.reserve(n);	150!
56
57	for (const auto& arg : args) {	508✔
58	Expression min_val = minimum(arg, parameters, assumptions, depth + 1);	358!
59	Expression max_val = maximum(arg, parameters, assumptions, depth + 1);	358!
60
61	if (min_val == SymEngine::null \|\| max_val == SymEngine::null) {	358!
62	return SymEngine::null;	×
63	}
64	bounds.emplace_back(min_val, max_val);	358!
65	}	358!
66
67	// Iterate over 2^n combinations
68	Expression min_product = SymEngine::null;	150!
69	const size_t total_combinations = 1ULL << n;	150✔
70
71	for (size_t mask = 0; mask < total_combinations; ++mask) {	982✔
72	Expression product = SymEngine::integer(1);	832!
73	for (size_t i = 0; i < n; ++i) {	2,960✔
74	const auto& bound = bounds[i];	2,128✔
75	Expression val = (mask & (1ULL << i)) ? bound.second : bound.first;	2,128!
76	product = symbolic::mul(product, val);	2,128!
77	}	2,128✔
78	if (min_product == SymEngine::null) {	832!
79	min_product = product;	150!
80	} else {	150✔
81	min_product = symbolic::min(min_product, product);	682!
82	}
83	}	832✔
84
85	return min_product;	150✔
86	}	300!
87
88	// Add
89	if (SymEngine::is_a<SymEngine::Add>(*expr)) {	745✔
90	auto add = SymEngine::rcp_static_cast<const SymEngine::Add>(expr);	459✔
91	const auto& args = add->get_args();	459!
92	Expression lbs = SymEngine::null;	459!
93	for (const auto& arg : args) {	1,190✔
94	auto lb = minimum(arg, parameters, assumptions, depth + 1);	995!
95	if (lb == SymEngine::null) {	995!
96	return SymEngine::null;	264!
97	}
98	if (lbs == SymEngine::null) {	731!
99	lbs = lb;	451!
100	} else {	451✔
101	lbs = symbolic::add(lbs, lb);	280!
102	}
103	}	995✔
104	return lbs;	195✔
105	}	459✔
106
107	// Max
108	if (SymEngine::is_a<SymEngine::Max>(*expr)) {	286✔
109	auto args = SymEngine::rcp_dynamic_cast<const SymEngine::Max>(expr)->get_args();	284!
110	Expression lbs = SymEngine::null;	284!
111	for (const auto& arg : args) {	576✔
112	auto lb = minimum(arg, parameters, assumptions, depth + 1);	566!
113	if (lb == SymEngine::null) {	566!
114	return SymEngine::null;	274!
115	}
116	if (lbs == SymEngine::null) {	292!
117	lbs = lb;	282!
118	} else {	282✔
119	lbs = symbolic::min(lbs, lb);	10!
120	}
121	}	566✔
122	return lbs;	10✔
123	}	284✔
124
125	// Min
126	if (SymEngine::is_a<SymEngine::Min>(*expr)) {	2!
127	auto args = SymEngine::rcp_dynamic_cast<const SymEngine::Min>(expr)->get_args();	2!
128	Expression lbs = SymEngine::null;	2!
129	for (const auto& arg : args) {	6✔
130	auto lb = minimum(arg, parameters, assumptions, depth + 1);	4!
131	if (lb == SymEngine::null) {	4!
132	return SymEngine::null;	×
133	}
134	if (lbs == SymEngine::null) {	4!
135	lbs = lb;	2!
136	} else {	2✔
137	lbs = symbolic::min(lbs, lb);	2!
138	}
139	}	4!
140	return lbs;	2✔
141	}	2✔
142
143	return SymEngine::null;	×
144	}	4,883✔
145
146	Expression maximum(const Expression expr, const SymbolSet& parameters, const Assumptions& assumptions, const size_t depth) {	2,950✔
147	if (depth > MAX_DEPTH) {	2,950!
148	return SymEngine::null;	×
149	}
150
151	if (SymEngine::is_a<SymEngine::NaN>(*expr)) {	2,950!
152	return SymEngine::null;	×
153	}
154
155	// Base Cases
156	if (SymEngine::is_a<SymEngine::Integer>(*expr)) {	2,950✔
157	return expr;	1,389✔
158	} else if (SymEngine::is_a<SymEngine::Infty>(*expr)) {	1,561!
159	return expr;	×
160	}
161
162	// Symbol
163	if (SymEngine::is_a<SymEngine::Symbol>(*expr)) {	1,561✔
164	auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(expr);	936✔
165	if (parameters.find(sym) != parameters.end()) {	936!
166	return sym;	8✔
167	}
168	if (assumptions.find(sym) != assumptions.end()) {	928!
169	return maximum(assumptions.at(sym).upper_bound_deprecated(), parameters, assumptions, depth + 1);	928!
170	}
171	return SymEngine::null;	×
172	}	936✔
173
174	if (SymEngine::is_a<symbolic::ZExtI64Function>(*expr)) {	625!
NEW 175	auto zext = SymEngine::rcp_static_cast<const symbolic::ZExtI64Function>(expr);	×
NEW 176	auto max_arg = maximum(zext->get_args()[0], parameters, assumptions, depth + 1);	×
NEW 177	if (max_arg == SymEngine::null) {	×
NEW 178	return SymEngine::null;	×
179	} else {
NEW 180	return symbolic::zext_i64(max_arg);	×
181	}
NEW 182	}	×
183
184	// Mul
185	if (SymEngine::is_a<SymEngine::Mul>(*expr)) {	625✔
186	auto mul = SymEngine::rcp_static_cast<const SymEngine::Mul>(expr);	150✔
187	const auto& args = mul->get_args();	150!
188	size_t n = args.size();	150✔
189
190	std::vector<std::pair<Expression, Expression>> bounds;	150✔
191	bounds.reserve(n);	150!
192
193	for (const auto& arg : args) {	508✔
194	Expression min_val = minimum(arg, parameters, assumptions, depth + 1);	358!
195	Expression max_val = maximum(arg, parameters, assumptions, depth + 1);	358!
196
197	if (min_val == SymEngine::null \|\| max_val == SymEngine::null) {	358!
198	return SymEngine::null;	×
199	}
200	bounds.emplace_back(min_val, max_val);	358!
201	}	358!
202
203	// Iterate over 2^n combinations
204	Expression max_product = SymEngine::null;	150!
205	const size_t total_combinations = 1ULL << n;	150✔
206
207	for (size_t mask = 0; mask < total_combinations; ++mask) {	982✔
208	Expression product = SymEngine::integer(1);	832!
209	for (size_t i = 0; i < n; ++i) {	2,960✔
210	const auto& bound = bounds[i];	2,128✔
211	Expression val = (mask & (1ULL << i)) ? bound.second : bound.first;	2,128!
212	product = symbolic::mul(product, val);	2,128!
213	}	2,128✔
214	if (max_product == SymEngine::null) {	832!
215	max_product = product;	150!
216	} else {	150✔
217	max_product = symbolic::max(max_product, product);	682!
218	}
219	}	832✔
220
221	return max_product;	150✔
222	}	300!
223
224	// Add
225	if (SymEngine::is_a<SymEngine::Add>(*expr)) {	475✔
226	auto add = SymEngine::rcp_static_cast<const SymEngine::Add>(expr);	471✔
227	const auto& args = add->get_args();	471!
228	Expression ubs = SymEngine::null;	471!
229	for (const auto& arg : args) {	1,498✔
230	auto ub = maximum(arg, parameters, assumptions, depth + 1);	1,027!
231	if (ub == SymEngine::null) {	1,027!
232	return SymEngine::null;	×
233	}
234	if (ubs == SymEngine::null) {	1,027!
235	ubs = ub;	471!
236	} else {	471✔
237	ubs = symbolic::add(ubs, ub);	556!
238	}
239	}	1,027!
240	return ubs;	471✔
241	}	471✔
242
243	// Max
244	if (SymEngine::is_a<SymEngine::Max>(*expr)) {	4✔
245	auto args = SymEngine::rcp_dynamic_cast<const SymEngine::Max>(expr)->get_args();	2!
246	Expression ubs = SymEngine::null;	2!
247	for (const auto& arg : args) {	6✔
248	auto ub = maximum(arg, parameters, assumptions, depth + 1);	4!
249	if (ub == SymEngine::null) {	4!
250	return SymEngine::null;	×
251	}
252	if (ubs == SymEngine::null) {	4!
253	ubs = ub;	2!
254	} else {	2✔
255	ubs = symbolic::max(ubs, ub);	2!
256	}
257	}	4!
258	return ubs;	2✔
259	}	2✔
260
261	// Min
262	if (SymEngine::is_a<SymEngine::Min>(*expr)) {	2!
263	auto args = SymEngine::rcp_dynamic_cast<const SymEngine::Min>(expr)->get_args();	2!
264	Expression ubs = SymEngine::null;	2!
265	for (const auto& arg : args) {	6✔
266	auto ub = maximum(arg, parameters, assumptions, depth + 1);	4!
267	if (ub == SymEngine::null) {	4!
268	return SymEngine::null;	×
269	}
270	if (ubs == SymEngine::null) {	4!
271	ubs = ub;	2!
272	} else {	2✔
273	ubs = symbolic::max(ubs, ub);	2!
274	}
275	}	4!
276	return ubs;	2✔
277	}	2✔
278
279	return SymEngine::null;	×
280	}	2,950✔
281
282	Expression minimum(const Expression expr, const SymbolSet& parameters, const Assumptions& assumptions) {	1,124✔
283	return minimum(expr, parameters, assumptions, 0);	1,124!
284	}	×
285
286	Expression maximum(const Expression expr, const SymbolSet& parameters, const Assumptions& assumptions) {	271✔
287	return maximum(expr, parameters, assumptions, 0);	271!
288	}	×
289
290	Expression minimum_new(
291	const Expression expr, const SymbolSet& parameters, const Assumptions& assumptions, const size_t depth, bool tight
292	);
293	Expression maximum_new(
294	const Expression expr, const SymbolSet& parameters, const Assumptions& assumptions, const size_t depth, bool tight
295	);
296
297	Expression minimum_new(	22✔
298	const Expression expr, const SymbolSet& parameters, const Assumptions& assumptions, const size_t depth, bool tight
299	) {
300	// End of recursion: fail
301	if (depth > MAX_DEPTH) {	22!
302	return SymEngine::null;	×
303	}
304	if (SymEngine::is_a<SymEngine::NaN>(*expr)) {	22!
305	return SymEngine::null;	×
306	}
307	if (SymEngine::is_a<SymEngine::Infty>(*expr)) {	22!
308	return SymEngine::null;	×
309	}
310	// End of recursion: success
311	if (SymEngine::is_a<SymEngine::Integer>(*expr)) {	22✔
312	return expr;	10✔
313	}
314	if (SymEngine::is_a<SymEngine::Symbol>(*expr)) {	12!
315	auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(expr);	12✔
316	if (parameters.find(sym) != parameters.end()) {	12!
317	return sym;	3✔
318	}
319	}	12✔
320
321	if (SymEngine::is_a<symbolic::ZExtI64Function>(*expr)) {	9!
NEW 322	auto zext = SymEngine::rcp_static_cast<const symbolic::ZExtI64Function>(expr);	×
NEW 323	auto min_arg = minimum_new(zext->get_args()[0], parameters, assumptions, depth + 1, tight);	×
NEW 324	if (min_arg == SymEngine::null) {	×
NEW 325	return SymEngine::null;	×
326	} else {
NEW 327	return symbolic::zext_i64(min_arg);	×
328	}
NEW 329	}	×
330
331	// Symbol
332	if (SymEngine::is_a<SymEngine::Symbol>(*expr)) {	9!
333	auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(expr);	9✔
334	if (assumptions.find(sym) != assumptions.end()) {	9!
335	if (tight) {	9!
336	if (assumptions.at(sym).tight_lower_bound().is_null()) {	9!
337	return SymEngine::null;	1!
338	}
339	return minimum_new(assumptions.at(sym).tight_lower_bound(), parameters, assumptions, depth + 1, tight);	8!
340	}
341	symbolic::Expression new_lb = SymEngine::null;	×
342	for (auto& lb : assumptions.at(sym).lower_bounds()) {	×
343	auto new_min = minimum_new(lb, parameters, assumptions, depth + 1, tight);	×
344	if (new_min.is_null()) {	×
345	continue;	×
346	}
347	if (new_lb.is_null()) {	×
348	new_lb = new_min;	×
349	continue;	×
350	}
351	new_lb = symbolic::max(new_lb, new_min);	×
352	}	×
353	return new_lb;	×
354	}	×
355	return SymEngine::null;	×
356	}	9✔
357
358	// Mul
359	if (SymEngine::is_a<SymEngine::Mul>(*expr)) {	×
360	auto mul = SymEngine::rcp_static_cast<const SymEngine::Mul>(expr);	×
361	const auto& args = mul->get_args();	×
362	size_t n = args.size();	×
363
364	std::vector<std::pair<Expression, Expression>> bounds;	×
365	bounds.reserve(n);	×
366
367	for (const auto& arg : args) {	×
368	Expression min_val = minimum_new(arg, parameters, assumptions, depth + 1, tight);	×
369	Expression max_val = maximum_new(arg, parameters, assumptions, depth + 1, tight);	×
370
371	if (min_val == SymEngine::null \|\| max_val == SymEngine::null) {	×
372	return SymEngine::null;	×
373	}
374	bounds.emplace_back(min_val, max_val);	×
375	}	×
376
377	// Iterate over 2^n combinations
378	Expression min_product = SymEngine::null;	×
379	const size_t total_combinations = 1ULL << n;	×
380
381	for (size_t mask = 0; mask < total_combinations; ++mask) {	×
382	Expression product = SymEngine::integer(1);	×
383	for (size_t i = 0; i < n; ++i) {	×
384	const auto& bound = bounds[i];	×
385	Expression val = (mask & (1ULL << i)) ? bound.second : bound.first;	×
386	product = symbolic::mul(product, val);	×
387	}	×
388	if (min_product == SymEngine::null) {	×
389	min_product = product;	×
390	} else {	×
391	min_product = symbolic::min(min_product, product);	×
392	}
393	}	×
394
395	return min_product;	×
396	}	×
397
398	// Add
399	if (SymEngine::is_a<SymEngine::Add>(*expr)) {	×
400	auto add = SymEngine::rcp_static_cast<const SymEngine::Add>(expr);	×
401	const auto& args = add->get_args();	×
402	Expression lbs = SymEngine::null;	×
403	for (const auto& arg : args) {	×
404	auto lb = minimum_new(arg, parameters, assumptions, depth + 1, tight);	×
405	if (lb == SymEngine::null) {	×
406	return SymEngine::null;	×
407	}
408	if (lbs == SymEngine::null) {	×
409	lbs = lb;	×
410	} else {	×
411	lbs = symbolic::add(lbs, lb);	×
412	}
413	}	×
414	return lbs;	×
415	}	×
416
417	// Max
418	if (SymEngine::is_a<SymEngine::Max>(*expr)) {	×
419	auto args = SymEngine::rcp_dynamic_cast<const SymEngine::Max>(expr)->get_args();	×
420	Expression lbs = SymEngine::null;	×
421	for (const auto& arg : args) {	×
422	auto lb = minimum_new(arg, parameters, assumptions, depth + 1, tight);	×
423	if (lb == SymEngine::null) {	×
424	return SymEngine::null;	×
425	}
426	if (lbs == SymEngine::null) {	×
427	lbs = lb;	×
428	} else {	×
429	lbs = symbolic::min(lbs, lb);	×
430	}
431	}	×
432	return lbs;	×
433	}	×
434
435	// Min
436	if (SymEngine::is_a<SymEngine::Min>(*expr)) {	×
437	auto args = SymEngine::rcp_dynamic_cast<const SymEngine::Min>(expr)->get_args();	×
438	Expression lbs = SymEngine::null;	×
439	for (const auto& arg : args) {	×
440	auto lb = minimum_new(arg, parameters, assumptions, depth + 1, tight);	×
441	if (lb == SymEngine::null) {	×
442	return SymEngine::null;	×
443	}
444	if (lbs == SymEngine::null) {	×
445	lbs = lb;	×
446	} else {	×
447	lbs = symbolic::min(lbs, lb);	×
448	}
449	}	×
450	return lbs;	×
451	}	×
452
453	return SymEngine::null;	×
454	}	22✔
455
456	Expression maximum_new(	29✔
457	const Expression expr, const SymbolSet& parameters, const Assumptions& assumptions, const size_t depth, bool tight
458	) {
459	// End of recursion: fail
460	if (depth > MAX_DEPTH) {	29!
461	return SymEngine::null;	×
462	}
463	if (SymEngine::is_a<SymEngine::NaN>(*expr)) {	29!
464	return SymEngine::null;	×
465	}
466	if (SymEngine::is_a<SymEngine::Infty>(*expr)) {	29!
467	return SymEngine::null;	×
468	}
469	// End of recursion: success
470	if (SymEngine::is_a<SymEngine::Integer>(*expr)) {	29✔
471	return expr;	10✔
472	}
473	if (SymEngine::is_a<SymEngine::Symbol>(*expr)) {	19✔
474	auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(expr);	15✔
475	if (parameters.find(sym) != parameters.end()) {	15!
476	return sym;	7✔
477	}
478	}	15✔
479
480	if (SymEngine::is_a<symbolic::ZExtI64Function>(*expr)) {	12!
NEW 481	auto zext = SymEngine::rcp_static_cast<const symbolic::ZExtI64Function>(expr);	×
NEW 482	auto max_arg = maximum_new(zext->get_args()[0], parameters, assumptions, depth + 1, tight);	×
NEW 483	if (max_arg == SymEngine::null) {	×
NEW 484	return SymEngine::null;	×
485	} else {
NEW 486	return symbolic::zext_i64(max_arg);	×
487	}
NEW 488	}	×
489
490	// Symbol
491	if (SymEngine::is_a<SymEngine::Symbol>(*expr)) {	12✔
492	auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(expr);	8✔
493	if (assumptions.find(sym) != assumptions.end()) {	8!
494	if (tight) {	8!
495	if (assumptions.at(sym).tight_upper_bound().is_null()) {	8!
496	return SymEngine::null;	1!
497	}
498	return maximum_new(assumptions.at(sym).tight_upper_bound(), parameters, assumptions, depth + 1, tight);	7!
499	}
500	symbolic::Expression new_ub = SymEngine::null;	×
501	for (auto& ub : assumptions.at(sym).upper_bounds()) {	×
502	auto new_max = maximum_new(ub, parameters, assumptions, depth + 1, tight);	×
503	if (new_max.is_null()) {	×
504	continue;	×
505	}
506	if (new_ub.is_null()) {	×
507	new_ub = new_max;	×
508	continue;	×
509	}
510	new_ub = symbolic::min(new_ub, new_max);	×
511	}	×
512	return new_ub;	×
513	}	×
514	return SymEngine::null;	×
515	}	8✔
516
517	// Mul
518	if (SymEngine::is_a<SymEngine::Mul>(*expr)) {	4!
519	auto mul = SymEngine::rcp_static_cast<const SymEngine::Mul>(expr);	×
520	const auto& args = mul->get_args();	×
521	size_t n = args.size();	×
522
523	std::vector<std::pair<Expression, Expression>> bounds;	×
524	bounds.reserve(n);	×
525
526	for (const auto& arg : args) {	×
527	Expression min_val = minimum_new(arg, parameters, assumptions, depth + 1, tight);	×
528	Expression max_val = maximum_new(arg, parameters, assumptions, depth + 1, tight);	×
529
530	if (min_val == SymEngine::null \|\| max_val == SymEngine::null) {	×
531	return SymEngine::null;	×
532	}
533	bounds.emplace_back(min_val, max_val);	×
534	}	×
535
536	// Iterate over 2^n combinations
537	Expression max_product = SymEngine::null;	×
538	const size_t total_combinations = 1ULL << n;	×
539
540	for (size_t mask = 0; mask < total_combinations; ++mask) {	×
541	Expression product = SymEngine::integer(1);	×
542	for (size_t i = 0; i < n; ++i) {	×
543	const auto& bound = bounds[i];	×
544	Expression val = (mask & (1ULL << i)) ? bound.second : bound.first;	×
545	product = symbolic::mul(product, val);	×
546	}	×
547	if (max_product == SymEngine::null) {	×
548	max_product = product;	×
549	} else {	×
550	max_product = symbolic::max(max_product, product);	×
551	}
552	}	×
553
554	return max_product;	×
555	}	×
556
557	// Add
558	if (SymEngine::is_a<SymEngine::Add>(*expr)) {	4!
559	auto add = SymEngine::rcp_static_cast<const SymEngine::Add>(expr);	4✔
560	const auto& args = add->get_args();	4!
561	Expression ubs = SymEngine::null;	4!
562	for (const auto& arg : args) {	12✔
563	auto ub = maximum_new(arg, parameters, assumptions, depth + 1, tight);	8!
564	if (ub == SymEngine::null) {	8!
565	return SymEngine::null;	×
566	}
567	if (ubs == SymEngine::null) {	8!
568	ubs = ub;	4!
569	} else {	4✔
570	ubs = symbolic::add(ubs, ub);	4!
571	}
572	}	8!
573	return ubs;	4✔
574	}	4✔
575
576	// Max
577	if (SymEngine::is_a<SymEngine::Max>(*expr)) {	×
578	auto args = SymEngine::rcp_dynamic_cast<const SymEngine::Max>(expr)->get_args();	×
579	Expression ubs = SymEngine::null;	×
580	for (const auto& arg : args) {	×
581	auto ub = maximum_new(arg, parameters, assumptions, depth + 1, tight);	×
582	if (ub == SymEngine::null) {	×
583	return SymEngine::null;	×
584	}
585	if (ubs == SymEngine::null) {	×
586	ubs = ub;	×
587	} else {	×
588	ubs = symbolic::max(ubs, ub);	×
589	}
590	}	×
591	return ubs;	×
592	}	×
593
594	// Min
595	if (SymEngine::is_a<SymEngine::Min>(*expr)) {	×
596	auto args = SymEngine::rcp_dynamic_cast<const SymEngine::Min>(expr)->get_args();	×
597	Expression ubs = SymEngine::null;	×
598	for (const auto& arg : args) {	×
599	auto ub = maximum_new(arg, parameters, assumptions, depth + 1, tight);	×
600	if (ub == SymEngine::null) {	×
601	return SymEngine::null;	×
602	}
603	if (ubs == SymEngine::null) {	×
604	ubs = ub;	×
605	} else {	×
606	ubs = symbolic::max(ubs, ub);	×
607	}
608	}	×
609	return ubs;	×
610	}	×
611
612	return SymEngine::null;	×
613	}	29✔
614
615	Expression minimum_new(const Expression expr, const SymbolSet& parameters, const Assumptions& assumptions, bool tight) {	14✔
616	return minimum_new(expr, parameters, assumptions, 0, tight);	14!
617	}	×
618
619	Expression maximum_new(const Expression expr, const SymbolSet& parameters, const Assumptions& assumptions, bool tight) {	14✔
620	return maximum_new(expr, parameters, assumptions, 0, tight);	14!
621	}	×
622
623	} // namespace symbolic
624	} // namespace sdfg

daisytuner / sdfglib / 20320588678

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