mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 08:58:44 +00:00
Code Activity

add a unit test to pdd

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-22 19:37:29 -08:00
parent 25b98f497a
commit 3aff0bd7db
1 changed files with 18 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/test/pdd.cpp
View file

@ -64,6 +64,23 @@ namespace dd {
std::cout << "result of reduce " << e << " by " << f << " is " << r_ef << "\n"; std::cout << "result of reduce " << e << " by " << f << " is " << r_ef << "\n";
pdd r_fe = m.reduce(f, e); pdd r_fe = m.reduce(f, e);
std::cout << "result of reduce " << f << " by " << e << " is " << r_fe << "\n" ; std::cout << "result of reduce " << f << " by " << e << " is " << r_fe << "\n" ;
VERIFY(r_fe == f);
}
static void test3() {
std::cout << "\ntest3\n";
pdd_manager m(4);
pdd a = m.mk_var(0);
pdd b = m.mk_var(1);
pdd c = m.mk_var(2);
pdd d = m.mk_var(3);
pdd e = a + c;
for (unsigned i = 0; i < 5; i++) {
e = e * e;
}
e = e * b;
std::cout << e << "\n";
} }
} }
@ -71,4 +88,5 @@ namespace dd {
void tst_pdd() { void tst_pdd() {
dd::test1(); dd::test1();
dd::test2(); dd::test2();
dd::test3();
} }