15494289007

Committed 06 Jun 2025 03:36PM UTC coverage: 57.304% (-0.4%) from 57.704%

Build # 15494289007

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #60 from daisytuner/kernels

removes kernel node in favor of function types

Run Details

78 of 99 new or added lines in 11 files covered. (78.79%)

91 existing lines in 14 files now uncovered.

7583 of 13233 relevant lines covered (57.3%)

116.04 hits per line

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

66.77

/src/symbolic/analysis.cpp

#include "sdfg/symbolic/analysis.h"

#include "sdfg/symbolic/symbolic.h"
#include "symengine/infinity.h"
#include "symengine/polys/basic_conversions.h"
#include "symengine/visitor.h"

namespace sdfg {
namespace symbolic {

Polynomial polynomial(const Expression& expr, const Symbol& symbol) {
    try {
        return SymEngine::from_basic<SymEngine::UExprPoly>(expr, symbol, true);
    } catch (SymEngine::SymEngineException& e) {
        return SymEngine::null;
    }
};

MultiPolynomial multi_polynomial(const Expression& expr, SymbolicVector& symbols) {
    try {
        SymbolicSet gens;
        for (auto& symbol : symbols) {
            gens.insert(symbol);
        }
        return SymEngine::from_basic<SymEngine::MExprPoly>(expr, gens);
    } catch (SymEngine::SymEngineException& e) {
        return SymEngine::null;
    }
};

AffineCoefficients affine_coefficients(MultiPolynomial& poly, SymbolicVector& symbols) {
    AffineCoefficients coefficients;
    for (auto& symbol : symbols) {
        coefficients[symbol] = 0;
    }
    coefficients[symbolic::symbol("__daisy_constant__")] = 0;

    auto& D = poly->get_poly().get_dict();
    for (auto& [exponents, coeff] : D) {
        // Check if coeff is an integer
        if (!SymEngine::is_a<SymEngine::Integer>(coeff)) {
            return {};
        }
        auto coeff_value =
            SymEngine::rcp_dynamic_cast<const SymEngine::Integer>(coeff.get_basic())->as_int();

        // Check if sum of exponents is <= 1
        symbolic::Symbol hot_symbol = symbolic::symbol("__daisy_constant__");
        unsigned total_deg = 0;
        for (size_t i = 0; i < exponents.size(); i++) {
            auto& e = exponents[i];
            if (e > 0) {
                hot_symbol = symbols[i];
            }
            total_deg += e;
        }
        if (total_deg > 1) {
            return {};
        }

        // Add coefficient to corresponding symbol
        coefficients[hot_symbol] = coefficients[hot_symbol] + coeff_value;
    }

    return coefficients;
}

std::vector<std::vector<Condition>> distribute_or(const std::vector<std::vector<Condition>>& C,
                                                  const std::vector<std::vector<Condition>>& D) {
    std::vector<std::vector<Condition>> out;
    for (auto& c : C)
        for (auto& d : D) {
            auto clause = c;
            clause.insert(clause.end(), d.begin(), d.end());
            out.emplace_back(std::move(clause));
        }
    return out;
}

std::vector<std::vector<Condition>> conjunctive_normal_form(const Condition& cond) {
    // Goal: Convert a condition into ANDs of ORs

    // Case: Not
    // Push negation inwards
    if (SymEngine::is_a<SymEngine::Not>(*cond)) {
        auto not_ = SymEngine::rcp_static_cast<const SymEngine::Not>(cond);
        auto arg = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(not_->get_arg());

        // Case: Not(not)
        if (SymEngine::is_a<SymEngine::Not>(*arg)) {
            auto not_not_ = SymEngine::rcp_static_cast<const SymEngine::Not>(arg);
            auto arg_ = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(not_not_->get_arg());
            return conjunctive_normal_form(arg_);
        }

        // Case: Not(And) (De Morgan)
        if (SymEngine::is_a<SymEngine::And>(*arg)) {
            auto and_ = SymEngine::rcp_static_cast<const SymEngine::And>(arg);
            auto args = and_->get_args();
            if (args.size() != 2) {
                throw CNFException("Non-binary And encountered");
            }
            auto arg0 = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(args[0]);
            auto arg1 = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(args[1]);
            auto de_morgan = symbolic::Or(symbolic::Not(arg0), symbolic::Not(arg1));
            return conjunctive_normal_form(de_morgan);
        }

        // Case: Not(Or) (De Morgan)
        if (SymEngine::is_a<SymEngine::Or>(*arg)) {
            auto or_ = SymEngine::rcp_static_cast<const SymEngine::Or>(arg);
            auto args = or_->get_args();
            if (args.size() != 2) {
                throw CNFException("Non-binary Or encountered");
            }
            auto arg0 = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(args[0]);
            auto arg1 = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(args[1]);
            auto de_morgan = symbolic::And(symbolic::Not(arg0), symbolic::Not(arg1));
            return conjunctive_normal_form(de_morgan);
        }

        // Case: Comparisons
        if (SymEngine::is_a<SymEngine::Equality>(*arg)) {
            auto eq_ = SymEngine::rcp_static_cast<const SymEngine::Equality>(arg);
            auto lhs = eq_->get_arg1();
            auto rhs = eq_->get_arg2();
            return conjunctive_normal_form(symbolic::Ne(lhs, rhs));
        }
        if (SymEngine::is_a<SymEngine::Unequality>(*arg)) {
            auto ne_ = SymEngine::rcp_static_cast<const SymEngine::Unequality>(arg);
            auto lhs = ne_->get_arg1();
            auto rhs = ne_->get_arg2();
            return conjunctive_normal_form(symbolic::Eq(lhs, rhs));
        }
        if (SymEngine::is_a<SymEngine::LessThan>(*arg)) {
            auto lt_ = SymEngine::rcp_static_cast<const SymEngine::LessThan>(arg);
            auto lhs = lt_->get_arg1();
            auto rhs = lt_->get_arg2();
            return conjunctive_normal_form(symbolic::Gt(lhs, rhs));
        }
        if (SymEngine::is_a<SymEngine::StrictLessThan>(*arg)) {
            auto lt_ = SymEngine::rcp_static_cast<const SymEngine::StrictLessThan>(arg);
            auto lhs = lt_->get_arg1();
            auto rhs = lt_->get_arg2();
            return conjunctive_normal_form(symbolic::Ge(lhs, rhs));
        }

        throw CNFException("Unknown Not encountered");
    }

    // Case: And
    if (SymEngine::is_a<SymEngine::And>(*cond)) {
        // CNF(A ∧ B) = CNF(A)  ∪  CNF(B)
        auto and_ = SymEngine::rcp_static_cast<const SymEngine::And>(cond);
        auto args = and_->get_args();
        std::vector<std::vector<Condition>> result;
        for (auto& arg : args) {
            auto arg_ = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(arg);
            auto cnf = conjunctive_normal_form(arg_);
            for (auto& clause : cnf) {
                result.push_back(clause);
            }
        }
        return result;
    }

    // Case: Or
    if (SymEngine::is_a<SymEngine::Or>(*cond)) {
        // CNF(A ∨ B) = distribute_or( CNF(A), CNF(B) )
        auto or_ = SymEngine::rcp_static_cast<const SymEngine::Or>(cond);
        auto args = or_->get_args();

        std::vector<std::vector<Condition>> result;
        auto arg_0 = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(args[0]);
        auto cnf_0 = conjunctive_normal_form(arg_0);
        for (auto& clause : cnf_0) {
            result.push_back(clause);
        }
        for (size_t i = 1; i < args.size(); i++) {
            auto arg = args[i];
            auto arg_ = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(arg);
            auto cnf = conjunctive_normal_form(arg_);
            result = distribute_or(result, cnf);
        }
        return result;
    }

    // Case: Literal
    return {{cond}};
}

Affine affine(const Expression& expr, const Symbol& symbol) {
    auto poly = symbolic::polynomial(expr, symbol);
    if (poly == SymEngine::null || poly->get_degree() > 1) {
        return {SymEngine::null, SymEngine::null};
    }
    if (poly->get_degree() == 0) {
        return {symbolic::integer(0), poly->get_coeff(0)};
    }
    return {poly->get_coeff(1), poly->get_coeff(0)};
};

Sign strict_monotonicity_affine(const Expression& func, const Symbol& symbol) {
    return strict_monotonicity_affine(func, symbol, {});
};

Sign strict_monotonicity_affine(const Expression& func, const symbolic::Assumptions& assumptions) {
    Sign sign = Sign::NONE;
    bool initialized = false;

    for (auto atom : atoms(func)) {
        auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(atom);
        if (!initialized) {
            sign = strict_monotonicity_affine(func, sym, assumptions);
            if (sign == Sign::NONE) {
                return Sign::NONE;
            }
            initialized = true;
            continue;
        }
        if (sign != strict_monotonicity_affine(func, sym, assumptions)) {
            return Sign::NONE;
        }
    }
    return sign;
};

Sign strict_monotonicity_affine(const Expression& func, const Symbol& symbol,
                                const symbolic::Assumptions& assumptions) {
    auto aff = symbolic::affine(func, symbol);
    if (aff.first == SymEngine::null) {
        return Sign::NONE;
    }

    if (SymEngine::is_a<SymEngine::Integer>(*aff.first)) {
        auto coeff = SymEngine::rcp_static_cast<const SymEngine::Integer>(aff.first);
        if (coeff->as_int() > 0) {
            return Sign::POSITIVE;
        } else if (coeff->as_int() < 0) {
            return Sign::NEGATIVE;
        } else {
            return Sign::NONE;
        }
    } else if (SymEngine::is_a<SymEngine::Symbol>(*aff.first)) {
        auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(aff.first);
        if (assumptions.find(sym) != assumptions.end()) {
            auto& a = assumptions.at(sym);
            if (a.is_positive()) {
                return Sign::POSITIVE;
            } else if (a.is_negative()) {
                return Sign::NEGATIVE;
            } else {
                return Sign::NONE;
            }
        }
    }

    return Sign::NONE;
};

Sign strict_monotonicity(const Expression& func, const Symbol& symbol) {
    return strict_monotonicity(func, symbol, {});
};

Sign strict_monotonicity(const Expression& func, const symbolic::Assumptions& assumptions) {
    if (symbolic::strict_monotonicity_affine(func, assumptions) != Sign::NONE) {
        return symbolic::strict_monotonicity_affine(func, assumptions);
    }
    return Sign::NONE;
};

Sign strict_monotonicity(const Expression& func, const Symbol& symbol,
                         const symbolic::Assumptions& assumptions) {
    if (symbolic::strict_monotonicity_affine(func, symbol, assumptions) != Sign::NONE) {
        return symbolic::strict_monotonicity_affine(func, symbol, assumptions);
    }

    return Sign::NONE;
};

Sign strict_monotonicity(const Expression& func) {
    for (auto& sym : symbolic::atoms(func)) {
        auto sym_ = SymEngine::rcp_static_cast<const SymEngine::Symbol>(sym);
        if (symbolic::strict_monotonicity(func, sym_) != Sign::POSITIVE) {
            return Sign::NONE;
        }
    }
    return Sign::POSITIVE;
};

bool contiguity_affine(const Expression& func, const Symbol& symbol) {
    return contiguity_affine(func, symbol, {});
};

bool contiguity_affine(const Expression& func, const Symbol& symbol,
                       const symbolic::Assumptions& assumptions) {
    auto aff = symbolic::affine(func, symbol);
    if (aff.first == SymEngine::null) {
        return false;
    }

    if (SymEngine::is_a<SymEngine::Integer>(*aff.first)) {
        auto coeff = SymEngine::rcp_static_cast<const SymEngine::Integer>(aff.first);
        if (coeff->as_int() == 1) {
            return true;
        }
    } else if (SymEngine::is_a<SymEngine::Symbol>(*aff.first)) {
        auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(aff.first);
        if (assumptions.find(sym) != assumptions.end()) {
            auto& a = assumptions.at(sym);
            if (symbolic::eq(a.lower_bound(), symbolic::integer(1)) &&
                symbolic::eq(a.upper_bound(), symbolic::integer(1))) {
                return true;
            }
        }
    }

    return false;
};

bool contiguity(const Expression& func, const Symbol& symbol) {
    return contiguity(func, symbol, {});
}

bool contiguity(const Expression& func, const Symbol& symbol,
                const symbolic::Assumptions& assumptions) {
    if (symbolic::contiguity_affine(func, symbol, assumptions)) {
        return true;
    }

    return false;
};

Expression inverse(const Symbol& lhs, const Expression& rhs) {
    if (!symbolic::uses(rhs, lhs)) {
        return SymEngine::null;
    }

    if (SymEngine::is_a<SymEngine::Add>(*rhs)) {
        auto add = SymEngine::rcp_static_cast<const SymEngine::Add>(rhs);
        auto arg_0 = add->get_args()[0];
        auto arg_1 = add->get_args()[1];
        if (!symbolic::eq(arg_0, lhs)) {
            std::swap(arg_0, arg_1);
        }
        if (!symbolic::eq(arg_0, lhs)) {
            return SymEngine::null;
        }
        if (!SymEngine::is_a<SymEngine::Integer>(*arg_1)) {
            return SymEngine::null;
        }
        return symbolic::sub(lhs, arg_1);
    } else if (SymEngine::is_a<SymEngine::Mul>(*rhs)) {
        auto mul = SymEngine::rcp_static_cast<const SymEngine::Mul>(rhs);
        auto arg_0 = mul->get_args()[0];
        auto arg_1 = mul->get_args()[1];
        if (!symbolic::eq(arg_0, lhs)) {
            std::swap(arg_0, arg_1);
        }
        if (!symbolic::eq(arg_0, lhs)) {
            return SymEngine::null;
        }
        if (!SymEngine::is_a<SymEngine::Integer>(*arg_1)) {
            return SymEngine::null;
        }
        return symbolic::div(lhs, arg_1);
    }

    return SymEngine::null;
};

bool contains_infinity(const Expression& expr) {
    if (SymEngine::atoms<const SymEngine::Infty>(*expr).empty()) {
        return false;
    }
    return true;
};

Expression lower_bound_analysis(const symbolic::Expression& expr,
                                symbolic::Assumptions& assumptions) {
    if (SymEngine::is_a<SymEngine::Integer>(*expr)) {
        return SymEngine::rcp_static_cast<const SymEngine::Integer>(expr);
    }
    if (SymEngine::is_a<SymEngine::Symbol>(*expr)) {
        auto symbol = SymEngine::rcp_static_cast<const SymEngine::Symbol>(expr);
        if (assumptions.find(symbol) != assumptions.end()) {
            return assumptions[symbol].lower_bound();
        }
        return symbolic::infty(-1);
    }

    // Attempt analysis via monotonicity
    auto sign = symbolic::strict_monotonicity(expr, assumptions);
    if (sign == symbolic::Sign::NONE) {
        return symbolic::infty(-1);
    }

    // Subsitute all symbols accordingly
    symbolic::Expression lower_bound = expr;
    for (auto atom : symbolic::atoms(expr)) {
        auto symbol = SymEngine::rcp_static_cast<const SymEngine::Symbol>(atom);
        if (sign == symbolic::Sign::NEGATIVE) {
            auto ub = assumptions[symbol].upper_bound();
            lower_bound = symbolic::subs(lower_bound, symbol, ub);
        } else {  // if (sign == symbolic::Sign::POSITIVE)
            auto lb = assumptions[symbol].lower_bound();
            lower_bound = symbolic::subs(lower_bound, symbol, lb);
        }
    }

    // End of recursion
    if (contains_infinity(lower_bound)) {
        return symbolic::infty(-1);
    } else {
        if (symbolic::atoms(lower_bound).empty()) {
            return lower_bound;
        } else {
            auto new_lb = lower_bound_analysis(lower_bound, assumptions);
            return new_lb;
        }
    }
};

Expression upper_bound_analysis(const symbolic::Expression& expr,
                                symbolic::Assumptions& assumptions) {
    if (SymEngine::is_a<SymEngine::Integer>(*expr)) {
        return SymEngine::rcp_static_cast<const SymEngine::Integer>(expr);
    }
    if (SymEngine::is_a<SymEngine::Symbol>(*expr)) {
        auto symbol = SymEngine::rcp_static_cast<const SymEngine::Symbol>(expr);
        if (assumptions.find(symbol) != assumptions.end()) {
            return assumptions[symbol].upper_bound();
        }
        return symbolic::infty(1);
    }

    // Attempt analysis via monotonicity
    auto sign = symbolic::strict_monotonicity(expr, assumptions);
    if (sign == symbolic::Sign::NONE) {
        return symbolic::infty(1);
    }

    // Subsitute all symbols accordingly
    symbolic::Expression upper_bound = expr;
    for (auto atom : symbolic::atoms(expr)) {
        auto symbol = SymEngine::rcp_static_cast<const SymEngine::Symbol>(atom);
        if (sign == symbolic::Sign::NEGATIVE) {
            auto lb = assumptions[symbol].lower_bound();
            upper_bound = symbolic::subs(upper_bound, symbol, lb);
        } else {  // if (sign == symbolic::Sign::POSITIVE)
            auto ub = assumptions[symbol].upper_bound();
            upper_bound = symbolic::subs(upper_bound, symbol, ub);
        }
    }

    // End of recursion
    if (contains_infinity(upper_bound)) {
        return symbolic::infty(1);
    } else {
        if (symbolic::atoms(upper_bound).empty()) {
            return upper_bound;
        } else {
            auto new_ub = upper_bound_analysis(upper_bound, assumptions);
            return new_ub;
        }
    }
};
}  // namespace symbolic
}  // namespace sdfg

