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

6 files changed, 8 insertions, 65 deletions

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 5ac56e027..5dc3043af 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -287,7 +287,6 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::STRING_PREFIX: out << "str.prefixof "; break;
   case kind::STRING_SUFFIX: out << "str.suffixof "; break;
   case kind::STRING_ITOS: out << "int.to.str "; break;
-  case kind::STRING_STOI_TOTAL:
   case kind::STRING_STOI: out << "str.to.int "; break;
   case kind::STRING_TO_REGEXP: out << "str.to.re "; break;
   case kind::REGEXP_CONCAT: out << "re.++ "; break;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ac8e5bfe7..7ada9d350 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1613,61 +1613,6 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
 		node = NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf );
 		break;
 	  }
-	  case kind::STRING_STOI: {
-		if(d_ufS2I.isNull()) {
-			std::vector< TypeNode > argTypes;
-			argTypes.push_back(NodeManager::currentNM()->stringType());
-			d_ufS2I = NodeManager::currentNM()->mkSkolem("__ufS2I", 
-								NodeManager::currentNM()->mkFunctionType(
-									argTypes, NodeManager::currentNM()->integerType()),
-								"uf str2int",
-								NodeManager::SKOLEM_EXACT_NAME);
-		}
-		Node cond;
-		if(n[0].isConst()) {
-			CVC4::String s = n[0].getConst<String>();
-			if(s.isNumber()) {
-				cond = NodeManager::currentNM()->mkConst( false );
-			} else {
-				cond = NodeManager::currentNM()->mkConst( true );
-			}
-		} else {
-			Node cc1 = n[0].eqNode(nm->mkConst(::CVC4::String("")));
-			Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
-			Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
-			Node b1 = NodeManager::currentNM()->mkBoundVar("x", NodeManager::currentNM()->integerType());
-			Node z1 = NodeManager::currentNM()->mkBoundVar("z1", NodeManager::currentNM()->stringType());
-			Node z2 = NodeManager::currentNM()->mkBoundVar("z2", NodeManager::currentNM()->stringType());
-			Node z3 = NodeManager::currentNM()->mkBoundVar("z3", NodeManager::currentNM()->stringType());
-			Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1, z1, z2, z3);
-			std::vector< Node > vec_n;
-			Node g = NodeManager::currentNM()->mkNode(kind::GEQ, b1, zero);
-			vec_n.push_back(g);
-			g = NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, n[0]), b1);
-			vec_n.push_back(g);
-			g = b1.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, z1) );
-			vec_n.push_back(g);
-			g = one.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, z2) );
-			vec_n.push_back(g);
-			g = n[0].eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, z1, z2, z3) );
-			vec_n.push_back(g);
-			for(unsigned i=0; i<=9; i++) {
-				char ch[2];
-				ch[0] = i + '0'; ch[1] = '\0';
-				std::string stmp(ch);
-				g = z2.eqNode( nm->mkConst(::CVC4::String(stmp)) ).negate();
-				vec_n.push_back(g);
-			}
-			Node cc2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, vec_n));
-			cc2 = NodeManager::currentNM()->mkNode(kind::EXISTS, b1v, cc2);
-			cond = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2));
-		}
-		Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_STOI_TOTAL, n[0]);
-		Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufS2I, n[0]);
-		node = NodeManager::currentNM()->mkNode( kind::ITE, cond, uf, totalf );
-
-		break;
-	  }
       case kind::DIVISION: {
         // partial function: division
         if(d_divByZero.isNull()) {
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();