na

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

src/ast/rewriter/seq_split.cpp

@@ -210,9 +210,7 @@ struct split_set::iterator::imp {
         }
 
         void consume() override {
-            TRACE(seq, tout << "concat-start: " << mk_pp(a, parent().i.m) << " " << mk_pp(b, parent().i.m) << "\n");
             while (!parent().has_split() && !at_end() && !a_it.failed() && !b_it.failed()) {
-                TRACE(seq, tout << "concat: " << mk_pp(a, parent().i.m) << " " << mk_pp(b, parent().i.m) << "\n");
                 if (a_it == a_end) {
                     auto [p, q] = *b_it;
                     parent().push_split(parent().i.rw.mk_re_append(a, p), q);

src/smt/seq_regex.cpp

@@ -172,39 +172,22 @@ namespace smt {
         VERIFY(str().is_in_re(e, s, r));
 
         TRACE(seq_regex, tout << "propagate in RE: " << lit.sign() << " " << mk_pp(e, m) << std::endl;);
-        STRACE(seq_regex_brief, tout << "PIR(" << mk_pp(s, m) << ","
-                                       << state_str(r) << ") ";);
 
-        // convert negative negative membership literals to positive
-        // ~(s in R) => s in C(R)
-        if (lit.sign()) {
-            expr_ref fml(re().mk_in_re(s, re().mk_complement(r)), m);
-            rewrite(fml);
-            literal nlit = th.mk_literal(fml);
-            if (lit == nlit) {
-                // is-nullable doesn't simplify for regexes with uninterpreted subterms
-                th.add_unhandled_expr(fml);
-            }
-            th.propagate_lit(nullptr, 1, &lit, nlit);
+        if (unfold_complement(lit, s, r))
             return;
-        }
 
         if (unfold_prefix(lit, s, r)) {
-            TRACE(seq_regex, tout << "unfolded prefix" << std::endl;);
-            STRACE(seq_regex_brief, tout << "unfold_prefix ";);
+            TRACE(seq_regex, tout << "unfolded prefix\n");
             return;
         }
 
         if (is_string_equality(lit, s, r)) {
-            TRACE(seq_regex, tout
-                << "simplified regex using string equality" << std::endl;);
-            STRACE(seq_regex_brief, tout << "string_eq ";);
+            TRACE(seq_regex, tout << "simplified regex using string equality\n");
             return;
         }
 
         if (factor_ite(lit, s, r)) {
-            TRACE(seq_regex, tout << "factored ite in regex" << std::endl;);
-            STRACE(seq_regex_brief, tout << "factor_ite ";);
+            TRACE(seq_regex, tout << "factored ite in regex\n");
             return;
         }
 
@@ -502,6 +485,64 @@ namespace smt {
         return false;
     }
 
+    bool seq_regex::final_check() {
+
+        return true;
+
+        // sketch:
+        // 
+        // check registered seq_cont if more case splits are needed.
+        // check registered atomic regex membership for membership
+        // fallback to initialize_accept?
+
+        expr *x = nullptr, *r = nullptr;
+        bool done = true;
+        for (auto s : m_split_conts) {
+            if (s->failed())
+                ;
+            else if (s->next_split())
+                done = false;
+            else if (s->failed()) {
+                done = false;
+
+                expr *e = ctx.bool_var2expr(s->lit().var());
+                VERIFY(str().is_in_re(e, x, r));
+                initialize_accept(s->lit(), x, r);
+            }
+            else
+                ; // some split literal is true
+        }
+        obj_map<expr, ptr_vector<expr>> var2regex;
+        for (auto lit : m_atomic_memberships) {
+            expr *e = ctx.bool_var2expr(lit.var());
+            VERIFY(str().is_in_re(e, x, r));
+            var2regex.insert_if_not_there(x, ptr_vector<expr>()).push_back(r);
+        }
+        for (auto const &[x, regexes] : var2regex) {
+            // synthesize a solution within intersection of regexes.
+            // if intersection is empty, report conflict.
+            // add guardrails for solution satisfying current length assignment to x
+            // if solution does not satisfy length constraints initialize_accept instead of retaining atomic
+
+        }
+        return done;
+    }
+
+    bool seq_regex::unfold_complement(literal lit, expr *s, expr *r) {
+        if (!lit.sign())
+            return false;
+        // convert negative negative membership literals to positive
+        // ~(s in R) => s in C(R)
+        expr_ref fml(re().mk_in_re(s, re().mk_complement(r)), m);
+        rewrite(fml);
+        literal nlit = th.mk_literal(fml);
+        if (lit == nlit) {
+            // is-nullable doesn't simplify for regexes with uninterpreted subterms
+            th.add_unhandled_expr(fml);
+        }
+        th.propagate_lit(nullptr, 1, &lit, nlit);
+        return true;
+    }
     
     bool seq_regex::factor_ite(literal lit, expr* s, expr* r) {
         bool_rewriter br(m);

src/smt/seq_regex.h

@@ -95,17 +95,8 @@ namespace smt {
     class seq_regex;
 
     class seq_regex {
-        // Data about a constraint of the form (str.in_re s R)
-        struct s_in_re {
-            literal m_lit;
-            expr*   m_s;
-            expr*   m_re;
-            bool    m_active;
-        s_in_re(literal l, expr* s, expr* r):
-            m_lit(l), m_s(s), m_re(r), m_active(true) {}
-        };
 
-            // a split continuation is a closure that contains a split set
+        // a split continuation is a closure that contains a split set
         // and in_re2 literals that were extracted from a partial split.
         // there are the following outcomes:
         // 1. it was not possible to split:failed()
@@ -129,13 +120,15 @@ namespace smt {
             split_cont(seq_regex &sr, split_set&& ss, literal lit, expr* u, expr* v, expr* r);
             bool failed() const;
             bool next_split();
+            literal lit() const { return m_lit; }            
         };
 
         theory_seq&                      th;
         context&                         ctx;
         ast_manager&                     m;
-        vector<s_in_re>                  m_s_in_re;
 
+        ptr_vector<split_cont> m_split_conts;  // split continuations
+        literal_vector m_atomic_memberships;   // str.in_re X r, where X is a variable
         /*
             state_graph for dead state detection, and associated methods
         */
@@ -179,6 +172,8 @@ namespace smt {
 
         bool unfold_prefix(literal lit, expr* s, expr* r);
 
+        bool unfold_complement(literal lit, expr *s, expr *r);
+
         bool factor_membership(literal lit, expr* s, expr* r);
 
         bool factor_ite(literal lit, expr* s, expr* r);
@@ -227,9 +222,7 @@ namespace smt {
 
         seq_regex(theory_seq& th);
 
-        bool final_check() {
-            return true;
-        }
+        bool final_check();
 
         void propagate_in_re(literal lit);