mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-08 08:51:55 +00:00
Code Activity

testing doc

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-09-20 19:01:15 -07:00
parent 2552c1530b
commit a50cbef877
10 changed files with 291 additions and 95 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/muz/rel/dl_instruction.cpp
View file

@ -154,6 +154,10 @@ namespace datalog {
display_body_impl(ctx, out, indentation);
}
void instruction::log_verbose(execution_context& ctx) {
IF_VERBOSE(2, display(ctx.get_rel_context(), verbose_stream()););
}
class instr_io : public instruction {
bool m_store;
func_decl_ref m_pred;
@ -162,6 +166,7 @@ namespace datalog {
instr_io(bool store, func_decl_ref pred, reg_idx reg)
: m_store(store), m_pred(pred), m_reg(reg) {}
virtual bool perform(execution_context & ctx) {
log_verbose(ctx);
if (m_store) {
if (ctx.reg(m_reg)) {
ctx.get_rel_context().store_relation(m_pred, ctx.release_reg(m_reg));
@ -237,6 +242,7 @@ namespace datalog {
instr_clone_move(bool clone, reg_idx src, reg_idx tgt)
: m_clone(clone), m_src(src), m_tgt(tgt) {}
virtual bool perform(execution_context & ctx) {
log_verbose(ctx);
ctx.make_empty(m_tgt);
if (m_clone) {
ctx.set_reg(m_tgt, ctx.reg(m_src) ? ctx.reg(m_src)->clone() : 0);
@ -296,6 +302,7 @@ namespace datalog {
dealloc(m_body);
}
virtual bool perform(execution_context & ctx) {
log_verbose(ctx);
TRACE("dl", tout << "loop entered\n";);
unsigned count = 0;
while (!control_is_empty(ctx)) {
@ -339,6 +346,7 @@ namespace datalog {
: m_rel1(rel1), m_rel2(rel2), m_cols1(col_cnt, cols1),
m_cols2(col_cnt, cols2), m_res(result) {}
virtual bool perform(execution_context & ctx) {
log_verbose(ctx);
ctx.make_empty(m_res);
if (!ctx.reg(m_rel1) || !ctx.reg(m_rel2)) {
return true;
@ -400,6 +408,7 @@ namespace datalog {
instr_filter_equal(ast_manager & m, reg_idx reg, const relation_element & value, unsigned col)
: m_reg(reg), m_value(value, m), m_col(col) {}
virtual bool perform(execution_context & ctx) {
log_verbose(ctx);
if (!ctx.reg(m_reg)) {
return true;
}
@ -447,6 +456,7 @@ namespace datalog {
instr_filter_identical(reg_idx reg, unsigned col_cnt, const unsigned * identical_cols)
: m_reg(reg), m_cols(col_cnt, identical_cols) {}
virtual bool perform(execution_context & ctx) {
log_verbose(ctx);
if (!ctx.reg(m_reg)) {
return true;
}
@ -493,6 +503,7 @@ namespace datalog {
if (!ctx.reg(m_reg)) {
return true;
}
log_verbose(ctx);
relation_mutator_fn * fn;
relation_base & r = *ctx.reg(m_reg);
@ -543,6 +554,7 @@ namespace datalog {
m_res(result) {}
virtual bool perform(execution_context & ctx) {
log_verbose(ctx);
if (!ctx.reg(m_src)) {
ctx.make_empty(m_res);
return true;
@ -601,6 +613,7 @@ namespace datalog {
instr_union(reg_idx src, reg_idx tgt, reg_idx delta, bool widen)
: m_src(src), m_tgt(tgt), m_delta(delta), m_widen(widen) {}
virtual bool perform(execution_context & ctx) {
log_verbose(ctx);
TRACE("dl", tout << "union " << m_src << " into " << m_tgt
<< " " << ctx.reg(m_src) << " " << ctx.reg(m_tgt) << "\n";);
if (!ctx.reg(m_src)) {
@ -713,6 +726,7 @@ namespace datalog {
reg_idx tgt) : m_projection(projection), m_src(src),
m_cols(col_cnt, cols), m_tgt(tgt) {}
virtual bool perform(execution_context & ctx) {
log_verbose(ctx);
ctx.make_empty(m_tgt);
if (!ctx.reg(m_src)) {
return true;
@ -778,6 +792,7 @@ namespace datalog {
m_cols2(joined_col_cnt, cols2), m_removed_cols(removed_col_cnt, removed_cols), m_res(result) {
}
virtual bool perform(execution_context & ctx) {
log_verbose(ctx);
ctx.make_empty(m_res);
if (!ctx.reg(m_rel1) || !ctx.reg(m_rel2)) {
return true;
@ -839,6 +854,7 @@ namespace datalog {
}
virtual bool perform(execution_context & ctx) {
log_verbose(ctx);
if (!ctx.reg(m_src)) {
ctx.make_empty(m_result);
return true;
@ -893,6 +909,7 @@ namespace datalog {
const unsigned * cols2)
: m_tgt(tgt), m_neg_rel(neg_rel), m_cols1(col_cnt, cols1), m_cols2(col_cnt, cols2) {}
virtual bool perform(execution_context & ctx) {
log_verbose(ctx);
if (!ctx.reg(m_tgt) || !ctx.reg(m_neg_rel)) {
return true;
}
@ -948,6 +965,7 @@ namespace datalog {
m_fact.push_back(val);
}
virtual bool perform(execution_context & ctx) {
log_verbose(ctx);
ctx.make_empty(m_tgt);
relation_base * rel = ctx.get_rel_context().get_rmanager().mk_empty_relation(m_sig, m_pred);
rel->add_fact(m_fact);
@ -980,6 +998,7 @@ namespace datalog {
public:
instr_mk_total(const relation_signature & sig, func_decl* p, reg_idx tgt) : m_sig(sig), m_pred(p), m_tgt(tgt) {}
virtual bool perform(execution_context & ctx) {
log_verbose(ctx);
ctx.make_empty(m_tgt);
ctx.set_reg(m_tgt, ctx.get_rel_context().get_rmanager().mk_full_relation(m_sig, m_pred));
return true;
@ -1006,6 +1025,7 @@ namespace datalog {
instr_mark_saturated(ast_manager & m, func_decl * pred)
: m_pred(pred, m) {}
virtual bool perform(execution_context & ctx) {
log_verbose(ctx);
ctx.get_rel_context().get_rmanager().mark_saturated(m_pred);
return true;
}
@ -1027,6 +1047,7 @@ namespace datalog {
instr_assert_signature(const relation_signature & s, reg_idx tgt)
: m_sig(s), m_tgt(tgt) {}
virtual bool perform(execution_context & ctx) {
log_verbose(ctx);
if (ctx.reg(m_tgt)) {
SASSERT(ctx.reg(m_tgt)->get_signature()==m_sig);
}

2
src/muz/rel/dl_instruction.h
View file

@ -222,6 +222,8 @@ namespace datalog {
Each line must be prepended by \c indentation and ended by a newline character.
*/
virtual void display_body_impl(rel_context const & ctx, std::ostream & out, std::string indentation) const {}
void log_verbose(execution_context& ctx);
public:
typedef execution_context::reg_type reg_type;
typedef execution_context::reg_idx reg_idx;

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

@ -50,6 +50,7 @@ doc* doc_manager::allocate(doc const& src) {
return r;
}
doc* doc_manager::allocate(tbv* t) {
SASSERT(t);
void* mm = m_alloc.allocate(sizeof(doc));
return new (mm) doc(t);
}
@ -85,9 +86,7 @@ void doc_manager::copy(doc& dst, doc const& src) {
for (unsigned i = 0; i < n; ++i) {
m.copy(dst.neg()[i], src.neg()[i]);
}
for (unsigned i = n; i < dst.neg().size(); ++i) {
dst.neg().erase(m, dst.neg().size()-1);
}
dst.neg().reset(m);
for (unsigned i = n; i < src.neg().size(); ++i) {
dst.neg().push_back(m.allocate(src.neg()[i]));
}
@ -110,12 +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;
for (unsigned i = 0; i < dst.neg().size(); ++i) {
if (!m.set_and(dst.neg()[i], dst.pos())) {
dst.neg().erase(m, i);
--i;
}
}
dst.neg().intersect(m, src.pos());
tbv_ref t(m);
for (unsigned i = 0; i < src.neg().size(); ++i) {
t = m.allocate(src.neg()[i]);
@ -279,6 +273,7 @@ bool doc_manager::intersect(doc const& A, doc const& B, doc& result) {
doc* doc_manager::project(doc_manager& dstm, unsigned n, bool const* to_delete, doc const& src) {
tbv_manager& dstt = dstm.m;
doc* r = dstm.allocate(dstt.project(n, to_delete, src.pos()));
SASSERT(r);
if (src.neg().is_empty()) {
return r;
@ -405,13 +400,21 @@ void doc_manager::complement(doc const& src, ptr_vector<doc>& result) {
result.push_back(allocate(src.neg()[i]));
}
}
// (A \ {A1}) \ (B \ {B1})
// (A & !A1 & & !B) | (A & B1 & !A1)
// A \ {A1 u B} u (A & B1) \ {A1}
void doc_manager::subtract(doc const& A, doc const& B, ptr_vector<doc>& result) {
doc_ref r(*this), r2(*this);
tbv_ref t(m);
r = allocate(A);
if (r->neg().insert(m, m.allocate(B.pos()))) {
t = m.allocate(B.pos());
if (m.set_and(*t, A.pos()) && r->neg().insert(m, t.detach())) {
result.push_back(r.detach());
r = allocate(A);
}
else {
result.push_back(allocate(A));
}
for (unsigned i = 0; i < B.neg().size(); ++i) {
r2 = allocate(B.neg()[i]);
if (set_and(*r, *r2)) {

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

@ -111,12 +111,16 @@ public:
}
void push_back(T* t) {
SASSERT(t);
m_elems.push_back(t);
}
void erase(M& m, unsigned idx) {
T* t = m_elems[idx];
m_elems.erase(t);
m.deallocate(t);
m.deallocate(m_elems[idx]);
unsigned sz = m_elems.size();
for (unsigned i = idx+1; i < sz; ++i) {
m_elems[i-1] = m_elems[i];
}
m_elems.resize(sz-1);
}
void reset(M& m) {
for (unsigned i = 0; i < m_elems.size(); ++i) {
@ -125,21 +129,20 @@ public:
m_elems.reset();
}
bool insert(M& m, T* t) {
SASSERT(t);
unsigned sz = size(), j = 0;
bool found = false;
for (unsigned i = 0; i < sz; ++i, ++j) {
if (m.contains(*m_elems[i], *t)) {
found = true;
}
if (!found && m.contains(*t, *m_elems[i])) {
m.deallocate(m_elems[i]);
--j;
}
else {
if (m.contains(*m_elems[i], *t)) {
found = true;
}
if (i != j) {
m_elems[j] = m_elems[i];
}
}
else if (i != j) {
m_elems[j] = m_elems[i];
}
}
if (j != sz) m_elems.resize(j);
if (found) {
@ -150,7 +153,7 @@ public:
}
return !found;
}
void intersect(M& m, T& t) {
void intersect(M& m, T const& t) {
unsigned sz = size();
unsigned j = 0;
for (unsigned i = 0; i < sz; ++i, ++j) {
@ -159,7 +162,7 @@ public:
--j;
}
else if (i != j) {
m_elems[i] = m_elems[j];
m_elems[j] = m_elems[i];
}
}
if (j != sz) m_elems.resize(j);
@ -233,13 +236,26 @@ public:
std::swap(*this, result);
}
void merge(M& m, unsigned lo, unsigned length, subset_ints const& equalities, bit_vector const& discard_cols) {
bool well_formed(M& m) const {
for (unsigned i = 0; i < size(); ++i) {
if (!m.well_formed(*m_elems[i])) return false;
}
return true;
}
void merge(M& m, unsigned lo, unsigned length, subset_ints const& equalities, bit_vector const& discard_cols) {
unsigned j = 0;
unsigned sz = size();
for (unsigned i = 0; i < sz; ++i, ++j) {
if (!m.merge(*m_elems[i], lo, length, equalities, discard_cols)) {
erase(m, i);
--i;
--j;
m.deallocate(m_elems[i]);
}
else if (i != j) {
m_elems[j] = m_elems[i];
}
}
if (j != sz) m_elems.resize(j);
}
void merge(M& m, unsigned lo1, unsigned lo2, unsigned length, bit_vector const& discard_cols) {

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

@ -92,7 +92,8 @@ tbv* tbv_manager::allocate(uint64 val, unsigned hi, unsigned lo) {
}
tbv* tbv_manager::allocate(tbv const& bv, unsigned const* permutation) {
tbv* r = allocate();
for (unsigned i = 0; i < num_tbits(); ++i) {
unsigned sz = num_tbits();
for (unsigned i = 0; i < sz; ++i) {
r->set(permutation[i], bv[i]);
}
return r;

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

@ -373,6 +373,7 @@ namespace datalog {
}
}
TRACE("doc", result->display(tout << "result:\n"););
SASSERT(r.well_formed(result->get_dm()));
return result;
}
};
@ -412,6 +413,7 @@ namespace datalog {
ud2.push_back(d2.detach());
}
TRACE("doc", tout << "final size: " << r->get_size_estimate_rows() << '\n';);
SASSERT(ud2.well_formed(dm2));
return r;
}
};
@ -431,20 +433,60 @@ namespace datalog {
rename_fn(udoc_relation const& t, unsigned cycle_len, const unsigned * cycle)
: convenient_relation_rename_fn(t.get_signature(), cycle_len, cycle) {
udoc_plugin& p = t.get_plugin();
ast_manager& m = p.get_ast_manager();
relation_signature const& sig1 = t.get_signature();
relation_signature const& sig2 = get_result_signature();
unsigned_vector permutation0, column_info;
for (unsigned i = 0; i < t.get_num_bits(); ++i) {
m_permutation.push_back(i);
}
unsigned len = t.column_num_bits(cycle[0]);
for (unsigned i = 0; i < sig1.size(); ++i) {
permutation0.push_back(i);
}
for (unsigned i = 0; i < cycle_len; ++i) {
unsigned j = (i + 1)%cycle_len;
unsigned col1 = cycle[i];
unsigned col2 = cycle[j];
unsigned lo1 = t.column_idx(col1);
unsigned lo2 = t.column_idx(col2);
permutation0[col2] = col1;
}
unsigned column = 0;
for (unsigned i = 0; i < sig2.size(); ++i) {
column_info.push_back(column);
column += p.num_sort_bits(sig2[i]);
}
column_info.push_back(column);
SASSERT(column == t.get_num_bits());
TRACE("doc",
sig1.output(m, tout << "sig1: "); tout << "\n";
sig2.output(m, tout << "sig2: "); tout << "\n";
tout << "permute: ";
for (unsigned i = 0; i < permutation0.size(); ++i) {
tout << permutation0[i] << " ";
}
tout << "\n";
tout << "cycle: ";
for (unsigned i = 0; i < cycle_len; ++i) {
tout << cycle[i] << " ";
}
tout << "\n";
);
// 0 -> 2
// [3:2:1] -> [1:2:3]
// [3,4,5,1,2,0]
for (unsigned i = 0; i < sig1.size(); ++i) {
unsigned len = t.column_num_bits(i);
unsigned lo1 = t.column_idx(i);
unsigned col2 = permutation0[i];
unsigned lo2 = column_info[col2];
SASSERT(lo2 + len <= t.get_num_bits());
SASSERT(lo1 + len <= t.get_num_bits());
for (unsigned k = 0; k < len; ++k) {
m_permutation[k + lo1] = k + lo2;
}
SASSERT(t.column_num_bits(col1) == t.column_num_bits(col2));
}
}
@ -457,10 +499,12 @@ namespace datalog {
udoc const& src = r.get_udoc();
udoc& dst = result->get_udoc();
doc_manager& dm = r.get_dm();
SASSERT(&result->get_dm() == &dm);
for (unsigned i = 0; i < src.size(); ++i) {
dst.push_back(dm.allocate(src[i], m_permutation.c_ptr()));
}
TRACE("doc", result->display(tout << "result:\n"););
SASSERT(dst.well_formed(dm));
return result;
}
};
@ -488,6 +532,8 @@ namespace datalog {
if (d) d1 = &d->get_udoc();
if (d1) d1->reset(dm);
r.get_plugin().mk_union(dm, r.get_udoc(), src.get_udoc(), d1);
SASSERT(r.get_udoc().well_formed(dm));
SASSERT(!d1 || d1->well_formed(dm));
TRACE("doc", _r.display(tout << "dst':\n"); );
}
};
@ -547,6 +593,7 @@ namespace datalog {
udoc& d = r.get_udoc();
doc_manager& dm = r.get_dm();
d.merge(dm, m_cols[0], m_size, m_equalities, m_empty_bv);
SASSERT(d.well_formed(dm));
TRACE("doc", tout << "final size: " << r.get_size_estimate_rows() << '\n';);
}
};
@ -575,6 +622,7 @@ namespace datalog {
virtual void operator()(relation_base & tb) {
udoc_relation & t = get(tb);
t.get_udoc().intersect(dm, *m_filter);
SASSERT(t.get_udoc().well_formed(t.get_dm()));
}
};
relation_mutator_fn * udoc_plugin::mk_filter_equal_fn(
@ -826,11 +874,15 @@ namespace datalog {
virtual void operator()(relation_base & tb) {
udoc_relation & t = get(tb);
udoc& u = t.get_udoc();
SASSERT(u.well_formed(dm));
u.intersect(dm, m_udoc);
SASSERT(u.well_formed(dm));
if (m_condition && !u.is_empty()) {
t.apply_guard(m_condition, u, m_equalities, m_empty_bv);
SASSERT(u.well_formed(dm));
}
u.simplify(dm);
SASSERT(u.well_formed(dm));
TRACE("doc", tout << "final size: " << t.get_size_estimate_rows() << '\n';);
}
};
@ -896,7 +948,12 @@ namespace datalog {
}
renamed_neg.push_back(newD.detach());
}
dst.subtract(t.get_dm(), renamed_neg);
TRACE("doc", dst.display(dm, tout) << "\n";
renamed_neg.display(dm, tout) << "\n";
);
dst.subtract(dm, renamed_neg);
TRACE("doc", dst.display(dm, tout) << "\n";);
SASSERT(dst.well_formed(dm));
renamed_neg.reset(t.get_dm());
}
void copy_column(
@ -971,17 +1028,23 @@ namespace datalog {
udoc const& u1 = t.get_udoc();
doc_manager& dm = t.get_dm();
udoc u2;
SASSERT(u1.well_formed(dm));
u2.copy(dm, u1);
SASSERT(u2.well_formed(dm));
u2.intersect(dm, m_udoc);
u2.merge(dm, m_roots, m_equalities, m_col_list);
SASSERT(u2.well_formed(dm));
u2.merge(dm, m_roots, m_equalities, m_col_list);
SASSERT(u2.well_formed(dm));
if (m_condition && !u2.is_empty()) {
t.apply_guard(m_condition, u2, m_equalities, m_col_list);
SASSERT(u2.well_formed(dm));
}
udoc_relation* r = get(t.get_plugin().mk_empty(get_result_signature()));
doc_manager& dm2 = r->get_dm();
for (unsigned i = 0; i < u2.size(); ++i) {
doc* d = dm.project(dm2, m_to_delete.size(), m_to_delete.c_ptr(), u2[i]);
r->get_udoc().insert(dm2, d);
SASSERT(r->get_udoc().well_formed(dm2));
}
u2.reset(dm);
return r;