mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

Merge branch 'develop' of github.com:/mtrberzi/z3 into develop

Browse source
This commit is contained in:
Murphy Berzish 2018-07-04 12:13:07 -04:00
parent 9826835e15 b68a38ff96
commit da41949f69
1 changed files with 43 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

44
src/smt/theory_str.cpp
View file

@ -1829,6 +1829,14 @@ namespace smt {
u.str.is_string(range1, range1val);
u.str.is_string(range2, range2val);
return zstring("[") + range1val + zstring("-") + range2val + zstring("]");
} 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("})");
} else if (u.re.is_full_seq(a_regex)) {
return zstring("(.*)");
} else if (u.re.is_full_char(a_regex)) {
@ -6644,6 +6652,7 @@ namespace smt {
ENSURE(u.is_re(re));
expr * sub1;
expr * sub2;
unsigned lo, hi;
if (u.re.is_to_re(re, sub1)) {
if (!u.str.is_string(sub1))
throw default_exception("regular expressions must be built from string literals");
@ -6663,6 +6672,9 @@ 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)) {
unsigned cx = estimate_regex_complexity(sub1);
return _qadd(lo, cx);
} else if (u.re.is_range(re, sub1, sub2)) {
SASSERT(u.str.is_string(sub1));
SASSERT(u.str.is_string(sub2));
@ -6684,6 +6696,7 @@ namespace smt {
ENSURE(u.is_re(re));
expr * sub1;
expr * sub2;
unsigned lo, hi;
if (u.re.is_to_re(re, sub1)) {
SASSERT(u.str.is_string(sub1));
zstring str;
@ -6702,7 +6715,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)) {
} else if (u.re.is_star(re, sub1) || u.re.is_plus(re, sub1) || u.re.is_loop(re, sub1, lo, hi)) {
unsigned cx = estimate_regex_complexity_under_complement(sub1);
return _qmul(2, cx);
} else if (u.re.is_range(re, sub1, sub2)) {
@ -6736,6 +6749,7 @@ namespace smt {
bool theory_str::check_regex_length_linearity_helper(expr * re, bool already_star) {
expr * sub1;
expr * sub2;
unsigned lo, hi;
if (u.re.is_to_re(re)) {
return true;
} else if (u.re.is_concat(re, sub1, sub2)) {
@ -6757,6 +6771,8 @@ 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)) {
return check_regex_length_linearity_helper(sub1, already_star);
} else {
TRACE("str", tout << "WARNING: unknown regex term " << mk_pp(re, get_manager()) << std::endl;);
UNREACHABLE(); return false;
@ -6767,6 +6783,7 @@ namespace smt {
void theory_str::check_subterm_lengths(expr * re, integer_set & lens) {
expr * sub1;
expr * sub2;
unsigned lo, hi;
if (u.re.is_to_re(re, sub1)) {
SASSERT(u.str.is_string(sub1));
zstring str;
@ -6821,6 +6838,14 @@ namespace smt {
lens.reset();
} else if (u.re.is_complement(re)) {
lens.reset();
} else if (u.re.is_loop(re, sub1, lo, hi)) {
integer_set lens_1;
check_subterm_lengths(sub1, lens_1);
for (unsigned i = lo; i <= hi; ++i) {
for (auto j : lens_1) {
lens.insert(i * j);
}
}
} else {
TRACE("str", tout << "WARNING: unknown regex term " << mk_pp(re, get_manager()) << std::endl;);
lens.reset();
@ -6842,6 +6867,7 @@ namespace smt {
ast_manager & m = get_manager();
expr * sub1;
expr * sub2;
unsigned lo, hi;
if (u.re.is_to_re(re, sub1)) {
if (!u.str.is_string(sub1))
throw default_exception("regular expressions must be built from string literals");
@ -6911,6 +6937,22 @@ namespace smt {
expr_ref retval(ctx.mk_eq_atom(lenVar, m_autil.mk_add_simplify(sum_terms)), m);
return retval;
}
} else if (u.re.is_loop(re, sub1, lo, hi)) {
expr * v1 = mk_int_var("rlen");
freeVariables.push_back(v1);
expr_ref r1 = infer_all_regex_lengths(v1, sub1, freeVariables);
expr_ref_vector v1_choices(m);
for (unsigned i = lo; i <= hi; ++i) {
rational rI(i);
expr_ref v1_i(ctx.mk_eq_atom(lenVar, m_autil.mk_mul(m_autil.mk_numeral(rI, true), v1)), m);
v1_choices.push_back(v1_i);
}
expr_ref_vector finalResult(m);
finalResult.push_back(r1);
finalResult.push_back(mk_or(v1_choices));
expr_ref retval(mk_and(finalResult), m);
SASSERT(retval);
return retval;
} else if (u.re.is_range(re, sub1, sub2)) {
SASSERT(u.str.is_string(sub1));
SASSERT(u.str.is_string(sub2));