add str.to-int in theory_str WIP

src/ast/rewriter/str_rewriter.cpp

@@ -25,6 +25,7 @@ Notes:
 #include<map>
 #include<set>
 #include<deque>
+#include<cctype>
 
 // 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);

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);

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<builtin_name> & 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));

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;