mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-03 11:25:40 +00:00
Code Activity

Fix pdd_iterator for non-zero constant polynomials

Browse source
This commit is contained in:
Jakob Rath 2023-09-28 11:42:08 +02:00
parent 78b5db3ce7
commit e96f69e76c
3 changed files with 47 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/dd/dd_pdd.cpp
View file

@ -1969,6 +1969,9 @@ namespace dd {
n = m.hi(n); n = m.hi(n);
} }
m_mono.coeff = m.val(n); m_mono.coeff = m.val(n);
// if m_pdd is constant and non-zero, the iterator should return a single monomial
if (m_nodes.empty() && !m_mono.coeff.is_zero())
m_nodes.push_back(std::make_pair(false, n));
} }
pdd_iterator pdd::begin() const { return pdd_iterator(*this, true); } pdd_iterator pdd::begin() const { return pdd_iterator(*this, true); }

2
src/math/dd/dd_pdd.h
View file

@ -570,7 +570,7 @@ namespace dd {
pdd_iterator& operator++() { next(); return *this; } pdd_iterator& operator++() { next(); return *this; }
pdd_iterator operator++(int) { auto tmp = *this; next(); return tmp; } pdd_iterator operator++(int) { auto tmp = *this; next(); return tmp; }
bool operator==(pdd_iterator const& other) const { return m_nodes == other.m_nodes; } bool operator==(pdd_iterator const& other) const { return m_nodes == other.m_nodes; }
bool operator!=(pdd_iterator const& other) const { return m_nodes != other.m_nodes; } bool operator!=(pdd_iterator const& other) const { return !operator==(other); }
}; };
class pdd_linear_iterator { class pdd_linear_iterator {

48
src/test/pdd.cpp
View file

@ -153,12 +153,49 @@ public:
pdd b = m.mk_var(1); pdd b = m.mk_var(1);
pdd c = m.mk_var(2); pdd c = m.mk_var(2);
pdd d = m.mk_var(3); pdd d = m.mk_var(3);
pdd p = (a + b)*(c + 3*d) + 2;
std::cout << p << "\n"; auto const check = [](unsigned const expected_num_monomials, pdd const& p) {
for (auto const& m : p) { unsigned count = 0;
std::cout << m << "\n"; std::cout << p << "\n";
} for (auto const& m : p) {
std::cout << " " << m << "\n";
++count;
}
VERIFY_EQ(expected_num_monomials, count);
};
check(9, (a + b + 2)*(c + 3*d + 5) + 2);
check(5, (a + b)*(c + 3*d) + 2);
check(1, a);
check(2, a + 5);
check(1, m.mk_val(5));
check(0, m.mk_val(0));
} }
static void linear_iterator() {
std::cout << "test linear iterator\n";
pdd_manager m(4);
pdd a = m.mk_var(0);
pdd b = m.mk_var(1);
pdd c = m.mk_var(2);
pdd d = m.mk_var(3);
pdd p = (a + b + 2)*(c + 3*d + 5) + 2;
std::cout << p << "\n";
for (auto const& m : p.linear_monomials())
std::cout << " " << m << "\n";
std::cout << a << "\n";
for (auto const& m : a.linear_monomials())
std::cout << " " << m << "\n";
pdd one = m.mk_val(5);
std::cout << one << "\n";
for (auto const& m : one.linear_monomials())
std::cout << " " << m << "\n";
pdd zero = m.mk_val(0);
std::cout << zero << "\n";
for (auto const& m : zero.linear_monomials())
std::cout << " " << m << "\n";
}
static void order() { static void order() {
std::cout << "order\n"; std::cout << "order\n";
pdd_manager m(4); pdd_manager m(4);
@ -693,6 +730,7 @@ void tst_pdd() {
dd::test::canonize(); dd::test::canonize();
dd::test::reset(); dd::test::reset();
dd::test::iterator(); dd::test::iterator();
dd::test::linear_iterator();
dd::test::order(); dd::test::order();
dd::test::order_lm(); dd::test::order_lm();
dd::test::mod4_operations(); dd::test::mod4_operations();