#7207

the utility that computes case analysis is brittle when the body of a function contains ite expressions that are not relevant to recursive unfolding.
The fold-rec occurrences that get inserted to harness large case splits work against throttling case generation: they get treated as recursive functions that have to be guarded.

src/ast/recfun_decl_plugin.cpp

@@ -90,17 +90,21 @@ namespace recfun {
         return r;
     }
 
-    bool def::contains_def(util& u, expr * e) {
+    bool util::contains_def(expr * e) {
         struct def_find_p : public i_expr_pred {
             util& u;
             def_find_p(util& u): u(u) {}
             bool operator()(expr* a) override { return is_app(a) && u.is_defined(to_app(a)->get_decl()); }
         };
-        def_find_p p(u);
-        check_pred cp(p, m, false);
+        def_find_p p(*this);
+        check_pred cp(p, m(), false);
         return cp(e);
     }
 
+    bool def::contains_def(util& u, expr * e) {
+        return u.contains_def(e);
+    }
+
     // does `e` contain any `ite` construct?
     // subject to the then/else branch using a recursive call,
     // but the guard does not.
@@ -293,7 +297,11 @@ namespace recfun {
                     if (m.is_ite(e, cond, th, el) && contains_def(u, cond)) {
                         // skip
                     }
+                    if (m.is_ite(e, cond, th, el) && !contains_def(u, th) && !contains_def(u, el)) {
+                        // 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);
                     } 
@@ -558,15 +566,16 @@ namespace recfun {
 
         expr_ref plugin::redirect_ite(replace& subst, unsigned n, var * const* vars, expr * e) {
             expr_ref result(e, m());
+            util u(m());
             while (true) {
                 obj_map<expr, unsigned> scores;
                 compute_scores(result, scores);
                 unsigned max_score = 0;
                 expr* max_expr = nullptr;
-                for (auto const& kv : scores) {
-                    if (m().is_ite(kv.m_key) && kv.m_value > max_score) {
-                        max_expr = kv.m_key;
-                        max_score = kv.m_value;
+                for (auto const& [k, v] : scores) {
+                    if (m().is_ite(k) && v > max_score && u.contains_def(k)) {
+                        max_expr = k;
+                        max_score = v;
                     }
                 }
                 if (max_score <= 4) 

src/ast/recfun_decl_plugin.h

@@ -251,6 +251,8 @@ namespace recfun {
         bool is_macro(func_decl* f) { return is_defined(f) && get_def(f).is_macro(); }
         bool is_num_rounds(expr * e) const { return is_app_of(e, m_fid, OP_NUM_ROUNDS); }
         bool owns_app(app * e) const { return e->get_family_id() == m_fid; }
+        bool contains_def(expr* e); // expression contains a def
+
 
         //<! don't use native theory if recursive function declarations are not populated with defs
         bool has_defs() const { return m_plugin->has_defs(); }

src/sat/smt/recfun_solver.cpp

@@ -271,7 +271,8 @@ namespace recfun {
         SASSERT(!n || !n->is_attached_to(get_id()));
         if (!n) 
             n = mk_enode(e, false);
-        SASSERT(!n->is_attached_to(get_id()));
+        if (n->is_attached_to(get_id()))
+            return true;
         euf::theory_var w = mk_var(n);
         ctx.attach_th_var(n, this, w);
         if (u().is_defined(e) && u().has_defs()) 

src/smt/theory_recfun.cpp

@@ -342,7 +342,7 @@ namespace smt {
             activate_guard(pred_applied, guards);
         }
 
-        TRACEFN("assert core " << preds);
+        TRACEFN("assert cases " << preds);
         // the disjunction of branches is asserted
         // to close the available cases.