mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

fixes for re.loop in theory_str

Browse source
This commit is contained in:
Murphy Berzish 2018-05-08 14:53:02 -07:00
parent 047f6c558c
commit b68a38ff96
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)) {
SASSERT(u.str.is_string(sub1));
zstring str;
@ -6662,6 +6671,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));
@ -6683,6 +6695,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;
@ -6701,7 +6714,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)) {
@ -6735,6 +6748,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)) {
@ -6756,6 +6770,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;
@ -6766,6 +6782,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);
@ -6820,6 +6837,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();
@ -6841,6 +6866,7 @@ namespace smt {
ast_manager & m = get_manager();
expr * sub1;
expr * sub2;
unsigned lo, hi;
if (u.re.is_to_re(re, sub1)) {
SASSERT(u.str.is_string(sub1));
zstring str;
@ -6909,6 +6935,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));