Treat arguments to recursive functions as beta redexes

An argument to a recursive function would escape the scope of the function application when the recursive function definitions are unfolded. Therefore, such argument occurrences need not be considered for extensional equality / equality sharing.

This filter is mostly relevant for recursive functions that take a lambda expression as argument. Lambda expressions / arrays that occur in shared occurrences are checked for extensionality.

src/sat/smt/recfun_solver.cpp

@@ -333,6 +333,11 @@ namespace recfun {
         return found;
     }
 
+    bool solver::is_beta_redex(euf::enode* p, euf::enode* n) const {
+        return is_defined(p) || is_case_pred(p);
+    }
+
+
     bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
         if (n->num_args() == 0)
             dep.insert(n, nullptr);

src/sat/smt/recfun_solver.h

@@ -108,6 +108,7 @@ namespace recfun {
         bool is_shared(euf::theory_var v) const override { return true; }
         void init_search() override {}
         bool should_research(sat::literal_vector const& core) override;
+        bool is_beta_redex(euf::enode* p, euf::enode* n) const;
         void add_assumptions(sat::literal_set& assumptions) override;
         bool tracking_assumptions() override { return true; }
     };

src/smt/theory_recfun.cpp

@@ -467,6 +467,15 @@ namespace smt {
         return found;
     }
 
+    /**
+     * n is an argument of p, if p is a function definition or case predicate,
+     * then there is no reason for the solver to enforce that equality on n is 
+     * fully determined. It is a beta-redex with respect to expanding p.
+     */
+    bool theory_recfun::is_beta_redex(enode* p, enode* n) const {
+        return is_defined(p) || is_case_pred(p);
+    }
+
     void theory_recfun::display(std::ostream & out) const {
         out << "recfun\n";
         out << "disabled guards:\n" << m_disabled_guards << "\n";

src/smt/theory_recfun.h

@@ -99,6 +99,7 @@ namespace smt {
         bool can_propagate() override;
         void propagate() override;
         bool should_research(expr_ref_vector &) override;
+        bool is_beta_redex(enode* p, enode* n) const override;
 
         void new_eq_eh(theory_var v1, theory_var v2) override {}
         void new_diseq_eh(theory_var v1, theory_var v2) override {}