From 8efa3c8ade0c8736d1364c8561e1428cefa4d93b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 10 Jun 2022 17:35:01 -0700 Subject: [PATCH] introduce notion of beta redex to deal with lambdas in non-extensional positions Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 1 + src/ast/ast.h | 2 +- src/smt/smt_context.cpp | 24 ++++++++++++++---------- src/smt/smt_context.h | 9 ++++++--- src/smt/smt_internalizer.cpp | 35 +++++++++++++++++------------------ src/smt/smt_theory.h | 7 +++++++ src/smt/theory_array_base.cpp | 9 +++++++++ src/smt/theory_array_base.h | 1 + src/smt/theory_seq.cpp | 26 ++++++++------------------ src/smt/theory_seq.h | 2 +- 10 files changed, 65 insertions(+), 51 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 56a98b05127..190da136637 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1677,6 +1677,7 @@ quantifier* ast_manager::is_lambda_def(func_decl* f) { return nullptr; } + void ast_manager::register_plugin(family_id id, decl_plugin * plugin) { SASSERT(m_plugins.get(id, 0) == 0); m_plugins.setx(id, plugin, 0); diff --git a/src/ast/ast.h b/src/ast/ast.h index fe7586afa6e..fcf83a65c0f 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1618,7 +1618,7 @@ class ast_manager { bool is_lambda_def(quantifier* q) const { return q->get_qid() == m_lambda_def; } void add_lambda_def(func_decl* f, quantifier* q); quantifier* is_lambda_def(func_decl* f); - + quantifier* is_lambda_def(app* e) { return is_lambda_def(e->get_decl()); } symbol const& lambda_def_qid() const { return m_lambda_def; } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 6f5fd6607e7..49fe8f22f84 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3737,15 +3737,12 @@ namespace smt { reset_model(); - if (m_last_search_failure != OK) { + if (m_last_search_failure != OK) return false; - } - if (status == l_false) { + if (status == l_false) return false; - } - if (status == l_true && !m_qmanager->has_quantifiers() && m_lambdas.empty()) { + if (status == l_true && !m_qmanager->has_quantifiers() && !has_lambda()) return false; - } if (status == l_true && m_qmanager->has_quantifiers()) { // possible outcomes DONE l_true, DONE l_undef, CONTINUE mk_proto_model(); @@ -3766,7 +3763,7 @@ namespace smt { break; } } - if (status == l_true && !m_lambdas.empty()) { + if (status == l_true && has_lambda()) { m_last_search_failure = LAMBDAS; status = l_undef; return false; @@ -4010,7 +4007,7 @@ namespace smt { TRACE("final_check_step", tout << "RESULT final_check: " << result << "\n";); if (result == FC_GIVEUP && f != OK) m_last_search_failure = f; - if (result == FC_DONE && !m_lambdas.empty()) { + if (result == FC_DONE && has_lambda()) { m_last_search_failure = LAMBDAS; result = FC_GIVEUP; } @@ -4468,9 +4465,8 @@ namespace smt { return false; } case 1: { - if (m_qmanager->is_shared(n)) { + if (m_qmanager->is_shared(n) && !m.is_lambda_def(n->get_expr()) && !m_lambdas.contains(n)) return true; - } // the variable is shared if the equivalence class of n // contains a parent application. @@ -4482,6 +4478,8 @@ namespace smt { app* p = parent->get_expr(); family_id fid = p->get_family_id(); if (fid != th_id && fid != m.get_basic_family_id()) { + if (is_beta_redex(parent, n)) + continue; TRACE("is_shared", tout << enode_pp(n, *this) << "\nis shared because of:\n" << enode_pp(parent, *this) << "\n";); @@ -4522,6 +4520,12 @@ namespace smt { } } + bool context::is_beta_redex(enode* p, enode* n) const { + family_id th_id = p->get_expr()->get_family_id(); + theory * th = get_theory(th_id); + return th && th->is_beta_redex(p, n); + } + bool context::get_value(enode * n, expr_ref & value) { sort * s = n->get_sort(); family_id fid = s->get_family_id(); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 0334a9daf7a..e2fc3a35fd1 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -773,7 +773,12 @@ namespace smt { void internalize_quantifier(quantifier * q, bool gate_ctx); - obj_hashtable m_lambdas, m_non_lambdas; + obj_map m_lambdas; + + bool has_lambda(); + + bool is_beta_redex(enode* p, enode* n) const; + void internalize_lambda(quantifier * q); void internalize_formula_core(app * n, bool gate_ctx); @@ -783,8 +788,6 @@ namespace smt { friend class set_enode_flag_trail; public: - - void add_non_lambda(quantifier* q); void set_enode_flag(bool_var v, bool is_new_var); diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 63e5b0e7b9c..45113635159 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -578,20 +578,19 @@ namespace smt { m_qmanager->add(q, generation); } + void context::internalize_lambda(quantifier * q) { TRACE("internalize_quantifier", tout << mk_pp(q, m) << "\n";); SASSERT(is_lambda(q)); - if (e_internalized(q)) { + if (e_internalized(q)) return; - } app_ref lam_name(m.mk_fresh_const("lambda", q->get_sort()), m); app_ref eq(m), lam_app(m); expr_ref_vector vars(m); vars.push_back(lam_name); unsigned sz = q->get_num_decls(); - for (unsigned i = 0; i < sz; ++i) { + for (unsigned i = 0; i < sz; ++i) vars.push_back(m.mk_var(sz - i - 1, q->get_decl_sort(i))); - } array_util autil(m); lam_app = autil.mk_select(vars.size(), vars.data()); eq = m.mk_eq(lam_app, q->get_expr()); @@ -599,28 +598,28 @@ namespace smt { expr * patterns[1] = { m.mk_pattern(lam_app) }; fa = m.mk_forall(sz, q->get_decl_sorts(), q->get_decl_names(), eq, 0, m.lambda_def_qid(), symbol::null, 1, patterns); internalize_quantifier(fa, true); - if (!e_internalized(lam_name)) internalize_uninterpreted(lam_name); - m_app2enode.setx(q->get_id(), get_enode(lam_name), nullptr); + if (!e_internalized(lam_name)) + internalize_uninterpreted(lam_name); + enode* lam_node = get_enode(lam_name); + push_trail(insert_obj_map(m_lambdas, lam_node)); + m_lambdas.insert(lam_node, q); + m_app2enode.setx(q->get_id(), lam_node, nullptr); m_l_internalized_stack.push_back(q); m_trail_stack.push_back(&m_mk_lambda_trail); bool_var bv = get_bool_var(fa); assign(literal(bv, false), nullptr); mark_as_relevant(bv); - if (m_non_lambdas.contains(q)) - return; - push_trail(insert_obj_trail(m_lambdas, q)); - m_lambdas.insert(q); } - void context::add_non_lambda(quantifier* q) { - if (m_non_lambdas.contains(q)) - return; - m_non_lambdas.insert(q); - push_trail(insert_obj_trail(m_non_lambdas, q)); - if (m_lambdas.contains(q)) { - m_lambdas.remove(q); - push_trail(remove_obj_trail(m_lambdas, q)); + bool context::has_lambda() { + for (auto const & [n, q] : m_lambdas) { + if (n->get_class_size() != 1) + return true; + for (enode* p : enode::parents(n)) + if (!is_beta_redex(p, n)) + return true; } + return false; } /** diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h index d723bfee887..c715f215f1e 100644 --- a/src/smt/smt_theory.h +++ b/src/smt/smt_theory.h @@ -321,6 +321,13 @@ namespace smt { virtual bool is_shared(theory_var v) const { return false; } + + /** + \brief Determine if node \c n under parent \c p is in a beta redex position. + */ + virtual bool is_beta_redex(enode* p, enode* n) const { + return false; + } /** \brief Return true if the theory has something to propagate diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index 33944c96c89..f6d4306a5f4 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -473,6 +473,15 @@ namespace smt { return false; } + bool theory_array_base::is_beta_redex(enode* p, enode* n) const { + if (is_select(p)) + return p->get_arg(0)->get_root() == n->get_root(); + if (is_map(p)) + return true; + return false; + } + + bool theory_array_base::is_select_arg(enode* r) { for (enode* n : r->get_parents()) if (is_select(n)) diff --git a/src/smt/theory_array_base.h b/src/smt/theory_array_base.h index a0550683f17..f0d698f26b7 100644 --- a/src/smt/theory_array_base.h +++ b/src/smt/theory_array_base.h @@ -142,6 +142,7 @@ namespace smt { // // -------------------------------------------------- bool is_shared(theory_var v) const override; + bool is_beta_redex(enode* p, enode* n) const override; void collect_shared_vars(sbuffer & result); unsigned mk_interface_eqs(); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 7ca0dfe4189..e1285e7496c 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1457,8 +1457,6 @@ bool theory_seq::internalize_term(app* term) { return true; } - suppress_lambda(term); - if (m.is_bool(term) && (m_util.str.is_in_re(term) || m_sk.is_skolem(term))) { bool_var bv = ctx.mk_bool_var(term); @@ -1486,26 +1484,18 @@ bool theory_seq::internalize_term(app* term) { mk_var(e); if (!ctx.relevancy()) { relevant_eh(term); - } - - + } return true; } -void theory_seq::suppress_lambda(app* term) { +bool theory_seq::is_beta_redex(enode* p, enode* n) const { + expr* term = p->get_expr(); if (!m_util.str.is_map(term) && !m_util.str.is_mapi(term) && !m_util.str.is_foldl(term) && !m_util.str.is_foldli(term)) - return; - - expr* fn = to_app(term)->get_arg(0); - quantifier* q = nullptr; - if (is_lambda(fn)) - q = to_quantifier(fn); - else if (is_app(fn)) - q = m.is_lambda_def(to_app(fn)->get_decl()); - - if (q) - ctx.add_non_lambda(q); + return false; + if (p->get_arg(0)->get_root() == n->get_root()) + return true; + return false; } @@ -3292,7 +3282,7 @@ bool theory_seq::should_research(expr_ref_vector & unsat_core) { k_min *= 2; if (m_util.is_seq(s_min)) k_min = std::max(m_util.str.min_length(s_min), k_min); - IF_VERBOSE(1, verbose_stream() << "(smt.seq :increase-length " << mk_pp(s_min, m) << " " << k_min << ")\n"); + IF_VERBOSE(1, verbose_stream() << "(smt.seq :increase-length " << mk_bounded_pp(s_min, m, 3) << " " << k_min << ")\n"); add_length_limit(s_min, k_min, false); return true; } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index b57c9122ce4..cf7e9da2323 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -388,7 +388,6 @@ namespace smt { bool internalize_atom(app* atom, bool) override; bool internalize_term(app*) override; void internalize_eq_eh(app * atom, bool_var v) override; - void suppress_lambda(app* term); void new_eq_eh(theory_var, theory_var) override; void new_diseq_eh(theory_var, theory_var) override; void assign_eh(bool_var v, bool is_true) override; @@ -413,6 +412,7 @@ namespace smt { void finalize_model(model_generator & mg) override; void init_search_eh() override; void validate_model(model& mdl) override; + bool is_beta_redex(enode* p, enode* n) const override; void init_model(expr_ref_vector const& es); app* get_ite_value(expr* a);