add partial evaluation cases for algebraic data-types for recursive f…

…unctions.
Z3Prover · Jun 16, 2024 · ef86f5f · ef86f5f
1 parent 81ebd52
commit ef86f5f
Show file tree

Hide file tree

Showing 2 changed files with 36 additions and 7 deletions.
diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp
@@ -301,7 +301,6 @@ namespace recfun {
                         // skip
                     }
                     else if (m.is_ite(e)) {
-                        verbose_stream() << "unfold " << mk_pp(e, m) << "\n";
                         // need to do a case split on `e`, forking the search space
                         b.to_split = st.cons_ite(to_app(e), b.to_split);
                     } 

diff --git a/src/ast/rewriter/recfun_rewriter.cpp b/src/ast/rewriter/recfun_rewriter.cpp
@@ -19,20 +19,50 @@ Module Name:
 
 #include "ast/rewriter/recfun_rewriter.h"
 #include "ast/rewriter/var_subst.h"
+#include "ast/datatype_decl_plugin.h"
+#include "ast/for_each_expr.h"
 
 br_status recfun_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
     if (m_rec.is_defined(f) && num_args > 0) {
-        for (unsigned i = 0; i < num_args; ++i) 
-            if (!m.is_value(args[i]))
-                return BR_FAILED;
         if (!m_rec.has_def(f))
             return BR_FAILED;
         recfun::def const& d = m_rec.get_def(f);
         if (!d.get_rhs())
             return BR_FAILED;
-        var_subst sub(m);
-        result = sub(d.get_rhs(), num_args, args);
-        return BR_REWRITE_FULL;
+        auto r = d.get_rhs();
+        bool safe_to_subst = true;
+        for (unsigned i = 0; i < num_args; ++i) 
+            if (!m.is_value(args[i]))
+                safe_to_subst = false;
+
+        // check if there is an argument that is a constructor
+        // such that the recursive function can be partially evaluated.
+        if (!safe_to_subst && !has_quantifiers(r)) {
+            datatype::util u(m);
+            auto is_decreasing = [&](unsigned i) {
+                bool is_dec = true;
+                unsigned idx = num_args - i - 1;
+                for (auto t : subterms::all(expr_ref(r, m)))
+                    if (is_app(t) && any_of(*to_app(t), [&](expr* e) { return is_var(e) && to_var(e)->get_idx() == idx; }))
+                        if (!u.is_accessor(t) && !u.is_is(t) && !u.is_recognizer(t))
+                            is_dec = false;
+                return is_dec;
+            };
+            for (unsigned i = 0; i < num_args; ++i) {
+                auto arg = args[i];
+                if (u.is_constructor(arg) && is_decreasing(i)) {
+                    safe_to_subst = true;
+                    break;
+                }
+            }            
+        }
+        if (safe_to_subst) {
+            var_subst sub(m);
+            result = sub(d.get_rhs(), num_args, args);
+            return BR_REWRITE_FULL;
+        }
+        return BR_FAILED;
+
     }
     else 
         return BR_FAILED;