From cc794a19bc7ae96b703e6ff5e5e7ccd65c4e456c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 9 Apr 2020 10:31:21 -0700 Subject: [PATCH] more on #3858 elim_term_ite Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/var_subst.h | 4 ++ src/muz/transforms/dl_mk_elim_term_ite.cpp | 74 ++++++++++++---------- 2 files changed, 46 insertions(+), 32 deletions(-) diff --git a/src/ast/rewriter/var_subst.h b/src/ast/rewriter/var_subst.h index ff0217585..546f86b92 100644 --- a/src/ast/rewriter/var_subst.h +++ b/src/ast/rewriter/var_subst.h @@ -49,6 +49,8 @@ public: Otherwise, (VAR 0) is stored in the first position, (VAR 1) in the second, and so on. */ expr_ref operator()(expr * n, unsigned num_args, expr * const * args); + inline expr_ref operator()(expr * n, expr_ref_vector const& args) { return (*this)(n, args.size(), args.c_ptr()); } + inline expr_ref operator()(expr * n, ptr_vector const& args) { return (*this)(n, args.size(), args.c_ptr()); } void reset() { m_reducer.reset(); } }; @@ -90,6 +92,8 @@ class expr_free_vars { ptr_vector m_sorts; ptr_vector m_todo; public: + expr_free_vars() {} + expr_free_vars(expr* e) { (*this)(e); } void reset(); void operator()(expr* e); void accumulate(expr* e); diff --git a/src/muz/transforms/dl_mk_elim_term_ite.cpp b/src/muz/transforms/dl_mk_elim_term_ite.cpp index ddf6aa3aa..a13491eba 100644 --- a/src/muz/transforms/dl_mk_elim_term_ite.cpp +++ b/src/muz/transforms/dl_mk_elim_term_ite.cpp @@ -17,27 +17,32 @@ Revision History: --*/ -#include "muz/transforms/dl_mk_elim_term_ite.h" -#include "tactic/core/blast_term_ite_tactic.h" #include "ast/ast_util.h" #include "ast/expr_abstract.h" +#include "tactic/core/blast_term_ite_tactic.h" #include "tactic/tactic.h" #include "tactic/core/elim_term_ite_tactic.h" +#include "muz/transforms/dl_mk_elim_term_ite.h" namespace { + /** + * collect uninterpreted constants that are contained in ground + */ struct uninterp_const_collector { - app_ref_vector &m_consts; - uninterp_const_collector(app_ref_vector &v) : m_consts(v) {} + app_ref_vector& m_consts; + expr_ref_vector const& m_ground; + uninterp_const_collector(app_ref_vector &v, expr_ref_vector const& g) : m_consts(v), m_ground(g) {} void operator()(var *v) {} void operator()(quantifier *n) {} void operator()(expr *a){} void operator()(app *a){ - if (is_uninterp_const(a)) {m_consts.push_back(a);}; + if (is_uninterp_const(a) && m_ground.contains(a)) + m_consts.push_back(a); } }; - void collect_uninterp_consts(expr *e, app_ref_vector &v) { - uninterp_const_collector c(v); + void collect_uninterp_consts(expr *e, app_ref_vector &v, expr_ref_vector const& g) { + uninterp_const_collector c(v, g); quick_for_each_expr(c, e); } @@ -47,9 +52,9 @@ namespace { term_ite_proc(ast_manager &m) : m(m) {} void operator()(var *v) {} void operator()(quantifier *n) {} - void operator()(expr *a){} - void operator()(app *a){ - if (m.is_term_ite(a)) throw found(); + void operator()(expr *a) { + if (m.is_term_ite(a)) + throw found(); } }; @@ -57,14 +62,16 @@ namespace { term_ite_proc f(m); try { quick_for_each_expr(f, e); - } catch (const term_ite_proc::found &) { + } + catch (const term_ite_proc::found &) { return true; } return false; } - bool has_term_ite(expr_ref &e) { return has_term_ite(e, e.m());} + bool has_term_ite(expr_ref &e) { return has_term_ite(e, e.m());} } + namespace datalog { mk_elim_term_ite::mk_elim_term_ite(context & ctx, unsigned priority) : rule_transformer::plugin(priority, false), @@ -75,18 +82,23 @@ namespace datalog { mk_elim_term_ite::~mk_elim_term_ite() {} + /** + \brief map free variables in e to ground, fresh, constants + m_ground is reset on every new rule so it is safe to assume + that the sorts in m_ground are consistent. + */ expr_ref mk_elim_term_ite::ground(expr* e) { - expr_free_vars fv; - fv(e); - if (m_ground.size() < fv.size()) - m_ground.resize(fv.size()); + expr_free_vars fv(e); + m_ground.reserve(fv.size()); for (unsigned i = 0, sz = fv.size(); i < sz; ++i) { - if (fv[i] && !m_ground.get(i)) + if (!fv[i]) + continue; + if (!m_ground.get(i)) m_ground[i] = m.mk_fresh_const("c", fv[i]); + SASSERT(m.get_sort(m_ground.get(i)) == fv[i]); } - var_subst vsub(m, false); - return vsub(e, m_ground.size(), m_ground.c_ptr()); + return vsub(e, m_ground); } bool mk_elim_term_ite::elim(rule &r, rule_set &new_rules){ @@ -96,13 +108,12 @@ namespace datalog { unsigned utsz = r.get_uninterpreted_tail_size(); unsigned tsz = r.get_tail_size(); expr_ref_vector new_conjs(m); - expr_ref tmp(m); for (unsigned i = utsz; i < tsz; ++i) new_conjs.push_back(r.get_tail(i)); flatten_and(new_conjs); - expr_ref fml1(m), fml2(m), body(m), head(m); + expr_ref fml1(m), fml2(m), body(m); // blast ite body = mk_and(new_conjs); @@ -127,12 +138,11 @@ namespace datalog { rule_ref new_rule(rm.mk(r.get_head(), tail.size(), tail.c_ptr(), nullptr, r.name(), false), rm); rm.mk_rule_rewrite_proof(r, *new_rule.get()); new_rules.add_rule(new_rule); - TRACE("dl_term_ite", tout << "No term-ite after blast_term_ite\n";); + TRACE("dl", tout << "No term-ite after blast_term_ite\n";); return true; } - TRACE("dl_term_ite", - tout << "Rule has term-ite after blasting, starting elimination\n";); + TRACE("dl", tout << "Rule has term-ite after blasting, starting elimination\n";); body = ground(body); // elim ite tactic_ref elim_term_ite = mk_elim_term_ite_tactic(m); @@ -145,6 +155,7 @@ namespace datalog { unsigned sz = g->num_exprs(); (*elim_term_ite)(g, result); if (result.size() == 1) { + // NSB code review: fragile test for effect goal_ref new_goal = result[0]; if (new_goal->num_exprs() != sz) { new_conjs.reset(); @@ -160,20 +171,20 @@ namespace datalog { body = mk_and(new_conjs); rw(body); - head = ground(r.get_head()); - - fml2 = m.mk_implies(body, head); + fml2 = m.mk_implies(body, ground(r.get_head())); if (has_term_ite(fml2)) return false; app_ref_vector consts(m); - collect_uninterp_consts(fml2, consts); + collect_uninterp_consts(fml2, consts, m_ground); + fml2 = mk_forall(m, consts.size(), consts.c_ptr(), fml2); proof_ref p(m); rm.mk_rule(fml2, p, new_rules, r.name()); - // TBD: breaks abstraction barrier: mk_rule could convert a single formula + + // NSB code review: breaks abstraction barrier: mk_rule could convert a single formula // into multiple rules rm.mk_rule_rewrite_proof(r, *new_rules.last()); - TRACE("dl_term_ite", tout << "New rule: " << fml2 << "\n";); + TRACE("dl", tout << "New rule: " << fml2 << "\n";); return true; } @@ -188,8 +199,7 @@ namespace datalog { bool change = false; for (auto *rule : source) { if (m_ctx.canceled()) { - change = false; - break; + return nullptr; } change |= elim(*rule, *rules); }