add detection of string equalities

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

src/ast/rewriter/seq_rewriter.cpp

@@ -2398,8 +2398,6 @@ bool seq_rewriter::non_overlap(expr_ref_vector const& p1, expr_ref_vector const&
 */
 
 bool seq_rewriter::rewrite_contains_pattern(expr* a, expr* b, expr_ref& result) {
-    
-
     vector<expr_ref_vector> patterns;
     expr* x = nullptr, *y = nullptr, *z = nullptr, *u = nullptr;
     if (!str().is_concat(a, x, y))

src/ast/rewriter/seq_rewriter.h

@@ -180,7 +180,6 @@ class seq_rewriter {
     br_status reduce_re_is_empty(expr* r, expr_ref& result);
 
 
-    bool is_re_contains_pattern(expr* r, vector<expr_ref_vector>& patterns);
     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);
@@ -252,6 +251,11 @@ public:
             result = m().mk_app(f, n, args);
         return result;
     }
+
+    /**
+     * check if regular expression is of the form all ++ s ++ all ++ t + u ++ all, where, s, t, u are sequences
+     */
+    bool is_re_contains_pattern(expr* r, vector<expr_ref_vector>& patterns);
         
     bool reduce_eq(expr* l, expr* r, expr_ref_pair_vector& new_eqs, bool& change);
 

src/smt/seq_regex.cpp

@@ -47,19 +47,37 @@ namespace smt {
     }
 
     /**
-     * is_string_equality holds of str.in_re s R, if R is of the form .* ++ x ++ .* ++ y ++ .* ++ 
+     * is_string_equality holds of str.in_re s R, 
+     * 
+     * s in (all ++ x ++ all ++ y ++ all)
+     * => 
      * s = fresh1 ++ x ++ fresh2 ++ y ++ fresh3
      * 
-     * example rewrite:
+     * TBD General rewrite possible:
-     * (str.in_re s .* ++ R) => s = x ++ y and (str.in_re y R)
+     *
-     * 
+     * s in (R ++ Q)
-     * is_string_equality is currently placed under propagate_accept.
+     * =>
-     * this allows extracting string equalities after processing regexes that are not
+     * s = x ++ y and x in R and y in Q
-     * simple unions of simple concatentations. Though, it may produce different equations for 
-     * alternate values of the unfolding index.
      */
 
     bool seq_regex::is_string_equality(literal lit) {
+        expr* s = nullptr, *r = nullptr;
+        expr* e = ctx.bool_var2expr(lit.var());
+        VERIFY(str().is_in_re(e, s, r));
+        vector<expr_ref_vector> patterns;
+        if (seq_rw().is_re_contains_pattern(r, patterns)) {
+            expr_ref t(m);
+            expr_ref_vector ts(m);
+            sort* seq_sort = m.get_sort(s);
+            ts.push_back(m.mk_fresh_const("seq.cont", seq_sort));
+            for (auto const& p : patterns) {
+                ts.append(p);
+                ts.push_back(m.mk_fresh_const("seq.cont", seq_sort));
+            }
+            t = th.mk_concat(ts, seq_sort);
+            th.propagate_eq(lit, s, t, true);
+            return true;
+        }
         return false;
     }
 
@@ -93,7 +111,12 @@ namespace smt {
 
         if (coallesce_in_re(lit))
             return;
-        
+
+#if 0
+        // Enable/disable to test effect
+        if (is_string_equality(lit))
+            return;
+#endif        
         //
         // TBD s in R => R != {}
         // non-emptiness enforcement could instead of here, 
@@ -170,9 +193,6 @@ namespace smt {
 
         TRACE("seq", tout << "propagate " << mk_pp(e, m) << "\n";);
 
-        if (is_string_equality(lit))
-            return true;
-
         if (block_unfolding(lit, idx))
             return true;