diff --git a/src/ast/rewriter/str_rewriter.cpp b/src/ast/rewriter/str_rewriter.cpp index 015898a64..db3885f28 100644 --- a/src/ast/rewriter/str_rewriter.cpp +++ b/src/ast/rewriter/str_rewriter.cpp @@ -25,6 +25,7 @@ Notes: #include #include #include +#include // Convert a regular expression to an e-NFA using Thompson's construction void nfa::convert_re(expr * e, unsigned & start, unsigned & end, str_util & m_strutil) { @@ -374,6 +375,41 @@ br_status str_rewriter::mk_str_Replace(expr * base, expr * source, expr * target } } +br_status str_rewriter::mk_str_to_int(expr * arg0, expr_ref & result) { + TRACE("t_str_rw", tout << "rewrite (str.to-int " << mk_pp(arg0, m()) << ")" << std::endl;); + + if (m_strutil.is_string(arg0)) { + std::string str = m_strutil.get_string_constant_value(arg0); + if (str.length() == 0) { + result = m_autil.mk_numeral(rational::zero(), true); + return BR_DONE; + } + + // interpret str as a natural number and rewrite to the corresponding integer. + // if this is not valid, rewrite to -1 + // TODO leading zeroes? + rational convertedRepresentation(0); + rational ten(10); + for (unsigned i = 0; i < str.length(); ++i) { + char digit = str.at(i); + if (isdigit((int)digit)) { + std::string sDigit(1, digit); + int val = atoi(sDigit.c_str()); + convertedRepresentation = (ten * convertedRepresentation) + rational(val); + } else { + // not a digit, invalid + TRACE("t_str_rw", tout << "str.to-int argument contains non-digit character '" << digit << "'" << std::endl;); + convertedRepresentation = rational::minus_one(); + break; + } + } + result = m_autil.mk_numeral(convertedRepresentation, true); + 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; @@ -520,6 +556,9 @@ br_status str_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_STR_REPLACE: SASSERT(num_args == 3); return mk_str_Replace(args[0], args[1], args[2], result); + case OP_STR_STR2INT: + SASSERT(num_args == 1); + return mk_str_to_int(args[0], result); case OP_STR_SUBSTR: SASSERT(num_args == 3); return mk_str_Substr(args[0], args[1], args[2], result); diff --git a/src/ast/rewriter/str_rewriter.h b/src/ast/rewriter/str_rewriter.h index d147e82e8..10898eae7 100644 --- a/src/ast/rewriter/str_rewriter.h +++ b/src/ast/rewriter/str_rewriter.h @@ -53,6 +53,7 @@ public: br_status mk_str_LastIndexof(expr * haystack, expr * needle, expr_ref & result); 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_re_Str2Reg(expr * str, expr_ref & result); br_status mk_re_RegexIn(expr * str, expr * re, expr_ref & result); diff --git a/src/ast/str_decl_plugin.cpp b/src/ast/str_decl_plugin.cpp index aa12e5946..e8455ffbd 100644 --- a/src/ast/str_decl_plugin.cpp +++ b/src/ast/str_decl_plugin.cpp @@ -36,6 +36,7 @@ str_decl_plugin::str_decl_plugin(): m_lastindexof_decl(0), m_substr_decl(0), m_replace_decl(0), + m_str2int_decl(0), m_re_str2regex_decl(0), m_re_regexin_decl(0), m_re_regexconcat_decl(0), @@ -67,6 +68,7 @@ void str_decl_plugin::finalize(void) { DEC_REF(m_lastindexof_decl); DEC_REF(m_substr_decl); DEC_REF(m_replace_decl); + DEC_REF(m_str2int_decl); DEC_REF(m_re_str2regex_decl); DEC_REF(m_re_regexin_decl); DEC_REF(m_re_regexconcat_decl); @@ -145,6 +147,9 @@ void str_decl_plugin::set_manager(ast_manager * m, family_id id) { m_manager->inc_ref(m_replace_decl); } + m_str2int_decl = m->mk_func_decl(symbol("str.to-int"), s, i, func_decl_info(id, OP_STR_STR2INT)); + m_manager->inc_ref(m_str2int_decl); + m_re_str2regex_decl = m->mk_func_decl(symbol("Str2Reg"), s, re, func_decl_info(id, OP_RE_STR2REGEX)); m_manager->inc_ref(m_re_str2regex_decl); @@ -196,6 +201,7 @@ func_decl * str_decl_plugin::mk_func_decl(decl_kind k) { case OP_STR_LASTINDEXOF: return m_lastindexof_decl; case OP_STR_SUBSTR: return m_substr_decl; case OP_STR_REPLACE: return m_replace_decl; + case OP_STR_STR2INT: return m_str2int_decl; case OP_RE_STR2REGEX: return m_re_str2regex_decl; case OP_RE_REGEXIN: return m_re_regexin_decl; case OP_RE_REGEXCONCAT: return m_re_regexconcat_decl; @@ -269,6 +275,7 @@ void str_decl_plugin::get_op_names(svector & op_names, symbol cons op_names.push_back(builtin_name("LastIndexof", OP_STR_LASTINDEXOF)); op_names.push_back(builtin_name("Substring", OP_STR_SUBSTR)); op_names.push_back(builtin_name("Replace", OP_STR_REPLACE)); + op_names.push_back(builtin_name("str.to-int", OP_STR_STR2INT)); op_names.push_back(builtin_name("Str2Reg", OP_RE_STR2REGEX)); op_names.push_back(builtin_name("RegexIn", OP_RE_REGEXIN)); op_names.push_back(builtin_name("RegexConcat", OP_RE_REGEXCONCAT)); diff --git a/src/ast/str_decl_plugin.h b/src/ast/str_decl_plugin.h index aa8204459..ba2b4f751 100644 --- a/src/ast/str_decl_plugin.h +++ b/src/ast/str_decl_plugin.h @@ -41,6 +41,8 @@ enum str_op_kind { OP_STR_LASTINDEXOF, OP_STR_SUBSTR, OP_STR_REPLACE, + // string-integer conversion + OP_STR_STR2INT, // regular expression operators OP_RE_STR2REGEX, OP_RE_REGEXIN, @@ -73,6 +75,7 @@ protected: func_decl * m_lastindexof_decl; func_decl * m_substr_decl; func_decl * m_replace_decl; + func_decl * m_str2int_decl; func_decl * m_re_str2regex_decl; func_decl * m_re_regexin_decl;