From 7ae9734db2bcd8b3555c52ac87c39a7774b528e6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 4 Apr 2020 22:56:35 -0700 Subject: [PATCH] fix #3752 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/der.cpp | 222 +++++++++++++++++---------------------- src/ast/rewriter/der.h | 7 +- 2 files changed, 99 insertions(+), 130 deletions(-) diff --git a/src/ast/rewriter/der.cpp b/src/ast/rewriter/der.cpp index 196750a46..fdc75e652 100644 --- a/src/ast/rewriter/der.cpp +++ b/src/ast/rewriter/der.cpp @@ -22,6 +22,7 @@ Revision History: #include "ast/occurs.h" #include "ast/for_each_expr.h" #include "ast/rewriter/rewriter_def.h" +#include "ast/ast_util.h" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" #include "ast/ast_smt2_pp.h" @@ -30,85 +31,65 @@ static bool is_var(expr * e, unsigned num_decls) { return is_var(e) && to_var(e)->get_idx() < num_decls; } -static bool is_neg_var(ast_manager & m, expr * e, unsigned num_decls) { - return m.is_not(e) && is_var(to_app(e)->get_arg(0)) && to_var(to_app(e)->get_arg(0))->get_idx() < num_decls; +static bool is_neg_var(ast_manager & m, expr * e, var*& v, unsigned num_decls) { + expr* n = nullptr; + return m.is_not(e, n) && is_var(n) && (v = to_var(n), v->get_idx() < num_decls); } /** \brief Return true if \c e is of the form (not (= VAR t)) or (not (iff VAR t)) or (iff VAR t) or (iff (not VAR) t) or (VAR IDX) or (not (VAR IDX)). The last case can be viewed + + Remark: Occurs check is not necessary here... the top-sort procedure will check for cycles... + */ bool der::is_var_diseq(expr * e, unsigned num_decls, var * & v, expr_ref & t) { - // (not (= VAR t)) and (not (iff VAR t)) cases expr *eq, * lhs, *rhs; - if (m_manager.is_not(e, eq) && m_manager.is_eq(eq, lhs, rhs)) { - if (!is_var(lhs, num_decls) && !is_var(rhs, num_decls)) - return false; + auto set_result = [&](var *w, expr* s) { + v = w; + t = s; + TRACE("der", tout << mk_pp(e, m) << "\n";); + return true; + }; + + // (not (= VAR t)) + if (m.is_not(e, eq) && m.is_eq(eq, lhs, rhs)) { if (!is_var(lhs, num_decls)) std::swap(lhs, rhs); - SASSERT(is_var(lhs, num_decls)); - // Remark: Occurs check is not necessary here... the top-sort procedure will check for cycles... - // if (occurs(lhs, rhs)) { - // return false; - // } - v = to_var(lhs); - t = rhs; - TRACE("der", tout << mk_pp(e, m_manager) << "\n";); - return true; + if (!is_var(lhs, num_decls)) + return false; + return set_result(to_var(lhs), rhs); } - // (iff VAR t) and (iff (not VAR) t) cases - else if (m_manager.is_eq(e, lhs, rhs) && m_manager.is_bool(lhs)) { + + // (= VAR t) + if (m.is_eq(e, lhs, rhs) && m.is_bool(lhs)) { // (iff VAR t) case - if (is_var(lhs, num_decls) || is_var(rhs, num_decls)) { - if (!is_var(lhs, num_decls)) - std::swap(lhs, rhs); - SASSERT(is_var(lhs, num_decls)); - // Remark: Occurs check is not necessary here... the top-sort procedure will check for cycles... - // if (occurs(lhs, rhs)) { - // return false; - // } - v = to_var(lhs); - t = m_manager.mk_not(rhs); - m_new_exprs.push_back(t); - TRACE("der", tout << mk_pp(e, m_manager) << "\n";); - return true; + if (!is_var(lhs, num_decls)) + std::swap(lhs, rhs); + if (is_var(lhs, num_decls)) { + rhs = mk_not(m, rhs); + m_new_exprs.push_back(rhs); + return set_result(to_var(lhs), rhs); } // (iff (not VAR) t) case - else if (is_neg_var(m_manager, lhs, num_decls) || is_neg_var(m_manager, rhs, num_decls)) { - if (!is_neg_var(m_manager, lhs, num_decls)) - std::swap(lhs, rhs); - SASSERT(is_neg_var(m_manager, lhs, num_decls)); - expr * lhs_var = to_app(lhs)->get_arg(0); - // Remark: Occurs check is not necessary here... the top-sort procedure will check for cycles... - // if (occurs(lhs_var, rhs)) { - // return false; - // } - v = to_var(lhs_var); - t = rhs; - TRACE("der", tout << mk_pp(e, m_manager) << "\n";); - return true; - } - else { - return false; + if (!is_neg_var(m, lhs, v, num_decls)) + std::swap(lhs, rhs); + if (is_neg_var(m, lhs, v, num_decls)) { + return set_result(v, rhs); } + return false; } - // VAR != false case - else if (is_var(e, num_decls)) { - t = m_manager.mk_false(); - v = to_var(e); - TRACE("der", tout << mk_pp(e, m_manager) << "\n";); - return true; + + // VAR + if (is_var(e, num_decls)) { + return set_result(to_var(e), m.mk_false()); } - // VAR != true case - else if (is_neg_var(m_manager, e, num_decls)) { - t = m_manager.mk_true(); - v = to_var(to_app(e)->get_arg(0)); - TRACE("der", tout << mk_pp(e, m_manager) << "\n";); - return true; - } - else { - return false; + + // (not VAR) + if (is_neg_var(m, e, v, num_decls)) { + return set_result(v, m.mk_true()); } + return false; } void der::operator()(quantifier * q, expr_ref & r, proof_ref & pr) { @@ -116,27 +97,28 @@ void der::operator()(quantifier * q, expr_ref & r, proof_ref & pr) { pr = nullptr; r = q; - TRACE("der", tout << mk_pp(q, m_manager) << "\n";); + TRACE("der", tout << mk_pp(q, m) << "\n";); // Keep applying it until r doesn't change anymore do { - proof_ref curr_pr(m_manager); + proof_ref curr_pr(m); q = to_quantifier(r); reduce1(q, r, curr_pr); if (q != r) reduced = true; - if (m_manager.proofs_enabled()) { - pr = m_manager.mk_transitivity(pr, curr_pr); + if (m.proofs_enabled()) { + pr = m.mk_transitivity(pr, curr_pr); } - } while (q != r && is_quantifier(r)); + } + while (q != r && is_quantifier(r)); // Eliminate variables that have become unused if (reduced && is_forall(r)) { quantifier * q = to_quantifier(r); - r = elim_unused_vars(m_manager, q, params_ref()); - if (m_manager.proofs_enabled()) { - proof * p1 = m_manager.mk_elim_unused_vars(q, r); - pr = m_manager.mk_transitivity(pr, p1); + r = elim_unused_vars(m, q, params_ref()); + if (m.proofs_enabled()) { + proof * p1 = m.mk_elim_unused_vars(q, r); + pr = m.mk_transitivity(pr, p1); } } m_new_exprs.reset(); @@ -152,11 +134,10 @@ void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) { expr * e = q->get_expr(); unsigned num_decls = q->get_num_decls(); var * v = nullptr; - expr_ref t(m_manager); + expr_ref t(m); - if (m_manager.is_or(e)) { + if (m.is_or(e)) { unsigned num_args = to_app(e)->get_num_args(); - unsigned i = 0; unsigned diseq_count = 0; unsigned largest_vinx = 0; @@ -167,11 +148,11 @@ void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) { m_pos2var.reserve(num_args, -1); // Find all disequalities - for (; i < num_args; i++) { + for (unsigned i = 0; i < num_args; i++) { if (is_var_diseq(to_app(e)->get_arg(i), num_decls, v, t)) { unsigned idx = v->get_idx(); - if(m_map.get(idx, 0) == 0) { - m_map.reserve(idx + 1, 0); + if (m_map.get(idx, nullptr) == nullptr) { + m_map.reserve(idx + 1); m_inx2var.reserve(idx + 1, 0); m_map[idx] = t; @@ -193,33 +174,33 @@ void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) { } } else { - TRACE("der_bug", tout << "Did not find any diseq\n" << mk_pp(q, m_manager) << "\n";); + TRACE("der_bug", tout << "Did not find any diseq\n" << mk_pp(q, m) << "\n";); r = q; } } // Remark: get_elimination_order/top-sort checks for cycles, but it is not invoked for unit clauses. // So, we must perform a occurs check here. else if (is_var_diseq(e, num_decls, v, t) && !occurs(v, t)) { - r = m_manager.mk_false(); + r = m.mk_false(); } else r = q; - if (m_manager.proofs_enabled()) { - pr = r == q ? nullptr : m_manager.mk_der(q, r); + if (m.proofs_enabled()) { + pr = r == q ? nullptr : m.mk_der(q, r); } } -void der_sort_vars(ptr_vector & vars, ptr_vector & definitions, unsigned_vector & order) { +static void der_sort_vars(ptr_vector & vars, expr_ref_vector & definitions, unsigned_vector & order) { order.reset(); // eliminate self loops, and definitions containing quantifiers. bool found = false; for (unsigned i = 0; i < definitions.size(); i++) { var * v = vars[i]; - expr * t = definitions[i]; + expr * t = definitions.get(i); if (t == nullptr || has_quantifiers(t) || occurs(v, t)) - definitions[i] = 0; + definitions[i] = nullptr; else found = true; // found at least one candidate } @@ -236,7 +217,7 @@ void der_sort_vars(ptr_vector & vars, ptr_vector & definitions, unsig unsigned vidx, num; for (unsigned i = 0; i < definitions.size(); i++) { - if (definitions[i] == 0) + if (!definitions.get(i)) continue; var * v = vars[i]; SASSERT(v->get_idx() == i); @@ -246,7 +227,7 @@ void der_sort_vars(ptr_vector & vars, ptr_vector & definitions, unsig start: frame & fr = todo.back(); expr * t = fr.first; - if (t->get_ref_count() > 1 && done.is_marked(t)) { + if (done.is_marked(t)) { todo.pop_back(); continue; } @@ -256,23 +237,23 @@ void der_sort_vars(ptr_vector & vars, ptr_vector & definitions, unsig if (fr.second == 0) { CTRACE("der_bug", vidx >= definitions.size(), tout << "vidx: " << vidx << "\n";); // Remark: The size of definitions may be smaller than the number of variables occurring in the quantified formula. - if (definitions.get(vidx, 0) != 0) { + if (definitions.get(vidx, nullptr) != nullptr) { if (visiting.is_marked(t)) { // cycle detected: remove t visiting.reset_mark(t); - definitions[vidx] = 0; + definitions[vidx] = nullptr; } else { visiting.mark(t); fr.second = 1; - todo.push_back(frame(definitions[vidx], 0)); + todo.push_back(frame(definitions.get(vidx), 0)); goto start; } } } else { SASSERT(fr.second == 1); - if (definitions.get(vidx, 0) != 0) { + if (definitions.get(vidx, nullptr) != nullptr) { visiting.reset_mark(t); order.push_back(vidx); } @@ -281,8 +262,7 @@ void der_sort_vars(ptr_vector & vars, ptr_vector & definitions, unsig // do nothing } } - if (t->get_ref_count() > 1) - done.mark(t); + done.mark(t); todo.pop_back(); break; case AST_QUANTIFIER: @@ -294,13 +274,12 @@ void der_sort_vars(ptr_vector & vars, ptr_vector & definitions, unsig while (fr.second < num) { expr * arg = to_app(t)->get_arg(fr.second); fr.second++; - if (arg->get_ref_count() > 1 && done.is_marked(arg)) + if (done.is_marked(arg)) continue; todo.push_back(frame(arg, 0)); goto start; } - if (t->get_ref_count() > 1) - done.mark(t); + done.mark(t); todo.pop_back(); break; default: @@ -316,23 +295,20 @@ void der::get_elimination_order() { m_order.reset(); TRACE("top_sort", - tout << "DEFINITIONS: " << std::endl; - for(unsigned i = 0; i < m_map.size(); i++) - if(m_map[i]) tout << "VAR " << i << " = " << mk_pp(m_map[i], m_manager) << std::endl; + tout << "DEFINITIONS: " << std::endl; + unsigned i = 0; + for (expr* e : m_map) { + if (e) tout << "VAR " << i << " = " << mk_pp(e, m) << std::endl; + ++i; + } ); - // der::top_sort ts(m_manager); + // der::top_sort ts(m); der_sort_vars(m_inx2var, m_map, m_order); TRACE("der", - tout << "Elimination m_order:" << std::endl; - for(unsigned i=0; iget_arg(i)); } unsigned sz = m_new_args.size(); - expr_ref t(m_manager); - t = (sz == 1) ? m_new_args[0] : m_manager.mk_or(sz, m_new_args.c_ptr()); + expr_ref t(m); + t = (sz == 1) ? m_new_args[0] : m.mk_or(sz, m_new_args.c_ptr()); expr_ref new_e = m_subst(t, m_subst_map.size(), m_subst_map.c_ptr()); // don't forget to update the quantifier patterns - expr_ref_buffer new_patterns(m_manager); - expr_ref_buffer new_no_patterns(m_manager); + expr_ref_buffer new_patterns(m); + expr_ref_buffer new_no_patterns(m); for (unsigned j = 0; j < q->get_num_patterns(); j++) { new_patterns.push_back(m_subst(q->get_pattern(j), m_subst_map.size(), m_subst_map.c_ptr())); } @@ -381,17 +357,16 @@ void der::apply_substitution(quantifier * q, expr_ref & r) { new_no_patterns.push_back(m_subst(q->get_no_pattern(j), m_subst_map.size(), m_subst_map.c_ptr())); } - r = m_manager.update_quantifier(q, new_patterns.size(), new_patterns.c_ptr(), - new_no_patterns.size(), new_no_patterns.c_ptr(), new_e); + r = m.update_quantifier(q, new_patterns.size(), new_patterns.c_ptr(), + new_no_patterns.size(), new_no_patterns.c_ptr(), new_e); } struct der_rewriter_cfg : public default_rewriter_cfg { + ast_manager& m; der m_der; - der_rewriter_cfg(ast_manager & m):m_der(m) {} - - ast_manager & m() const { return m_der.m(); } + der_rewriter_cfg(ast_manager & m): m(m), m_der(m) {} bool reduce_quantifier(quantifier * old_q, expr * new_body, @@ -399,8 +374,9 @@ struct der_rewriter_cfg : public default_rewriter_cfg { expr * const * new_no_patterns, expr_ref & result, proof_ref & result_pr) { - quantifier_ref q1(m()); - q1 = m().update_quantifier(old_q, old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns, new_body); + quantifier_ref q1(m); + q1 = m.update_quantifier(old_q, old_q->get_num_patterns(), new_patterns, + old_q->get_num_no_patterns(), new_no_patterns, new_body); m_der(q1, result, result_pr); return true; } @@ -424,18 +400,12 @@ der_rewriter::~der_rewriter() { dealloc(m_imp); } -ast_manager & der_rewriter::m() const { - return m_imp->m(); -} - - void der_rewriter::operator()(expr * t, expr_ref & result, proof_ref & result_pr) { m_imp->operator()(t, result, result_pr); } - void der_rewriter::cleanup() { - ast_manager & m = m_imp->m(); + ast_manager & m = m_imp->m_cfg.m; dealloc(m_imp); m_imp = alloc(imp, m); } diff --git a/src/ast/rewriter/der.h b/src/ast/rewriter/der.h index 4dcf1e537..7db4f215c 100644 --- a/src/ast/rewriter/der.h +++ b/src/ast/rewriter/der.h @@ -123,11 +123,11 @@ Revision History: (forall (X Y) (or X /= s C[X])) --> (forall (Y) C[Y]) */ class der { - ast_manager & m_manager; + ast_manager & m; var_subst m_subst; expr_ref_buffer m_new_exprs; - ptr_vector m_map; + expr_ref_vector m_map; int_vector m_pos2var; ptr_vector m_inx2var; unsigned_vector m_order; @@ -153,8 +153,7 @@ class der { void reduce1(quantifier * q, expr_ref & r, proof_ref & pr); public: - der(ast_manager & m):m_manager(m),m_subst(m),m_new_exprs(m),m_subst_map(m),m_new_args(m) {} - ast_manager & m() const { return m_manager; } + der(ast_manager & m):m(m),m_subst(m),m_new_exprs(m),m_map(m), m_subst_map(m),m_new_args(m) {} void operator()(quantifier * q, expr_ref & r, proof_ref & pr); };