switch to total function str.to.int: maps invalid and non-digit strings to 0

4 files changed, 8 insertions, 9 deletions

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 09f536b15..7fbefe251 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -22,8 +22,7 @@ operator STRING_STRREPL 3 "string replace"
 operator STRING_PREFIX 2 "string prefixof"
 operator STRING_SUFFIX 2 "string suffixof"
 operator STRING_ITOS 1 "integer to string"
-operator STRING_STOI 1 "string to integer (user symbol)"
-operator STRING_STOI_TOTAL 1 "string to integer (internal symbol)"
+operator STRING_STOI 1 "string to integer (total function)"
 
 #sort CHAR_TYPE \
 #    Cardinality::INTEGERS \
@@ -120,7 +119,6 @@ typerule STRING_PREFIX ::CVC4::theory::strings::StringPrefixOfTypeRule
 typerule STRING_SUFFIX ::CVC4::theory::strings::StringSuffixOfTypeRule
 typerule STRING_ITOS ::CVC4::theory::strings::StringIntToStrTypeRule
 typerule STRING_STOI ::CVC4::theory::strings::StringStrToIntTypeRule
-typerule STRING_STOI_TOTAL ::CVC4::theory::strings::StringStrToIntTypeRule
 
 typerule STRING_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule
 
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 056cd9eb5..d8b20d890 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -57,7 +57,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
     d_equalityEngine.addFunctionKind(kind::STRING_STRCTN);
     d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR_TOTAL);
     d_equalityEngine.addFunctionKind(kind::STRING_ITOS);
-    d_equalityEngine.addFunctionKind(kind::STRING_STOI_TOTAL);
+    d_equalityEngine.addFunctionKind(kind::STRING_STOI);
 
     d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
     d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
@@ -408,7 +408,7 @@ void TheoryStrings::preRegisterTerm(TNode n) {
   case kind::STRING_CONCAT:
   case kind::STRING_SUBSTR_TOTAL:
   case kind::STRING_ITOS:
-  case kind::STRING_STOI_TOTAL:
+  case kind::STRING_STOI:
 	d_equalityEngine.addTerm(n);
 	break;
   //case kind::STRING_ITOS:
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index d27dcfc9e..d5b5d9e55 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -319,7 +319,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 		} else {
 			throw LogicException("string int.to.str not supported in this release");
 		}
-	} else if( t.getKind() == kind::STRING_STOI_TOTAL ) {
+	} else if( t.getKind() == kind::STRING_STOI ) {
 		if(options::stringExp()) {
 			Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
 			Node nine = NodeManager::currentNM()->mkConst( ::CVC4::Rational(9) );
@@ -357,9 +357,10 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 			vec_n.push_back(g);
 			g = t[0].eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, z1, z2, z3) );
 			vec_n.push_back(g);
+			char ch[2];
+			ch[1] = '\0';
 			for(unsigned i=0; i<=9; i++) {
-				char ch[2];
-				ch[0] = i + '0'; ch[1] = '\0';
+				ch[0] = i + '0';
 				std::string stmp(ch);
 				g = z2.eqNode( NodeManager::currentNM()->mkConst(::CVC4::String(stmp)) ).negate();
 				vec_n.push_back(g);
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index c3f63f803..f0467507d 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -450,7 +450,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
 			std::string stmp = static_cast<std::ostringstream*>( &(std::ostringstream() << i) )->str();
 			retNode = NodeManager::currentNM()->mkConst( ::CVC4::String(stmp) );
 		}
-	} else if(node.getKind() == kind::STRING_STOI_TOTAL) {
+	} else if(node.getKind() == kind::STRING_STOI) {
 		if(node[0].isConst()) {
 			CVC4::String s = node[0].getConst<String>();
 			int rt = s.toNumber();