enable theory propagation of regex accept condition

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

src/ast/seq_decl_plugin.cpp

@@ -1325,6 +1325,8 @@ unsigned seq_util::re::min_length(expr* r) const {
         return std::max(min_length(r1), min_length(r2));
     if (is_loop(r, r1, lo, hi))
         return u.max_mul(lo, min_length(r1));
+    if (is_range(r)) 
+        return 1;
     if (is_to_re(r, s)) 
         return u.str.min_length(s);
     return 0;

src/smt/seq_regex.cpp

@@ -35,13 +35,30 @@ namespace smt {
     arith_util& seq_regex::a() { return th.m_autil; }
     void seq_regex::rewrite(expr_ref& e) { th.m_rewrite(e); }
 
+    bool seq_regex::can_propagate() const {
+        for (auto const& p : m_to_propagate) {
+            literal trigger = p.m_trigger;
+            if (trigger == null_literal || ctx.get_assignment(trigger) != l_undef)
+                return true;
+        }
+        return false;
+    }
+
     bool seq_regex::propagate() {
         bool change = false;
         for (unsigned i = 0; !ctx.inconsistent() && i < m_to_propagate.size(); ++i) {
-            if (propagate(m_to_propagate[i])) {
+            propagation_lit const& pl = m_to_propagate[i];
+            literal trigger = pl.m_trigger;
+            if (trigger != null_literal && ctx.get_assignment(trigger) == l_undef)
+                continue;
+            if (propagate(pl.m_lit, trigger)) {
                 m_to_propagate.erase_and_swap(i--);
                 change = true;
             }
+            else if (trigger != pl.m_trigger) {
+                m_to_propagate.set(i, propagation_lit(pl.m_lit, trigger));
+            }
+                
         }
         return change;
     }
@@ -148,8 +165,10 @@ namespace smt {
     }
 
     void seq_regex::propagate_accept(literal lit) {
-        if (!propagate(lit))
+        // std::cout << "PA ";
-            m_to_propagate.push_back(lit);
+        literal t = null_literal;
+        if (!propagate(lit, t))
+            m_to_propagate.push_back(propagation_lit(lit, t));
                                      }
 
     /**
@@ -165,7 +184,7 @@ namespace smt {
      * (accept s i r) & len(s) > i => (accept s (+ i 1) D(nth(s,i), r))
      */
     
-    bool seq_regex::propagate(literal lit) {
+    bool seq_regex::propagate(literal lit, literal& trigger) {
         SASSERT(!lit.sign());
 
         expr* s = nullptr, *i = nullptr, *r = nullptr;
@@ -173,6 +192,8 @@ namespace smt {
         unsigned idx = 0;
         VERIFY(sk().is_accept(e, s, i, idx, r));
 
+        // std::cout << "\nP " << idx << " " << r->get_id() << " ";
+
         TRACE("seq", tout << "propagate " << mk_pp(e, m) << "\n";);
 
         if (re().is_empty(r)) {
@@ -185,7 +206,7 @@ namespace smt {
 
         propagate_nullable(lit, s, idx, r);
 
-        return propagate_derivative(lit, e, s, i, idx, r);
+        return propagate_derivative(lit, e, s, i, idx, r, trigger);
     }
 
     /**
@@ -208,6 +229,7 @@ namespace smt {
      */
 
     void seq_regex::propagate_nullable(literal lit, expr* s, unsigned idx, expr* r) {
+        // std::cout << "PN ";
         expr_ref is_nullable = seq_rw().is_nullable(r);
         rewrite(is_nullable);
         literal len_s_ge_i = th.m_ax.mk_ge(th.mk_len(s), idx);
@@ -216,6 +238,8 @@ namespace smt {
         }
         else if (m.is_false(is_nullable)) {
             th.propagate_lit(nullptr, 1, &lit, th.m_ax.mk_ge(th.mk_len(s), idx + 1));
+            //unsigned len = std::max(1u, re().min_length(r));
+            //th.propagate_lit(nullptr, 1, &lit, th.m_ax.mk_ge(th.mk_len(s), idx + re().min_length(r)));
         }
         else {
             literal is_nullable_lit = th.mk_literal(is_nullable);
@@ -237,8 +261,9 @@ namespace smt {
         }
     }
     
-    bool seq_regex::propagate_derivative(literal lit, expr* e, expr* s, expr* i, unsigned idx, expr* r) {
+    bool seq_regex::propagate_derivative(literal lit, expr* e, expr* s, expr* i, unsigned idx, expr* r, literal& trigger) {
         // (accept s i R) & len(s) > i => (accept s (+ i 1) D(nth(s, i), R)) or conds
+        // std::cout << "PD ";
         expr_ref d(m);
         expr_ref head = th.mk_nth(s, i);
 
@@ -271,6 +296,7 @@ namespace smt {
             case l_undef: 
 #if 1
                 ctx.mark_as_relevant(lcond);
+                trigger = lcond;
                 return false;
 #else
                 if (re().is_empty(tt)) {
@@ -303,6 +329,7 @@ namespace smt {
             conds.push_back(th.mk_literal(sk().mk_accept(s, a().mk_int(idx + 1), d)));
         th.add_axiom(conds);        
         TRACE("seq", tout << "unfold " << head << "\n" << mk_pp(r, m) << "\n";);
+        // std::cout << "D ";
         return true;
     }
 

src/smt/seq_regex.h

@@ -36,11 +36,19 @@ namespace smt {
             m_lit(l), m_s(s), m_re(r), m_active(true) {}
         };
 
+        struct propagation_lit {
+            literal m_lit;
+            literal m_trigger;
+            propagation_lit(literal lit, literal t): m_lit(lit), m_trigger(t) {}
+            propagation_lit(literal lit): m_lit(lit), m_trigger(null_literal) {}
+            propagation_lit(): m_lit(null_literal), m_trigger(null_literal) {}
+        };
+
         theory_seq&      th;
         context&         ctx;
         ast_manager&     m;
         vector<s_in_re> m_s_in_re;
-        scoped_vector<literal> m_to_propagate;
+        scoped_vector<propagation_lit> m_to_propagate;
 
         seq_util& u();
         class seq_util::re& re();
@@ -55,13 +63,13 @@ namespace smt {
 
         bool coallesce_in_re(literal lit);
 
-        bool propagate(literal lit);
+        bool propagate(literal lit, literal& trigger);
 
         bool block_unfolding(literal lit, unsigned i);
 
         void propagate_nullable(literal lit, expr* s, unsigned idx, expr* r);
 
-        bool propagate_derivative(literal lit, expr* e, expr* s, expr* i, unsigned idx, expr* r);
+        bool propagate_derivative(literal lit, expr* e, expr* s, expr* i, unsigned idx, expr* r, literal& trigger);
 
         expr_ref mk_first(expr* r);
 
@@ -88,6 +96,8 @@ namespace smt {
 
         void pop_scope(unsigned num_scopes) { m_to_propagate.pop_scope(num_scopes); }
 
+        bool can_propagate() const;
+
         bool propagate();
 
         void propagate_in_re(literal lit);

src/smt/theory_seq.cpp

@@ -2525,6 +2525,8 @@ void theory_seq::add_dependency(dependency*& dep, enode* a, enode* b) {
 void theory_seq::propagate() {
     if (ctx.get_fparams().m_seq_use_unicode)
         m_unicode.propagate();
+    if (ctx.get_fparams().m_seq_use_derivatives && m_regex.can_propagate())
+        m_regex.propagate();
     while (m_axioms_head < m_axioms.size() && !ctx.inconsistent()) {
         expr_ref e(m);
         e = m_axioms[m_axioms_head].get();