From 6910c0d5ebb000e1975ca53850dc70d0c4311aaa Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 27 Jul 2020 18:10:14 -0700
Subject: [PATCH] Revert "Seq rewriter integration (#4597)" (#4598)

This reverts commit e90f01006c176b981f9c77f8cb00f9f278e895d1.
---
 src/ast/rewriter/seq_rewriter.cpp | 244 ++++--------------------------
 src/ast/rewriter/seq_rewriter.h   |  12 +-
 2 files changed, 31 insertions(+), 225 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index afc000c33..563b56b76 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -2200,15 +2200,11 @@ expr_ref seq_rewriter::re_predicate(expr* cond, sort* seq_sort) {
 }
 
 expr_ref seq_rewriter::is_nullable(expr* r) {
-    STRACE("seq_verbose", tout << "is_nullable: "
-                               << mk_pp(r, m()) << std::endl;);
     expr_ref result(m_op_cache.find(_OP_RE_IS_NULLABLE, r, nullptr), m());
     if (!result) {
         result = is_nullable_rec(r);
         m_op_cache.insert(_OP_RE_IS_NULLABLE, r, nullptr, result);        
     }
-    STRACE("seq_verbose", tout << "is_nullable result: "
-                               << mk_pp(result, m()) << std::endl;);
     return result;
 }
 
@@ -2387,15 +2383,11 @@ br_status seq_rewriter::mk_re_derivative(expr* ele, expr* r, expr_ref& result) {
         Duplicate nested conditions are eliminated.
 */
 expr_ref seq_rewriter::mk_derivative(expr* ele, expr* r) {
-    STRACE("seq_verbose", tout << "derivative: " << mk_pp(ele, m())
-                               << "," << mk_pp(r, m()) << std::endl;);
     expr_ref result(m_op_cache.find(OP_RE_DERIVATIVE, ele, r), m());
     if (!result) {
         result = mk_derivative_rec(ele, r);
         m_op_cache.insert(OP_RE_DERIVATIVE, ele, r, result);
     }
-    STRACE("seq_verbose", tout << "derivative result: "
-                               << mk_pp(result, m()) << std::endl;);
     return result;
 }
 
@@ -2411,129 +2403,40 @@ expr_ref seq_rewriter::mk_der_concat(expr* r1, expr* r2) {
     return mk_der_op(OP_RE_CONCAT, r1, r2);
 }
 
-/*
-    Utility functions to decide char <, ==, and <=.
-    Return true if deduced, false if unknown.
-*/
-bool seq_rewriter::lt_char(expr* ch1, expr* ch2) {
-    unsigned u1, u2;
-    return u().is_const_char(ch1, u1) &&
-           u().is_const_char(ch2, u2) && (u1 < u2);
-}
-bool seq_rewriter::eq_char(expr* ch1, expr* ch2) {
-    return ch1 == ch2;
-}
-bool seq_rewriter::le_char(expr* ch1, expr* ch2) {
-    return eq_char(ch1, ch2) || lt_char(ch1, ch2);
-}
-
-/*
-    Utility function to decide if a simple predicate (ones that appear
-    as the conditions in if-then-else expressions in derivatives)
-    implies another.
-
-    Return true if we deduce that a implies b, false if unknown.
-
-    Current cases handled:
-    - a and b are char <= constraints, or negations of char <= constraints
-*/
-bool seq_rewriter::pred_implies(expr* a, expr* b) {
-    STRACE("seq_verbose", tout << "pred_implies: "
-                               << "," << mk_pp(a, m())
-                               << "," << mk_pp(b, m()) << std::endl;);
-    expr *cha1 = nullptr, *cha2 = nullptr, *nota = nullptr,
-         *chb1 = nullptr, *chb2 = nullptr, *notb = nullptr;
-    if (m().is_not(a, nota) &&
-        m().is_not(b, notb)) {
-        return pred_implies(notb, nota);
-    }
-    else if (u().is_char_le(a, cha1, cha2) &&
-             u().is_char_le(b, chb1, chb2)) {
-        return le_char(chb1, cha1) && le_char(cha2, chb2);
-    }
-    else if (u().is_char_le(a, cha1, cha2) &&
-             m().is_not(b, notb) &&
-             u().is_char_le(notb, chb1, chb2)) {
-        return (le_char(chb2, cha1) && lt_char(cha2, chb1)) ||
-               (lt_char(chb2, cha1) && le_char(cha2, chb1));
-    }
-    else if (u().is_char_le(b, chb1, chb2) &&
-             m().is_not(a, nota) &&
-             u().is_char_le(nota, cha1, cha2)) {
-        return le_char(chb1, cha2) && le_char(cha1, chb2);
-    }
-    return false;
-}
-
 /*
     Apply a binary operation, preserving BDD normal form on derivative expressions.
 
     Preconditions:
-        - k is a binary op code on REs: one of concat, intersection, or union
-          (not difference)
+        - k is a binary op code on REs (concat, intersection, or union)
         - a and b are in BDD form
 
     Postcondition:
         - result is in BDD form
 */
 expr_ref seq_rewriter::mk_der_op_rec(decl_kind k, expr* a, expr* b) {
-    STRACE("seq_verbose", tout << "mk_der_op_rec: " << k
-                               << "," << mk_pp(a, m())
-                               << "," << mk_pp(b, m()) << std::endl;);
     expr* ca = nullptr, *a1 = nullptr, *a2 = nullptr;
     expr* cb = nullptr, *b1 = nullptr, *b2 = nullptr;
     expr_ref result(m());
-    // Simplify if-then-elses whenever possible
     auto mk_ite = [&](expr* c, expr* a, expr* b) {
         return (a == b) ? a : m().mk_ite(c, a, b);
     };
-    // Use character code to order conditions
-    auto get_id = [&](expr* e) {
-        expr *ch1 = nullptr, *ch2 = nullptr;
-        unsigned ch;
-        if (u().is_char_le(e, ch1, ch2) && u().is_const_char(ch2, ch))
-            return ch;
-        // Fallback: use expression ID (but use same ID for complement)
-        re().is_complement(e, e);
-        return e->get_id();
-    };
     if (m().is_ite(a, ca, a1, a2)) {
-        expr_ref r1(m()), r2(m());
-        expr_ref notca(m().mk_not(ca), m());
         if (m().is_ite(b, cb, b1, b2)) {
-            // --- Core logic for combining two BDDs
-            expr_ref notcb(m().mk_not(cb), m());
             if (ca == cb) {
-                r1 = mk_der_op(k, a1, b1);
-                r2 = mk_der_op(k, a2, b2);
+                expr_ref r1 = mk_der_op(k, a1, b1);
+                expr_ref r2 = mk_der_op(k, a2, b2);
                 result = mk_ite(ca, r1, r2);
                 return result;
             }
-            // Order with higher IDs on the outside
-            if (get_id(ca) < get_id(cb)) {
-                std::swap(a, b);
-                std::swap(ca, cb);
-                std::swap(notca, notcb);
-                std::swap(a1, b1);
-                std::swap(a2, b2);
+            else if (ca->get_id() < cb->get_id()) {
+                expr_ref r1 = mk_der_op(k, a, b1);
+                expr_ref r2 = mk_der_op(k, a, b2);
+                result = mk_ite(cb, r1, r2);
+                return result;
             }
-            // Simplify if there is a relationship between ca and cb
-            if (pred_implies(ca, cb)) {
-                r1 = mk_der_op(k, a1, b1);
-            }
-            else if (pred_implies(ca, notcb)) {
-                r1 = mk_der_op(k, a1, b2);
-            }
-            if (pred_implies(notca, cb)) {
-                r2 = mk_der_op(k, a2, b1);
-            }
-            else if (pred_implies(notca, notcb)) {
-                r2 = mk_der_op(k, a2, b2);
-            }
-            // --- End core logic
         }
-        if (!r1) r1 = mk_der_op(k, a1, b);
-        if (!r2) r2 = mk_der_op(k, a2, b);
+        expr_ref r1 = mk_der_op(k, a1, b);
+        expr_ref r2 = mk_der_op(k, a2, b);
         result = mk_ite(ca, r1, r2);
         return result;
     }
@@ -2598,8 +2501,6 @@ expr_ref seq_rewriter::mk_der_op(decl_kind k, expr* a, expr* b) {
 }
 
 expr_ref seq_rewriter::mk_der_compl(expr* r) {
-    STRACE("seq_verbose", tout << "mk_der_compl: " << mk_pp(r, m())
-                               << std::endl;);
     expr_ref result(m_op_cache.find(OP_RE_COMPLEMENT, r, nullptr), m());
     if (!result) {
         expr* c = nullptr, * r1 = nullptr, * r2 = nullptr;
@@ -2613,71 +2514,6 @@ expr_ref seq_rewriter::mk_der_compl(expr* r) {
     return result;
 }
 
-/*
-    Make an re_predicate with an arbitrary condition cond, enforcing
-    derivative normal form on how conditions are written.
-
-    Tries to rewrites everything to (ele <= x) constraints:
-    (ele = a) => ite(ele <= a-1, none, ite(ele <= a, epsilon, none))
-    (a = ele) => "
-    (a <= ele) => ite(ele <= a-1, none, epsilon)
-    (not p)   => mk_der_compl(...)
-    (p and q) => mk_der_inter(...)
-    (p or q)  => mk_der_union(...)
-
-    Postcondition: result is in BDD form
-*/
-expr_ref seq_rewriter::mk_der_cond(expr* cond, expr* ele, sort* seq_sort) {
-    STRACE("seq_verbose", tout << "mk_der_cond: "
-        <<  mk_pp(cond, m()) << ", " << mk_pp(ele, m()) << std::endl;);
-    sort *ele_sort = nullptr;
-    VERIFY(u().is_seq(seq_sort, ele_sort));
-    SASSERT(ele_sort == m().get_sort(ele));
-    expr *c1 = nullptr, *c2 = nullptr, *ch1 = nullptr, *ch2 = nullptr;
-    unsigned ch = 0;
-    expr_ref result(m()), r1(m()), r2(m());
-    if (m().is_eq(cond, ch1, ch2)) {
-        r1 = u().mk_le(ch1, ch2);
-        r1 = mk_der_cond(r1, ele, seq_sort);
-        r2 = u().mk_le(ch2, ch1);
-        r2 = mk_der_cond(r2, ele, seq_sort);
-        result = mk_der_inter(r1, r2);
-    }
-    else if (u().is_char_le(cond, ch1, ch2) &&
-             u().is_const_char(ch1, ch) && (ch2 == ele)) {
-        if (ch > 0) {
-            result = u().mk_char(ch - 1);
-            result = u().mk_le(ele, result);
-            result = re_predicate(result, seq_sort);
-            result = mk_der_compl(result);
-        }
-        else {
-            result = m().mk_true();
-            result = re_predicate(result, seq_sort);
-        }
-    }
-    else if (m().is_not(cond, c1)) {
-        result = mk_der_cond(c1, ele, seq_sort);
-        result = mk_der_compl(result);
-    }
-    else if (m().is_and(cond, c1, c2)) {
-        r1 = mk_der_cond(c1, ele, seq_sort);
-        r2 = mk_der_cond(c2, ele, seq_sort);
-        result = mk_der_inter(r1, r2);
-    }
-    else if (m().is_or(cond, c1, c2)) {
-        r1 = mk_der_cond(c1, ele, seq_sort);
-        r2 = mk_der_cond(c2, ele, seq_sort);
-        result = mk_der_union(r1, r2);
-    }
-    else {
-        result = re_predicate(cond, seq_sort);
-    }
-    STRACE("seq_verbose", tout << "mk_der_cond result: "
-        <<  mk_pp(result, m()) << std::endl;);
-    return result;
-}
-
 expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
     expr_ref result(m());
     sort* seq_sort = nullptr, *ele_sort = nullptr;
@@ -2752,19 +2588,14 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
         expr_ref hd(m()), tl(m());
         if (get_head_tail(r1, hd, tl)) {
             // head must be equal; if so, derivative is tail
-            // Use mk_der_cond to normalize
-            STRACE("seq_verbose", tout << "deriv to_re" << std::endl;);
-            result = m().mk_eq(ele, hd);
-            result = mk_der_cond(result, ele, seq_sort);
-            expr_ref r1(re().mk_to_re(tl), m());
-            result = mk_der_concat(result, r1);
-            return result;
+            result = re().mk_to_re(tl);
+            return re_and(m_br.mk_eq_rw(ele, hd), result);
         }
         else if (str().is_empty(r1)) {
             return mk_empty();
         }
-#if 0
         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 = re().mk_to_re(tl);
@@ -2773,8 +2604,10 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
                            mk_empty(),
                            re_and(m_br.mk_eq_rw(ele, hd), result));
             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)) {
         // Reverses are rewritten so that the only derivative case is
@@ -2782,16 +2615,14 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
         // This is analagous to the previous is_to_re case.
         expr_ref hd(m()), tl(m());
         if (get_head_tail_reversed(r2, hd, tl)) {
-            // Use mk_der_cond to normalize
-            STRACE("seq_verbose", tout << "deriv reverse to_re" << std::endl;);
-            result = m().mk_eq(ele, tl);
-            result = mk_der_cond(result, ele, seq_sort);
-            result = mk_der_concat(result, re().mk_reverse(re().mk_to_re(hd)));
-            return result;
+            return re_and(m_br.mk_eq_rw(ele, tl), re().mk_reverse(re().mk_to_re(hd)));
         }
         else if (str().is_empty(r2)) {
             return mk_empty();
         }
+        else {
+            return expr_ref(re().mk_derivative(ele, r), m());
+        }
     }
     else if (re().is_range(r, r1, r2)) {
         // r1, r2 are sequences.
@@ -2800,14 +2631,8 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
             if (s1.length() == 1 && s2.length() == 1) {
                 expr_ref ch1(m_util.mk_char(s1[0]), m());
                 expr_ref ch2(m_util.mk_char(s2[0]), m());
-                // Use mk_der_cond to normalize
-                STRACE("seq_verbose", tout << "deriv range zstring" << std::endl;);
-                expr_ref p1(u().mk_le(ch1, ele), m());
-                p1 = mk_der_cond(p1, ele, seq_sort);
-                expr_ref p2(u().mk_le(ele, ch2), m());
-                p2 = mk_der_cond(p2, ele, seq_sort);
-                result = mk_der_inter(p1, p2);
-                return result;
+                return mk_der_inter(re_predicate(m_util.mk_le(ch1, ele), seq_sort),
+                                    re_predicate(m_util.mk_le(ele, ch2), seq_sort));
             }
             else {
                 return mk_empty();
@@ -2815,14 +2640,8 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
         }
         expr* e1 = nullptr, *e2 = nullptr;
         if (str().is_unit(r1, e1) && str().is_unit(r2, e2)) {
-            // Use mk_der_cond to normalize
-            STRACE("seq_verbose", tout << "deriv range str" << std::endl;);
-            expr_ref p1(u().mk_le(e1, ele), m());
-            p1 = mk_der_cond(p1, ele, seq_sort);
-            expr_ref p2(u().mk_le(ele, e2), m());
-            p2 = mk_der_cond(p2, ele, seq_sort);
-            result = mk_der_inter(p1, p2);
-            return result;
+            return mk_der_inter(re_predicate(m_util.mk_le(e1, ele), seq_sort),
+                                re_predicate(m_util.mk_le(ele, e2), seq_sort));
         }
     }
     else if (re().is_full_char(r)) {
@@ -2832,14 +2651,10 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
         array_util array(m());
         expr* args[2] = { p, ele };
         result = array.mk_select(2, args);
-        // Use mk_der_cond to normalize
-        STRACE("seq_verbose", tout << "deriv of_pred" << std::endl;);
-        return mk_der_cond(result, ele, seq_sort);
+        return re_predicate(result, seq_sort);
     }
-    // stuck cases: re.derivative, variable,
-    // str.to_re if the head of the string can't be obtained,
-    // and re.reverse if not applied to a string or if the tail char
-    // of the string can't be obtained
+    // stuck cases: re().is_derivative, variable, ...
+    // and re().is_reverse if the reverse is not applied to a string
     return expr_ref(re().mk_derivative(ele, r), m());
 }
 
@@ -3006,9 +2821,6 @@ Disabled rewrite:
 */
 br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
 
-    STRACE("seq_verbose", tout << "mk_str_in_regexp: " << mk_pp(a, m())
-                               << ", " << mk_pp(b, m()) << std::endl;);
-
     if (re().is_empty(b)) {
         result = m().mk_false();
         return BR_DONE;
@@ -4295,7 +4107,6 @@ seq_rewriter::op_cache::op_cache(ast_manager& m):
 expr* seq_rewriter::op_cache::find(decl_kind op, expr* a, expr* b) {
     op_entry e(op, a, b, nullptr);
     m_table.find(e, e);
-
     return e.r;
 }
 
@@ -4311,6 +4122,5 @@ void seq_rewriter::op_cache::cleanup() {
     if (m_table.size() >= m_max_cache_size) {
         m_trail.reset();
         m_table.reset();
-        STRACE("seq_verbose", tout << "Derivative op cache reset" << std::endl;);
     }
 }
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 5fc3febb5..6435143b7 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -182,7 +182,7 @@ class seq_rewriter {
     expr_ref mk_seq_concat(expr* a, expr* b);    
 
     // Calculate derivative, memoized and enforcing a normal form
-    expr_ref is_nullable_rec(expr* r);
+    expr_ref mk_derivative(expr* ele, expr* r);
     expr_ref mk_derivative_rec(expr* ele, expr* r);
     expr_ref mk_der_op(decl_kind k, expr* a, expr* b);
     expr_ref mk_der_op_rec(decl_kind k, expr* a, expr* b);
@@ -190,12 +190,8 @@ class seq_rewriter {
     expr_ref mk_der_union(expr* a, expr* b);
     expr_ref mk_der_inter(expr* a, expr* b);
     expr_ref mk_der_compl(expr* a);
-    expr_ref mk_der_cond(expr* cond, expr* ele, sort* seq_sort);
+    expr_ref mk_der_reverse(expr* a);
 
-    bool lt_char(expr* ch1, expr* ch2);
-    bool eq_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;
     bool is_subset(expr* r1, expr* r2) const;
 
@@ -287,6 +283,7 @@ class seq_rewriter {
     class seq_util::str& str() { return u().str; }
     class seq_util::str const& str() const { return u().str; }
 
+    expr_ref is_nullable_rec(expr* r);
     void intersect(unsigned lo, unsigned hi, svector<std::pair<unsigned, unsigned>>& ranges);
 
 public:
@@ -333,9 +330,8 @@ public:
 
     void add_seqs(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_pair_vector& new_eqs);
 
-    // Expose derivative and nullability check
+    // Check for acceptance of the empty string
     expr_ref is_nullable(expr* r);
-    expr_ref mk_derivative(expr* ele, expr* r);
 
     // heuristic elimination of element from condition that comes form a derivative.
     // special case optimization for conjunctions of equalities, disequalities and ranges.