introduce notion of beta redex to deal with lambdas in non-extensional positions

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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);

src/ast/ast.h

@@ -1618,7 +1618,7 @@ public:
     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; }
 

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() && !has_lambda()) 
-        if (status == l_true && !m_qmanager->has_quantifiers() && m_lambdas.empty()) {
             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();

src/smt/smt_context.h

@@ -773,7 +773,12 @@ namespace smt {
 
         void internalize_quantifier(quantifier * q, bool gate_ctx);
 
-        obj_hashtable<quantifier> m_lambdas, m_non_lambdas;
+        obj_map<enode, quantifier*> 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);
@@ -784,8 +789,6 @@ namespace smt {
 
     public:
         
-        void add_non_lambda(quantifier* q);
-        
         void set_enode_flag(bool_var v, bool is_new_var);
 
     protected:

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);
+        if (!e_internalized(lam_name)) 
-        m_app2enode.setx(q->get_id(), get_enode(lam_name), nullptr);
+            internalize_uninterpreted(lam_name);
+        enode* lam_node = get_enode(lam_name);
+        push_trail(insert_obj_map<enode, quantifier*>(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<quantifier>(m_lambdas, q));
-        m_lambdas.insert(q);
     }
 
-    void context::add_non_lambda(quantifier* q) {
+    bool context::has_lambda() {
-        if (m_non_lambdas.contains(q))
+        for (auto const & [n, q] : m_lambdas) {
-            return;
+            if (n->get_class_size() != 1) 
-        m_non_lambdas.insert(q);
+                return true;
-        push_trail(insert_obj_trail<quantifier>(m_non_lambdas, q));
+            for (enode* p : enode::parents(n)) 
-        if (m_lambdas.contains(q)) {
+                if (!is_beta_redex(p, n)) 
-            m_lambdas.remove(q);
+                    return true;
-            push_trail(remove_obj_trail<quantifier>(m_lambdas, q));
         }
+        return false;
     }
 
     /**

src/smt/smt_theory.h

@@ -322,6 +322,13 @@ namespace smt {
             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
         */

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)) 

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<theory_var> & result);
         unsigned mk_interface_eqs();
 

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);
@@ -1487,25 +1485,17 @@ bool theory_seq::internalize_term(app* term) {
     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;
+        return false;
-    
+    if (p->get_arg(0)->get_root() == n->get_root())
-    expr* fn = to_app(term)->get_arg(0);
+        return true;
-    quantifier* q = nullptr;
+    return false;
-    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);
 }
 
 
@@ -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;
     }

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);