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

Test and fix PDD subst_val (#5185)

Browse source
This commit is contained in:
Jakob Rath 2021-04-15 17:35:46 +02:00 • committed by GitHub
parent bb7754a767
commit 7067fc16ae
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 51 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -240,7 +240,7 @@ namespace dd {
break;
case pdd_subst_val_op:
while (!is_val(q) && !is_val(p)) {
if (level(p) < level(q)) q = lo(q);
if (level(p) < level(q)) q = hi(q);
else break;
}
if (is_val(p) || is_val(q)) return p;

50
src/test/pdd.cpp
View file

@ -509,6 +509,55 @@ public :
SASSERT((3*a*b).pow(3) == 27*a*a*a*b*b*b);
}
static void subst_val() {
std::cout << "subst_val\n";
pdd_manager m(4, pdd_manager::mod2N_e, 2);
unsigned const va = 0;
unsigned const vb = 1;
unsigned const vc = 2;
unsigned const vd = 3;
pdd const a = m.mk_var(va);
pdd const b = m.mk_var(vb);
pdd const c = m.mk_var(vc);
pdd const d = m.mk_var(vd);
{
pdd const p = 2*a + b + 1;
SASSERT(p.subst_val(va, rational(0)) == b + 1);
}
{
pdd const p = a + 2*b;
SASSERT(p.subst_val(va, rational(0)) == 2*b);
SASSERT(p.subst_val(va, rational(2)) == 2*b + 2);
SASSERT(p.subst_val(vb, rational(0)) == a);
SASSERT(p.subst_val(vb, rational(1)) == a + 2);
SASSERT(p.subst_val(vb, rational(2)) == a);
SASSERT(p.subst_val(vb, rational(3)) == a + 2);
SASSERT(p.subst_val(va, rational(0)).subst_val(vb, rational(3)) == 2*m.one());
}
{
pdd const p = a + b + c + d;
vector<std::pair<unsigned, rational>> sub;
sub.push_back({vb, rational(2)});
sub.push_back({vc, rational(3)});
SASSERT(p.subst_val(sub) == a + d + 1);
}
{
pdd const p = (a + b) * (b + c) * (c + d);
vector<std::pair<unsigned, rational>> sub;
sub.push_back({vb, rational(2)});
sub.push_back({vc, rational(3)});
SASSERT(p.subst_val(sub) == (a + 2) * (d + 3));
sub.push_back({va, rational(3)});
sub.push_back({vd, rational(2)});
SASSERT(p.subst_val(sub) == m.one());
}
}
};
}
@ -528,4 +577,5 @@ void tst_pdd() {
dd::test::max_pow2_divisor();
dd::test::binary_resolve();
dd::test::pow();
dd::test::subst_val();
}