20770413849

Committed 06 Jan 2026 10:50PM UTC coverage: 62.168% (+21.4%) from 40.764%

Build # 20770413849

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #433 from daisytuner/clang-coverage

updates clang coverage flags

Run Details

14988 of 24109 relevant lines covered (62.17%)

88.57 hits per line

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

51.88

/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) {	8✔
12	CNF out;	8✔
13	for (auto& c : C)	8✔
14	for (auto& d : D) {	15✔
15	auto clause = c;	15✔
16	clause.insert(clause.end(), d.begin(), d.end());	15✔
17	out.emplace_back(std::move(clause));	15✔
18	}	15✔
19	return out;	8✔
20	}	8✔
21
22	CNF conjunctive_normal_form(const Condition cond) {	275✔
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)) {	275✔
27	auto expr = SymEngine::rcp_static_cast<const SymEngine::Relational>(cond);	41✔
28	auto arg1 = expr->get_arg1();	41✔
29	auto arg2 = expr->get_arg2();	41✔
30	if (!SymEngine::is_a_Relational(arg1) && !SymEngine::is_a_Relational(arg2)) {	41✔
31	return {{cond}};	36✔
32	}	36✔
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✔
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	);	2✔
42	} else if (symbolic::is_false(arg2)) {	2✔
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)) {	3✔
47	if (symbolic::is_true(arg1)) {	2✔
48	return conjunctive_normal_form(symbolic::Not(SymEngine::rcp_static_cast<const SymEngine::Boolean>(arg2))	1✔
49	);	1✔
50	} else if (symbolic::is_true(arg2)) {	1✔
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✔
55	} else if (symbolic::is_false(arg2)) {	1✔
56	return conjunctive_normal_form(SymEngine::rcp_static_cast<const SymEngine::Boolean>(arg1));	×
57	}	×
58	}	2✔
59
60	return {{cond}}; // Return the condition as a single clause	×
61	}	5✔
62
63	// Case: Not
64	// Push negation inwards
65	if (SymEngine::is_a<SymEngine::Not>(*cond)) {	234✔
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)) {	234✔
133	// CNF(A ∧ B) = CNF(A) ∪ CNF(B)
134	auto and_ = SymEngine::rcp_static_cast<const SymEngine::And>(cond);	20✔
135	auto args = and_->get_args();	20✔
136	CNF result;	20✔
137	for (auto& arg : args) {	40✔
138	auto arg_ = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(arg);	40✔
139	auto cnf = conjunctive_normal_form(arg_);	40✔
140	for (auto& clause : cnf) {	40✔
141	result.push_back(clause);	40✔
142	}	40✔
143	}	40✔
144	return result;	20✔
145	}	20✔
146
147	// Case: Or
148	if (SymEngine::is_a<SymEngine::Or>(*cond)) {	214✔
149	// CNF(A ∨ B) = distribute_or( CNF(A), CNF(B) )
150	auto or_ = SymEngine::rcp_static_cast<const SymEngine::Or>(cond);	7✔
151	auto args = or_->get_args();	7✔
152
153	CNF result;	7✔
154	auto arg_0 = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(args[0]);	7✔
155	auto cnf_0 = conjunctive_normal_form(arg_0);	7✔
156	for (auto& clause : cnf_0) {	9✔
157	result.push_back(clause);	9✔
158	}	9✔
159	for (size_t i = 1; i < args.size(); i++) {	15✔
160	auto arg = args[i];	8✔
161	auto arg_ = SymEngine::rcp_dynamic_cast<const SymEngine::Boolean>(arg);	8✔
162	auto cnf = conjunctive_normal_form(arg_);	8✔
163	result = distribute_or(result, cnf);	8✔
164	}	8✔
165	return result;	7✔
166	}	7✔
167
168	// Case: Literal
169	return {{cond}};	207✔
170	}	214✔
171
172	} // namespace symbolic
173	} // namespace sdfg

daisytuner / sdfglib / 20770413849

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