mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

DoC: verify the result of a bunch of unit tests with SMT

Browse source 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2014-10-09 09:44:27 +01:00
parent d038c7bf89
commit 60aad7a662
1 changed files with 11 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/test/udoc_relation.cpp
View file

@ -204,15 +204,18 @@ public:
datalog::relation_join_fn* join_fn = p.mk_join_fn(*t1, *t2, jc1.size(), jc1.c_ptr(), jc2.c_ptr());
SASSERT(join_fn);
t = (*join_fn)(*t1, *t2);
cr.verify_join(*t1, *t2, *t, jc1, jc2);
t->display(std::cout); std::cout << "\n";
t->deallocate();
t = (*join_fn)(*t1, *t3);
cr.verify_join(*t1, *t3, *t, jc1, jc2);
SASSERT(t->empty());
t->display(std::cout); std::cout << "\n";
t->deallocate();
t = (*join_fn)(*t3, *t3);
cr.verify_join(*t3, *t3, *t, jc1, jc2);
SASSERT(t->empty());
t->display(std::cout); std::cout << "\n";
t->deallocate();
@ -231,11 +234,13 @@ public:
pc.push_back(0);
datalog::relation_transformer_fn* proj_fn = p.mk_project_fn(*t1, pc.size(), pc.c_ptr());
t = (*proj_fn)(*t1);
cr.verify_project(*t1, *t, pc);
t->display(std::cout); std::cout << "\n";
t->deallocate();
t1->reset();
t = (*proj_fn)(*t1);
cr.verify_project(*t1, *t, pc);
t->display(std::cout); std::cout << "\n";
t->deallocate();
@ -243,6 +248,7 @@ public:
t1->add_fact(fact2);
t1->add_fact(fact3);
t = (*proj_fn)(*t1);
cr.verify_project(*t1, *t, pc);
t1->display(std::cout); std::cout << "\n";
t->display(std::cout); std::cout << "\n";
t->deallocate();
@ -260,10 +266,15 @@ public:
t2->add_fact(fact2);
t1->add_fact(fact3);
expr_ref t10(m);
t1->to_formula(t10);
expr_ref delta0(m);
delta->to_formula(delta0);
rel_union union_fn = p.mk_union_fn(*t1, *t2, 0);
t1->display(std::cout << "t1 before:"); std::cout << "\n";
(*union_fn)(*t1, *t2, delta);
cr.verify_union(t10, *t2, *t1, delta0, delta);
t1->display(std::cout << "t1 after:"); std::cout << "\n";
delta->display(std::cout << "delta:"); std::cout << "\n";