15612270835

Committed 12 Jun 2025 01:44PM UTC coverage: 60.871% (-0.8%) from 61.71%

Build # 15612270835

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #68 from daisytuner/loop-types

refactors symbolic analysis into polynomials, extreme values and cnf

Run Details

638 of 862 new or added lines in 24 files covered. (74.01%)

334 existing lines in 20 files now uncovered.

6571 of 10795 relevant lines covered (60.87%)

100.35 hits per line

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

53.97

/src/symbolic/conjunctive_normal_form.cpp

#include "sdfg/symbolic/conjunctive_normal_form.h"

#include "sdfg/symbolic/extreme_values.h"

namespace sdfg {
namespace symbolic {

CNF distribute_or(const CNF& C, const CNF& D) {
    CNF 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;
}

CNF 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();
        CNF 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();

        CNF 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}};
}

Expression upper_bound(const CNF& cnf, const Symbol& indvar) {
    std::vector<Expression> candidates;

    for (const auto& clause : cnf) {
        for (const auto& literal : clause) {
            // Comparison: indvar < expr
            if (SymEngine::is_a<SymEngine::StrictLessThan>(*literal)) {
                auto lt = SymEngine::rcp_static_cast<const SymEngine::StrictLessThan>(literal);
                if (symbolic::eq(lt->get_arg1(), indvar) && !uses(lt->get_arg2(), indvar)) {
                    auto ub = symbolic::sub(lt->get_arg2(), symbolic::one());
                    candidates.push_back(ub);
                }
            }
            // Comparison: indvar <= expr
            else if (SymEngine::is_a<SymEngine::LessThan>(*literal)) {
                auto le = SymEngine::rcp_static_cast<const SymEngine::LessThan>(literal);
                if (symbolic::eq(le->get_arg1(), indvar) && !uses(le->get_arg2(), indvar)) {
                    candidates.push_back(le->get_arg2());
                }
            }
            // Comparison: indvar == expr
            else if (SymEngine::is_a<SymEngine::Equality>(*literal)) {
                auto eq = SymEngine::rcp_static_cast<const SymEngine::Equality>(literal);
                if (symbolic::eq(eq->get_arg1(), indvar) && !uses(eq->get_arg2(), indvar)) {
                    candidates.push_back(eq->get_arg2());
                }
            }
        }
    }

    if (candidates.empty()) {
        return SymEngine::null;
    }

    // Return the smallest upper bound across all candidate constraints
    Expression result = candidates[0];
    for (size_t i = 1; i < candidates.size(); ++i) {
        result = symbolic::min(result, candidates[i]);
    }

    return result;
}

}  // namespace symbolic
}  // namespace sdfg

