From dde0c9bd0d51844d1279f109fae744977ffdfe8b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 8 Apr 2020 04:34:36 -0700 Subject: [PATCH] fix #3833 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.h | 16 +++++++++++ src/ast/expr_abstract.cpp | 4 +-- src/ast/expr_abstract.h | 2 ++ src/muz/spacer/spacer_manager.cpp | 2 +- .../dl_mk_quantifier_abstraction.cpp | 27 +++++++++---------- src/qe/qe.cpp | 11 +++----- src/tactic/goal.cpp | 2 +- 7 files changed, 39 insertions(+), 25 deletions(-) diff --git a/src/ast/ast.h b/src/ast/ast.h index d81abc559..9ae559cc5 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1883,6 +1883,22 @@ public: app * mk_app(func_decl * decl, unsigned num_args, expr * const * args); + app* mk_app(func_decl* decl, ref_vector const& args) { + return mk_app(decl, args.size(), args.c_ptr()); + } + + app* mk_app(func_decl* decl, ref_vector const& args) { + return mk_app(decl, args.size(), (expr*const*)args.c_ptr()); + } + + app * mk_app(func_decl * decl, ptr_vector const& args) { + return mk_app(decl, args.size(), args.c_ptr()); + } + + app * mk_app(func_decl * decl, ptr_vector const& args) { + return mk_app(decl, args.size(), (expr*const*)args.c_ptr()); + } + app * mk_app(func_decl * decl, expr * const * args) { return mk_app(decl, decl->get_arity(), args); } diff --git a/src/ast/expr_abstract.cpp b/src/ast/expr_abstract.cpp index 022045a1d..e9d7f9ada 100644 --- a/src/ast/expr_abstract.cpp +++ b/src/ast/expr_abstract.cpp @@ -85,10 +85,10 @@ void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const* unsigned new_base = base + q->get_num_decls(); for (unsigned i = 0; i < q->get_num_patterns(); ++i) { - expr_abstract(m, new_base, num_bound, bound, q->get_pattern(i), result1); + result1 = expr_abstract(m, new_base, num_bound, bound, q->get_pattern(i)); patterns.push_back(result1.get()); } - expr_abstract(m, new_base, num_bound, bound, q->get_expr(), result1); + result1 = expr_abstract(m, new_base, num_bound, bound, q->get_expr()); b = m.update_quantifier(q, patterns.size(), patterns.c_ptr(), result1.get()); m_pinned.push_back(b); m_map.insert(curr, b); diff --git a/src/ast/expr_abstract.h b/src/ast/expr_abstract.h index a57a04b68..2bf43c61f 100644 --- a/src/ast/expr_abstract.h +++ b/src/ast/expr_abstract.h @@ -34,6 +34,8 @@ public: void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result); inline expr_ref expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n) { expr_ref r(m); expr_abstract(m, base, num_bound, bound, n, r); return r; } +inline expr_ref expr_abstract(expr_ref_vector const& bound, expr* n) { return expr_abstract(bound.m(), 0, bound.size(), bound.c_ptr(), n); } +inline expr_ref expr_abstract(app_ref_vector const& bound, expr* n) { return expr_abstract(bound.m(), 0, bound.size(), (expr*const*)bound.c_ptr(), n); } expr_ref mk_forall(ast_manager& m, unsigned num_bound, app* const* bound, expr* n); expr_ref mk_exists(ast_manager& m, unsigned num_bound, app* const* bound, expr* n); diff --git a/src/muz/spacer/spacer_manager.cpp b/src/muz/spacer/spacer_manager.cpp index f6f634e71..928837c25 100644 --- a/src/muz/spacer/spacer_manager.cpp +++ b/src/muz/spacer/spacer_manager.cpp @@ -94,7 +94,7 @@ void inductive_property::to_model(model_ref& md) const { for (unsigned j = 0; j < sig.size(); ++j) { sig_vars.push_back(m.mk_const(sig[sig.size() - j - 1])); } - expr_ref q = expr_abstract(m, 0, sig_vars.size(), sig_vars.c_ptr(), prop); + expr_ref q = expr_abstract(sig_vars, prop); md->register_decl(ri.m_pred, q); } TRACE("spacer", tout << *md;); diff --git a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp index 7eb46a943..9c823c57d 100644 --- a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp +++ b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp @@ -67,8 +67,8 @@ namespace datalog { void operator()(model_ref & old_model) override { model_ref new_model = alloc(model, m); for (unsigned i = 0; i < m_new_funcs.size(); ++i) { - func_decl* p = m_new_funcs[i].get(); - func_decl* q = m_old_funcs[i].get(); + func_decl* p = m_new_funcs.get(i); + func_decl* q = m_old_funcs.get(i); expr_ref_vector const& sub = m_subst[i]; sort_ref_vector const& sorts = m_sorts[i]; bool_vector const& is_bound = m_bound[i]; @@ -76,7 +76,6 @@ namespace datalog { expr_ref body(m); unsigned arity_q = q->get_arity(); SASSERT(0 < p->get_arity()); - func_interp* g = alloc(func_interp, m, arity_q); if (f) { body = f->get_interp(); @@ -88,11 +87,11 @@ namespace datalog { for (unsigned i = 0; i < p->get_arity(); ++i) { args.push_back(m.mk_var(i, p->get_domain(i))); } - body = m.mk_app(p, args.size(), args.c_ptr()); + body = m.mk_app(p, args); } // Create quantifier wrapper around body. - TRACE("dl", tout << mk_pp(body, m) << "\n";); + TRACE("dl", tout << body << "\n";); // 1. replace variables by the compound terms from // the original predicate. expr_safe_replace rep(m); @@ -102,7 +101,7 @@ namespace datalog { rep(body); rep.reset(); - TRACE("dl", tout << mk_pp(body, m) << "\n";); + TRACE("dl", tout << body << "\n";); // 2. replace bound variables by constants. expr_ref_vector consts(m), bound(m), _free(m); svector names; @@ -123,21 +122,21 @@ namespace datalog { rep(body); rep.reset(); - TRACE("dl", tout << mk_pp(body, m) << "\n";); + TRACE("dl", tout << body << "\n";); // 3. abstract and quantify those variables that should be bound. - expr_abstract(m, 0, bound.size(), bound.c_ptr(), body, body); + body = expr_abstract(bound, body); body = m.mk_forall(names.size(), bound_sorts.c_ptr(), names.c_ptr(), body); - TRACE("dl", tout << mk_pp(body, m) << "\n";); + TRACE("dl", tout << body << "\n";); // 4. replace remaining constants by variables. - for (unsigned i = 0; i < _free.size(); ++i) { - rep.insert(_free[i].get(), m.mk_var(i, m.get_sort(_free[i].get()))); + unsigned j = 0; + for (expr* f : _free) { + rep.insert(f, m.mk_var(j++, m.get_sort(f))); } rep(body); - g->set_else(body); - TRACE("dl", tout << mk_pp(body, m) << "\n";); - new_model->register_decl(q, g); + new_model->register_decl(q, body); + TRACE("dl", tout << body << "\n";); } old_model = new_model; } diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp index 0fe618e01..fbdac726c 100644 --- a/src/qe/qe.cpp +++ b/src/qe/qe.cpp @@ -2077,7 +2077,7 @@ namespace qe { if (num_vars > 0) { ptr_vector sorts; vector names; - ptr_vector free_vars; + app_ref_vector free_vars(m); for (unsigned i = 0; i < num_vars; ++i) { contains_app contains_x(m, vars[i]); if (contains_x(fml)) { @@ -2087,8 +2087,7 @@ namespace qe { } } if (!free_vars.empty()) { - expr_ref tmp(m); - expr_abstract(m, 0, free_vars.size(), (expr*const*)free_vars.c_ptr(), fml, tmp); + expr_ref tmp = expr_abstract(free_vars, fml); fml = m.mk_exists(free_vars.size(), sorts.c_ptr(), names.c_ptr(), tmp, 1); } } @@ -2279,9 +2278,7 @@ namespace qe { void expr_quant_elim::abstract_expr(unsigned sz, expr* const* bound, expr_ref& fml) { if (sz > 0) { - expr_ref tmp(m); - expr_abstract(m, 0, sz, bound, fml, tmp); - fml = tmp; + fml = expr_abstract(m, 0, sz, bound, fml); } } @@ -2620,7 +2617,7 @@ namespace qe { } var_shifter shift(m); shift(result, vars.size(), result); - expr_abstract(m, 0, vars.size(), (expr*const*)vars.c_ptr(), result, result); + result = expr_abstract(vars, result); TRACE("qe", tout << "abstracted" << mk_pp(result, m) << "\n";); ptr_vector sorts; svector names; diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp index 348f54878..497d760b1 100644 --- a/src/tactic/goal.cpp +++ b/src/tactic/goal.cpp @@ -305,7 +305,7 @@ void goal::update(unsigned i, expr * f, proof * pr, expr_dependency * d) { } } else { - SASSERT(!m().proofs_enabled()); + SASSERT(!proofs_enabled()); expr_ref fr(f, m()); quick_process(true, fr, d); if (!m_inconsistent) {