mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-17 07:01:27 +00:00
Code Activity

adding validation code to doc/udoc

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-09-23 17:10:00 -07:00
parent 54506408f9
commit 1111c0494f
13 changed files with 328 additions and 104 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2,6 +2,8 @@
#include "dl_relation_manager.h"
#include "qe_util.h"
#include "ast_util.h"
#include "smt_kernel.h"
namespace datalog {
@ -292,13 +294,17 @@ namespace datalog {
doc_manager& dm;
doc_manager& dm1;
doc_manager& dm2;
unsigned_vector m_orig_cols1;
unsigned_vector m_orig_cols2;
public:
join_fn(udoc_plugin& p, udoc_relation const& t1, udoc_relation const& t2, unsigned col_cnt,
const unsigned * cols1, const unsigned * cols2)
: convenient_relation_join_fn(t1.get_signature(), t2.get_signature(), col_cnt, cols1, cols2),
dm(p.dm(get_result_signature())),
dm1(t1.get_dm()),
dm2(t2.get_dm()) {
dm2(t2.get_dm()),
m_orig_cols1(m_cols1),
m_orig_cols2(m_cols2) {
t1.expand_column_vector(m_cols1);
t2.expand_column_vector(m_cols2);
}
@ -396,9 +402,12 @@ 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()));
DEBUG_CODE(p.verify_join(r1, r2, *result, m_orig_cols1.size(), m_orig_cols1.c_ptr(), m_orig_cols2.c_ptr()););
return result;
}
};
relation_join_fn * udoc_plugin::mk_join_fn(
const relation_base & t1, const relation_base & t2,
unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) {
@ -407,6 +416,7 @@ namespace datalog {
}
return alloc(join_fn, *this, get(t1), get(t2), col_cnt, cols1, cols2);
}
class udoc_plugin::project_fn : public convenient_relation_project_fn {
svector<bool> m_to_delete;
public:
@ -550,6 +560,9 @@ namespace datalog {
udoc_relation const& src = get(_src);
udoc_relation* d = get(_delta);
doc_manager& dm = r.get_dm();
ast_manager& m = r.get_plugin().get_ast_manager();
expr_ref fml0(m);
DEBUG_CODE(r.to_formula(fml0););
udoc* d1 = 0;
if (d) d1 = &d->get_udoc();
if (d1) d1->reset(dm);
@ -557,7 +570,9 @@ 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"););
IF_VERBOSE(3, r.display(verbose_stream() << "union: "););
IF_VERBOSE(3, if (d) d->display(verbose_stream() << "delta: "););
DEBUG_CODE(r.get_plugin().verify_union(fml0, src, r, d););
}
};
void udoc_plugin::mk_union(doc_manager& dm, udoc& dst, udoc const& src, udoc* delta) {
@ -907,7 +922,8 @@ namespace datalog {
class udoc_plugin::filter_interpreted_fn : public relation_mutator_fn {
union_find_default_ctx union_ctx;
doc_manager& dm;
expr_ref m_condition;
expr_ref m_original_condition;
expr_ref m_reduced_condition;
udoc m_udoc;
bit_vector m_empty_bv;
subset_ints m_equalities;
@ -915,7 +931,8 @@ namespace datalog {
public:
filter_interpreted_fn(const udoc_relation & t, ast_manager& m, app *condition) :
dm(t.get_dm()),
m_condition(m),
m_original_condition(condition, m),
m_reduced_condition(m),
m_equalities(union_ctx) {
unsigned num_bits = t.get_num_bits();
m_empty_bv.resize(num_bits, false);
@ -923,12 +940,12 @@ namespace datalog {
for (unsigned i = 0; i < num_bits; ++i) {
m_equalities.mk_var();
}
t.extract_guard(condition, guard, m_condition);
t.extract_guard(condition, guard, m_reduced_condition);
t.compile_guard(guard, m_udoc, m_empty_bv);
TRACE("doc",
tout << "original condition: " << mk_pp(condition, m) << "\n";
tout << "remaining condition: " << m_condition << "\n";
tout << "remaining condition: " << m_reduced_condition << "\n";
m_udoc.display(dm, tout) << "\n";);
}
@ -936,18 +953,22 @@ namespace datalog {
m_udoc.reset(dm);
}
virtual void operator()(relation_base & tb) {
virtual void operator()(relation_base & tb) {
udoc_relation & t = get(tb);
udoc& u = t.get_udoc();
ast_manager& m = m_condition.get_manager();
ast_manager& m = m_reduced_condition.get_manager();
expr_ref fml0(m);
DEBUG_CODE(t.to_formula(fml0););
SASSERT(u.well_formed(dm));
u.intersect(dm, m_udoc);
SASSERT(u.well_formed(dm));
t.apply_guard(m_condition, u, m_equalities, m_empty_bv);
t.apply_guard(m_reduced_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';);
IF_VERBOSE(3, t.display(verbose_stream()););
DEBUG_CODE(t.get_plugin().verify_filter(fml0, t, m_original_condition););
}
};
relation_mutator_fn * udoc_plugin::mk_filter_interpreted_fn(const relation_base & t, app * condition) {
@ -1048,7 +1069,8 @@ namespace datalog {
class udoc_plugin::filter_proj_fn : public convenient_relation_project_fn {
union_find_default_ctx union_ctx;
doc_manager& dm;
expr_ref m_condition;
expr_ref m_original_condition;
expr_ref m_reduced_condition;
udoc m_udoc;
bit_vector m_col_list; // map: col idx -> bool (whether the column is to be removed)
svector<bool> m_to_delete; // same
@ -1060,7 +1082,8 @@ namespace datalog {
unsigned col_cnt, const unsigned * removed_cols) :
convenient_relation_project_fn(t.get_signature(), col_cnt, removed_cols),
dm(t.get_dm()),
m_condition(m),
m_original_condition(condition, m),
m_reduced_condition(m),
m_equalities(union_ctx) {
t.expand_column_vector(m_removed_cols);
unsigned num_bits = t.get_num_bits();
@ -1075,9 +1098,9 @@ namespace datalog {
for (unsigned i = 0; i < m_removed_cols.size(); ++i) {
m_to_delete[m_removed_cols[i]] = true;
}
expr_ref guard(m), non_eq_cond(m);
expr_ref guard(m), non_eq_cond(condition, m);
t.extract_equalities(condition, non_eq_cond, m_equalities, m_roots);
t.extract_guard(non_eq_cond, guard, m_condition);
t.extract_guard(non_eq_cond, guard, m_reduced_condition);
t.compile_guard(guard, m_udoc, m_col_list);
}
@ -1088,26 +1111,31 @@ namespace datalog {
udoc_relation const & t = get(tb);
udoc const& u1 = t.get_udoc();
doc_manager& dm = t.get_dm();
ast_manager& m = m_condition.get_manager();
ast_manager& m = m_reduced_condition.get_manager();
udoc u2;
SASSERT(u1.well_formed(dm));
u2.copy(dm, u1);
SASSERT(u2.well_formed(dm));
u2.intersect(dm, m_udoc);
SASSERT(u2.well_formed(dm));
u2.merge(dm, m_roots, m_equalities, m_col_list);
SASSERT(u2.well_formed(dm));
t.apply_guard(m_condition, u2, m_equalities, m_col_list);
SASSERT(u2.well_formed(dm));
t.apply_guard(m_reduced_condition, u2, m_equalities, m_col_list);
SASSERT(u2.well_formed(dm));
DEBUG_CODE(
expr_ref fml0(m);
udoc_relation* r_test = get(t.get_plugin().mk_empty(t.get_signature()));
r_test->get_udoc().insert(dm, u2);
t.to_formula(fml0);
t.get_plugin().verify_filter(fml0, *r_test, m_original_condition);
r_test->deallocate(););
udoc_relation* r = get(t.get_plugin().mk_empty(get_result_signature()));
doc_manager& dm2 = r->get_dm();
// std::cout << "Size of union: " << u2.size() << "\n";
for (unsigned i = 0; i < u2.size(); ++i) {
doc* d = dm.project(dm2, m_to_delete.size(), m_to_delete.c_ptr(), u2[i]);
dm.verify_project(m, dm2, m_to_delete.c_ptr(), u2[i], *d);
r->get_udoc().insert(dm2, d);
SASSERT(r->get_udoc().well_formed(dm2));
}
u2.reset(dm);
IF_VERBOSE(3, r->display(verbose_stream() << "filter result:\n"););
IF_VERBOSE(3, r->display(verbose_stream() << "filter project result:\n"););
return r;
}
};
@ -1117,5 +1145,113 @@ namespace datalog {
return check_kind(t)?alloc(filter_proj_fn, get(t), get_ast_manager(), condition, removed_col_cnt, removed_cols):0;
}
// TBD: move this to relation validation module like table_checker.
void udoc_plugin::verify_join(relation_base const& t1, relation_base const& t2, relation_base const& t,
unsigned sz, unsigned const* cols1, unsigned const* cols2) {
ast_manager& m = get_ast_manager();
expr_ref fml1(m), fml2(m), fml3(m);
relation_signature const& sig1 = t1.get_signature();
relation_signature const& sig2 = t2.get_signature();
relation_signature const& sig = t.get_signature();
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 udoc_plugin::verify_filter(expr* fml0, relation_base const& t, expr* cond) {
expr_ref fml1(m), fml2(m);
fml1 = m.mk_and(fml0, cond);
t.to_formula(fml2);
relation_signature const& sig = t.get_signature();
expr_ref_vector vars(m);
var_subst sub(m, false);
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(fml2, vars.size(), vars.c_ptr(), fml2);
check_equiv(fml1, fml2);
}
void udoc_plugin::check_equiv(expr* fml1, expr* fml2) {
TRACE("doc", tout << mk_pp(fml1, m) << "\n";
tout << mk_pp(fml2, m) << "\n";);
smt_params fp;
smt::kernel solver(m, fp);
expr_ref tmp(m);
tmp = m.mk_not(m.mk_eq(fml1, fml2));
solver.assert_expr(tmp);
lbool res = solver.check();
IF_VERBOSE(3, verbose_stream() << "result of verification: " << res << "\n";);
if (res != l_false) {
throw 0;
}
SASSERT(res == l_false);
}
void udoc_plugin::verify_union(expr* fml0, relation_base const& src, relation_base const& dst, relation_base const* delta) {
expr_ref fml1(m), fml2(m), fml3(m);
src.to_formula(fml1);
dst.to_formula(fml2);
fml1 = m.mk_or(fml1, fml0);
relation_signature const& sig = dst.get_signature();
expr_ref_vector vars(m);
var_subst sub(m, false);
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(fml2, vars.size(), vars.c_ptr(), fml2);
check_equiv(fml1, fml2);
if (delta) {
delta->to_formula(fml3);
// dst >= delta >= dst \ fml0
// dst \ fml0 == delta & dst & \ fml0
// dst & delta = delta
expr_ref fml4(m), fml5(m);
fml4 = m.mk_and(fml2, m.mk_not(fml0));
fml5 = m.mk_and(fml3, fml4);
sub(fml4, vars.size(), vars.c_ptr(), fml4);
sub(fml5, vars.size(), vars.c_ptr(), fml5);
check_equiv(fml4, fml5);
fml4 = m.mk_and(fml3, fml2);
sub(fml3, vars.size(), vars.c_ptr(), fml3);
sub(fml4, vars.size(), vars.c_ptr(), fml4);
check_equiv(fml3, fml4);
}
}
}