mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

use manager reference as before

Browse source
This commit is contained in:
Jakob Rath 2023-07-08 20:06:24 +02:00
parent a339cd1aff
commit 397acd0089
1 changed files with 13 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1934,23 +1934,23 @@ namespace dd {
std::ostream& operator<<(std::ostream& out, pdd const& b) { return b.display(out); }
void pdd_iterator::next() {
auto& m = m_pdd.m;
auto& m = m_pdd.manager();
while (!m_nodes.empty()) {
auto& p = m_nodes.back();
if (p.first && !m->is_val(p.second)) {
if (p.first && !m.is_val(p.second)) {
p.first = false;
m_mono.vars.pop_back();
unsigned n = m->lo(p.second);
if (m->is_val(n) && m->val(n).is_zero()) {
unsigned n = m.lo(p.second);
if (m.is_val(n) && m.val(n).is_zero()) {
m_nodes.pop_back();
continue;
}
while (!m->is_val(n)) {
while (!m.is_val(n)) {
m_nodes.push_back(std::make_pair(true, n));
m_mono.vars.push_back(m->var(n));
n = m->hi(n);
m_mono.vars.push_back(m.var(n));
n = m.hi(n);
}
m_mono.coeff = m->val(n);
m_mono.coeff = m.val(n);
break;
}
else {
@ -1961,13 +1961,13 @@ namespace dd {
void pdd_iterator::first() {
unsigned n = m_pdd.root;
auto& m = m_pdd.m;
while (!m->is_val(n)) {
auto& m = m_pdd.manager();
while (!m.is_val(n)) {
m_nodes.push_back(std::make_pair(true, n));
m_mono.vars.push_back(m->var(n));
n = m->hi(n);
m_mono.vars.push_back(m.var(n));
n = m.hi(n);
}
m_mono.coeff = m->val(n);
m_mono.coeff = m.val(n);
}
pdd_iterator pdd::begin() const { return pdd_iterator(*this, true); }