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

fixing join

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-09-22 11:08:23 -07:00
parent 75b11d2b75
commit 4cf8905a8f
2 changed files with 163 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -304,13 +304,16 @@ namespace datalog {
}
void join(doc const& d1, doc const& d2, udoc& result) {
doc* d = dm.allocateX();
doc_ref d(dm);
tbv_ref t(dm.tbvm());
d = dm.allocateX();
tbv& pos = d->pos();
utbv& neg = d->neg();
unsigned mid = dm1.num_tbits();
unsigned hi = dm.num_tbits();
pos.set(d1.pos(), mid-1, 0);
pos.set(d2.pos(), hi-1, mid);
SASSERT(dm.well_formed(*d));
// first fix bits
for (unsigned i = 0; i < m_cols1.size(); ++i) {
unsigned idx1 = m_cols1[i];
@ -321,13 +324,15 @@ namespace datalog {
if (v1 == BIT_x) {
if (v2 != BIT_x)
pos.set(idx1, v2);
} else if (v2 == BIT_x) {
}
else if (v2 == BIT_x) {
pos.set(idx2, v1);
} else if (v1 != v2) {
dm.deallocate(d);
}
else if (v1 != v2) {
// columns don't match
return;
}
SASSERT(dm.well_formed(*d));
}
// fix equality of don't care columns
for (unsigned i = 0; i < m_cols1.size(); ++i) {
@ -338,32 +343,39 @@ namespace datalog {
if (v1 == BIT_x && v2 == BIT_x) {
// add to subtracted TBVs: 1xx0 and 0xx1
tbv* r = dm.tbvm().allocate(pos);
r->set(idx1, BIT_0);
r->set(idx2, BIT_1);
neg.push_back(r);
r = dm.tbvm().allocate(pos);
r->set(idx1, BIT_1);
r->set(idx2, BIT_0);
neg.push_back(r);
t = dm.tbvm().allocate(pos);
t->set(idx1, BIT_0);
t->set(idx2, BIT_1);
neg.push_back(t.detach());
t = dm.tbvm().allocate(pos);
t->set(idx1, BIT_1);
t->set(idx2, BIT_0);
neg.push_back(t.detach());
}
SASSERT(dm.well_formed(*d));
}
// handle subtracted TBVs: 1010 -> 1010xxx
for (unsigned i = 0; i < d1.neg().size(); ++i) {
tbv* t = dm.tbvm().allocate();
t->set(d1.neg()[i], mid-1, 0);
t->set(d2.pos(), hi - 1, mid);
neg.push_back(t);
t = dm.tbvm().allocate();
t->set(d1.neg()[i], mid - 1, 0);
t->set(d2.pos(), hi - 1, mid);
if (dm.tbvm().set_and(*t, pos)) {
neg.push_back(t.detach());
}
SASSERT(dm.well_formed(*d));
}
for (unsigned i = 0; i < d2.neg().size(); ++i) {
tbv* t = dm.tbvm().allocate();
t->set(d1.pos(), mid-1, 0);
t = dm.tbvm().allocate();
t->set(d1.pos(), mid- 1, 0);
t->set(d2.neg()[i], hi - 1, mid);
neg.push_back(t);
if (dm.tbvm().set_and(*t, pos)) {
neg.push_back(t.detach());
}
SASSERT(dm.well_formed(*d));
}
result.insert(dm, d);
SASSERT(dm.well_formed(*d));
result.insert(dm, d.detach());
}
virtual relation_base * operator()(const relation_base & _r1, const relation_base & _r2) {

130
src/test/udoc_relation.cpp
View file

@ -16,6 +16,7 @@
#include "rel_context.h"
#include "bv_decl_plugin.h"
class udoc_tester {
typedef datalog::relation_base relation_base;
typedef datalog::udoc_relation udoc_relation;
@ -40,6 +41,56 @@ class udoc_tester {
datalog::context m_ctx;
datalog::rel_context rc;
udoc_plugin& p;
tbit choose_tbit() {
switch (m_rand(3)) {
case 0: return BIT_0;
case 1: return BIT_1;
default : return BIT_x;
}
}
tbv* mk_rand_tbv(doc_manager& dm) {
tbv* result = dm.tbvm().allocate();
for (unsigned i = 0; i < dm.num_tbits(); ++i) {
(*result).set(i, choose_tbit());
}
return result;
}
tbv* mk_rand_tbv(doc_manager& dm, tbv const& pos) {
tbv* result = dm.tbvm().allocate();
for (unsigned i = 0; i < dm.num_tbits(); ++i) {
if (pos[i] == BIT_x) {
(*result).set(i, choose_tbit());
}
else {
(*result).set(i, pos[i]);
}
}
return result;
}
doc* mk_rand_doc(doc_manager& dm, unsigned num_diff) {
tbv_ref t(dm.tbvm());
t = mk_rand_tbv(dm);
doc* result = dm.allocate(*t);
SASSERT(dm.tbvm().equals(*t, result->pos()));
for (unsigned i = 0; i < num_diff; ++i) {
result->neg().push_back(mk_rand_tbv(dm, result->pos()));
}
SASSERT(dm.well_formed(*result));
return result;
}
void mk_rand_udoc(doc_manager& dm, unsigned num_elems, unsigned num_diff, udoc& result) {
result.reset(dm);
for (unsigned i = 0; i < num_elems; ++i) {
result.push_back(mk_rand_doc(dm, num_diff));
}
}
public:
udoc_tester(): m_init(m), bv(m), m_vars(m), m_ctx(m, m_reg, m_smt_params), rc(m_ctx),
p(dynamic_cast<udoc_plugin&>(*rc.get_rmanager().get_relation_plugin(symbol("doc"))))
@ -88,6 +139,8 @@ public:
udoc_relation* t1, *t2, *t3;
expr_ref fml(m);
test_join(1000);
test_rename();
test_filter_neg();
@ -366,6 +419,83 @@ public:
check_permutation(t1, cycle);
}
void test_join(unsigned num_rounds) {
for (unsigned i = 0; i < num_rounds; ++i) {
test_join();
}
}
void test_join() {
relation_signature sig;
sig.push_back(bv.mk_sort(2));
sig.push_back(bv.mk_sort(3));
udoc_relation* t1, *t2;
relation_base* t;
t1 = mk_rand(sig);
t2 = mk_rand(sig);
unsigned_vector jc1, jc2;
jc1.push_back(0);
jc2.push_back(0);
scoped_ptr<datalog::relation_join_fn> join_fn;
join_fn = p.mk_join_fn(*t1, *t2, jc1.size(), jc1.c_ptr(), jc2.c_ptr());
t = (*join_fn)(*t1, *t2);
verify_join(*t1, *t2, *t, jc1.size(), jc1.c_ptr(), jc2.c_ptr());
t1->display(std::cout);
t2->display(std::cout);
t->display(std::cout);
std::cout << "\n";
t1->deallocate();
t2->deallocate();
t->deallocate();
}
udoc_relation* mk_rand(relation_signature const& sig) {
udoc_relation* t = mk_empty(sig);
mk_rand_udoc(t->get_dm(), 3, 3, t->get_udoc());
return t;
}
void verify_join(relation_base const& t1, relation_base& t2, relation_base& t,
unsigned sz, unsigned const* cols1, unsigned const* cols2) {
relation_signature const& sig1 = t1.get_signature();
relation_signature const& sig2 = t2.get_signature();
relation_signature const& sig = t.get_signature();
expr_ref fml1(m), fml2(m), fml3(m);
var_ref var1(m), var2(m);
t1.to_formula(fml1);
t2.to_formula(fml2);
t.to_formula(fml3);
var_subst sub(m, false);
expr_ref_vector vars(m);
for (unsigned i = 0; i < sig2.size(); ++i) {
vars.push_back(m.mk_var(i + sig1.size(), sig2[i]));
}
sub(fml2, vars.size(), vars.c_ptr(), fml2);
fml1 = m.mk_and(fml1, fml2);
for (unsigned i = 0; i < sz; ++i) {
unsigned v1 = cols1[i];
unsigned v2 = cols2[i];
var1 = m.mk_var(v1, sig1[v1]);
var2 = m.mk_var(v2 + sig1.size(), sig2[v2]);
fml1 = m.mk_and(m.mk_eq(var1, var2), fml1);
}
vars.reset();
for (unsigned i = 0; i < sig.size(); ++i) {
std::stringstream strm;
strm << "x" << i;
vars.push_back(m.mk_const(symbol(strm.str().c_str()), sig[i]));
}
sub(fml1, vars.size(), vars.c_ptr(), fml1);
sub(fml3, vars.size(), vars.c_ptr(), fml3);
check_equiv(fml1, fml3);
}
void check_permutation(relation_base* t1, unsigned_vector const& cycle) {
scoped_ptr<datalog::relation_transformer_fn> rename;
rename = p.mk_rename_fn(*t1, cycle.size(), cycle.c_ptr());