mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-05 07:23:58 +00:00
Code Activity

add str.from-int in theory_str rewriter

Browse source
This commit is contained in:
Murphy Berzish 2016-11-09 15:54:22 -05:00
parent 4aa2d965b3
commit fff1fadf3b
4 changed files with 32 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -410,6 +410,25 @@ br_status str_rewriter::mk_str_to_int(expr * arg0, expr_ref & result) {
}
br_status str_rewriter::mk_str_from_int(expr * arg0, expr_ref & result) {
TRACE("t_str_rw", tout << "rewrite (str.from-int " << mk_pp(arg0, m()) << ")" << std::endl;);
rational arg0Int;
if (m_autil.is_numeral(arg0, arg0Int)) {
// (str.from-int N) with N non-negative is the corresponding string in decimal notation.
// otherwise it is the empty string
if (arg0Int.is_nonneg()) {
std::string str = arg0Int.to_string();
result = m_strutil.mk_string(str);
TRACE("t_str_rw", tout << "convert non-negative integer constant to " << str << std::endl;);
} else {
result = m_strutil.mk_string("");
TRACE("t_str_rw", tout << "convert invalid integer constant to empty string" << std::endl;);
}
return BR_DONE;
}
return BR_FAILED;
}
br_status str_rewriter::mk_str_Substr(expr * base, expr * start, expr * len, expr_ref & result) {
TRACE("t_str_rw", tout << "rewrite (Substr " << mk_pp(base, m()) << " " << mk_pp(start, m()) << " " << mk_pp(len, m()) << ")" << std::endl;);
rational startVal, lenVal;
@ -559,6 +578,9 @@ br_status str_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
case OP_STR_STR2INT:
SASSERT(num_args == 1);
return mk_str_to_int(args[0], result);
case OP_STR_INT2STR:
SASSERT(num_args == 1);
return mk_str_from_int(args[0], result);
case OP_STR_SUBSTR:
SASSERT(num_args == 3);
return mk_str_Substr(args[0], args[1], args[2], result);

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

@ -54,6 +54,7 @@ public:
br_status mk_str_Replace(expr * base, expr * source, expr * target, expr_ref & result);
br_status mk_str_Substr(expr * base, expr * start, expr * len, expr_ref & result);
br_status mk_str_to_int(expr * arg0, expr_ref & result);
br_status mk_str_from_int(expr * arg0, 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);