tune axioms for derivatives

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

src/ast/rewriter/arith_rewriter.cpp

@@ -239,6 +239,60 @@ bool arith_rewriter::is_bound(expr * arg1, expr * arg2, op_kind kind, expr_ref &
     return false;
 }
 
+
+bool arith_rewriter::is_non_negative(expr* e) {
+    seq_util seq(m());
+    if (seq.str.is_length(e))
+        return true;
+    // TBD: check for even power
+    return false;
+}
+
+/**
+ * perform static analysis on arg1 to determine a non-negative lower bound.
+ * a + b + r1 <= r2 -> false if r1 > r2 and a >= 0, b >= 0
+ * a + b + r1 >= r2 -> false if r1 < r2 and a <= 0, b <= 0
+*/
+bool arith_rewriter::is_separated(expr* arg1, expr* arg2, op_kind kind, expr_ref& result) {
+    if (kind != LE && kind != GE)
+        return false;
+    rational bound(0), r1, r2;
+    expr_ref narg(m());
+    bool has_bound = true;
+    if (!m_util.is_numeral(arg2, r2))
+        return false;
+    auto update_bound = [&](expr* arg) {
+        if (m_util.is_numeral(arg, r1)) {
+            bound += r1;
+            return;
+        }
+        if (kind == LE && is_non_negative(arg))
+            return;
+        if (kind == GE && is_neg_poly(arg, narg) && is_non_negative(narg))
+            return;
+        has_bound = false;
+    };
+    if (m_util.is_add(arg1)) {
+        for (expr* arg : *to_app(arg1)) {
+            update_bound(arg);
+        }
+    }
+    else {
+        update_bound(arg1);
+    }
+    if (!has_bound)
+        return false;
+    if (kind == LE && r1 > r2) {
+        result = m().mk_false();
+        return true;
+    }
+    if (kind == GE && r1 < r2) {
+        result = m().mk_false();
+        return true;
+    }
+    return false;
+}
+
 bool arith_rewriter::elim_to_real_var(expr * var, expr_ref & new_var) {
     numeral val;
     if (m_util.is_numeral(var, val)) {
@@ -427,6 +481,8 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin
             ANUM_LE_GE_EQ();
         }
     }
+    if (is_separated(arg1, arg2, kind, result))
+        return BR_DONE;
     if (is_bound(arg1, arg2, kind, result))
         return BR_DONE;
     if (is_bound(arg2, arg1, inv(kind), result))

src/ast/rewriter/arith_rewriter.h

@@ -64,6 +64,8 @@ class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
     enum op_kind { LE, GE, EQ };
     static op_kind inv(op_kind k) { return k == LE ? GE : (k == GE ? LE : EQ); }
     bool is_bound(expr * arg1, expr * arg2, op_kind kind, expr_ref & result);
+    bool is_separated(expr * arg1, expr * arg2, op_kind kind, expr_ref & result);
+    bool is_non_negative(expr* e);
     br_status mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kind, expr_ref & result);
 
     bool elim_to_real_var(expr * var, expr_ref & new_var);

src/ast/rewriter/seq_rewriter.cpp

