z3str3: recognize two-argument re.loop

Author: mtrberzi

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;);