mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

Fix pdd_manager::degree(PDD, unsigned) and add unit tests (#5155)

Browse source 
* Fix pdd_manager::degree(PDD, unsigned) and add unit tests

* Another marking opportunity
This commit is contained in:
Jakob Rath 2021-04-07 21:32:35 +02:00 • committed by GitHub
parent 276756dce9
commit c85db571ab
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 71 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1005,28 +1005,32 @@ namespace dd {
unsigned pdd_manager::degree(PDD p, unsigned v) {
init_mark();
unsigned level_v = level(v);
unsigned level_v = m_var2level[v];
unsigned max_d = 0, d = 0;
m_todo.push_back(p);
while (!m_todo.empty()) {
PDD r = m_todo.back();
if (is_marked(r))
if (is_marked(r))
m_todo.pop_back();
else if (is_val(r))
m_todo.pop_back();
else if (level(r) < level_v)
m_todo.pop_back();
else if (level(r) == level_v) {
d = 1;
while (!is_val(hi(r)) && level(hi(r)) == level_v) {
d = 0;
do {
++d;
set_mark(r);
r = hi(r);
}
} while (!is_val(r) && level(r) == level_v);
max_d = std::max(d, max_d);
m_todo.pop_back();
}
else
m_todo.push_back(lo(r)).push_back(hi(r));
else {
set_mark(r);
m_todo.pop_back();
m_todo.push_back(lo(r)).push_back(hi(r));
}
}
return max_d;
}

60
src/test/pdd.cpp
View file

@ -322,6 +322,65 @@ public :
SASSERT(!(2*a*b + 3*b + 2).is_never_zero());
}
static void degree_of_variables() {
std::cout << "degree of variables\n";
pdd_manager m(4, pdd_manager::mod2N_e, 3);
unsigned va = 0;
unsigned vb = 1;
unsigned vc = 2;
pdd a = m.mk_var(va);
pdd b = m.mk_var(vb);
pdd c = m.mk_var(vc);
SASSERT(a.var() == va);
SASSERT(b.var() == vb);
SASSERT(a.degree(va) == 1);
SASSERT(a.degree(vb) == 0);
SASSERT(a.degree(vc) == 0);
SASSERT(c.degree(vc) == 1);
SASSERT(c.degree(vb) == 0);
SASSERT(c.degree(va) == 0);
{
pdd p = a * a * a;
SASSERT(p.degree(va) == 3);
SASSERT(p.degree(vb) == 0);
}
{
pdd p = b * a;
SASSERT(p.degree(va) == 1);
SASSERT(p.degree(vb) == 1);
SASSERT(p.degree(vc) == 0);
}
{
pdd p = (a*a*b + b*a*b + b + a*c)*a + b*b*c;
SASSERT(p.degree(va) == 3);
SASSERT(p.degree(vb) == 2);
SASSERT(p.degree(vc) == 1);
}
{
// check that skipping marked nodes works (1)
pdd p = b*a + c*a*a*a;
SASSERT(p.degree(va) == 3);
}
{
// check that skipping marked nodes works (2)
pdd p = (b+c)*(a*a*a);
SASSERT(p.degree(va) == 3);
}
{
// check that skipping marked nodes works (3)
pdd p = a*a*a*b*b*b*c + a*a*a*b*b*b;
SASSERT(p.degree(va) == 3);
}
}
};
}
@ -336,4 +395,5 @@ void tst_pdd() {
dd::test::order();
dd::test::order_lm();
dd::test::mod4_operations();
dd::test::degree_of_variables();
}