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

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 5ac56e02764fed7e6b80ac0af361a96892f48ca8..5dc3043af7cc1914997c1774f50efb0782508f71 100644 (file)
--- 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 ac8e5bfe74f5e56a8fd9046b57c7f07902481a06..7ada9d35046d6617e79897bd57eb30ddc4aa40d5 100644 (file)
--- 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 09f536b1572f8ecc70c0a67ea18c06a70ab0a6ca..7fbefe251e57880198901ad35c2d9fb5c46115c8 100644 (file)
--- 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 056cd9eb54c8ae6588b1b8da87640bef8b802a23..d8b20d890e115af783420c8f9755320fcecea211 100644 (file)
--- 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 d27dcfc9ea7b138aea42fd7a7dc2db3dea3bab94..d5b5d9e5575eaa1af3da4797426080fc0f479586 100644 (file)
--- 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 c3f63f8038f73eb66b73ff628277d5b26343887a..f0467507d8dce3688532a8d4752a762dff892543 100644 (file)
--- 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();