1	#include "sdfg/symbolic/conjunctive_normal_form.h"
2
3	#include "sdfg/symbolic/extreme_values.h"
4
5	namespace sdfg {
6	namespace symbolic {
7
8	CNF distribute_or(const CNF& C, const CNF& D) {	4✔
9	CNF out;	4✔
10	for (auto& c : C)	9✔
11	for (auto& d : D) {	12✔
12	auto clause = c;	7✔
13	clause.insert(clause.end(), d.begin(), d.end());	7✔
14	out.emplace_back(std::move(clause));	7✔
15	}	7✔
16	return out;	4✔
17	}	4✔
18
19	CNF conjunctive_normal_form(const Condition& cond) {	131✔
20	// Goal: Convert a condition into ANDs of ORs
21
22	// Case: Not
23	// Push negation inwards
24	if (SymEngine::is_a<SymEngine::Not>(*cond)) {	131✔
NEW 25	auto not_ = SymEngine::rcp_static_cast<const SymEngine::Not>(cond);	×
NEW 26	auto arg = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(not_->get_arg());	×
27
28	// Case: Not(not)
NEW 29	if (SymEngine::is_a<SymEngine::Not>(*arg)) {	×
NEW 30	auto not_not_ = SymEngine::rcp_static_cast<const SymEngine::Not>(arg);	×
NEW 31	auto arg_ = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(not_not_->get_arg());	×
NEW 32	return conjunctive_normal_form(arg_);	×
NEW 33	}	×
34
35	// Case: Not(And) (De Morgan)
NEW 36	if (SymEngine::is_a<SymEngine::And>(*arg)) {	×
NEW 37	auto and_ = SymEngine::rcp_static_cast<const SymEngine::And>(arg);	×
NEW 38	auto args = and_->get_args();	×
NEW 39	if (args.size() != 2) {	×
NEW 40	throw CNFException("Non-binary And encountered");	×
41	}
NEW 42	auto arg0 = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(args[0]);	×
NEW 43	auto arg1 = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(args[1]);	×
NEW 44	auto de_morgan = symbolic::Or(symbolic::Not(arg0), symbolic::Not(arg1));	×
NEW 45	return conjunctive_normal_form(de_morgan);	×
NEW 46	}	×
47
48	// Case: Not(Or) (De Morgan)
NEW 49	if (SymEngine::is_a<SymEngine::Or>(*arg)) {	×
NEW 50	auto or_ = SymEngine::rcp_static_cast<const SymEngine::Or>(arg);	×
NEW 51	auto args = or_->get_args();	×
NEW 52	if (args.size() != 2) {	×
NEW 53	throw CNFException("Non-binary Or encountered");	×
54	}
NEW 55	auto arg0 = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(args[0]);	×
NEW 56	auto arg1 = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(args[1]);	×
NEW 57	auto de_morgan = symbolic::And(symbolic::Not(arg0), symbolic::Not(arg1));	×
NEW 58	return conjunctive_normal_form(de_morgan);	×
NEW 59	}	×
60
61	// Case: Comparisons
NEW 62	if (SymEngine::is_a<SymEngine::Equality>(*arg)) {	×
NEW 63	auto eq_ = SymEngine::rcp_static_cast<const SymEngine::Equality>(arg);	×
NEW 64	auto lhs = eq_->get_arg1();	×
NEW 65	auto rhs = eq_->get_arg2();	×
NEW 66	return conjunctive_normal_form(symbolic::Ne(lhs, rhs));	×
NEW 67	}	×
NEW 68	if (SymEngine::is_a<SymEngine::Unequality>(*arg)) {	×
NEW 69	auto ne_ = SymEngine::rcp_static_cast<const SymEngine::Unequality>(arg);	×
NEW 70	auto lhs = ne_->get_arg1();	×
NEW 71	auto rhs = ne_->get_arg2();	×
NEW 72	return conjunctive_normal_form(symbolic::Eq(lhs, rhs));	×
NEW 73	}	×
NEW 74	if (SymEngine::is_a<SymEngine::LessThan>(*arg)) {	×
NEW 75	auto lt_ = SymEngine::rcp_static_cast<const SymEngine::LessThan>(arg);	×
NEW 76	auto lhs = lt_->get_arg1();	×
NEW 77	auto rhs = lt_->get_arg2();	×
NEW 78	return conjunctive_normal_form(symbolic::Gt(lhs, rhs));	×
NEW 79	}	×
NEW 80	if (SymEngine::is_a<SymEngine::StrictLessThan>(*arg)) {	×
NEW 81	auto lt_ = SymEngine::rcp_static_cast<const SymEngine::StrictLessThan>(arg);	×
NEW 82	auto lhs = lt_->get_arg1();	×
NEW 83	auto rhs = lt_->get_arg2();	×
NEW 84	return conjunctive_normal_form(symbolic::Ge(lhs, rhs));	×
NEW 85	}	×
86
NEW 87	throw CNFException("Unknown Not encountered");	×
NEW 88	}	×
89
90	// Case: And
91	if (SymEngine::is_a<SymEngine::And>(*cond)) {	131✔
92	// CNF(A ∧ B) = CNF(A) ∪ CNF(B)
93	auto and_ = SymEngine::rcp_static_cast<const SymEngine::And>(cond);	7✔
94	auto args = and_->get_args();	7✔
95	CNF result;	7✔
96	for (auto& arg : args) {	21✔
97	auto arg_ = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(arg);	14✔
98	auto cnf = conjunctive_normal_form(arg_);	14✔
99	for (auto& clause : cnf) {	28✔
100	result.push_back(clause);	14✔
101	}
102	}	14✔
103	return result;	7✔
104	}	7✔
105
106	// Case: Or
107	if (SymEngine::is_a<SymEngine::Or>(*cond)) {	124✔
108	// CNF(A ∨ B) = distribute_or( CNF(A), CNF(B) )
109	auto or_ = SymEngine::rcp_static_cast<const SymEngine::Or>(cond);	4✔
110	auto args = or_->get_args();	4✔
111
112	CNF result;	4✔
113	auto arg_0 = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(args[0]);	4✔
114	auto cnf_0 = conjunctive_normal_form(arg_0);	4✔
115	for (auto& clause : cnf_0) {	9✔
116	result.push_back(clause);	5✔
117	}
118	for (size_t i = 1; i < args.size(); i++) {	8✔
119	auto arg = args[i];	4✔
120	auto arg_ = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(arg);	4✔
121	auto cnf = conjunctive_normal_form(arg_);	4✔
122	result = distribute_or(result, cnf);	4✔
123	}	4✔
124	return result;	4✔
125	}	4✔
126
127	// Case: Literal
128	return {{cond}};	120✔
129	}	131✔
130
131	Expression upper_bound(const CNF& cnf, const Symbol& indvar) {	102✔
132	std::vector<Expression> candidates;	102✔
133
134	for (const auto& clause : cnf) {	207✔
135	for (const auto& literal : clause) {	212✔
136	// Comparison: indvar < expr
137	if (SymEngine::is_a<SymEngine::StrictLessThan>(*literal)) {	107✔
138	auto lt = SymEngine::rcp_static_cast<const SymEngine::StrictLessThan>(literal);	95✔
139	if (symbolic::eq(lt->get_arg1(), indvar) && !uses(lt->get_arg2(), indvar)) {	95✔
140	auto ub = symbolic::sub(lt->get_arg2(), symbolic::one());	95✔
141	candidates.push_back(ub);	95✔
142	}	95✔
143	}	95✔
144	// Comparison: indvar <= expr
145	else if (SymEngine::is_a<SymEngine::LessThan>(*literal)) {	12✔
146	auto le = SymEngine::rcp_static_cast<const SymEngine::LessThan>(literal);	2✔
147	if (symbolic::eq(le->get_arg1(), indvar) && !uses(le->get_arg2(), indvar)) {	2✔
148	candidates.push_back(le->get_arg2());	2✔
149	}	2✔
150	}	2✔
151	// Comparison: indvar == expr
152	else if (SymEngine::is_a<SymEngine::Equality>(*literal)) {	10✔
NEW 153	auto eq = SymEngine::rcp_static_cast<const SymEngine::Equality>(literal);	×
NEW 154	if (symbolic::eq(eq->get_arg1(), indvar) && !uses(eq->get_arg2(), indvar)) {	×
NEW 155	candidates.push_back(eq->get_arg2());	×
NEW 156	}	×
NEW 157	}	×
158	}
159	}
160
161	if (candidates.empty()) {	102✔
162	return SymEngine::null;	6✔
163	}
164
165	// Return the smallest upper bound across all candidate constraints
166	Expression result = candidates[0];	96✔
167	for (size_t i = 1; i < candidates.size(); ++i) {	97✔
168	result = symbolic::min(result, candidates[i]);	1✔
169	}	1✔
170
171	return result;	96✔
172	}	198✔
173
174	} // namespace symbolic
175	} // namespace sdfg

daisytuner / sdfglib / 15612270835

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