From 4938ea7be615627e8994d59c25930cc1d5092974 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 27 Apr 2020 11:44:25 -0700 Subject: [PATCH] fix #4123 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 2 +- src/ast/ast.h | 2 +- src/smt/CMakeLists.txt | 1 + src/tactic/arith/purify_arith_tactic.cpp | 41 +++++++----------------- 4 files changed, 15 insertions(+), 31 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 48d922f29..bc7bd5edb 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1981,7 +1981,7 @@ void ast_manager::delete_node(ast * n) { } if (m_debug_ref_count) { m_debug_free_indices.insert(n->m_id,0); - } + } deallocate_node(n, ::get_node_size(n)); } } diff --git a/src/ast/ast.h b/src/ast/ast.h index 2b24d5558..4dc59542d 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -489,7 +489,7 @@ protected: void dec_ref() { SASSERT(m_ref_count > 0); - m_ref_count --; + --m_ref_count; } ast(ast_kind k):m_id(UINT_MAX), m_kind(k), m_mark1(false), m_mark2(false), m_mark_shared_occs(false), m_ref_count(0) { diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt index f6afd539f..a8f7303e7 100644 --- a/src/smt/CMakeLists.txt +++ b/src/smt/CMakeLists.txt @@ -10,6 +10,7 @@ z3_add_component(smt expr_context_simplifier.cpp fingerprints.cpp mam.cpp + model_sweeper.cpp old_interval.cpp qi_queue.cpp seq_axioms.cpp diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index a4760c0ac..c981cf8af 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -726,44 +726,27 @@ struct purify_arith_proc { r(q->get_expr(), new_body, new_body_pr); unsigned num_vars = r.cfg().m_new_vars.size(); expr_ref_vector & cnstrs = r.cfg().m_new_cnstrs; - if (true || !cnstrs.empty()) { + if (num_vars == 0 && !cnstrs.empty()) { cnstrs.push_back(new_body); - new_body = m().mk_and(cnstrs.size(), cnstrs.c_ptr()); + new_body = m().mk_and(cnstrs); } TRACE("purify_arith", tout << "num_vars: " << num_vars << "\n"; - tout << "body: " << mk_ismt2_pp(q->get_expr(), m()) << "\nnew_body: " << mk_ismt2_pp(new_body, m()) << "\n";); + tout << "body: " << mk_ismt2_pp(q->get_expr(), m()) << "\nnew_body: " << new_body << "\n";); if (num_vars == 0) { result = m().update_quantifier(q, new_body); + if (m_produce_proofs) { + auto& cnstr_prs = r.cfg().m_new_cnstr_prs; + result_pr = m().mk_rewrite_star(q->get_expr(), new_body, cnstr_prs.size(), cnstr_prs.c_ptr()); + result_pr = m().mk_quant_intro(q, to_quantifier(result.get()), result_pr); + r.cfg().push_cnstr_pr(result_pr); + } } else { - // Add new constraints - // Open space for new variables - var_shifter shifter(m()); - shifter(new_body, num_vars, new_body); - // Rename fresh constants in r.cfg().m_new_vars to variables - ptr_buffer sorts; - buffer names; - expr_substitution subst(m(), false, false); - for (unsigned i = 0; i < num_vars; i++) { - expr * c = r.cfg().m_new_vars.get(i); - sort * s = get_sort(c); - sorts.push_back(s); - names.push_back(m().mk_fresh_var_name("x")); - unsigned idx = num_vars - i - 1; - subst.insert(c, m().mk_var(idx, s)); + result = q; + if (m_produce_proofs) { + r.cfg().push_cnstr_pr(nullptr); } - scoped_ptr replacer = mk_default_expr_replacer(m(), false); - replacer->set_substitution(&subst); - (*replacer)(new_body, new_body); - new_body = m().mk_exists(num_vars, sorts.c_ptr(), names.c_ptr(), new_body, q->get_weight()); - result = m().update_quantifier(q, new_body); - } - if (m_produce_proofs) { - auto& cnstr_prs = r.cfg().m_new_cnstr_prs; - result_pr = m().mk_rewrite_star(q->get_expr(), new_body, cnstr_prs.size(), cnstr_prs.c_ptr()); - result_pr = m().mk_quant_intro(q, to_quantifier(result.get()), result_pr); - r.cfg().push_cnstr_pr(result_pr); } }