From 1fce2905ece8b119461ab475c79a30a0ea45b1c6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 9 Apr 2020 19:38:08 -0700 Subject: [PATCH] fix #3832 Signed-off-by: Nikolaj Bjorner --- src/muz/transforms/dl_mk_bit_blast.cpp | 10 +++++++--- src/muz/transforms/dl_mk_rule_inliner.cpp | 16 +++++++++++++--- src/muz/transforms/dl_mk_rule_inliner.h | 2 ++ src/smt/theory_arith_nl.h | 5 ++--- 4 files changed, 24 insertions(+), 9 deletions(-) diff --git a/src/muz/transforms/dl_mk_bit_blast.cpp b/src/muz/transforms/dl_mk_bit_blast.cpp index ef5ce8be4..8242d6458 100644 --- a/src/muz/transforms/dl_mk_bit_blast.cpp +++ b/src/muz/transforms/dl_mk_bit_blast.cpp @@ -190,13 +190,17 @@ namespace datalog { m_g_vars.push_back(m_f_vars.back()); } } + if (f->get_family_id() != null_family_id) { + return BR_FAILED; + } func_decl* g = nullptr; + if (!m_pred2blast.find(f, g)) { ptr_vector domain; - for (unsigned i = 0; i < m_args.size(); ++i) { - domain.push_back(m.get_sort(m_args[i].get())); + for (expr* arg : m_args) { + domain.push_back(m.get_sort(arg)); } g = m_context.mk_fresh_head_predicate(f->get_name(), symbol("bv"), m_args.size(), domain.c_ptr(), f); m_old_funcs.push_back(f); @@ -205,7 +209,7 @@ namespace datalog { m_dst->inherit_predicate(*m_src, f, g); } - result = m.mk_app(g, m_args.size(), m_args.c_ptr()); + result = m.mk_app(g, m_args); result_pr = nullptr; return BR_DONE; } diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp index ce69dad85..f06efec6f 100644 --- a/src/muz/transforms/dl_mk_rule_inliner.cpp +++ b/src/muz/transforms/dl_mk_rule_inliner.cpp @@ -172,7 +172,8 @@ namespace datalog { tgt.norm_vars(m_context.get_rule_manager()); - SASSERT(!has_quantifier(src)); + if (has_quantifier(src)) + throw has_new_quantifier(); if (!m_unifier.unify_rules(tgt, tail_index, src)) { return false; @@ -425,7 +426,11 @@ namespace datalog { unsigned i = 0; for (; i < pt_len && !inlining_allowed(orig, r->get_decl(i)); ++i) {}; - SASSERT(!has_quantifier(*r.get())); + CTRACE("dl", has_quantifier(*r.get()), r->display(m_context, tout);); + if (has_quantifier(*r.get())) { + tgt.add_rule(r); + continue; + } if (i == pt_len) { //there's nothing we can inline in this rule @@ -842,7 +847,12 @@ namespace datalog { if (m_context.get_params().xform_inline_eager()) { TRACE("dl", source.display(tout << "before eager inlining\n");); plan_inlining(source); - something_done = transform_rules(source, *res); + try { + something_done = transform_rules(source, *res); + } + catch (has_new_quantifier) { + return nullptr; + } VERIFY(res->close()); //this transformation doesn't break the negation stratification // try eager inlining if (do_eager_inlining(res)) { diff --git a/src/muz/transforms/dl_mk_rule_inliner.h b/src/muz/transforms/dl_mk_rule_inliner.h index 8cf738bd8..aebf79e10 100644 --- a/src/muz/transforms/dl_mk_rule_inliner.h +++ b/src/muz/transforms/dl_mk_rule_inliner.h @@ -82,6 +82,8 @@ namespace datalog { class mk_rule_inliner : public rule_transformer::plugin { + struct has_new_quantifier {}; + class visitor : public st_visitor { context& m_context; unsigned_vector m_unifiers; diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 37b8181a6..a5a04f45a 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -166,8 +166,7 @@ std::pair theory_arith::analyze_monomial(expr * m) const { unsigned c = 0; int free_var_idx = -1; int idx = 0; - for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) { - expr * arg = to_app(m)->get_arg(i); + for (expr * arg : *to_app(m)) { if (m_util.is_numeral(arg)) continue; if (var == nullptr) { @@ -202,7 +201,7 @@ std::pair theory_arith::analyze_monomial(expr * m) const { template expr * theory_arith::get_monomial_body(expr * m) const { SASSERT(m_util.is_mul(m)); - if (m_util.is_numeral(to_app(m)->get_arg(0))) + if (to_app(m)->get_num_args() == 2 && m_util.is_numeral(to_app(m)->get_arg(0))) return to_app(m)->get_arg(1); return m; }