From 06f34bd42bb1297af7b2461924d96b05744649b6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 1 Aug 2020 16:54:05 -0700 Subject: [PATCH] tidy Signed-off-by: Nikolaj Bjorner --- src/smt/seq_regex.cpp | 73 +++++++++++++++++++++---------------------- 1 file changed, 36 insertions(+), 37 deletions(-) diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index f24b744bdea..76ee4595dd2 100644 --- a/src/smt/seq_regex.cpp +++ b/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; + } /**