From b0bf2f1792d871cbecd96c50f8ae4f855cc75f3f Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Sun, 6 Oct 2019 20:33:33 -0400
Subject: [PATCH] z3str3: recognize two-argument re.loop

---
 src/smt/theory_str.cpp | 22 ++++++++++++++--------
 1 file changed, 14 insertions(+), 8 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index f4ac682d7..46c60b621 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -1922,11 +1922,17 @@ namespace smt {
         } else if (u.re.is_loop(a_regex)) {
         	expr * body;
         	unsigned lo, hi;
-        	u.re.is_loop(a_regex, body, lo, hi);
-        	rational rLo(lo);
-        	rational rHi(hi);
-        	zstring bodyStr = get_std_regex_str(body);
-        	return zstring("(") + bodyStr + zstring("{") + zstring(rLo.to_string().c_str()) + zstring(",") + zstring(rHi.to_string().c_str()) + zstring("})");
+        	// There are two variants of loop: a 2-argument version and a 3-argument version.
+        	if (u.re.is_loop(a_regex, body, lo, hi)) {
+        	    rational rLo(lo);
+        	    rational rHi(hi);
+        	    zstring bodyStr = get_std_regex_str(body);
+        	    return zstring("(") + bodyStr + zstring("{") + zstring(rLo.to_string().c_str()) + zstring(",") + zstring(rHi.to_string().c_str()) + zstring("})");
+        	} else if (u.re.is_loop(a_regex, body, lo)) {
+        	    rational rLo(lo);
+        	    zstring bodyStr = get_std_regex_str(body);
+        	    return zstring("(") + bodyStr + zstring("{") + zstring(rLo.to_string().c_str()) + zstring("+") + zstring("})");
+        	}
         } else if (u.re.is_full_seq(a_regex)) {
             return zstring("(.*)");
         } else if (u.re.is_full_char(a_regex)) {
@@ -6732,7 +6738,7 @@ namespace smt {
         } else if (u.re.is_star(re, sub1) || u.re.is_plus(re, sub1)) {
             unsigned cx = estimate_regex_complexity(sub1);
             return _qmul(2, cx);
-        } else if (u.re.is_loop(re, sub1, lo, hi)) {
+        } else if (u.re.is_loop(re, sub1, lo, hi) || u.re.is_loop(re, sub1, lo)) {
         	unsigned cx = estimate_regex_complexity(sub1);
         	return _qadd(lo, cx);
         } else if (u.re.is_range(re, sub1, sub2)) {
@@ -6775,7 +6781,7 @@ namespace smt {
             unsigned cx1 = estimate_regex_complexity_under_complement(sub1);
             unsigned cx2 = estimate_regex_complexity_under_complement(sub2);
             return _qmul(cx1, cx2);
-        } else if (u.re.is_star(re, sub1) || u.re.is_plus(re, sub1) || u.re.is_loop(re, sub1, lo, hi)) {
+        } else if (u.re.is_star(re, sub1) || u.re.is_plus(re, sub1) || u.re.is_loop(re, sub1, lo, hi) || u.re.is_loop(re, sub1, lo)) {
             unsigned cx = estimate_regex_complexity_under_complement(sub1);
             return _qmul(2, cx);
         } else if (u.re.is_range(re, sub1, sub2)) {
@@ -6831,7 +6837,7 @@ namespace smt {
         } else if (u.re.is_complement(re)) {
             // TODO can we do better?
             return false;
-        } else if (u.re.is_loop(re, sub1, lo, hi)) {
+        } else if (u.re.is_loop(re, sub1, lo, hi) || u.re.is_loop(re, sub1, lo)) {
         	return check_regex_length_linearity_helper(sub1, already_star);
         } else {
             TRACE("str", tout << "WARNING: unknown regex term " << mk_pp(re, get_manager()) << std::endl;);