mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-21 16:16:38 +00:00
Code Activity

pdd_linear_iterator

Browse source
This commit is contained in:
Jakob Rath 2023-07-08 20:08:03 +02:00
parent 397acd0089
commit 28810e55a0
2 changed files with 65 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1148,6 +1148,7 @@ namespace dd {
unsigned pdd_manager::max_pow2_divisor(PDD p) {
init_mark();
unsigned min_j = UINT_MAX;
SASSERT(m_todo.empty());
m_todo.push_back(p);
while (!m_todo.empty()) {
PDD r = m_todo.back();
@ -1986,5 +1987,32 @@ namespace dd {
return out;
}
void pdd_linear_iterator::first() {
m_next = m_pdd.root;
next();
}
}
void pdd_linear_iterator::next() {
SASSERT(m_next != pdd_manager::null_pdd);
auto& m = m_pdd.manager();
while (!m.is_val(m_next)) {
unsigned const var = m.var(m_next);
rational const val = m.offset(m.hi(m_next));
m_next = m.lo(m_next);
if (!val.is_zero()) {
m_mono = {val, var};
return;
}
}
m_next = pdd_manager::null_pdd;
}
pdd_linear_iterator pdd::pdd_linear_monomials::begin() const {
return pdd_linear_iterator(m_pdd, true);
}
pdd_linear_iterator pdd::pdd_linear_monomials::end() const {
return pdd_linear_iterator(m_pdd, false);
}
} // namespace dd

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

@ -45,6 +45,7 @@ namespace dd {
class pdd;
class pdd_manager;
class pdd_iterator;
class pdd_linear_iterator;
class pdd_manager {
public:
@ -53,13 +54,14 @@ namespace dd {
friend test;
friend pdd;
friend pdd_iterator;
friend pdd_linear_iterator;
typedef unsigned PDD;
typedef vector<std::pair<rational,unsigned_vector>> monomials_t;
const PDD null_pdd = UINT_MAX;
const PDD zero_pdd = 0;
const PDD one_pdd = 1;
static constexpr PDD null_pdd = UINT_MAX;
static constexpr PDD zero_pdd = 0;
static constexpr PDD one_pdd = 1;
enum pdd_op {
pdd_add_op = 2,
@ -400,6 +402,7 @@ namespace dd {
friend test;
friend class pdd_manager;
friend class pdd_iterator;
friend class pdd_linear_iterator;
unsigned root;
pdd_manager* m;
pdd(unsigned root, pdd_manager& pm): root(root), m(&pm) { m->inc_ref(root); }
@ -501,6 +504,16 @@ namespace dd {
pdd_iterator begin() const;
pdd_iterator end() const;
class pdd_linear_monomials {
friend class pdd;
pdd const& m_pdd;
pdd_linear_monomials(pdd const& p): m_pdd(p) {}
public:
pdd_linear_iterator begin() const;
pdd_linear_iterator end() const;
};
pdd_linear_monomials linear_monomials() const { return pdd_linear_monomials(*this); }
pdd_manager& manager() const { return *m; }
};
@ -558,6 +571,26 @@ namespace dd {
bool operator!=(pdd_iterator const& other) const { return m_nodes != other.m_nodes; }
};
class pdd_linear_iterator {
friend class pdd::pdd_linear_monomials;
pdd m_pdd;
std::pair<rational, unsigned> m_mono;
pdd_manager::PDD m_next = pdd_manager::null_pdd;
pdd_linear_iterator(pdd const& p, bool at_start): m_pdd(p) { if (at_start) first(); }
void first();
void next();
public:
using value_type = std::pair<rational, unsigned>; // coefficient and variable
using reference = value_type const&;
using pointer = value_type const*;
reference operator*() const { return m_mono; }
pointer operator->() const { return &m_mono; }
pdd_linear_iterator& operator++() { next(); return *this; }
pdd_linear_iterator operator++(int) { auto tmp = *this; next(); return tmp; }
bool operator==(pdd_linear_iterator const& other) const { return m_next == other.m_next; }
bool operator!=(pdd_linear_iterator const& other) const { return m_next != other.m_next; }
};
class val_pp {
pdd_manager const& m;
rational const& val;