Updated regex derivative engine

src/ast/rewriter/seq_axioms.cpp

@@ -850,7 +850,7 @@ namespace seq {
             add_clause(~eq, ge10k);
 
         for (unsigned i = 0; i < k; ++i) {
-            expr* ch = seq.str.mk_nth_i(ubvs, i);
+            expr* ch = seq.str.mk_nth_c(ubvs, i);
             is_digit = seq.mk_char_is_digit(ch);
             add_clause(~ge_len, is_digit);
         }

src/ast/rewriter/seq_rewriter.h

@@ -117,20 +117,20 @@ class seq_rewriter {
     class op_cache {
         struct op_entry {
             decl_kind k;
-            expr* a, *b, *r;
-            op_entry(decl_kind k, expr* a, expr* b, expr* r): k(k), a(a), b(b), r(r) {}
-            op_entry():k(0), a(nullptr), b(nullptr), r(nullptr) {}
+            expr* a, *b, *c, *r;
+            op_entry(decl_kind k, expr* a, expr* b, expr* c, expr* r): k(k), a(a), b(b), c(c), r(r) {}
+            op_entry():k(0), a(nullptr), b(nullptr), c(nullptr), r(nullptr) {}
         };
 
         struct hash_entry {
             unsigned operator()(op_entry const& e) const { 
-                return mk_mix(e.k, e.a ? e.a->get_id() : 0, e.b ? e.b->get_id() : 0);
+                return combine_hash(mk_mix(e.k, e.a ? e.a->get_id() : 0, e.b ? e.b->get_id() : 0), e.c ? e.c->get_id() : 0);
             }
         };
 
         struct eq_entry {
-            bool operator()(op_entry const& a, op_entry const& b) const { 
-                return a.k == b.k && a.a == b.a && a.b == b.b;
+            bool operator()(op_entry const& a, op_entry const& b) const {
+                return a.k == b.k && a.a == b.a && a.b == b.b && a.c == b.c;
             }
         };
 
@@ -143,8 +143,8 @@ class seq_rewriter {
 
     public:
         op_cache(ast_manager& m);
-        expr* find(decl_kind op, expr* a, expr* b);
-        void insert(decl_kind op, expr* a, expr* b, expr* r);
+        expr* find(decl_kind op, expr* a, expr* b, expr* c);
+        void insert(decl_kind op, expr* a, expr* b, expr* c, expr* r);
     };
 
     seq_util       m_util;
@@ -208,8 +208,24 @@ class seq_rewriter {
     bool check_deriv_normal_form(expr* r, int level = 3);
     #endif
 
+    void mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref& result);
+
+    expr_ref mk_antimirov_deriv(expr* e, expr* r, expr* path);
+    expr_ref mk_in_antimirov_rec(expr* s, expr* d);
+    expr_ref mk_in_antimirov(expr* s, expr* d);
+
+    expr_ref mk_antimirov_deriv_intersection(expr* d1, expr* d2, expr* path);
+    expr_ref mk_antimirov_deriv_concat(expr* d, expr* r);
+    expr_ref mk_antimirov_deriv_negate(expr* d);
+    expr_ref mk_antimirov_deriv_union(expr* d1, expr* d2);
+    expr_ref mk_regex_reverse(expr* r);
+    expr_ref mk_regex_concat(expr* r1, expr* r2);
+
+    expr_ref simplify_path(expr* path);
+
     bool lt_char(expr* ch1, expr* ch2);
     bool eq_char(expr* ch1, expr* ch2);
+    bool neq_char(expr* ch1, expr* ch2);
     bool le_char(expr* ch1, expr* ch2);
     bool pred_implies(expr* a, expr* b);
     bool are_complements(expr* r1, expr* r2) const;
@@ -286,6 +302,8 @@ class seq_rewriter {
     expr_ref zero() { return expr_ref(m_autil.mk_int(0), m()); }
     expr_ref one() { return expr_ref(m_autil.mk_int(1), m()); }
     expr_ref minus_one() { return expr_ref(m_autil.mk_int(-1), m()); }
+    expr_ref mk_sub(expr* a, rational const& n);
+    expr_ref mk_sub(expr* a, unsigned n) { return mk_sub(a, rational(n)); }
 
     bool is_suffix(expr* s, expr* offset, expr* len);
     bool is_prefix(expr* s, expr* offset, expr* len);
@@ -379,9 +397,19 @@ class seq_rewriter {
 
     void add_seqs(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_pair_vector& new_eqs);
 
-    // Expose derivative and nullability check
+    /*
+    create the nullability check for r
+    */
     expr_ref is_nullable(expr* r);
+    /*
+    make the derivative of r wrt the given element ele
+    */
     expr_ref mk_derivative(expr* ele, expr* r);
+    /*
+    make the derivative of r wrt the canonical variable v0 = (:var 0), 
+    for example mk_derivative(a+) = (if (v0 = 'a') then a* else [])
+    */
+    expr_ref mk_derivative(expr* r);
 
     // heuristic elimination of element from condition that comes form a derivative.
     // special case optimization for conjunctions of equalities, disequalities and ranges.