@@ -2079,7 +2079,7 @@ expr_ref seq_rewriter::kleene_predicate(expr* cond, sort* seq_sort) {
 
 expr_ref seq_rewriter::is_nullable(expr* r) {
     SASSERT(m_util.is_re(r));
-    expr* r1 = nullptr, *r2 = nullptr;
+    expr* r1 = nullptr, *r2 = nullptr, *cond = nullptr;
     unsigned lo = 0, hi = 0;
     expr_ref result(m());
     if (re().is_concat(r, r1, r2) ||
@@ -2120,6 +2120,9 @@ expr_ref seq_rewriter::is_nullable(expr* r) {
         expr* emptystr = m_util.str.mk_empty(seq_sort);
         result = m().mk_eq(emptystr, r1);
     }
+    else if (m().is_ite(r, cond, r1, r2)) {
+        result = m().mk_ite(cond, is_nullable(r1), is_nullable(r2));
+    }
     else {
         sort* seq_sort = nullptr;
         VERIFY(m_util.is_re(r, seq_sort));
@@ -2663,8 +2666,15 @@ br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) {
 }
 
 bool seq_rewriter::has_cofactor(expr* r, expr_ref& cond, expr_ref& th, expr_ref& el) {
+    if (m().is_ite(r)) {
+        cond = to_app(r)->get_arg(0);
+        th = to_app(r)->get_arg(1);
+        el = to_app(r)->get_arg(2);
+        return true;
+    }
     expr_ref_vector trail(m()), args_th(m()), args_el(m());
     expr* c = nullptr, *tt = nullptr, *ee = nullptr;
+    cond = nullptr;
     obj_map<expr,expr*> cache_th, cache_el;
     expr_mark no_cofactor, visited;
     ptr_vector<expr> todo;

src/ast/rewriter/seq_rewriter.h

@@ -233,6 +233,7 @@ public:
 
     br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
     br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);
+    br_status mk_bool_app(func_decl* f, unsigned n, expr* const* args, expr_ref& result);
 
     bool reduce_eq(expr* l, expr* r, expr_ref_pair_vector& new_eqs, bool& change);
 
@@ -242,8 +243,6 @@ public:
 
     void add_seqs(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_pair_vector& new_eqs);
 
-    br_status mk_bool_app(func_decl* f, unsigned n, expr* const* args, expr_ref& result);
-
     expr_ref derivative(expr* hd, expr* r);
 
     expr_ref is_nullable(expr* r);

src/smt/seq_regex.cpp

@@ -31,12 +31,9 @@ namespace smt {
     class seq_util::str& seq_regex::str() { return th.m_util.str; }
     seq_rewriter& seq_regex::seq_rw() { return th.m_seq_rewrite; }
     seq_skolem& seq_regex::sk() { return th.m_sk; }
+    arith_util& seq_regex::a() { return th.m_autil; }
     void seq_regex::rewrite(expr_ref& e) { th.m_rewrite(e); }
 
-    void seq_regex::propagate_in_re(literal lit) {
-        if (!propagate(lit))
-            m_to_propagate.push_back(lit);
-    }
 
     bool seq_regex::propagate() {
         bool change = false;
@@ -57,24 +54,16 @@ namespace smt {
      * (not (str.in.re s r)) => (str.in.re s (complement r))
      * (str.in.re s r) => r != {}
      * 
-     * (str.in.re s r[if(c,r1,r2)]) & c => (str.in.re s r[r1])
-     * (str.in.re s r[if(c,r1,r2)]) & ~c => (str.in.re s r[r2])
-     * (str.in.re s r) & s = "" => nullable(r)
-     * s != "" => s = unit(head) ++ tail
-     * (str.in.re s r) & s != "" => (str.in.re tail D(head,r))
+     * (str.in.re s r) => (accept s 0 r)
      */
-    
-    bool seq_regex::propagate(literal lit) {
+
+    void seq_regex::propagate_in_re(literal lit) {
         expr* s = nullptr, *r = nullptr;
         expr* e = ctx.bool_var2expr(lit.var());
         VERIFY(str().is_in_re(e, s, r));
 
         TRACE("seq", tout << "propagate " << mk_pp(e, m) << "\n";);
 
-        // only positive assignments of membership propagation are relevant.
-        if (lit.sign() && sk().is_tail(s)) 
-            return true;
-
         // convert negative negative membership literals to positive
         // ~(s in R) => s in C(R)
         if (lit.sign()) {
@@ -82,43 +71,99 @@ namespace smt {
             rewrite(fml);
             literal nlit = th.mk_literal(fml);
             th.propagate_lit(nullptr, 1, &lit, nlit);
-            return true;
+            return;
         }
 
-        if (!sk().is_tail(s) && coallesce_in_re(lit))
-            return true;
+        if (coallesce_in_re(lit))
+            return;
 
-        // TBD
-        // for !sk().is_tail(s):  s in R => R != {}
-        if (false && !sk().is_tail(s)) {
+        // TBD s in R => R != {}
+        if (false) {
             expr_ref is_empty(m.mk_eq(r, re().mk_empty(m.get_sort(s))), m);
             rewrite(is_empty);
             literal is_emptyl = th.mk_literal(is_empty);
             if (ctx.get_assignment(is_emptyl) != l_false) {
                 th.propagate_lit(nullptr, 1, &lit, ~is_emptyl);
-                return true;
+                return;
             }
         }
 
-        if (block_unfolding(lit, s))
+        expr_ref zero(a().mk_int(0), m);
+        expr_ref acc = sk().mk_accept(s, zero, r);
+        literal acc_lit = th.mk_literal(acc);
+
+        th.propagate_lit(nullptr, 1, &lit, acc_lit);
+    }
+
+    void seq_regex::propagate_accept(literal lit) {
+        if (!propagate(lit))
+            m_to_propagate.push_back(lit);
+    }
+
+
+    /**
+     * Propagate the atom (accept s i r)
+     * 
+     * Propagation implements the following inference rules
+     *
+     * (accept s i r[if(c,r1,r2)]) & c => (accept s i r[r1])
+     * (accept s i r[if(c,r1,r2)]) & ~c => (accept s i r[r2])
+     * (accept s i r) & len(s) <= i => nullable(r)
+     * (accept s r) & len(s) > i => (accept s (+ i 1) D(nth(s,i), r))
+     */
+    
+    bool seq_regex::propagate(literal lit) {
+        SASSERT(!lit.sign());
+
+        expr* s = nullptr, *i = nullptr, *r = nullptr;
+        expr* e = ctx.bool_var2expr(lit.var());
+        VERIFY(sk().is_accept(e, s, i, r));
+        unsigned idx = 0;
+        rational n;
+        VERIFY(a().is_numeral(i, n)); 
+        SASSERT(n.is_unsigned());
+        idx = n.get_unsigned();
+
+        TRACE("seq", tout << "propagate " << mk_pp(e, m) << "\n";);
+
+        if (block_unfolding(lit, idx))
             return true;
+
+        // s in R & len(s) <= i => nullable(R)
+        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:
+            ctx.mark_as_relevant(len_s_le_i);
+            return false;
+        case l_true: {
+            expr_ref is_nullable = seq_rw().is_nullable(r);
+            rewrite(is_nullable);
+            th.add_axiom(~lit, ~len_s_le_i, th.mk_literal(is_nullable));
+            return true;
+        }
+        case l_false:
+            break;
+        }
        
         // s in R[if(p,R1,R2)] & p => s in R[R1]
         // s in R[if(p,R1,R2)] & ~p => s in R[R2]
+
+        // TBD combine the two places that perform co-factor rewriting
         expr_ref cond(m), tt(m), el(m);
         if (seq_rw().has_cofactor(r, cond, tt, el)) {
+            rewrite(cond);
             literal lcond = th.mk_literal(cond), next_lit;
             switch (ctx.get_assignment(lcond)) {
             case l_true: {
                 rewrite(tt);
                 literal lits[2] = { lit, lcond };
-                next_lit = th.mk_literal(re().mk_in_re(s, tt));
+                next_lit = th.mk_literal(sk().mk_accept(s, i, tt));
                 th.propagate_lit(nullptr, 2, lits, next_lit);
                 return true;
             }
             case l_false: {
                 rewrite(el);
-                next_lit = th.mk_literal(re().mk_in_re(s, el));
+                next_lit = th.mk_literal(sk().mk_accept(s, i, el));
                 literal lits[2] = { lit, ~lcond };
                 th.propagate_lit(nullptr, 2, lits, next_lit);
                 return true;
@@ -129,34 +174,51 @@ namespace smt {
             }
         }
 
-        // s in R & s = "" => nullable(R)
-        literal is_empty = th.mk_eq(s, str().mk_empty(m.get_sort(s)), false);
-        expr_ref is_nullable = seq_rw().is_nullable(r);
-        rewrite(is_nullable);
-        th.add_axiom(~lit, ~is_empty, th.mk_literal(is_nullable));
-        switch (ctx.get_assignment(is_empty)) {
-        case l_undef:
-            ctx.mark_as_relevant(is_empty);
-            return false;
-        case l_true:
-            return true;
-        case l_false:
-            break;
-        }
-
-        // s in R & s != "" => s = head ++ tail
-        // s in R & s != "" => tail in D(head, R)
-        expr_ref head(m), tail(m), d(m);
-        expr* h = nullptr;
-        sk().decompose(s, head, tail);
-        if (!str().is_unit(head, h))
-            throw default_exception("expected a unit");
-        d = seq_rw().derivative(h, r);
+        // s in R & len(s) > i => tail(s,i) in D(nth(s, i), R)
+        expr_ref head(m), d(m), i_next(m);
+        head = th.mk_nth(s, i);        
+        i_next = a().mk_int(idx + 1);
+        d = seq_rw().derivative(head, r);
         if (!d) 
             throw default_exception("unable to expand derivative");
-        th.add_axiom(is_empty, th.mk_eq(s, th.mk_concat(head, tail), false));
-        th.add_axiom(~lit, is_empty, th.mk_literal(re().mk_in_re(tail, d)));
 
+        // immediately expand a co-factor here so that condition on the character
+        // is expanded.
+
+        literal_vector conds;
+        while (seq_rw().has_cofactor(d, cond, tt, el)) {
+            rewrite(cond);
+            literal lcond = th.mk_literal(cond);
+            bool is_undef = false;
+            switch (ctx.get_assignment(lcond)) {
+            case l_true: 
+                conds.push_back(~lcond);
+                d = tt;
+                break;
+            case l_false:
+                conds.push_back(lcond);
+                d = el;
+                break;
+            case l_undef:
+                ctx.mark_as_relevant(lcond);
+                d = m.mk_ite(cond, tt, el);
+                is_undef = true;
+                break;
+            }
+            if (is_undef)
+                break;
+            rewrite(d);
+        }
+        if (conds.empty()) {
+            th.add_axiom(~lit, len_s_le_i, th.mk_literal(sk().mk_accept(s, i_next, d)));
+        }
+        else {
+            conds.push_back(~lit);
+            conds.push_back(len_s_le_i);
+            conds.push_back(th.mk_literal(sk().mk_accept(s, i_next, d)));
+            for (literal lit : conds) ctx.mark_as_relevant(lit);
+            ctx.mk_th_axiom(th.get_id(), conds.size(), conds.c_ptr());
+        }
         TRACE("seq", tout << "head " << head << "\n";
               tout << mk_pp(r, m) << "\n";);
         return true;
@@ -172,11 +234,8 @@ namespace smt {
      * Limiting the depth of unfolding s below such lengths is not useful.
      */
 
-    bool seq_regex::block_unfolding(literal lit, expr* s) {
+    bool seq_regex::block_unfolding(literal lit, unsigned i) {
         expr* t = nullptr;
-        unsigned i = 0;
-        if (!sk().is_tail_u(s, t, i))
-            return false;
         if (i > th.m_max_unfolding_depth && 
             th.m_max_unfolding_lit != null_literal && 
             ctx.get_assignment(th.m_max_unfolding_lit) == l_true && 

src/smt/seq_regex.h

@@ -47,14 +47,15 @@ namespace smt {
         class seq_util::str& str();
         seq_rewriter& seq_rw();
         seq_skolem& sk();
+        arith_util& a();
 
         void rewrite(expr_ref& e);
 
-        bool propagate(literal lit);
-
         bool coallesce_in_re(literal lit);
 
-        bool block_unfolding(literal lit, expr* s);
+        bool propagate(literal lit);
+
+        bool block_unfolding(literal lit, unsigned i);
 
         expr_ref mk_first(expr* r);
 
@@ -72,6 +73,8 @@ namespace smt {
 
         void propagate_in_re(literal lit);
 
+        void propagate_accept(literal lit);
+
         void propagate_eq(expr* r1, expr* r2);
 
         void propagate_ne(expr* r1, expr* r2);

src/smt/seq_skolem.h

@@ -59,6 +59,7 @@ namespace smt {
 
         expr_ref mk_align(expr* e1, expr* e2, expr* e3, expr* e4) { return mk(m_seq_align, e1, e2, e3, e4); }
         expr_ref mk_accept(expr_ref_vector const& args) { return expr_ref(seq.mk_skolem(m_accept, args.size(), args.c_ptr(), m.mk_bool_sort()), m); }
+        expr_ref mk_accept(expr* s, expr* i, expr* r) { return mk(m_accept, s, i, r, nullptr, m.mk_bool_sort()); }
         expr_ref mk_indexof_left(expr* t, expr* s, expr* offset = nullptr) { return mk(m_indexof_left, t, s, offset); }
         expr_ref mk_indexof_right(expr* t, expr* s, expr* offset = nullptr) { return mk(m_indexof_right, t, s, offset); }
         expr_ref mk_last_indexof_left(expr* t, expr* s, expr* offset = nullptr) { return mk("seq.last_indexof_left", t, s, offset); }
@@ -95,9 +96,15 @@ namespace smt {
         bool is_step(expr* e, expr*& s, expr*& idx, expr*& re, expr*& i, expr*& j, expr*& t) const;
         bool is_accept(expr* acc) const {  return is_skolem(m_accept, acc); }
         bool is_accept(expr* a, expr*& s, expr*& i, expr*& r, expr*& n) const { 
-            return is_accept(a) && (s = to_app(a)->get_arg(0), i = to_app(a)->get_arg(1), 
-                                    r = to_app(a)->get_arg(2), n = to_app(a)->get_arg(3), 
-                                    true); 
+            return is_accept(a) && to_app(a)->get_num_args() == 4 && 
+                (s = to_app(a)->get_arg(0), i = to_app(a)->get_arg(1), 
+                 r = to_app(a)->get_arg(2), n = to_app(a)->get_arg(3), 
+                 true); 
+        }
+        bool is_accept(expr* a, expr*& s, expr*& i, expr*& r) const {
+            return is_accept(a) && to_app(a)->get_num_args() == 3 &&
+                (s = to_app(a)->get_arg(0), i = to_app(a)->get_arg(1),
+                 r = to_app(a)->get_arg(2), true);
         }
         bool is_post(expr* e, expr*& s, expr*& start);
         bool is_pre(expr* e, expr*& s, expr*& i);

src/smt/theory_seq.cpp

@@ -1535,7 +1535,8 @@ bool theory_seq::internalize_term(app* term) {
         return true;
     }
 
-    if (ctx.get_fparams().m_seq_use_derivatives && m_util.str.is_in_re(term)) {
+    if (ctx.get_fparams().m_seq_use_derivatives && 
+        (m_util.str.is_in_re(term) || m_sk.is_accept(term))) {
         bool_var bv = ctx.mk_bool_var(term);
         ctx.set_var_theory(bv, get_id());
         ctx.mark_as_relevant(bv);
@@ -3053,7 +3054,12 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
     }
     else if (is_accept(e)) {
         if (is_true) {
-            propagate_accept(lit, e);
+            if (ctx.get_fparams().m_seq_use_derivatives) {
+                m_regex.propagate_accept(lit);
+            }
+            else {
+                propagate_accept(lit, e);
+            }
         }
     }
     else if (m_sk.is_step(e)) {