15656007340

Committed 14 Jun 2025 08:51PM UTC coverage: 13.234% (-49.9%) from 63.144%

Build # 15656007340

Build Type

Pull #76

github

Committed by

web-flow

Commit Message

Merge 9586c8161 into 413c53212

Pull Request Pull Request #76: New Loop Dependency Analysis

Run Details

361 of 465 new or added lines in 7 files covered. (77.63%)

6215 existing lines in 110 files now uncovered.

1612 of 12181 relevant lines covered (13.23%)

13.64 hits per line

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

17.46

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

daisytuner / sdfglib / 15656007340

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