15684905458

Committed 16 Jun 2025 03:21PM UTC coverage: 64.973% (+0.004%) from 64.969%

Build # 15684905458

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #83 from daisytuner/cnf-fix

checks for relational in cnf analysis

Run Details

12 of 20 new or added lines in 1 file covered. (60.0%)

1 existing line in 1 file now uncovered.

8069 of 12419 relevant lines covered (64.97%)

118.94 hits per line

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

56.79

/src/symbolic/conjunctive_normal_form.cpp

#include "sdfg/symbolic/conjunctive_normal_form.h"

#include <symengine/logic.h>

#include "sdfg/symbolic/extreme_values.h"
#include "sdfg/symbolic/symbolic.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: Comparison with boolean literals
    if (SymEngine::is_a<SymEngine::Equality>(*cond) ||
        SymEngine::is_a<SymEngine::Unequality>(*cond)) {
        auto expr = SymEngine::rcp_static_cast<const SymEngine::Relational>(cond);
        auto arg1 = expr->get_arg1();
        auto arg2 = expr->get_arg2();
        if (!SymEngine::is_a_Relational(*arg1) && !SymEngine::is_a_Relational(*arg2)) {
            return {{cond}};
        }

        if (SymEngine::is_a<SymEngine::Equality>(*expr)) {
            if (symbolic::is_true(arg1)) {
                return conjunctive_normal_form(
                    SymEngine::rcp_static_cast<const SymEngine::Boolean>(arg2));
            } else if (symbolic::is_true(arg2)) {
                return conjunctive_normal_form(
                    SymEngine::rcp_static_cast<const SymEngine::Boolean>(arg1));
            } else if (symbolic::is_false(arg1)) {
                return conjunctive_normal_form(
                    symbolic::Not(SymEngine::rcp_static_cast<const SymEngine::Boolean>(arg2)));
            } else if (symbolic::is_false(arg2)) {
                return conjunctive_normal_form(
                    symbolic::Not(SymEngine::rcp_static_cast<const SymEngine::Boolean>(arg1)));
            }
        } else if (SymEngine::is_a<SymEngine::Unequality>(*expr)) {
            if (symbolic::is_true(arg1)) {
                return conjunctive_normal_form(
                    symbolic::Not(SymEngine::rcp_static_cast<const SymEngine::Boolean>(arg2)));
            } else if (symbolic::is_true(arg2)) {
                return conjunctive_normal_form(
                    symbolic::Not(SymEngine::rcp_static_cast<const SymEngine::Boolean>(arg1)));
            } else if (symbolic::is_false(arg1)) {
                return conjunctive_normal_form(
                    SymEngine::rcp_static_cast<const SymEngine::Boolean>(arg2));
            } else if (symbolic::is_false(arg2)) {
                return conjunctive_normal_form(
                    SymEngine::rcp_static_cast<const SymEngine::Boolean>(arg1));
            }
        }

        return {{cond}};  // Return the condition as a single clause
    }

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

daisytuner / sdfglib / 15684905458

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