register unhandled expressions

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

src/ast/rewriter/seq_rewriter.cpp

@@ -2181,16 +2181,16 @@ expr_ref seq_rewriter::re_predicate(expr* cond, sort* seq_sort) {
     return re_and(cond, re_with_empty);
 }
 
-expr_ref seq_rewriter::is_nullable_rec(expr* r) {
+expr_ref seq_rewriter::is_nullable(expr* r) {
     expr_ref result(m_op_cache.find(_OP_RE_IS_NULLABLE, r, nullptr), m());
     if (!result) {
-        result = is_nullable(r);
+        result = is_nullable_rec(r);
         m_op_cache.insert(_OP_RE_IS_NULLABLE, r, nullptr, result);        
     }
     return result;
 }
 
-expr_ref seq_rewriter::is_nullable(expr* r) {
+expr_ref seq_rewriter::is_nullable_rec(expr* r) {
     SASSERT(m_util.is_re(r) || m_util.is_seq(r));
     expr* r1 = nullptr, *r2 = nullptr, *cond = nullptr;
     sort* seq_sort = nullptr;
@@ -2199,14 +2199,14 @@ expr_ref seq_rewriter::is_nullable(expr* r) {
     expr_ref result(m());
     if (re().is_concat(r, r1, r2) ||
         re().is_intersection(r, r1, r2)) { 
-        m_br.mk_and(is_nullable_rec(r1), is_nullable_rec(r2), result);
+        m_br.mk_and(is_nullable(r1), is_nullable(r2), result);
     }
     else if (re().is_union(r, r1, r2)) {
-        m_br.mk_or(is_nullable_rec(r1), is_nullable_rec(r2), result);
+        m_br.mk_or(is_nullable(r1), is_nullable(r2), result);
     }
     else if (re().is_diff(r, r1, r2)) {
-        m_br.mk_not(is_nullable_rec(r2), result);
+        m_br.mk_not(is_nullable(r2), result);
-        m_br.mk_and(result, is_nullable_rec(r1), result);
+        m_br.mk_and(result, is_nullable(r1), result);
     }
     else if (re().is_star(r) || 
         re().is_opt(r) ||
@@ -2225,22 +2225,22 @@ expr_ref seq_rewriter::is_nullable(expr* r) {
         (re().is_loop(r, r1, lo) && lo > 0) ||
         (re().is_loop(r, r1, lo, hi) && lo > 0) ||
         (re().is_reverse(r, r1))) {
-        result = is_nullable_rec(r1);
+        result = is_nullable(r1);
     }
     else if (re().is_complement(r, r1)) {
-        m_br.mk_not(is_nullable_rec(r1), result);
+        m_br.mk_not(is_nullable(r1), result);
     }
     else if (re().is_to_re(r, r1)) {        
-        result = is_nullable_rec(r1);
+        result = is_nullable(r1);
     }
     else if (m().is_ite(r, cond, r1, r2)) {
-        result = m().mk_ite(cond, is_nullable_rec(r1), is_nullable_rec(r2));
+        result = m().mk_ite(cond, is_nullable(r1), is_nullable(r2));
     }
     else if (m_util.is_re(r, seq_sort)) {
         result = re().mk_in_re(str().mk_empty(seq_sort), r);
     }
     else if (str().is_concat(r, r1, r2)) {
-        m_br.mk_and(is_nullable_rec(r1), is_nullable_rec(r2), result);
+        m_br.mk_and(is_nullable(r1), is_nullable(r2), result);
     }
     else if (str().is_empty(r)) {
         result = m().mk_true();
@@ -2574,7 +2574,17 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
             return mk_empty();
         }
         else {
+#if 0
+            hd = str().mk_nth_i(r1, m_autil.mk_int(0));
+            tl = str().mk_substr(r1, m_autil.mk_int(1), m_autil.mk_sub(str().mk_length(r1), m_autil.mk_int(1)));
+            result = 
+                m().mk_ite(m_br.mk_eq_rw(r1, str().mk_empty(m().get_sort(r1))), 
+                           mk_empty(),
+                           re_and(m_br.mk_eq_rw(ele, hd), re().mk_to_re(tl)));
+            return result;
+#else
             return expr_ref(re().mk_derivative(ele, r), m());
+#endif
         }
     }
     else if (re().is_reverse(r, r1) && re().is_to_re(r1, r2)) {

src/smt/seq_regex.cpp

@@ -101,7 +101,7 @@ namespace smt {
         expr* e = ctx.bool_var2expr(lit.var());
         VERIFY(str().is_in_re(e, s, r));
 
-        TRACE("seq", tout << "propagate " << mk_pp(e, m) << "\n";);
+        TRACE("seq", tout << "propagate " << lit.sign() << " " << mk_pp(e, m) << "\n";);
 
         // convert negative negative membership literals to positive
         // ~(s in R) => s in C(R)
@@ -109,6 +109,10 @@ namespace smt {
             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;
         }
@@ -138,6 +142,8 @@ namespace smt {
         expr_ref acc = sk().mk_accept(s, zero, r);
         literal acc_lit = th.mk_literal(acc);
 
+        TRACE("seq", tout << "propagate " << acc << "\n";);
+
         th.propagate_lit(nullptr, 1, &lit, acc_lit);
     }
 
@@ -177,7 +183,7 @@ namespace smt {
         if (block_unfolding(lit, idx))
             return true;
 
-        propagate_nullable(lit, e, s, idx, r);
+        propagate_nullable(lit, s, idx, r);
 
         return propagate_derivative(lit, e, s, i, idx, r);
     }
@@ -187,9 +193,21 @@ namespace smt {
 
        (accept s i r) => len(s) >= i
        (accept s i r) & ~nullable(r) => len(s) >= i + 1
+
+       evaluate nullable(r):
+       nullable(r) := true -> propagate: (accept s i r) => len(s) >= i
+       nullable(r) := false -> propagate: (accept s i r) => len(s) >= i + 1
+ 
+       Otherwise: 
+       propagate: (accept s i r) => len(s) >= i
+       evaluate len(s) <= i:
+       len(s) <= i := undef -> axiom:     (accept s i r) & len(s) <= i => nullable(r)
+       len(s) <= i := true  -> propagate: (accept s i r) & len(s) <= i => nullable(r)
+       len(s) <= i := false -> noop.
+    
      */
 
-    void seq_regex::propagate_nullable(literal lit, expr* e, expr* s, unsigned idx, expr* r) {
+    void seq_regex::propagate_nullable(literal lit, expr* s, unsigned idx, expr* r) {
         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);
@@ -200,14 +218,16 @@ namespace smt {
             th.propagate_lit(nullptr, 1, &lit, th.m_ax.mk_ge(th.mk_len(s), idx + 1));
         }
         else {
+            literal is_nullable_lit = th.mk_literal(is_nullable);
+            ctx.mark_as_relevant(is_nullable_lit);
             literal len_s_le_i = th.m_ax.mk_le(th.mk_len(s), idx);
             switch (ctx.get_assignment(len_s_le_i)) {
             case l_undef:
-                th.add_axiom(~lit, ~len_s_le_i, th.mk_literal(is_nullable));
+                th.add_axiom(~lit, ~len_s_le_i, is_nullable_lit);
                 break;
             case l_true: {
                 literal lits[2] = { lit, len_s_le_i };
-                th.propagate_lit(nullptr, 2, lits, th.mk_literal(is_nullable));
+                th.propagate_lit(nullptr, 2, lits, is_nullable_lit);
                 break;
             }
             case l_false:

src/smt/seq_regex.h

@@ -59,7 +59,7 @@ namespace smt {
 
         bool block_unfolding(literal lit, unsigned i);
 
-        void propagate_nullable(literal lit, expr* e, expr* s, unsigned idx, expr* r);
+        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);
 

src/smt/theory_seq.cpp

@@ -2878,8 +2878,11 @@ literal theory_seq::mk_simplified_literal(expr * _e) {
 
 literal theory_seq::mk_literal(expr* _e) {
     expr_ref e(_e, m);
-    ensure_enode(e);
+    bool is_not = m.is_not(_e, _e);
-    return ctx.get_literal(e);
+    ensure_enode(_e);
+    literal lit = ctx.get_literal(_e);
+    if (is_not) lit.neg();
+    return lit;
 }
 
 literal theory_seq::mk_seq_eq(expr* a, expr* b) {
@@ -3338,12 +3341,16 @@ void theory_seq::relevant_eh(app* n) {
         m_util.str.is_from_code(n) ||
         m_util.str.is_to_code(n) ||
         m_util.str.is_is_digit(n)) {
+        add_unhandled_expr(n);
+    }
+}
+
+void theory_seq::add_unhandled_expr(expr* n) {
     if (!m_unhandled_expr) {
         ctx.push_trail(value_trail<context, expr*>(m_unhandled_expr));
         m_unhandled_expr = n;
     }
 }
-}
 
 
 eautomaton* theory_seq::get_automaton(expr* re) {

src/smt/theory_seq.h

@@ -506,6 +506,7 @@ namespace smt {
         bool set_empty(expr* x);
         bool is_complex(eq const& e);
         lbool regex_are_equal(expr* r1, expr* r2);
+        void add_unhandled_expr(expr* e);
 
         bool check_extensionality();
         bool check_contains();