From 8f7494cb0456ff85003cc83f7f08cdedba5d1b27 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 31 Oct 2012 20:29:28 -0700 Subject: [PATCH] disable buggy code in slicer: it removes conjuncts for non-sliced variables. It should use the same criteria as the slice recognizer. reported by Arie Gurfinkel Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_mk_slice.cpp | 67 ++++++++++++--------- src/muz_qe/dl_mk_slice.h | 2 + src/muz_qe/horn_subsume_model_converter.cpp | 2 +- src/muz_qe/pdr_util.cpp | 12 +++- 4 files changed, 52 insertions(+), 31 deletions(-) diff --git a/src/muz_qe/dl_mk_slice.cpp b/src/muz_qe/dl_mk_slice.cpp index 4edfb5b65..0b9115e57 100644 --- a/src/muz_qe/dl_mk_slice.cpp +++ b/src/muz_qe/dl_mk_slice.cpp @@ -429,6 +429,33 @@ namespace datalog { } } + void mk_slice::solve_vars(rule& r, uint_set& used_vars, uint_set& parameter_vars) { + expr_ref_vector conjs = get_tail_conjs(r); + for (unsigned j = 0; j < conjs.size(); ++j) { + expr* e = conjs[j].get(); + expr_ref r(m); + unsigned v; + if (is_eq(e, v, r) && is_output(v) && m_var_is_sliceable[v]) { + TRACE("dl", tout << "is_eq: " << mk_pp(e, m) << " " << (m_solved_vars[v].get()?"solved":"new") << "\n";); + add_var(v); + if (!m_solved_vars[v].get()) { + add_free_vars(parameter_vars, r); + m_solved_vars[v] = r; + } + else { + // variables can only be solved once. + add_free_vars(used_vars, e); + add_free_vars(used_vars, m_solved_vars[v].get()); + used_vars.insert(v); + } + } + else { + add_free_vars(used_vars, e); + } + } + } + + bool mk_slice::prune_rule(rule& r) { TRACE("dl", r.display(m_ctx, tout << "prune:\n"); ); bool change = false; @@ -452,30 +479,8 @@ namespace datalog { // Collect the set of variables that are solved. // Collect the occurrence count of the variables per conjunct. // - expr_ref_vector conjs = get_tail_conjs(r); uint_set used_vars, parameter_vars; - for (unsigned j = 0; j < conjs.size(); ++j) { - expr* e = conjs[j].get(); - expr_ref r(m); - unsigned v; - if (is_eq(e, v, r) && is_output(v) && m_var_is_sliceable[v]) { - TRACE("dl", tout << "is_eq: " << mk_pp(e, m) << " " << (m_solved_vars[v].get()?"solved":"new") << "\n";); - add_var(v); - if (!m_solved_vars[v].get()) { - add_free_vars(parameter_vars, r); - m_solved_vars[v] = r; - } - else { - // variables can only be solved once. - add_free_vars(used_vars, e); - add_free_vars(used_vars, m_solved_vars[v].get()); - used_vars.insert(v); - } - } - else { - add_free_vars(used_vars, e); - } - } + solve_vars(r, used_vars, parameter_vars); uint_set::iterator it = used_vars.begin(), end = used_vars.end(); for (; it != end; ++it) { if (*it < m_var_is_sliceable.size()) { @@ -725,9 +730,11 @@ namespace datalog { } } + void mk_slice::update_rule(rule& r, rule_set& dst) { rule* new_rule; if (rule_updated(r)) { + init_vars(r); app_ref_vector tail(m); app_ref head(m); ptr_vector sorts; @@ -742,10 +749,12 @@ namespace datalog { expr_ref_vector conjs = get_tail_conjs(r); m_solved_vars.reset(); + +#if 0 uint_set used_vars; - unsigned v; expr_ref b(m); + TBD: buggy code: for (unsigned i = 0; i < conjs.size(); ++i) { expr* e = conjs[i].get(); if (is_eq(e, v, b)) { @@ -772,15 +781,17 @@ namespace datalog { add_free_vars(used_vars, e); } } +#endif for (unsigned i = 0; i < conjs.size(); ++i) { expr* e = conjs[i].get(); - if (is_eq(e, v, b) && m_solved_vars[v].get() && !used_vars.contains(v)) { +#if 0 + if (false && is_eq(e, v, b) && m_solved_vars[v].get() && !used_vars.contains(v)) { TRACE("dl", tout << "removing conjunct: " << mk_pp(e, m) << "\n";); // skip conjunct } - else { - tail.push_back(to_app(e)); - } +#endif + tail.push_back(to_app(e)); + } new_rule = rm.mk(head.get(), tail.size(), tail.c_ptr(), (const bool*) 0); diff --git a/src/muz_qe/dl_mk_slice.h b/src/muz_qe/dl_mk_slice.h index ef331534d..cf6d8ad62 100644 --- a/src/muz_qe/dl_mk_slice.h +++ b/src/muz_qe/dl_mk_slice.h @@ -89,6 +89,8 @@ namespace datalog { void update_predicate(app* p, app_ref& q); + void solve_vars(rule& r, uint_set& used_vars, uint_set& parameter_vars); + public: /** \brief Create slice rule transformer for \c goal predicate. When applying the transformer, diff --git a/src/muz_qe/horn_subsume_model_converter.cpp b/src/muz_qe/horn_subsume_model_converter.cpp index 048f492fe..374333a9c 100644 --- a/src/muz_qe/horn_subsume_model_converter.cpp +++ b/src/muz_qe/horn_subsume_model_converter.cpp @@ -195,7 +195,7 @@ void horn_subsume_model_converter::operator()(model_ref& mr) { body = m.mk_or(e, body); } m_rewrite(body); - mr->register_decl(h, m.mk_or(e, body)); + mr->register_decl(h, body); } else { func_interp* f = mr->get_func_interp(h); diff --git a/src/muz_qe/pdr_util.cpp b/src/muz_qe/pdr_util.cpp index c4a897503..a543593b3 100644 --- a/src/muz_qe/pdr_util.cpp +++ b/src/muz_qe/pdr_util.cpp @@ -916,6 +916,7 @@ bool model_evaluator::check_model(ptr_vector const& formulas) { class test_diff_logic { ast_manager& m; arith_util a; + bv_util bv; bool m_is_dl; bool is_numeric(expr* e) const { @@ -1017,14 +1018,21 @@ bool model_evaluator::check_model(ptr_vector const& formulas) { return false; } family_id fid = to_app(e)->get_family_id(); + + if (fid == null_family_id && + !m.is_bool(e) && + to_app(e)->get_num_args() > 0) { + return true; + } return fid != m.get_basic_family_id() && fid != null_family_id && - fid != a.get_family_id(); + fid != a.get_family_id() && + fid != bv.get_family_id(); } public: - test_diff_logic(ast_manager& m): m(m), a(m), m_is_dl(true) {} + test_diff_logic(ast_manager& m): m(m), a(m), bv(m), m_is_dl(true) {} void operator()(expr* e) { if (!m_is_dl) {