diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp index a8ad720b07..2bf6850d56 100644 --- a/src/ast/pattern/pattern_inference.cpp +++ b/src/ast/pattern/pattern_inference.cpp @@ -540,7 +540,7 @@ bool pattern_inference_cfg::is_forbidden(app * n) const { // Remark: skolem constants should not be used in patterns, since they do not // occur outside of the quantifier. That is, Z3 will never match this kind of // pattern. - if (m_params.m_pi_avoid_skolems && decl->is_skolem()) { + if (false && m_params.m_pi_avoid_skolems && decl->is_skolem()) { CTRACE(pattern_inference_skolem, decl->is_skolem(), tout << "ignoring: " << mk_pp(n, m) << "\n";); return true; } diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 8dc181a2f9..67c19ae9f1 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -12,7 +12,7 @@ def_module_params(module_name='smt', ('ematching', BOOL, True, 'E-Matching based quantifier instantiation'), ('ho_matching', BOOL, False, 'higher-order matching for quantifier instantiation'), ('ho_matching_bound', UINT, 10000, 'per-problem expansion-step budget of the higher-order matching search; bounds the (undecidable) HO unification to guarantee termination'), - ('term_enumeration', BOOL, True, 'use term enumeration to populate instantiation sets for higher-order variables during model-based quantifier instantiation'), + ('term_enumeration', BOOL, False, 'use term enumeration to populate instantiation sets for higher-order variables during model-based quantifier instantiation'), ('phase_selection', UINT, 3, 'phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences, 7 - theory'), ('phase_caching_on', UINT, 400, 'number of conflicts while phase caching is on'), ('phase_caching_off', UINT, 100, 'number of conflicts while phase caching is off'), diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index e0423599dc..a528a69e09 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -872,7 +872,9 @@ namespace smt { lits.push_back(~lit); if (!m.is_true(cond)) { expr_ref ncond(mk_not(m, cond), m); - lits.push_back(th.mk_literal(mk_forall(m, hd, ncond))); + expr_ref facond = mk_forall(m, hd, ncond); + ctx.internalize(facond, true); // make sure fa is internalized, and assumed in positive polarity only. + lits.push_back(th.mk_literal(facond)); } expr_ref is_empty1 = sk().mk_is_empty(r, re().mk_union(u, r), n); lits.push_back(th.mk_literal(is_empty1)); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index f0105ff633..7938c70742 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -983,6 +983,8 @@ namespace smt { void internalize(expr * n, bool gate_ctx, unsigned generation); + enode *non_ground_internalize(expr *e); + clause * mk_clause(unsigned num_lits, literal * lits, justification * j, clause_kind k = CLS_AUX, clause_del_eh * del_eh = nullptr); void mk_clause(literal l1, literal l2, justification * j); diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 3e8e5bb0fc..908f505893 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -419,6 +419,28 @@ namespace smt { internalize_rec(n, gate_ctx); } + enode *context::non_ground_internalize(expr *e) { + if (e_internalized(e)) + return get_enode(e); + if (is_ground(e)) { + internalize(e, false); + return get_enode(e); + } + for (auto arg : subterms::ground(expr_ref(e, m))) { + if ((is_forall(arg) || is_exists(arg)) && !e_internalized(arg)) { + expr_ref fn(m.mk_fresh_const("proxy-expr", e->get_sort()), m); + expr_ref eq(m.mk_eq(fn, e), m); + assert_expr(eq); + internalize_assertions(); + if (!e_internalized(fn)) + internalize(fn, false); + return get_enode(fn); + } + } + internalize(e, false); + return get_enode(e); + } + void context::internalize(expr* const* exprs, unsigned num_exprs, bool gate_ctx) { internalize_deep(exprs, num_exprs); for (unsigned i = 0; i < num_exprs; ++i) diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp index b762e757e5..cba15a0f33 100644 --- a/src/smt/smt_theory.cpp +++ b/src/smt/smt_theory.cpp @@ -152,7 +152,8 @@ namespace smt { expr_ref e(_e, m); bool is_not = m.is_not(_e, _e); if (!ctx.e_internalized(_e)) { - ctx.internalize(_e, is_quantifier(_e)); + auto n = ctx.non_ground_internalize(_e); + _e = n->get_expr(); } literal lit = ctx.get_literal(_e); ctx.mark_as_relevant(lit); diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index 86652d12ba..fb5aaf89e4 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -626,17 +626,8 @@ namespace smt { for (unsigned i = 0; i < lam->get_num_decls(); ++i) args.push_back(mk_epsilon(lam->get_decl_sort(i)).first); expr_ref val(mk_select(args), m); - ctx.get_rewriter()(val); - if (has_quantifiers(val)) { - expr_ref fn(m.mk_fresh_const("lambda-body", val->get_sort()), m); - expr_ref eq(m.mk_eq(fn, val), m); - ctx.assert_expr(eq); - ctx.internalize_assertions(); - val = fn; - } - ctx.internalize(def, false); - ctx.internalize(val.get(), false); - return try_assign_eq(val.get(), def); + auto val_e = ctx.non_ground_internalize(val); + return try_assign_eq(val_e->get_expr(), def); } bool theory_array_full::instantiate_choice_axiom(enode* ch) {