diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp index b02aac4eab..87f17beb87 100644 --- a/src/ast/pattern/pattern_inference.cpp +++ b/src/ast/pattern/pattern_inference.cpp @@ -121,6 +121,7 @@ void pattern_inference_cfg::collect::operator()(expr * n, unsigned num_bindings) SASSERT(m_info.empty()); SASSERT(m_todo.empty()); SASSERT(m_cache.empty()); + SASSERT(is_well_sorted(m, n)); m_num_bindings = num_bindings; m_todo.push_back(entry(n, 0)); while (!m_todo.empty()) { @@ -173,21 +174,15 @@ void pattern_inference_cfg::collect::save_candidate(expr * n, unsigned delta) { switch (n->get_kind()) { case AST_VAR: { unsigned idx = to_var(n)->get_idx(); - if (idx >= delta) { - idx = idx - delta; - uint_set free_vars; - if (idx < m_num_bindings) - free_vars.insert(idx); - info * i = nullptr; - if (delta == 0) - i = alloc(info, m, n, free_vars, 1); - else - i = alloc(info, m, m.mk_var(idx, to_var(n)->get_sort()), free_vars, 1); - save(n, delta, i); - } - else { + if (idx >= m_num_bindings + delta) { save(n, delta, nullptr); + return; } + uint_set free_vars; + if (delta <= idx) + free_vars.insert(idx - delta); + info * i = alloc(info, m, n, free_vars, 1); + save(n, delta, i); return; } case AST_APP: { @@ -243,7 +238,8 @@ void pattern_inference_cfg::collect::save_candidate(expr * n, unsigned delta) { // stating properties about these operators. family_id fid = c->get_family_id(); decl_kind k = c->get_decl_kind(); - if (!free_vars.empty() && + if (!free_vars.empty() && + delta == 0 && (fid != m_afid || (fid == m_afid && !m_owner.m_nested_arith_only && (k == OP_DIV || k == OP_IDIV || k == OP_MOD || k == OP_REM || k == OP_MUL)))) { TRACE(pattern_inference, tout << "potential candidate: \n" << mk_pp(new_node, m) << "\n";); m_owner.add_candidate(new_node, free_vars, size); @@ -254,30 +250,15 @@ void pattern_inference_cfg::collect::save_candidate(expr * n, unsigned delta) { quantifier * q = to_quantifier(n); unsigned num_decls = q->get_num_decls(); info * body_info = nullptr; - m_cache.find(entry(q->get_expr(), delta + num_decls), body_info); - if (body_info == nullptr) { + expr *body = q->get_expr(); + m_cache.find(entry(body, delta + num_decls), body_info); + if (!body_info) { save(n, delta, nullptr); return; } - // The lambda/quantifier itself is a valid sub-term in a pattern. - // body_info->m_node was normalized into the *outer* quantifier's de - // Bruijn space (the enclosing binders, including this lambda's own - // num_decls binders, were stripped). Re-wrapping it under the lambda - // therefore requires shifting the (outer) free variables back up by - // num_decls so they do not collide with the lambda's bound variables. - // The lambda's own bound variables never occur in body_info (any - // sub-term referring to them was rejected as a candidate), so the - // shift is always sound. - expr * body = body_info->m_node.get(); - expr_ref new_body(m); - if (num_decls > 0) { - var_shifter shift(m); - shift(body, num_decls, new_body); - } - else - new_body = body; + expr *new_body = body_info->m_node.get(); quantifier_ref new_q(m); - if (new_body.get() != q->get_expr()) + if (new_body != q->get_expr()) new_q = m.update_quantifier(q, new_body); else new_q = q; diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp index ff656b7ef4..e452651571 100644 --- a/src/cmd_context/tptp_frontend.cpp +++ b/src/cmd_context/tptp_frontend.cpp @@ -553,10 +553,9 @@ class tptp_parser { // Multi-argument A * B > C is represented as Array(A, Array(B, C)) (curried). sort* get_ho_sort(ptr_vector const& domain, sort* range) { sort* s = range; - for (int i = (int)domain.size() - 1; i >= 0; --i) { - s = m_array.mk_array_sort(domain[i], s); - m_pinned_sorts.push_back(s); - } + for (unsigned i = domain.size(); i-- > 0; ) + s = m_array.mk_array_sort(domain[i], s); + m_pinned_sorts.push_back(s); return s; } @@ -1535,7 +1534,7 @@ class tptp_parser { // For function-style definitions, wrap value in lambdas if (!param_vars.empty()) { expr_ref result = value; - for (int i = (int)param_vars.size() - 1; i >= 0; --i) { + for (unsigned i = param_vars.size(); i-- > 0; ) { expr_ref abs_body(m); expr_abstract(m, 0, 1, (expr* const*)¶m_vars[i], result, abs_body); sort* s = param_vars[i]->get_sort(); @@ -1976,7 +1975,7 @@ class tptp_parser { // Create nested single-variable lambdas (curried) to match our curried array encoding. // ^[X:A, Y:B] : body becomes ^[X:A] : (^[Y:B] : body) with sort Array(A, Array(B, body_sort)) expr_ref result = body; - for (int i = (int)vars.size() - 1; i >= 0; --i) { + for (unsigned i = vars.size(); i-- > 0; ) { expr_ref abs_body(m); expr_abstract(m, 0, 1, (expr* const*)&vars[i], result, abs_body); sort* s = vars[i]->get_sort(); @@ -2877,6 +2876,7 @@ expr_ref tptp_parser::parse_term() { if (!m_array.is_array(e_sort)) { sort* arg_sort = arg->get_sort(); sort* arr_sort = m_array.mk_array_sort(arg_sort, m_univ); + m_pinned_sorts.push_back(arr_sort); e = coerce_arg(e, arr_sort); } else { sort* dom = get_array_domain(e_sort, 0); diff --git a/src/solver/assertions/asserted_formulas.cpp b/src/solver/assertions/asserted_formulas.cpp index 32b8bb9b65..6abf5dbb96 100644 --- a/src/solver/assertions/asserted_formulas.cpp +++ b/src/solver/assertions/asserted_formulas.cpp @@ -496,6 +496,7 @@ void asserted_formulas::simplify_fmls::operator()() { expr_ref result(m); proof_ref result_pr(m); simplify(j, result, result_pr); + SASSERT(is_well_sorted(m, j.fml())); if (m.proofs_enabled()) { if (!result_pr) result_pr = m.mk_rewrite(j.fml(), result); result_pr = m.mk_modus_ponens(j.pr(), result_pr);