1	#include "sdfg/symbolic/analysis.h"
2
3	#include "sdfg/symbolic/symbolic.h"
4	#include "symengine/infinity.h"
5	#include "symengine/polys/basic_conversions.h"
6	#include "symengine/visitor.h"
7
8	namespace sdfg {
9	namespace symbolic {
10
11	Polynomial polynomial(const Expression& expr, const Symbol& symbol) {	379✔
12	try {
13	return SymEngine::from_basic<SymEngine::UExprPoly>(expr, symbol, true);	379✔
14	} catch (SymEngine::SymEngineException& e) {	3✔
15	return SymEngine::null;	3✔
16	}	3✔
17	};	382✔
18
19	MultiPolynomial multi_polynomial(const Expression& expr, SymbolicVector& symbols) {	2✔
20	try {
21	SymbolicSet gens;	2✔
22	for (auto& symbol : symbols) {	6✔
23	gens.insert(symbol);	4✔
24	}
25	return SymEngine::from_basic<SymEngine::MExprPoly>(expr, gens);	2✔
26	} catch (SymEngine::SymEngineException& e) {	2✔
27	return SymEngine::null;	×
28	}	×
29	};	2✔
30
31	AffineCoefficients affine_coefficients(MultiPolynomial& poly, SymbolicVector& symbols) {	2✔
32	AffineCoefficients coefficients;	2✔
33	for (auto& symbol : symbols) {	6✔
34	coefficients[symbol] = 0;	4✔
35	}
36	coefficients[symbolic::symbol("__daisy_constant__")] = 0;	2✔
37
38	auto& D = poly->get_poly().get_dict();	2✔
39	for (auto& [exponents, coeff] : D) {	17✔
40	// Check if coeff is an integer
41	if (!SymEngine::is_a<SymEngine::Integer>(coeff)) {	4✔
42	return {};	1✔
43	}
44	auto coeff_value =	3✔
45	SymEngine::rcp_dynamic_cast<const SymEngine::Integer>(coeff.get_basic())->as_int();	3✔
46
47	// Check if sum of exponents is <= 1
48	symbolic::Symbol hot_symbol = symbolic::symbol("__daisy_constant__");	3✔
49	unsigned total_deg = 0;	3✔
50	for (size_t i = 0; i < exponents.size(); i++) {	9✔
51	auto& e = exponents[i];	6✔
52	if (e > 0) {	6✔
53	hot_symbol = symbols[i];	2✔
54	}	2✔
55	total_deg += e;	6✔
56	}	6✔
57	if (total_deg > 1) {	3✔
58	return {};	×
59	}
60
61	// Add coefficient to corresponding symbol
62	coefficients[hot_symbol] = coefficients[hot_symbol] + coeff_value;	3✔
63	}	3✔
64
65	return coefficients;	1✔
66	}	2✔
67
68	std::vector<std::vector<Condition>> distribute_or(const std::vector<std::vector<Condition>>& C,	1✔
69	const std::vector<std::vector<Condition>>& D) {
70	std::vector<std::vector<Condition>> out;	1✔
71	for (auto& c : C)	3✔
72	for (auto& d : D) {	6✔
73	auto clause = c;	4✔
74	clause.insert(clause.end(), d.begin(), d.end());	4✔
75	out.emplace_back(std::move(clause));	4✔
76	}	4✔
77	return out;	1✔
78	}	1✔
79
80	std::vector<std::vector<Condition>> conjunctive_normal_form(const Condition& cond) {	7✔
81	// Goal: Convert a condition into ANDs of ORs
82
83	// Case: Not
84	// Push negation inwards
85	if (SymEngine::is_a<SymEngine::Not>(*cond)) {	7✔
86	auto not_ = SymEngine::rcp_static_cast<const SymEngine::Not>(cond);	×
87	auto arg = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(not_->get_arg());	×
88
89	// Case: Not(not)
90	if (SymEngine::is_a<SymEngine::Not>(*arg)) {	×
91	auto not_not_ = SymEngine::rcp_static_cast<const SymEngine::Not>(arg);	×
92	auto arg_ = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(not_not_->get_arg());	×
93	return conjunctive_normal_form(arg_);	×
94	}	×
95
96	// Case: Not(And) (De Morgan)
97	if (SymEngine::is_a<SymEngine::And>(*arg)) {	×
98	auto and_ = SymEngine::rcp_static_cast<const SymEngine::And>(arg);	×
99	auto args = and_->get_args();	×
100	if (args.size() != 2) {	×
101	throw CNFException("Non-binary And encountered");	×
102	}
103	auto arg0 = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(args[0]);	×
104	auto arg1 = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(args[1]);	×
105	auto de_morgan = symbolic::Or(symbolic::Not(arg0), symbolic::Not(arg1));	×
106	return conjunctive_normal_form(de_morgan);	×
107	}	×
108
109	// Case: Not(Or) (De Morgan)
110	if (SymEngine::is_a<SymEngine::Or>(*arg)) {	×
111	auto or_ = SymEngine::rcp_static_cast<const SymEngine::Or>(arg);	×
112	auto args = or_->get_args();	×
113	if (args.size() != 2) {	×
114	throw CNFException("Non-binary Or encountered");	×
115	}
116	auto arg0 = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(args[0]);	×
117	auto arg1 = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(args[1]);	×
118	auto de_morgan = symbolic::And(symbolic::Not(arg0), symbolic::Not(arg1));	×
119	return conjunctive_normal_form(de_morgan);	×
120	}	×
121
122	// Case: Comparisons
123	if (SymEngine::is_a<SymEngine::Equality>(*arg)) {	×
124	auto eq_ = SymEngine::rcp_static_cast<const SymEngine::Equality>(arg);	×
125	auto lhs = eq_->get_arg1();	×
126	auto rhs = eq_->get_arg2();	×
127	return conjunctive_normal_form(symbolic::Ne(lhs, rhs));	×
128	}	×
129	if (SymEngine::is_a<SymEngine::Unequality>(*arg)) {	×
130	auto ne_ = SymEngine::rcp_static_cast<const SymEngine::Unequality>(arg);	×
131	auto lhs = ne_->get_arg1();	×
132	auto rhs = ne_->get_arg2();	×
133	return conjunctive_normal_form(symbolic::Eq(lhs, rhs));	×
134	}	×
135	if (SymEngine::is_a<SymEngine::LessThan>(*arg)) {	×
136	auto lt_ = SymEngine::rcp_static_cast<const SymEngine::LessThan>(arg);	×
137	auto lhs = lt_->get_arg1();	×
138	auto rhs = lt_->get_arg2();	×
139	return conjunctive_normal_form(symbolic::Gt(lhs, rhs));	×
140	}	×
141	if (SymEngine::is_a<SymEngine::StrictLessThan>(*arg)) {	×
142	auto lt_ = SymEngine::rcp_static_cast<const SymEngine::StrictLessThan>(arg);	×
143	auto lhs = lt_->get_arg1();	×
144	auto rhs = lt_->get_arg2();	×
145	return conjunctive_normal_form(symbolic::Ge(lhs, rhs));	×
146	}	×
147
148	throw CNFException("Unknown Not encountered");	×
149	}	×
150
151	// Case: And
152	if (SymEngine::is_a<SymEngine::And>(*cond)) {	7✔
153	// CNF(A ∧ B) = CNF(A) ∪ CNF(B)
154	auto and_ = SymEngine::rcp_static_cast<const SymEngine::And>(cond);	2✔
155	auto args = and_->get_args();	2✔
156	std::vector<std::vector<Condition>> result;	2✔
157	for (auto& arg : args) {	6✔
158	auto arg_ = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(arg);	4✔
159	auto cnf = conjunctive_normal_form(arg_);	4✔
160	for (auto& clause : cnf) {	8✔
161	result.push_back(clause);	4✔
162	}
163	}	4✔
164	return result;	2✔
165	}	2✔
166
167	// Case: Or
168	if (SymEngine::is_a<SymEngine::Or>(*cond)) {	5✔
169	// CNF(A ∨ B) = distribute_or( CNF(A), CNF(B) )
170	auto or_ = SymEngine::rcp_static_cast<const SymEngine::Or>(cond);	1✔
171	auto args = or_->get_args();	1✔
172
173	std::vector<std::vector<Condition>> result;	1✔
174	auto arg_0 = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(args[0]);	1✔
175	auto cnf_0 = conjunctive_normal_form(arg_0);	1✔
176	for (auto& clause : cnf_0) {	3✔
177	result.push_back(clause);	2✔
178	}
179	for (size_t i = 1; i < args.size(); i++) {	2✔
180	auto arg = args[i];	1✔
181	auto arg_ = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(arg);	1✔
182	auto cnf = conjunctive_normal_form(arg_);	1✔
183	result = distribute_or(result, cnf);	1✔
184	}	1✔
185	return result;	1✔
186	}	1✔
187
188	// Case: Literal
189	return {{cond}};	4✔
190	}	7✔
191
192	Affine affine(const Expression& expr, const Symbol& symbol) {	374✔
193	auto poly = symbolic::polynomial(expr, symbol);	374✔
194	if (poly == SymEngine::null \|\| poly->get_degree() > 1) {	374✔
195	return {SymEngine::null, SymEngine::null};	3✔
196	}
197	if (poly->get_degree() == 0) {	371✔
198	return {symbolic::integer(0), poly->get_coeff(0)};	2✔
199	}
200	return {poly->get_coeff(1), poly->get_coeff(0)};	369✔
201	};	374✔
202
203	Sign strict_monotonicity_affine(const Expression& func, const Symbol& symbol) {	4✔
204	return strict_monotonicity_affine(func, symbol, {});	4✔
205	};	×
206
207	Sign strict_monotonicity_affine(const Expression& func, const symbolic::Assumptions& assumptions) {	17✔
208	Sign sign = Sign::NONE;	17✔
209	bool initialized = false;	17✔
210
211	for (auto atom : atoms(func)) {	58✔
212	auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(atom);	41✔
213	if (!initialized) {	41✔
214	sign = strict_monotonicity_affine(func, sym, assumptions);	17✔
215	if (sign == Sign::NONE) {	17✔
216	return Sign::NONE;	×
217	}
218	initialized = true;	17✔
219	continue;	17✔
220	}
221	if (sign != strict_monotonicity_affine(func, sym, assumptions)) {	24✔
222	return Sign::NONE;	11✔
223	}
224	}	41✔
225	return sign;	6✔
226	};	17✔
227
228	Sign strict_monotonicity_affine(const Expression& func, const Symbol& symbol,	361✔
229	const symbolic::Assumptions& assumptions) {
230	auto aff = symbolic::affine(func, symbol);	361✔
231	if (aff.first == SymEngine::null) {	361✔
232	return Sign::NONE;	1✔
233	}
234
235	if (SymEngine::is_a<SymEngine::Integer>(*aff.first)) {	360✔
236	auto coeff = SymEngine::rcp_static_cast<const SymEngine::Integer>(aff.first);	331✔
237	if (coeff->as_int() > 0) {	331✔
238	return Sign::POSITIVE;	329✔
239	} else if (coeff->as_int() < 0) {	2✔
240	return Sign::NEGATIVE;	1✔
241	} else {
242	return Sign::NONE;	1✔
243	}
244	} else if (SymEngine::is_a<SymEngine::Symbol>(*aff.first)) {	360✔
245	auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(aff.first);	29✔
246	if (assumptions.find(sym) != assumptions.end()) {	29✔
247	auto& a = assumptions.at(sym);	22✔
248	if (a.is_positive()) {	22✔
249	return Sign::POSITIVE;	15✔
250	} else if (a.is_negative()) {	7✔
251	return Sign::NEGATIVE;	2✔
252	} else {
253	return Sign::NONE;	5✔
254	}
255	}
256	}	29✔
257
258	return Sign::NONE;	7✔
259	};	361✔
260
261	Sign strict_monotonicity(const Expression& func, const Symbol& symbol) {	156✔
262	return strict_monotonicity(func, symbol, {});	156✔
263	};	×
264
265	Sign strict_monotonicity(const Expression& func, const symbolic::Assumptions& assumptions) {	6✔
266	if (symbolic::strict_monotonicity_affine(func, assumptions) != Sign::NONE) {	6✔
267	return symbolic::strict_monotonicity_affine(func, assumptions);	2✔
268	}
269	return Sign::NONE;	4✔
270	};	6✔
271
272	Sign strict_monotonicity(const Expression& func, const Symbol& symbol,	156✔
273	const symbolic::Assumptions& assumptions) {
274	if (symbolic::strict_monotonicity_affine(func, symbol, assumptions) != Sign::NONE) {	156✔
275	return symbolic::strict_monotonicity_affine(func, symbol, assumptions);	155✔
276	}
277
278	return Sign::NONE;	1✔
279	};	156✔
280
281	Sign strict_monotonicity(const Expression& func) {	×
282	for (auto& sym : symbolic::atoms(func)) {	×
283	auto sym_ = SymEngine::rcp_static_cast<const SymEngine::Symbol>(sym);	×
284	if (symbolic::strict_monotonicity(func, sym_) != Sign::POSITIVE) {	×
285	return Sign::NONE;	×
286	}
287	}	×
288	return Sign::POSITIVE;	×
289	};	×
290
291	bool contiguity_affine(const Expression& func, const Symbol& symbol) {	2✔
292	return contiguity_affine(func, symbol, {});	2✔
293	};	×
294
295	bool contiguity_affine(const Expression& func, const Symbol& symbol,	9✔
296	const symbolic::Assumptions& assumptions) {
297	auto aff = symbolic::affine(func, symbol);	9✔
298	if (aff.first == SymEngine::null) {	9✔
299	return false;	1✔
300	}
301
302	if (SymEngine::is_a<SymEngine::Integer>(*aff.first)) {	8✔
303	auto coeff = SymEngine::rcp_static_cast<const SymEngine::Integer>(aff.first);	6✔
304	if (coeff->as_int() == 1) {	6✔
305	return true;	5✔
306	}
307	} else if (SymEngine::is_a<SymEngine::Symbol>(*aff.first)) {	8✔
308	auto sym = SymEngine::rcp_static_cast<const SymEngine::Symbol>(aff.first);	2✔
309	if (assumptions.find(sym) != assumptions.end()) {	2✔
310	auto& a = assumptions.at(sym);	2✔
311	if (symbolic::eq(a.lower_bound(), symbolic::integer(1)) &&	3✔
312	symbolic::eq(a.upper_bound(), symbolic::integer(1))) {	1✔
313	return true;	1✔
314	}
315	}	1✔
316	}	2✔
317
318	return false;	2✔
319	};	9✔
320
321	bool contiguity(const Expression& func, const Symbol& symbol) {	5✔
322	return contiguity(func, symbol, {});	5✔
323	}	×
324
325	bool contiguity(const Expression& func, const Symbol& symbol,	5✔
326	const symbolic::Assumptions& assumptions) {
327	if (symbolic::contiguity_affine(func, symbol, assumptions)) {	5✔
328	return true;	4✔
329	}
330
331	return false;	1✔
332	};	5✔
333
334	Expression inverse(const Symbol& lhs, const Expression& rhs) {	1✔
335	if (!symbolic::uses(rhs, lhs)) {	1✔
336	return SymEngine::null;	1✔
337	}
338
339	if (SymEngine::is_a<SymEngine::Add>(*rhs)) {	×
340	auto add = SymEngine::rcp_static_cast<const SymEngine::Add>(rhs);	×
341	auto arg_0 = add->get_args()[0];	×
342	auto arg_1 = add->get_args()[1];	×
343	if (!symbolic::eq(arg_0, lhs)) {	×
344	std::swap(arg_0, arg_1);	×
345	}	×
346	if (!symbolic::eq(arg_0, lhs)) {	×
347	return SymEngine::null;	×
348	}
349	if (!SymEngine::is_a<SymEngine::Integer>(*arg_1)) {	×
350	return SymEngine::null;	×
351	}
352	return symbolic::sub(lhs, arg_1);	×
353	} else if (SymEngine::is_a<SymEngine::Mul>(*rhs)) {	×
354	auto mul = SymEngine::rcp_static_cast<const SymEngine::Mul>(rhs);	×
355	auto arg_0 = mul->get_args()[0];	×
356	auto arg_1 = mul->get_args()[1];	×
357	if (!symbolic::eq(arg_0, lhs)) {	×
358	std::swap(arg_0, arg_1);	×
359	}	×
360	if (!symbolic::eq(arg_0, lhs)) {	×
361	return SymEngine::null;	×
362	}
363	if (!SymEngine::is_a<SymEngine::Integer>(*arg_1)) {	×
364	return SymEngine::null;	×
365	}
366	return symbolic::div(lhs, arg_1);	×
367	}	×
368
369	return SymEngine::null;	×
370	};	1✔
371
372	bool contains_infinity(const Expression& expr) {	24✔
373	if (SymEngine::atoms<const SymEngine::Infty>(*expr).empty()) {	24✔
374	return false;	4✔
375	}
376	return true;	20✔
377	};	24✔
378
379	Expression lower_bound_analysis(const symbolic::Expression& expr,	5✔
380	symbolic::Assumptions& assumptions) {
381	if (SymEngine::is_a<SymEngine::Integer>(*expr)) {	5✔
382	return SymEngine::rcp_static_cast<const SymEngine::Integer>(expr);	1✔
383	}
384	if (SymEngine::is_a<SymEngine::Symbol>(*expr)) {	4✔
385	auto symbol = SymEngine::rcp_static_cast<const SymEngine::Symbol>(expr);	1✔
386	if (assumptions.find(symbol) != assumptions.end()) {	1✔
387	return assumptions[symbol].lower_bound();	1✔
388	}
UNCOV 389	return symbolic::infty(-1);	×
390	}	1✔
391
392	// Attempt analysis via monotonicity
393	auto sign = symbolic::strict_monotonicity(expr, assumptions);	3✔
394	if (sign == symbolic::Sign::NONE) {	3✔
395	return symbolic::infty(-1);	2✔
396	}
397
398	// Subsitute all symbols accordingly
399	symbolic::Expression lower_bound = expr;	1✔
400	for (auto atom : symbolic::atoms(expr)) {	4✔
401	auto symbol = SymEngine::rcp_static_cast<const SymEngine::Symbol>(atom);	3✔
402	if (sign == symbolic::Sign::NEGATIVE) {	3✔
403	auto ub = assumptions[symbol].upper_bound();	×
404	lower_bound = symbolic::subs(lower_bound, symbol, ub);	×
405	} else { // if (sign == symbolic::Sign::POSITIVE)	×
406	auto lb = assumptions[symbol].lower_bound();	3✔
407	lower_bound = symbolic::subs(lower_bound, symbol, lb);	3✔
408	}	3✔
409	}	3✔
410
411	// End of recursion
412	if (contains_infinity(lower_bound)) {	1✔
413	return symbolic::infty(-1);	×
414	} else {
415	if (symbolic::atoms(lower_bound).empty()) {	1✔
416	return lower_bound;	1✔
417	} else {
418	auto new_lb = lower_bound_analysis(lower_bound, assumptions);	×
419	return new_lb;	×
420	}	×
421	}
422	};	5✔
423
424	Expression upper_bound_analysis(const symbolic::Expression& expr,	5✔
425	symbolic::Assumptions& assumptions) {
426	if (SymEngine::is_a<SymEngine::Integer>(*expr)) {	5✔
427	return SymEngine::rcp_static_cast<const SymEngine::Integer>(expr);	1✔
428	}
429	if (SymEngine::is_a<SymEngine::Symbol>(*expr)) {	4✔
430	auto symbol = SymEngine::rcp_static_cast<const SymEngine::Symbol>(expr);	1✔
431	if (assumptions.find(symbol) != assumptions.end()) {	1✔
432	return assumptions[symbol].upper_bound();	1✔
433	}
UNCOV 434	return symbolic::infty(1);	×
435	}	1✔
436
437	// Attempt analysis via monotonicity
438	auto sign = symbolic::strict_monotonicity(expr, assumptions);	3✔
439	if (sign == symbolic::Sign::NONE) {	3✔
440	return symbolic::infty(1);	2✔
441	}
442
443	// Subsitute all symbols accordingly
444	symbolic::Expression upper_bound = expr;	1✔
445	for (auto atom : symbolic::atoms(expr)) {	4✔
446	auto symbol = SymEngine::rcp_static_cast<const SymEngine::Symbol>(atom);	3✔
447	if (sign == symbolic::Sign::NEGATIVE) {	3✔
448	auto lb = assumptions[symbol].lower_bound();	×
449	upper_bound = symbolic::subs(upper_bound, symbol, lb);	×
450	} else { // if (sign == symbolic::Sign::POSITIVE)	×
451	auto ub = assumptions[symbol].upper_bound();	3✔
452	upper_bound = symbolic::subs(upper_bound, symbol, ub);	3✔
453	}	3✔
454	}	3✔
455
456	// End of recursion
457	if (contains_infinity(upper_bound)) {	1✔
458	return symbolic::infty(1);	×
459	} else {
460	if (symbolic::atoms(upper_bound).empty()) {	1✔
461	return upper_bound;	1✔
462	} else {
463	auto new_ub = upper_bound_analysis(upper_bound, assumptions);	×
464	return new_ub;	×
465	}	×
466	}
467	};	5✔
468	} // namespace symbolic
469	} // namespace sdfg

daisytuner / sdfglib / 15494289007

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