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 bug in union_fn: delta should not be reset, it is shared among several union computations

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-09-24 16:46:00 -07:00
parent 6457654e2e
commit 979d1f913a
6 changed files with 86 additions and 77 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

65
src/muz/rel/check_relation.cpp
View file

@ -17,8 +17,8 @@ namespace datalog {
check_relation::~check_relation() {
m_relation->deallocate();
}
void check_relation::check_equiv(expr* f1, expr* f2) const {
get_plugin().check_equiv(f1, f2);
void check_relation::check_equiv(char const* objective, expr* f1, expr* f2) const {
get_plugin().check_equiv(objective, f1, f2);
}
void check_relation::consistent_formula() {
expr_ref fml(m);
@ -53,7 +53,7 @@ namespace datalog {
m_relation->add_fact(f);
m_relation->to_formula(fml1);
m_fml = m.mk_or(m_fml, mk_eq(f));
check_equiv(ground(m_fml), ground(fml1));
check_equiv("add_fact", ground(m_fml), ground(fml1));
m_fml = fml1;
}
void check_relation::add_new_fact(const relation_fact & f) {
@ -61,20 +61,20 @@ namespace datalog {
m_relation->add_new_fact(f);
m_relation->to_formula(fml1);
m_fml = m.mk_or(m_fml, mk_eq(f));
check_equiv(ground(m_fml), ground(fml1));
check_equiv("add_fact", ground(m_fml), ground(fml1));
m_fml = fml1;
}
bool check_relation::empty() const {
bool result = m_relation->empty();
if (result && !m.is_false(m_fml)) {
check_equiv(m.mk_false(), ground(m_fml));
check_equiv("empty", m.mk_false(), ground(m_fml));
}
return result;
}
bool check_relation::fast_empty() const {
bool result = m_relation->fast_empty();
if (result && !m.is_false(m_fml)) {
check_equiv(m.mk_false(), ground(m_fml));
check_equiv("fast_empty", m.mk_false(), ground(m_fml));
}
return result;
}
@ -89,10 +89,10 @@ namespace datalog {
fml1 = mk_eq(f);
fml2 = m.mk_and(m_fml, fml1);
if (result) {
check_equiv(ground(fml1), ground(fml2));
check_equiv("contains fact", ground(fml1), ground(fml2));
}
else if (!m.is_false(m_fml)) {
check_equiv(ground(fml2), m.mk_false());
check_equiv("contains fact", ground(fml2), m.mk_false());
}
return result;
}
@ -102,7 +102,7 @@ namespace datalog {
result->m_relation = m_relation->clone();
result->m_relation->to_formula(result->m_fml);
if (m_fml != result->m_fml) {
check_equiv(ground(m_fml), ground(result->m_fml));
check_equiv("clone", ground(m_fml), ground(result->m_fml));
}
return result;
}
@ -113,7 +113,7 @@ namespace datalog {
result->m_relation->to_formula(result->m_fml);
expr_ref fml(m);
fml = m.mk_not(m_fml);
check_equiv(ground(fml), ground(result->m_fml));
check_equiv("complement", ground(fml), ground(result->m_fml));
return result;
}
void check_relation::to_formula(expr_ref& fml) const {
@ -153,11 +153,19 @@ namespace datalog {
}
relation_base * check_relation_plugin::mk_empty(const relation_signature & sig) {
relation_base* r = m_base->mk_empty(sig);
return alloc(check_relation, *this, sig, r);
check_relation* result = alloc(check_relation, *this, sig, r);
if (result->m_fml != m.mk_false()) {
check_equiv("mk_empty", result->ground(result->m_fml), m.mk_false());
}
return result;
}
relation_base * check_relation_plugin::mk_full(func_decl* p, const relation_signature & s) {
relation_base* r = m_base->mk_full(p, s);
return alloc(check_relation, *this, s, r);
check_relation* result = alloc(check_relation, *this, s, r);
if (result->m_fml != m.mk_true()) {
check_equiv("mk_full", result->ground(result->m_fml), m.mk_true());
}
return result;
}
class check_relation_plugin::join_fn : public convenient_relation_join_fn {
@ -239,7 +247,7 @@ namespace datalog {
sub(f2, vars2.size(), vars2.c_ptr(), fml2);
bound.reverse();
fml1 = m.mk_exists(bound.size(), bound.c_ptr(), names.c_ptr(), fml1);
check_equiv(fml1, fml2);
check_equiv("project", fml1, fml2);
}
void check_relation_plugin::verify_permutation(
@ -277,7 +285,7 @@ namespace datalog {
subst(fml1, vars.size(), vars.c_ptr(), fml1);
subst(fml2, vars.size(), vars.c_ptr(), fml2);
check_equiv(fml1, fml2);
check_equiv("permutation", fml1, fml2);
}
void check_relation_plugin::verify_join(relation_base const& t1, relation_base const& t2, relation_base const& t,
@ -314,7 +322,7 @@ namespace datalog {
}
sub(fml1, vars.size(), vars.c_ptr(), fml1);
sub(fml3, vars.size(), vars.c_ptr(), fml3);
check_equiv(fml1, fml3);
check_equiv("join", fml1, fml3);
}
void check_relation_plugin::verify_filter(expr* fml0, relation_base const& t, expr* cond) {
@ -332,10 +340,10 @@ namespace datalog {
}
sub(fml1, vars.size(), vars.c_ptr(), fml1);
sub(fml2, vars.size(), vars.c_ptr(), fml2);
check_equiv(fml1, fml2);
check_equiv("filter", fml1, fml2);
}
void check_relation_plugin::check_equiv(expr* fml1, expr* fml2) {
void check_relation_plugin::check_equiv(char const* objective, expr* fml1, expr* fml2) {
TRACE("doc", tout << mk_pp(fml1, m) << "\n";
tout << mk_pp(fml2, m) << "\n";);
smt_params fp;
@ -345,7 +353,7 @@ namespace datalog {
solver.assert_expr(tmp);
lbool res = solver.check();
if (res == l_false) {
IF_VERBOSE(3, verbose_stream() << "verified\n";);
IF_VERBOSE(3, verbose_stream() << objective << " verified\n";);
}
else {
IF_VERBOSE(3, verbose_stream() << "NOT verified " << res << "\n";
@ -371,23 +379,24 @@ namespace datalog {
sub(fml1, vars.size(), vars.c_ptr(), fml1);
sub(fml2, vars.size(), vars.c_ptr(), fml2);
check_equiv(fml1, fml2);
check_equiv("union", fml1, fml2);
if (delta) {
delta->to_formula(fml3);
// dst >= delta >= dst \ fml0
IF_VERBOSE(3, verbose_stream() << "verify delta\n";
verbose_stream() << fml3 << "\n";);
// 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);
check_equiv("union delta low", 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("union delta high", fml3, fml4);
}
}
@ -560,7 +569,7 @@ namespace datalog {
expr_ref fml = t.m_fml;
t.rb().to_formula(t.m_fml);
fml = p.m.mk_and(fml, p.m.mk_eq(p.m.mk_var(m_col, t.get_signature()[m_col]), m_val));
p.check_equiv(t.ground(fml), t.ground(t.m_fml));
p.check_equiv("filter_equal", t.ground(fml), t.ground(t.m_fml));
}
};
relation_mutator_fn * check_relation_plugin::mk_filter_equal_fn(
@ -586,11 +595,11 @@ namespace datalog {
}
virtual void operator()(relation_base& tb, const relation_base& negb) {
IF_VERBOSE(0, verbose_stream() << "TBD: verify filter_negation\n";);
check_relation& t = get(tb);
check_relation const& n = get(negb);
check_relation_plugin& p = t.get_plugin();
(*m_filter)(t.rb(), n.rb());
IF_VERBOSE(0, verbose_stream() << "TBD: verify filter_negation\n";);
t.rb().to_formula(t.m_fml);
}
};

4
src/muz/rel/check_relation.h
View file

@ -34,7 +34,7 @@ namespace datalog {
ast_manager& m;
relation_base* m_relation;
expr_ref m_fml;
void check_equiv(expr* f1, expr* f2) const;
void check_equiv(char const* objective, expr* f1, expr* f2) const;
expr_ref mk_eq(relation_fact const& f) const;
public:
check_relation(check_relation_plugin& p, relation_signature const& s, relation_base* r);
@ -137,7 +137,7 @@ namespace datalog {
void check_equiv(expr* f1, expr* f2);
void check_equiv(char const* objective, expr* f1, expr* f2);
};

84
src/muz/rel/dl_compiler.cpp
View file

@ -589,49 +589,8 @@ namespace datalog {
dealloc = true;
}
//enforce negative predicates
unsigned ut_len=r->get_uninterpreted_tail_size();
for(unsigned i=pt_len; i<ut_len; i++) {
app * neg_tail = r->get_tail(i);
func_decl * neg_pred = neg_tail->get_decl();
variable_intersection neg_intersection(m_context.get_manager());
neg_intersection.populate(single_res_expr, neg_tail);
unsigned_vector t_cols(neg_intersection.size(), neg_intersection.get_cols1());
unsigned_vector neg_cols(neg_intersection.size(), neg_intersection.get_cols2());
unsigned neg_len = neg_tail->get_num_args();
for(unsigned i=0; i<neg_len; i++) {
expr * e = neg_tail->get_arg(i);
if(is_var(e)) {
continue;
}
SASSERT(is_app(e));
relation_sort arg_sort;
m_context.get_rel_context()->get_rmanager().from_predicate(neg_pred, i, arg_sort);
reg_idx new_reg;
bool new_dealloc;
make_add_constant_column(head_pred, filtered_res, arg_sort, to_app(e), new_reg, new_dealloc, acc);
if (dealloc)
make_dealloc_non_void(filtered_res, acc);
dealloc = new_dealloc;
filtered_res = new_reg; // here filtered_res value gets changed !!
t_cols.push_back(single_res_expr.size());
neg_cols.push_back(i);
single_res_expr.push_back(e);
}
SASSERT(t_cols.size()==neg_cols.size());
reg_idx neg_reg = m_pred_regs.find(neg_pred);
if (!dealloc)
make_clone(filtered_res, filtered_res, acc);
acc.push_back(instruction::mk_filter_by_negation(filtered_res, neg_reg, t_cols.size(),
t_cols.c_ptr(), neg_cols.c_ptr()));
dealloc = true;
}
// enforce interpreted tail predicates
unsigned ut_len=r->get_uninterpreted_tail_size();
unsigned ft_len = r->get_tail_size(); // full tail
ptr_vector<expr> tail;
for (unsigned tail_index = ut_len; tail_index < ft_len; ++tail_index) {
@ -737,6 +696,47 @@ namespace datalog {
dealloc = true;
}
//enforce negative predicates
for (unsigned i = pt_len; i<ut_len; i++) {
app * neg_tail = r->get_tail(i);
func_decl * neg_pred = neg_tail->get_decl();
variable_intersection neg_intersection(m_context.get_manager());
neg_intersection.populate(single_res_expr, neg_tail);
unsigned_vector t_cols(neg_intersection.size(), neg_intersection.get_cols1());
unsigned_vector neg_cols(neg_intersection.size(), neg_intersection.get_cols2());
unsigned neg_len = neg_tail->get_num_args();
for (unsigned i = 0; i<neg_len; i++) {
expr * e = neg_tail->get_arg(i);
if (is_var(e)) {
continue;
}
SASSERT(is_app(e));
relation_sort arg_sort;
m_context.get_rel_context()->get_rmanager().from_predicate(neg_pred, i, arg_sort);
reg_idx new_reg;
bool new_dealloc;
make_add_constant_column(head_pred, filtered_res, arg_sort, to_app(e), new_reg, new_dealloc, acc);
if (dealloc)
make_dealloc_non_void(filtered_res, acc);
dealloc = new_dealloc;
filtered_res = new_reg; // here filtered_res value gets changed !!
t_cols.push_back(single_res_expr.size());
neg_cols.push_back(i);
single_res_expr.push_back(e);
}
SASSERT(t_cols.size() == neg_cols.size());
reg_idx neg_reg = m_pred_regs.find(neg_pred);
if (!dealloc)
make_clone(filtered_res, filtered_res, acc);
acc.push_back(instruction::mk_filter_by_negation(filtered_res, neg_reg, t_cols.size(),
t_cols.c_ptr(), neg_cols.c_ptr()));
dealloc = true;
}
#if 0
// this version is potentially better for non-symbolic tables,
// since it constraints each unbound column at a time (reducing the

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

@ -346,7 +346,7 @@ namespace datalog {
print_container(m_controls, out);
}
virtual void display_body_impl(rel_context_base const & ctx, std::ostream & out, std::string indentation) const {
m_body->display_indented(ctx, out, indentation+" ");
// m_body->display_indented(ctx, out, indentation+" ");
}
};

2
src/muz/rel/rel_context.cpp
View file

@ -157,6 +157,7 @@ namespace datalog {
break;
}
TRACE("dl", m_context.display(tout););
//IF_VERBOSE(3, m_context.display_smt2(0,0,verbose_stream()););
if (m_context.get_params().print_aig().size()) {
const char *filename = static_cast<const char*>(m_context.get_params().print_aig().c_ptr());
@ -580,7 +581,6 @@ namespace datalog {
void rel_context::updt_params() {
if (m_context.check_relation() != symbol::null &&
m_context.check_relation() != symbol("null")) {
std::cout << m_context.check_relation() << "\n";
symbol cr("check_relation");
m_context.set_default_relation(cr);
relation_plugin* p = get_rmanager().get_relation_plugin(cr);

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

@ -561,11 +561,9 @@ namespace datalog {
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);
IF_VERBOSE(3, r.display(verbose_stream() << "orig: "););
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));
@ -1051,6 +1049,7 @@ namespace datalog {
}
std::swap(dst, result);
if (dst.is_empty()) {
IF_VERBOSE(3, tb.display(verbose_stream()););
return;
}
@ -1070,6 +1069,7 @@ namespace datalog {
TRACE("doc", dst.display(dm, tout) << "\n";);
SASSERT(dst.well_formed(dm));
renamed_neg.reset(t.get_dm());
IF_VERBOSE(3, tb.display(verbose_stream()););
}
void copy_column(
doc& dst, doc const& src,