tidy

Signed-off-by: Nikolaj Bjorner <[email protected]>

src/smt/seq_regex.cpp

@@ -157,47 +157,46 @@ namespace smt {
     */
     expr_ref seq_regex::get_overapprox_regex(expr* s) {
         expr_ref s_to_re(re().mk_to_re(s), m);
-        expr_ref epsilon(re().mk_epsilon(m.get_sort(s)), m);
         expr_ref dotstar(re().mk_full_seq(m.get_sort(s_to_re)), m);
-        if (m.is_value(s)) {
-            return s_to_re;
-        }
-        else {
+        if (m.is_value(s)) 
+            s_to_re;
+
+        if (str().is_concat(s)) {
             expr_ref_vector es(m);
-            expr_ref s_approx(m);
-            if (str().is_concat(s)) {
-                str().get_concat(s, es);
-                //here it is known that es is nonempty or else s would be a value
-                expr_ref e_approx(m), last(m);
-                for (expr* e : es) {
-                    e_approx = get_overapprox_regex(e);
-                    if (!s_approx)
-                        s_approx = e_approx;
-                    else if (last != dotstar || e_approx != dotstar)
-                        s_approx = re().mk_concat(e_approx, s_approx);
-                        last = e_approx;
-                }
-                return s_approx;
-            }
-            else if (m.is_ite(s)) {
-                s_approx = get_overapprox_regex(to_app(s)->get_arg(1));
-                //if either branch approximates to .* then the result is also .*
-                if (!re().is_full_seq(s_approx)) {
-                    expr_ref r2 = get_overapprox_regex(to_app(s)->get_arg(2));
-                    if (re().is_full_seq(r2)) {
-                        s_approx = r2;
-                    }
-                    else if (s_approx != r2) {
-                        s_approx = re().mk_union(s_approx, r2);
-                    }
-                }
-                return s_approx;
-            }
-            else {
-                // TBD: other app expressions that can be approximated
-                return dotstar;
+            str().get_concat(s, es);            
+            expr_ref s_approx(m), e_approx(m), last(m);
+            for (expr* e : es) {
+                e_approx = get_overapprox_regex(e);
+                if (!s_approx)
+                    s_approx = e_approx;
+                else if (last != dotstar || e_approx != dotstar)
+                    s_approx = re().mk_concat(s_approx, e_approx);
+                last = e_approx;
             }
+            if (!s_approx)
+                s_approx = re().mk_epsilon(m.get_sort(s));
+
+            return s_approx;
+        }
+
+        expr* c = nullptr, *r1 = nullptr, *r2 = nullptr;
+        if (m.is_ite(s, c, r1, r2)) {
+            // if either branch approximates to .* then the result is also .*
+
+            expr_ref s_approx1 = get_overapprox_regex(r1);
+            if (re().is_full_seq(s_approx1))
+                return s_approx1;
+
+            expr_ref s_approx2 = get_overapprox_regex(r2);
+            if (re().is_full_seq(s_approx2)) 
+                return s_approx2;
+
+            return expr_ref(re().mk_union(s_approx1, s_approx2), m);
         }
+
+        // TBD: other app expressions that can be approximated
+        return dotstar;
+
     }
 
     /**