mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-10 21:20:52 +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 Nikolaj Bjorner
parent c575aa3973
commit f8562380d6
2 changed files with 71 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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();
}