16069945621

Committed 04 Jul 2025 08:56AM UTC coverage: 64.375% (-0.2%) from 64.606%

Build # 16069945621

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #137 from daisytuner/clang-format

runs clang-format on codebase

Run Details

609 of 827 new or added lines in 63 files covered. (73.64%)

46 existing lines in 30 files now uncovered.

8578 of 13325 relevant lines covered (64.38%)

177.24 hits per line

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

50.0

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

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

daisytuner / sdfglib / 16069945621

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