mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

testing filter interpreted

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-09-19 18:18:40 -07:00
parent 6a8623ef0c
commit 25914c0492
3 changed files with 93 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/muz/rel/doc.h
View file

@ -220,6 +220,18 @@ public:
push_back(m.allocate(other[i]));
}
}
void simplify(M& m) {
union_bvec result;
for (unsigned i = 0; i < size(); ++i) {
if (m.fold_neg(*m_elems[i])) {
result.insert(m, m_elems[i]);
}
else {
m.deallocate(m_elems[i]);
}
}
std::swap(*this, result);
}
void merge(M& m, unsigned lo, unsigned length, subset_ints & equalities, bit_vector const& discard_cols) {
for (unsigned i = 0; i < size(); ++i) {

1
src/muz/rel/udoc_relation.cpp
View file

@ -739,6 +739,7 @@ namespace datalog {
if (m_condition && !u.is_empty()) {
t.apply_guard(m_condition, u, m_empty_bv);
}
u.simplify(dm);
TRACE("dl", tout << "final size: " << t.get_size_estimate_rows() << '\n';);
}
};

88
src/test/udoc_relation.cpp
View file

@ -21,6 +21,9 @@ class udoc_tester {
typedef datalog::udoc_relation udoc_relation;
typedef datalog::udoc_plugin udoc_plugin;
typedef datalog::relation_signature relation_signature;
typedef datalog::relation_fact relation_fact;
typedef scoped_ptr<datalog::relation_mutator_fn> rel_mut;
typedef scoped_ptr<datalog::relation_union_fn> rel_union;
struct init {
init(ast_manager& m) {
@ -61,6 +64,7 @@ public:
sig.push_back(bv.mk_sort(12));
sig.push_back(bv.mk_sort(6));
sig.push_back(bv.mk_sort(12));
datalog::relation_fact fact1(m), fact2(m), fact3(m);
fact1.push_back(bv.mk_numeral(rational(1), 12));
@ -73,7 +77,15 @@ public:
fact3.push_back(bv.mk_numeral(rational(16), 6));
fact3.push_back(bv.mk_numeral(rational(4), 12));
relation_signature sig2;
sig2.push_back(bv.mk_sort(3));
sig2.push_back(bv.mk_sort(6));
sig2.push_back(bv.mk_sort(3));
sig2.push_back(bv.mk_sort(3));
sig2.push_back(bv.mk_sort(3));
relation_base* t;
udoc_relation* t1, *t2, *t3;
expr_ref fml(m);
// empty
{
@ -97,9 +109,9 @@ public:
// join
{
udoc_relation* t1 = mk_full(sig);
udoc_relation* t2 = mk_full(sig);
udoc_relation* t3 = mk_empty(sig);
t1 = mk_full(sig);
t2 = mk_full(sig);
t3 = mk_empty(sig);
unsigned_vector jc1, jc2;
jc1.push_back(1);
jc2.push_back(1);
@ -128,7 +140,7 @@ public:
// project
{
std::cout << "project\n";
udoc_relation* t1 = mk_full(sig);
t1 = mk_full(sig);
unsigned_vector pc;
pc.push_back(0);
datalog::relation_transformer_fn* proj_fn = p.mk_project_fn(*t1, pc.size(), pc.c_ptr());
@ -155,7 +167,7 @@ public:
// rename
{
udoc_relation* t1 = mk_empty(sig);
t1 = mk_empty(sig);
unsigned_vector cycle;
cycle.push_back(0);
cycle.push_back(2);
@ -175,14 +187,14 @@ public:
// union
{
udoc_relation* t1 = mk_empty(sig);
udoc_relation* t2 = mk_empty(sig);
t1 = mk_empty(sig);
t2 = mk_empty(sig);
udoc_relation* delta = mk_full(sig);
t2->add_fact(fact1);
t2->add_fact(fact2);
t1->add_fact(fact3);
datalog::relation_union_fn* union_fn = p.mk_union_fn(*t1, *t2, 0);
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);
@ -195,9 +207,69 @@ public:
}
// filter_identical
{
t1 = mk_empty(sig2);
unsigned_vector id;
id.push_back(0);
id.push_back(2);
id.push_back(4);
datalog::relation_mutator_fn* filter_id = p.mk_filter_identical_fn(*t1, id.size(), id.c_ptr());
relation_fact f1(m);
f1.push_back(bv.mk_numeral(rational(1),3));
f1.push_back(bv.mk_numeral(rational(1),6));
f1.push_back(bv.mk_numeral(rational(1),3));
f1.push_back(bv.mk_numeral(rational(1),3));
f1.push_back(bv.mk_numeral(rational(1),3));
t1->add_fact(f1);
f1[4] = bv.mk_numeral(rational(2),3);
t1->add_fact(f1);
t1->display(std::cout); std::cout << "\n";
(*filter_id)(*t1);
t1->display(std::cout); std::cout << "\n";
t1->deallocate();
dealloc(filter_id);
}
// filter_interpreted
{
std::cout << "filter interpreted\n";
t1 = mk_full(sig2);
t2 = mk_full(sig2);
var_ref v0(m.mk_var(0, bv.mk_sort(3)),m);
var_ref v1(m.mk_var(1, bv.mk_sort(6)),m);
var_ref v2(m.mk_var(2, bv.mk_sort(3)),m);
var_ref v3(m.mk_var(3, bv.mk_sort(3)),m);
var_ref v4(m.mk_var(4, bv.mk_sort(3)),m);
app_ref cond1(m), cond2(m), cond3(m), cond4(m);
app_ref cond5(m), cond6(m), cond7(m), cond8(m);
cond1 = m.mk_true();
cond2 = m.mk_false();
cond3 = m.mk_eq(v0, v2);
cond4 = m.mk_not(m.mk_eq(v0, v2));
cond5 = m.mk_eq(v0, bv.mk_numeral(rational(2), 3));
rel_union union_fn = p.mk_union_fn(*t1, *t2, 0);
rel_mut fint1 = p.mk_filter_interpreted_fn(*t1, cond1);
rel_mut fint2 = p.mk_filter_interpreted_fn(*t1, cond2);
rel_mut fint3 = p.mk_filter_interpreted_fn(*t1, cond3);
rel_mut fint4 = p.mk_filter_interpreted_fn(*t1, cond4);
rel_mut fint5 = p.mk_filter_interpreted_fn(*t1, cond5);
(*fint1)(*t1);
t1->display(std::cout << "filter: " << cond1 << " "); std::cout << "\n";
(*fint2)(*t1);
t1->display(std::cout << "filter: " << cond2 << " "); std::cout << "\n";
(*union_fn)(*t1, *t2);
(*fint3)(*t1);
t1->display(std::cout << "filter: " << cond3 << " "); std::cout << "\n";
(*fint4)(*t1);
t1->display(std::cout << "filter: " << cond4 << " "); std::cout << "\n";
(*union_fn)(*t1, *t2);
(*fint5)(*t1);
t1->display(std::cout << "filter: " << cond5 << " "); std::cout << "\n";
t1->deallocate();
t2->deallocate();
}
// filter_by_negation
// filter_interpreted_project