add Margus' unfold-fold operation and consolidate range-predicate recognizer/constructor.

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

src/ast/rewriter/seq_range_collapse.cpp

@@ -176,11 +176,14 @@ namespace seq {
             return true;
         }
 
-        if (re.is_of_pred(r, a)) {
-            sort *char_sort = nullptr;
-            VERIFY(u.is_seq(seq_sort, char_sort));
+        if (re.is_of_pred(r, a) && is_lambda(a)) {
+            auto q = to_quantifier(a);
+            if (q->get_num_decls() != 1)
+                return false;
+            auto body = q->get_expr();
+            sort *char_sort = q->get_decl_sort(0);
             expr_ref var(m.mk_var(0, char_sort), m);
-            if (pred_to_rp(m, u, var, a, out))
+            if (u.get_char_plugin().get_family_id() == char_sort->get_family_id() && pred_to_rp(m, u, var, body, out))
                 return true;
         }
 
@@ -239,4 +242,29 @@ namespace seq {
         return expr_ref(m.mk_lambda(1, &char_sort, &char_sym, body), m);
     }
 
+    expr_ref unfold_fold(seq_rewriter &rw, expr *r) {
+        auto &m = rw.m();
+        auto& u = rw.u();
+        expr_ref_pair_vector cofactors(m);  
+        rw.brz_derivative_cofactors(r, cofactors);
+        if (cofactors.empty()) 
+            return expr_ref(u.re.mk_empty(r->get_sort()), m);
+        
+        sort *seq_sort = nullptr, *char_sort = nullptr;
+        VERIFY(u.is_re(r, seq_sort));
+        VERIFY(u.is_seq(seq_sort, char_sort));
+        expr_ref var(m.mk_var(0, char_sort), m);
+        expr_ref result(m);
+        symbol ch("ch");
+        for (auto const &[c, cof] : cofactors) {
+            auto prefix = u.re.mk_of_pred(m.mk_lambda(1, &char_sort, &ch, c));
+            auto term = u.re.mk_concat(prefix, cof);
+            if (result) 
+                result = u.re.mk_union(term, result);            
+            else 
+                result = term;                   
+        }
+        return result;
+    }
+
 }

src/ast/rewriter/seq_range_collapse.h

@@ -26,6 +26,7 @@ Authors:
 #pragma once
 
 #include "ast/rewriter/seq_range_predicate.h"
+#include "ast/rewriter/seq_rewriter.h"
 #include "ast/seq_decl_plugin.h"
 
 namespace seq {
@@ -68,4 +69,18 @@ namespace seq {
      */
     expr_ref range_predicate_to_regex(seq_util& u, range_predicate const& p, sort* seq_sort);
 
+    /**
+    * Unfolds and then folds the given regex expression.
+    * Unfolding, produces the symbolic derivative which is an expression with a free variable var 0
+    * of the character sort.
+     * Folding produces a regex expression that is equivalent to the original one.
+     * It is obtained by taking the cofactors of the unfold, and producing a range predicate
+     * from the conditions with var 0.
+     * Formally:
+     * cofactors F_i[var 0], r_i            <- unfold(r)
+     * of_pred(\lambda ch . F_i[ch]) . r_i  <- fold(F_i[var 0], r_i)
+     * union_i of_pred(\ ch. F_i[ch]) . r_i <- fold(unfold(r))
+    */
+    expr_ref unfold_fold(seq_rewriter &rw, expr *r);
+
 }