From 696345170410c79640f347948bc7126c41081ce4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 16 Dec 2021 20:13:29 -0800
Subject: [PATCH] na

---
 src/ast/rewriter/seq_rewriter.cpp | 141 ++++++++++++++----------------
 1 file changed, 67 insertions(+), 74 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 16c2e57c84f..12b5449eb9f 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -3380,21 +3380,20 @@ expr_ref seq_rewriter::merge_regex_sets(expr* r1, expr* r2, expr* unit,
     sort* seq_sort;
     expr_ref result(unit, m());
     expr_ref_vector prefix(m());
-    expr* a, * ar, * ar1, * b, * br, * br1;
+    expr* a, * ar1, * b,  * br1;
     VERIFY(m_util.is_re(r1, seq_sort));
     SASSERT(m_util.is_re(r2));
     SASSERT(r2->get_sort() == r1->get_sort());
     // Ordering of expressions used by merging, 0 means unordered, -1 means e1 < e2, 1 means e2 < e1
     auto compare = [&](expr* x, expr* y) {
-        expr* z;
-        unsigned int xid, yid;
+        expr* z = nullptr;
         // TODO: consider also the case of A{0,l}++B having the same id as A*++B
         // in which case return 0
         if (x == y)
             return 0;
 
-        xid = (re().is_complement(x, z) ? z->get_id() : x->get_id());
-        yid = (re().is_complement(y, z) ? z->get_id() : y->get_id());
+        unsigned xid = (re().is_complement(x, z) ? z->get_id() : x->get_id());
+        unsigned yid = (re().is_complement(y, z) ? z->get_id() : y->get_id());
         SASSERT(xid != yid);
         return (xid < yid ? -1 : 1);
     };
@@ -3406,84 +3405,78 @@ expr_ref seq_rewriter::merge_regex_sets(expr* r1, expr* r2, expr* unit,
         }
         return result;
     };
-    if (r1 == r2)
-        result = r1;
-    else if (are_complements(r1, r2))
-        // TODO: loops
-        return expr_ref(unit, m());       
-    else {
-        ar = r1;
-        br = r2;
-        while (true) {;
-            if (ar == br) 
-                return composeresult(ar);
+    expr* ar = r1;
+    expr* br = r2;
+    while (true) {        
+        if (ar == br)
+            return composeresult(ar);
 
-            if (are_complements(ar, br)) 
-                return expr_ref(unit, m());
+        if (are_complements(ar, br))
+            return expr_ref(unit, m());
 
-            if (test(br, b, br1) && !test(ar, a, ar1)) 
-                std::swap(ar, br);
-
-            if (test(br, b, br1)) {
-                VERIFY(test(ar, a, ar1));
-                if (are_complements(a, b)) 
-                    return expr_ref(unit, m());
-                switch (compare(a, b)) {
-                case 0:
-                    // a == b
-                    prefix.push_back(a);
-                    ar = ar1;
-                    br = br1;
-                    break;
-                case -1:                    
-                    // a < b
-                    prefix.push_back(a);
-                    ar = ar1;
-                    break;
-                default:
-                    // b < a
-                    prefix.push_back(b);
-                    br = br1;
-                    break;
-                }
-                continue;
-            }
+        if (test(br, b, br1) && !test(ar, a, ar1))
+            std::swap(ar, br);
 
-            if (test(ar, a, ar1)) {
-                // br is not decomposable
-                if (are_complements(a, br)) 
-                    return expr_ref(unit, m());
-                switch (compare(a, br)) {
-                case 0:
-                    // result = prefix ++ ar
-                    return composeresult(ar);
-                case -1:
-                    // a < br
-                    prefix.push_back(a);
-                    ar = ar1;
-                    break;
-                case 1:
-                    // br < a, result = prefix ++ (br) ++ ar
-                    prefix.push_back(br);
-                    return composeresult(ar);
-                default:
-                    UNREACHABLE();
-                }
-                continue;
+        // both ar, br are decomposable
+        if (test(br, b, br1)) {
+            VERIFY(test(ar, a, ar1));
+            if (are_complements(a, b))
+                return expr_ref(unit, m());
+            switch (compare(a, b)) {
+            case 0:
+                // a == b
+                prefix.push_back(a);
+                ar = ar1;
+                br = br1;
+                break;
+            case -1:
+                // a < b
+                prefix.push_back(a);
+                ar = ar1;
+                break;
+            case 1:
+                // b < a
+                prefix.push_back(b);
+                br = br1;
+                break;
+            default:
+                UNREACHABLE();
             }
+            continue;
+        }
 
-            // neither ar nor br is decomposable
-            if (compare(ar, br) == -1) 
-                std::swap(ar, br);
-            // br < ar, result = prefix ++ (br) ++ (ar) 
-            prefix.push_back(br);
-            return composeresult(ar);
+        // ar is decomposable, br is not decomposable
+        if (test(ar, a, ar1)) {            
+            if (are_complements(a, br))
+                return expr_ref(unit, m());
+            switch (compare(a, br)) {
+            case 0:
+                // result = prefix ++ ar
+                return composeresult(ar);
+            case -1:
+                // a < br
+                prefix.push_back(a);
+                ar = ar1;
+                break;
+            case 1:
+                // br < a, result = prefix ++ (br) ++ ar
+                prefix.push_back(br);
+                return composeresult(ar);
+            default:
+                UNREACHABLE();
+            }
+            continue;
         }
+
+        // neither ar nor br is decomposable
+        if (compare(ar, br) == -1)
+            std::swap(ar, br);
+        // br < ar, result = prefix ++ (br) ++ (ar) 
+        prefix.push_back(br);
+        return composeresult(ar);
     }
-    return result;
 }
 
-
 expr_ref seq_rewriter::mk_regex_reverse(expr* r) {
     expr* r1 = nullptr, * r2 = nullptr, * c = nullptr;
     unsigned lo = 0, hi = 0;