From b71a64365d78618ae64083a99af2d1d6b90993d2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 27 Jul 2020 19:34:32 -0700
Subject: [PATCH] sketch fixed-length heuristic

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_rewriter.cpp | 31 +++++++++++++++++++++++++++++++
 src/ast/rewriter/seq_rewriter.h   |  1 +
 src/ast/seq_decl_plugin.cpp       |  2 ++
 3 files changed, 34 insertions(+)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index afc000c33..708ec1978 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -3063,6 +3063,24 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
         return BR_REWRITE_FULL;
     }
 
+#if 0
+    unsigned len = 0;
+    if (has_fixed_length_constraint(b, len)) {
+        expr_ref len_lim(m().mk_eq(m_autil.mk_int(len), str().mk_length(a)), m());
+        // this forces derivatives. Perhaps not a good thing for intersections.
+        // alternative is to hoist out the smallest length constraining regex
+        // and keep the result for the sequence expression that is kept without rewriting
+        // or alternative is to block rewriting on this expression in some way.
+        expr_ref_vector args(m());
+        for (unsigned i = 0; i < len; ++i) {
+            args.push_back(str().mk_unit(str().mk_nth_i(a, m_autil.mk_int(i))));
+        }
+        expr_ref in_re(re().mk_in_re(str().mk_concat(args, m().get_sort(a)), b), m());
+        result = m().mk_and(len_lim, in_re);
+        return BR_REWRITE_FULL;
+    }
+#endif
+
     // Disabled rewrites
     if (false && re().is_complement(b, b1)) {
         result = m().mk_not(re().mk_in_re(a, b1));
@@ -3074,6 +3092,19 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
     return BR_FAILED;
 }
 
+bool seq_rewriter::has_fixed_length_constraint(expr* a, unsigned& len) {
+    unsigned minl = re().min_length(a), maxl = re().max_length(a);
+    if (minl == maxl) {
+        len = minl;
+        return true;
+    }
+    expr* b = nullptr, *c = nullptr;
+    if (re().is_intersection(a, b, c)) {
+        return has_fixed_length_constraint(b, len) || has_fixed_length_constraint(c, len);
+    }
+    return false;
+}
+
 br_status seq_rewriter::mk_str_to_regexp(expr* a, expr_ref& result) {
     return BR_FAILED;
 }
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 5fc3febb5..16f9c6048 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -249,6 +249,7 @@ class seq_rewriter {
     bool non_overlap(expr_ref_vector const& p1, expr_ref_vector const& p2) const;
     bool non_overlap(zstring const& p1, zstring const& p2) const;
     bool rewrite_contains_pattern(expr* a, expr* b, expr_ref& result);
+    bool has_fixed_length_constraint(expr* a, unsigned& len);
 
     br_status mk_bool_app_helper(bool is_and, unsigned n, expr* const* args, expr_ref& result);
     br_status mk_eq_helper(expr* a, expr* b, expr_ref& result);
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 9764ba18c..ce1516f41 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -1353,6 +1353,8 @@ unsigned seq_util::re::max_length(expr* r) const {
         return std::min(max_length(r1), max_length(r2));
     if (is_loop(r, r1, lo, hi))
         return u.max_mul(hi, max_length(r1));
+    if (is_range(r)) 
+        return 1;
     if (is_to_re(r, s)) 
         return u.str.max_length(s);
     return UINT_MAX;