Updated regex derivative engine #5567

veanes · 2021-09-24T12:41:17Z

Rewrote/updated several derivate related algos both for correctness and performance.
Main changes involve more efficient use of algebraic laws and avoidance of unnecessary rewrites that in many cases were causing orders of magnitude of overhead.
Several open issues should be addressed by the updated engine.
Some old code is still there for convenience to debug possible regressions, that will eventually be removed, once any new regression bugs have been flushed out.

src/ast/seq_decl_plugin.cpp

src/ast/rewriter/seq_rewriter.cpp

src/smt/seq_regex.cpp

NikolajBjorner · 2021-10-05T01:59:13Z

We lost some rewrites

From re.smt2: These should have been rewritten to true:

(str.in_re "" (re.* (str.to_re "a")))
(str.in_re "" (re.* (str.to_re "a")))
(str.in_re "" (str.to_re ""))
(not (str.in_re "" (re.+ re.allchar)))
(not (str.in_re "" (re.+ re.allchar)))

NikolajBjorner · 2021-10-05T02:05:14Z

re_rewrites.smt2 exposes a reference count leak.

E.g., fix by taking a reference count in callee.

 expr_ref seq_rewriter::mk_antimirov_deriv(expr* e, expr* r, expr* path) {
+    expr_ref _path(path, m()), _r(r, ());
     expr_ref result(m_op_cache.find(OP_RE_DERIVATIVE, e, r, path), m());
     if (!result) {
         mk_antimirov_deriv_rec(e, r, path, result);
@@ -3204,6 +3205,7 @@ expr_ref seq_rewriter::mk_antimirov_deriv_intersection(expr* d1, expr* d2, expr*
 
 expr_ref seq_rewriter::mk_antimirov_deriv_concat(expr* d, expr* r) {
     expr_ref result(m());
+    expr_ref _r(r, m()), _d(d, m());
     expr* c, * t, * e;
     if (m().is_ite(d, c, t, e))
         result = m().mk_ite(c, mk_antimirov_deriv_concat(t, r), mk_antimirov_deriv_concat(e, r));

src/ast/rewriter/seq_rewriter.cpp

NikolajBjorner · 2021-10-07T02:27:10Z

    else if (re().is_of_pred(r, r1)) {
        array_util array(m());
        expr* args[2] = { r1, e };
        result = array.mk_select(2, args);
        // Use mk_der_cond to normalize
        STRACE("seq_verbose", tout << "deriv of_pred" << std::endl;);
        result = mk_der_cond(result, e, seq_sort);
    }
    else
        // stuck cases
        result = re().mk_derivative(e, r);

Need case for is_of_pred.
Some functionality is shared between mk_antimirov_derivative_rec and mk_deriv_rec.

NikolajBjorner · 2021-10-07T02:28:34Z

Also need REWRITE_FULL, REWRITE1 is not enough


    if (get_head_tail(a, hd, tl)) {
        //result = re().mk_in_re(tl, re().mk_derivative(hd, b));
        //result = re().mk_in_re(tl, mk_derivative(hd, b));
        result = mk_in_antimirov(tl, mk_antimirov_deriv(hd, b, m().mk_true()));
        return BR_REWRITE_FULL;
    }

veanes · 2021-10-07T03:02:37Z

I addressed the above comments, but I probably need to revisit where I need to use mk_der_cond as in the missing case of .is_of_pred, at some point I omitted relying on the BDD-like structure -- wanted to do this in a more principled way I wanted instead to use BDDs based on bits in the characters. But I understand this heuristic helps in general with simplifications and detecting unsat cases.

NikolajBjorner · 2021-10-07T03:44:05Z

bdd "structure" shouldn't matter (much) for of-pred.

veanes · 2021-10-07T04:25:22Z

Your suggested fixes actually took care of all the failing builds. I was expecting more failures. I guess something I don't understand (and essentially violated the "protocol") is the BR_REWRITE... status flags. We could maybe spend a meeting (say an hour or so) on these and go over the overarching logic, could also be in person at work.

src/ast/seq_decl_plugin.cpp

src/ast/seq_decl_plugin.h

NikolajBjorner · 2021-10-07T15:50:11Z

src/ast/rewriter/seq_rewriter.cpp

+    rational jv;
+    if (str().is_extract(t, s, j, k) && m_autil.is_numeral(j, jv) && jv.is_nonneg()) {
+        unsigned i;
+        expr_ref k_min_1(str().is_len_sub(k, l, s_, i) && s == s_ ? 


need to rewrite this

pre-condition jv.is_unsigned() allows jv.get_unsigned(). Pre-condition jv.is_nonneg() does not allow jv.get_uint32()

review for when indices are negative

NikolajBjorner · 2021-10-07T15:50:18Z

src/ast/rewriter/seq_rewriter.cpp

+    if (str().is_extract(t, s, j, k) && m_autil.is_numeral(j, jv) && jv.is_nonneg()) {
+        unsigned i;
+        // k = |s_| - i, l = |s_| implies that lastpos = j + k - 1 = k + j - 1 = j + l - i - 1 = l + j - i - 1
+        expr_ref lastpos(str().is_len_sub(k, l, s_, i) && s == s_ ? 


need to rewrite this

pre-condition jv.is_unsigned() allows jv.get_unsigned(). Pre-condition jv.is_nonneg() does not allow jv.get_uint32()
review for when indices are negative

NikolajBjorner · 2021-10-07T15:51:32Z

src/ast/rewriter/seq_rewriter.cpp

-    expr_ref one(m_autil.mk_int(1), m());
-    if (str().is_extract(t, s, j, k))
-        result = str().mk_substr(s, j, m_autil.mk_sub(k, one));
+    if (str().is_extract(t, s, j, k)) {


something required inline simplification here. It might be too brittle to assume results of such functions are simplified.

NikolajBjorner · 2021-10-07T15:52:34Z

src/ast/rewriter/seq_rewriter.cpp

@@ -2881,7 +2896,8 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) {
 br_status seq_rewriter::mk_re_derivative(expr* ele, expr* r, expr_ref& result) {
    result = mk_derivative(ele, r);
    // TBD: we may even declare BR_DONE here and potentially miss some simplifications
-    return re().is_derivative(result) ? BR_DONE : BR_REWRITE_FULL;
+    // return re().is_derivative(result) ? BR_DONE : BR_REWRITE_FULL;
+    return BR_DONE;


it was changed, because...

NikolajBjorner · 2021-10-07T15:53:20Z

src/ast/rewriter/seq_rewriter.cpp

 expr_ref seq_rewriter::mk_derivative(expr* ele, expr* r) {
-    STRACE("seq_verbose", tout << "derivative: " << mk_pp(ele, m())
+    /*STRACE("seq_verbose", tout << "derivative: " << mk_pp(ele, m())


remove commented out code

NikolajBjorner · 2021-10-07T15:54:00Z

src/ast/rewriter/seq_rewriter.cpp

+}
+
+expr_ref seq_rewriter::mk_antimirov_deriv(expr* e, expr* r, expr* path) {
+    // Take reference count of path and r


why not reference count on e?

NikolajBjorner · 2021-10-07T15:54:26Z

src/ast/rewriter/seq_rewriter.cpp

+                result = re().mk_ite_simplify(m().mk_eq(e, h), re().mk_to_re(t), nothing());
+        }
+        else
+        {


NikolajBjorner · 2021-10-07T15:55:31Z

src/ast/rewriter/seq_rewriter.cpp

+                result = nothing();
+            else
+                // observe that the precondition |r1|>0 of mk_seq_rest is implied by c1
+                result = re().mk_ite_simplify(c1, re().mk_reverse(re().mk_to_re(mk_seq_butlast(r1))), nothing());


m_br.mk_ite

NikolajBjorner · 2021-10-07T15:57:06Z

src/ast/rewriter/seq_rewriter.cpp

+            result = mk_antimirov_deriv_union(c1, re().mk_ite_simplify(r1nullable, mk_antimirov_deriv(e, r2, path), nothing()));
+    }
+    else if (m().is_ite(r, c, r1, r2)) {
+        c1 = simplify_path(m().mk_and(c, path));


sometimes called, other times using m_bv.mk_and.
Should the path expression be considered as an ADT?

NikolajBjorner · 2021-10-07T15:58:24Z

src/ast/rewriter/seq_rewriter.cpp

+        result = mk_antimirov_deriv_intersection(
+            mk_antimirov_deriv(e, r1, path),
+            mk_antimirov_deriv_negate(mk_antimirov_deriv(e, r2, path)), m().mk_true());
+    else if (re().is_of_pred(r, r1)) {


hoist to self-contained function that gets used also the other place

NikolajBjorner · 2021-10-07T15:59:55Z

src/ast/rewriter/seq_rewriter.cpp

+    // Take reference count of r and d
+    expr_ref _r(r, m()), _d(d, m());
+    expr* c, * t, * e;
+    if (m().is_ite(d, c, t, e))


what is cost model for this rewrite?

NikolajBjorner · 2021-10-07T16:00:08Z

src/ast/rewriter/seq_rewriter.cpp

+}
+
+expr_ref seq_rewriter::mk_antimirov_deriv_union(expr* d1, expr* d2)
+{


NikolajBjorner · 2021-10-07T16:01:39Z

src/ast/rewriter/seq_rewriter.cpp

+        // s in [] <==> false, also: s in () <==> false when |s|>0
+        result = m().mk_false();
+    else if (m().is_ite(d, c, d1, d2))
+        result = re().mk_ite_simplify(c, mk_in_antimirov_rec(s, d1), mk_in_antimirov_rec(s, d2));


m_br.mk_ite

NikolajBjorner · 2021-10-07T16:03:02Z

src/ast/rewriter/seq_rewriter.cpp

+    return result;
+}
+
+/*


seems more reasonable to have a path.push method that does this instead of creating mk_and then simplifying

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

veanes requested a review from NikolajBjorner September 24, 2021 12:41

NikolajBjorner reviewed Sep 25, 2021

View reviewed changes

src/ast/seq_decl_plugin.cpp Outdated Show resolved Hide resolved

NikolajBjorner reviewed Sep 25, 2021

View reviewed changes

src/ast/rewriter/seq_rewriter.cpp Show resolved Hide resolved

NikolajBjorner reviewed Sep 25, 2021

View reviewed changes

src/ast/rewriter/seq_rewriter.cpp Outdated Show resolved Hide resolved

NikolajBjorner reviewed Sep 25, 2021

View reviewed changes

src/ast/rewriter/seq_rewriter.cpp Show resolved Hide resolved

NikolajBjorner reviewed Sep 28, 2021

View reviewed changes

src/smt/seq_regex.cpp Outdated Show resolved Hide resolved

veanes force-pushed the newderiv branch from 3794f81 to beaa45e Compare September 28, 2021 00:54

NikolajBjorner reviewed Oct 5, 2021

View reviewed changes

src/ast/rewriter/seq_rewriter.cpp Outdated Show resolved Hide resolved

NikolajBjorner reviewed Oct 7, 2021

View reviewed changes

src/ast/seq_decl_plugin.cpp Outdated Show resolved Hide resolved

NikolajBjorner reviewed Oct 7, 2021

View reviewed changes

src/ast/seq_decl_plugin.cpp Outdated Show resolved Hide resolved

NikolajBjorner reviewed Oct 7, 2021

View reviewed changes

src/ast/seq_decl_plugin.h Outdated Show resolved Hide resolved

NikolajBjorner reviewed Oct 7, 2021

View reviewed changes

src/ast/seq_decl_plugin.h Show resolved Hide resolved

veanes added 11 commits October 6, 2021 22:30

updated derivative engine

890a66c

some edit

1fdb655

further improvements in derivative code

60f39b0

more deriv code edits and re::to_str update

c4275df

optimized mk_deriv_accept

0a4cb03

fixed PR comments

ab92030

small syntax fix

11479a2

updated some simplifications

dec03d1

bugfix:forgot to_re before reverse

0eea583

fixed PR comments

f948a63

more PR comment fixes

612588f

veanes added 2 commits October 6, 2021 22:30

more PR comment fixes

7ecbc62

forgot to delete

b62fdca

veanes force-pushed the newderiv branch from b01e31e to b62fdca Compare October 7, 2021 05:30

deleting unused definition

3d5b27e

NikolajBjorner reviewed Oct 7, 2021

View reviewed changes

src/ast/rewriter/seq_rewriter.cpp Outdated

}

expr_ref seq_rewriter::mk_antimirov_deriv_union(expr* d1, expr* d2)

{

Copy link

Contributor

NikolajBjorner Oct 7, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

format

NikolajBjorner reviewed Oct 7, 2021

View reviewed changes

NikolajBjorner added 2 commits October 8, 2021 12:07

fixes

90e8a3c

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

fixes

691fdf0

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

NikolajBjorner merged commit 146f462 into Z3Prover:master Oct 8, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Updated regex derivative engine #5567

Updated regex derivative engine #5567

veanes commented Sep 24, 2021

NikolajBjorner commented Oct 5, 2021

NikolajBjorner commented Oct 5, 2021

NikolajBjorner commented Oct 7, 2021

NikolajBjorner commented Oct 7, 2021

veanes commented Oct 7, 2021

NikolajBjorner commented Oct 7, 2021

veanes commented Oct 7, 2021

NikolajBjorner Oct 7, 2021

NikolajBjorner Oct 7, 2021

NikolajBjorner Oct 7, 2021

NikolajBjorner Oct 7, 2021

NikolajBjorner Oct 7, 2021

NikolajBjorner Oct 7, 2021

NikolajBjorner Oct 7, 2021

NikolajBjorner Oct 7, 2021

NikolajBjorner Oct 7, 2021

NikolajBjorner Oct 7, 2021

NikolajBjorner Oct 7, 2021

NikolajBjorner Oct 7, 2021

NikolajBjorner Oct 7, 2021

NikolajBjorner Oct 7, 2021

Updated regex derivative engine #5567

Updated regex derivative engine #5567

Conversation

veanes commented Sep 24, 2021

NikolajBjorner commented Oct 5, 2021

NikolajBjorner commented Oct 5, 2021

NikolajBjorner commented Oct 7, 2021

NikolajBjorner commented Oct 7, 2021

veanes commented Oct 7, 2021

NikolajBjorner commented Oct 7, 2021

veanes commented Oct 7, 2021

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment