mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-18 09:12:16 +00:00
Code Activity

add rewrite for theory_str rewriter RegexPlus

Browse source 
fixes regex-013.smt2
This commit is contained in:
Murphy Berzish 2016-08-31 19:22:04 -04:00
parent 5e22bc57c8
commit f9b4f21683
2 changed files with 13 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ast/rewriter/str_rewriter.cpp
View file

@ -425,6 +425,15 @@ br_status str_rewriter::mk_re_RegexIn(expr * str, expr * re, expr_ref & result)
return BR_FAILED; return BR_FAILED;
} }
br_status str_rewriter::mk_re_RegexStar(expr * re, expr_ref & result) {
if (m_strutil.is_re_RegexStar(re)) {
result = re;
return BR_REWRITE_FULL;
} else {
return BR_FAILED;
}
}
br_status str_rewriter::mk_re_RegexPlus(expr * re, expr_ref & result) { br_status str_rewriter::mk_re_RegexPlus(expr * re, expr_ref & result) {
/* /*
* Two optimizations are possible if we inspect 're'. * Two optimizations are possible if we inspect 're'.
@ -523,6 +532,9 @@ br_status str_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
case OP_RE_REGEXPLUS: case OP_RE_REGEXPLUS:
SASSERT(num_args == 1); SASSERT(num_args == 1);
return mk_re_RegexPlus(args[0], result); return mk_re_RegexPlus(args[0], result);
case OP_RE_REGEXSTAR:
SASSERT(num_args == 1);
return mk_re_RegexStar(args[0], result);
case OP_RE_REGEXCHARRANGE: case OP_RE_REGEXCHARRANGE:
SASSERT(num_args == 2); SASSERT(num_args == 2);
return mk_re_RegexCharRange(args[0], args[1], result); return mk_re_RegexCharRange(args[0], args[1], result);

1
src/ast/rewriter/str_rewriter.h
View file

@ -57,6 +57,7 @@ public:
br_status mk_re_Str2Reg(expr * str, expr_ref & result); br_status mk_re_Str2Reg(expr * str, expr_ref & result);
br_status mk_re_RegexIn(expr * str, expr * re, expr_ref & result); br_status mk_re_RegexIn(expr * str, expr * re, expr_ref & result);
br_status mk_re_RegexPlus(expr * re, expr_ref & result); br_status mk_re_RegexPlus(expr * re, expr_ref & result);
br_status mk_re_RegexStar(expr * re, expr_ref & result);
br_status mk_re_RegexCharRange(expr * start, expr * end, expr_ref & result); br_status mk_re_RegexCharRange(expr * start, expr * end, expr_ref & result);
bool reduce_eq(expr * l, expr * r, expr_ref_vector & lhs, expr_ref_vector & rhs, bool & change); bool reduce_eq(expr * l, expr * r, expr_ref_vector & lhs, expr_ref_vector & rhs, bool & change);