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

fix bugs in doc

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-09-22 03:22:26 -07:00
parent 8c34cfca31
commit 75b11d2b75
4 changed files with 102 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/muz/rel/doc.cpp
View file

@ -109,7 +109,7 @@ doc& doc_manager::fillX(doc& src) {
bool doc_manager::set_and(doc& dst, doc const& src) {
// (A \ B) & (C \ D) = (A & C) \ (B u D)
if (!m.set_and(dst.pos(), src.pos())) return false;
dst.neg().intersect(m, src.pos());
dst.neg().intersect(m, dst.pos());
tbv_ref t(m);
for (unsigned i = 0; i < src.neg().size(); ++i) {
t = m.allocate(src.neg()[i]);
@ -117,6 +117,7 @@ bool doc_manager::set_and(doc& dst, doc const& src) {
dst.neg().insert(m, t.detach());
}
}
SASSERT(well_formed(dst));
return (src.neg().is_empty() || fold_neg(dst));
}
bool doc_manager::set_and(doc& dst, tbv const& src) {
@ -150,11 +151,12 @@ bool doc_manager::fold_neg(doc& dst) {
}
else { // count == 1:
dst.pos().set(index, neg(dst.neg()[i][index]));
dst.neg().erase(tbvm(), i);
dst.neg().intersect(tbvm(), dst.pos());
goto start_over;
}
}
}
SASSERT(well_formed(dst));
return true;
}

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

@ -175,20 +175,17 @@ public:
}
}
void intersect(M& m, union_bvec const& other) {
union_bvec result;
unsigned sz1 = size();
unsigned sz2 = other.size();
T* inter = m.allocate();
for (unsigned i = 0; i < sz1; ++i) {
for (unsigned j = 0; j < sz2; ++j) {
if (m.intersect(*m_elems[i], other[j], *inter)) {
result.push_back(inter);
inter = m.allocate();
}
unsigned sz = other.size();
union_bvec tmp, result;
for (unsigned i = 0; i < sz; ++i) {
tmp.copy(m, *this);
tmp.intersect(m, other[i]);
for (unsigned j = 0; j < tmp.size(); ++j) {
result.push_back(tmp.m_elems[j]);
}
tmp.m_elems.reset();
}
m.deallocate(inter);
std::swap(result, *this);
std::swap(*this, result);
result.reset(m);
}
void subtract(M& m, union_bvec const& other) {

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

@ -382,6 +382,7 @@ namespace datalog {
}
}
TRACE("doc", result->display(tout << "result:\n"););
IF_VERBOSE(3, result->display(verbose_stream() << "join result:\n"););
SASSERT(r.well_formed(result->get_dm()));
return result;
}
@ -544,6 +545,7 @@ namespace datalog {
SASSERT(r.get_udoc().well_formed(dm));
SASSERT(!d1 || d1->well_formed(dm));
TRACE("doc", _r.display(tout << "dst':\n"); );
IF_VERBOSE(3, _r.display(verbose_stream() << "union result:\n"););
}
};
void udoc_plugin::mk_union(doc_manager& dm, udoc& dst, udoc const& src, udoc* delta) {
@ -1045,6 +1047,7 @@ namespace datalog {
SASSERT(r->get_udoc().well_formed(dm2));
}
u2.reset(dm);
IF_VERBOSE(3, r->display(verbose_stream() << "filter result:\n"););
return r;
}
};

87
src/test/doc.cpp
View file

@ -113,6 +113,47 @@ class test_doc_cls {
default : return BIT_x;
}
}
tbv* mk_rand_tbv() {
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(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(unsigned num_diff) {
tbv_ref t(dm.tbvm());
t = mk_rand_tbv();
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(result->pos()));
}
SASSERT(dm.well_formed(*result));
return result;
}
void mk_rand_udoc(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(num_diff));
}
}
expr_ref mk_conj(tbv& t) {
expr_ref result(m);
expr_ref_vector conjs(m);
@ -284,6 +325,12 @@ class test_doc_cls {
fml = m.mk_not(m.mk_eq(fml1, fml2));
solver.assert_expr(fml);
lbool res = solver.check();
if (res != l_false) {
TRACE("doc",
tout << mk_pp(fml1, m) << "\n";
tout << mk_pp(fml2, m) << "\n";
);
}
SASSERT(res == l_false);
}
@ -349,6 +396,43 @@ public:
ds2.reset(dm);
//sub:{xxx \ {1x0, 0x1}}
//result:{100}
for (unsigned i = 0; i < 1000; ++i) {
udoc d1, d2;
mk_rand_udoc(3, 3, d1);
mk_rand_udoc(3, 3, d2);
fml1 = to_formula(d1, dm, to_delete.c_ptr());
fml2 = to_formula(d2, dm, to_delete.c_ptr());
d1.subtract(dm, d2);
fml3 = to_formula(d1, dm, to_delete.c_ptr());
fml1 = m.mk_and(fml1, m.mk_not(fml2));
check_equiv(fml1, fml3);
d1.reset(dm);
d2.reset(dm);
}
}
void test_intersect() {
expr_ref fml1(m), fml2(m), fml3(m);
svector<bool> to_delete(m_vars.size(), false);
for (unsigned i = 0; i < 10000; ++i) {
udoc d1, d2;
mk_rand_udoc(3, 3, d1);
mk_rand_udoc(3, 3, d2);
fml1 = to_formula(d1, dm, to_delete.c_ptr());
fml2 = to_formula(d2, dm, to_delete.c_ptr());
TRACE("doc",
d1.display(dm, tout) << "\n";
d2.display(dm, tout) << "\n";);
d1.intersect(dm, d2);
TRACE("doc", d1.display(dm, tout) << "\n";);
SASSERT(d1.well_formed(dm));
fml3 = to_formula(d1, dm, to_delete.c_ptr());
fml1 = m.mk_and(fml1, fml2);
check_equiv(fml1, fml3);
d1.reset(dm);
d2.reset(dm);
}
}
};
@ -356,7 +440,8 @@ public:
void tst_doc() {
test_doc_cls tp(4);
test_doc_cls tp(4);
tp.test_intersect();
tp.test_subtract();
tp.test_merge(200,7);
tp.test_project(200,7);