Remove support for conversions between uint32/uint16 and string. (#1069)

* Remove support for conversions between uint32/uint16 and string.

* Temporarily disable regression.

4 files changed, 12 insertions, 75 deletions

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 3cdff9cba..3a5fd59e9 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -24,10 +24,6 @@ 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 (total function)"
-operator STRING_U16TOS 1 "uint16 to string"
-operator STRING_STOU16 1 "string to uint16"
-operator STRING_U32TOS 1 "uint32 to string"
-operator STRING_STOU32 1 "string to uint32"
 
 #sort CHAR_TYPE \
 #    Cardinality::INTEGERS \
@@ -114,10 +110,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_U16TOS ::CVC4::theory::strings::StringIntToStrTypeRule
-typerule STRING_STOU16 ::CVC4::theory::strings::StringStrToIntTypeRule
-typerule STRING_U32TOS ::CVC4::theory::strings::StringIntToStrTypeRule
-typerule STRING_STOU32 ::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 babf77a74..412cc727d 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -100,11 +100,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u,
   getExtTheory()->addFunctionKind(kind::STRING_SUBSTR);
   getExtTheory()->addFunctionKind(kind::STRING_STRIDOF);
   getExtTheory()->addFunctionKind(kind::STRING_ITOS);
-  getExtTheory()->addFunctionKind(kind::STRING_U16TOS);
-  getExtTheory()->addFunctionKind(kind::STRING_U32TOS);
   getExtTheory()->addFunctionKind(kind::STRING_STOI);
-  getExtTheory()->addFunctionKind(kind::STRING_STOU16);
-  getExtTheory()->addFunctionKind(kind::STRING_STOU32);
   getExtTheory()->addFunctionKind(kind::STRING_STRREPL);
   getExtTheory()->addFunctionKind(kind::STRING_STRCTN);
   getExtTheory()->addFunctionKind(kind::STRING_IN_REGEXP);
@@ -118,10 +114,6 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u,
     d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR);
     d_equalityEngine.addFunctionKind(kind::STRING_ITOS);
     d_equalityEngine.addFunctionKind(kind::STRING_STOI);
-    d_equalityEngine.addFunctionKind(kind::STRING_U16TOS);
-    d_equalityEngine.addFunctionKind(kind::STRING_STOU16);
-    d_equalityEngine.addFunctionKind(kind::STRING_U32TOS);
-    d_equalityEngine.addFunctionKind(kind::STRING_STOU32);
     d_equalityEngine.addFunctionKind(kind::STRING_STRIDOF);
     d_equalityEngine.addFunctionKind(kind::STRING_STRREPL);
   }
@@ -410,7 +402,7 @@ int TheoryStrings::getReduction( int effort, Node n, Node& nr ) {
           return 1;
         }else{
           // for STRING_SUBSTR, STRING_STRCTN with pol=-1,
-          //     STRING_STRIDOF, STRING_ITOS, STRING_U16TOS, STRING_U32TOS, STRING_STOI, STRING_STOU16, STRING_STOU32, STRING_STRREPL
+          //     STRING_STRIDOF, STRING_ITOS, STRING_STOI, STRING_STRREPL
           std::vector< Node > new_nodes;
           Node res = d_preproc.simplify( n, new_nodes );
           Assert( res!=n );
@@ -604,8 +596,7 @@ void TheoryStrings::preRegisterTerm(TNode n) {
     //check for logic exceptions
     if( !options::stringExp() ){
       if( n.getKind()==kind::STRING_STRIDOF ||
-          n.getKind() == kind::STRING_ITOS || n.getKind() == kind::STRING_U16TOS || n.getKind() == kind::STRING_U32TOS ||
-          n.getKind() == kind::STRING_STOI || n.getKind() == kind::STRING_STOU16 || n.getKind() == kind::STRING_STOU32 ||
+          n.getKind() == kind::STRING_ITOS || n.getKind() == kind::STRING_STOI ||
           n.getKind() == kind::STRING_STRREPL || n.getKind() == kind::STRING_STRCTN ){
         std::stringstream ss;
         ss << "Term of kind " << n.getKind() << " not supported in default mode, try --strings-exp";
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index ca49727ef..1a61cb449 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -152,7 +152,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     Node rr = NodeManager::currentNM()->mkNode( kind::ITE, cond, left, right );
     new_nodes.push_back( rr );
     retNode = skk;
-  } else if( t.getKind() == kind::STRING_ITOS || t.getKind() == kind::STRING_U16TOS || t.getKind() == kind::STRING_U32TOS ) {
+  } else if( t.getKind() == kind::STRING_ITOS ) {
     //Node num = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE,
     //        NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero),
     //        t[0], NodeManager::currentNM()->mkNode(kind::UMINUS, t[0])));
@@ -166,15 +166,6 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, pret);
 
     Node nonneg = NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero);
-    if(t.getKind()==kind::STRING_U16TOS) {
-      nonneg = NodeManager::currentNM()->mkNode(kind::AND, nonneg, NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(UINT16_MAX) ), t[0]));
-      Node lencond = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(5) ), lenp);
-      new_nodes.push_back(lencond);
-    } else if(t.getKind()==kind::STRING_U32TOS) {
-      nonneg = NodeManager::currentNM()->mkNode(kind::AND, nonneg, NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(UINT32_MAX) ), t[0]));
-      Node lencond = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) ), lenp);
-      new_nodes.push_back(lencond);
-    }
 
     Node lem = NodeManager::currentNM()->mkNode(kind::EQUAL, nonneg.negate(),
       pret.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") ))//lenp.eqNode(d_zero)
@@ -266,7 +257,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
               NodeManager::currentNM()->mkConst(::CVC4::String("-")), pret))));
     new_nodes.push_back( conc );*/
     retNode = pret;
-  } else if( t.getKind() == kind::STRING_STOI || t.getKind() == kind::STRING_STOU16 || t.getKind() == kind::STRING_STOU32 ) {
+  } else if( t.getKind() == kind::STRING_STOI ) {
     Node str = t[0];
     Node pret;
     if( options::stringUfReduct() ){
@@ -304,13 +295,6 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
       t[0].eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("0"))),
       t.eqNode(d_zero));
     new_nodes.push_back(lem);*/
-    if(t.getKind()==kind::STRING_U16TOS) {
-      lem = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst(::CVC4::String("5")), lenp);
-      new_nodes.push_back(lem);
-    } else if(t.getKind()==kind::STRING_U32TOS) {
-      lem = NodeManager::currentNM()->mkNode(kind::GEQ, NodeManager::currentNM()->mkConst(::CVC4::String("9")), lenp);
-      new_nodes.push_back(lem);
-    }
     //cc1
     Node cc1 = str.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("")));
     //cc1 = NodeManager::currentNM()->mkNode(kind::AND, ufP0.eqNode(negone), cc1);
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index de9b60d87..d475305fb 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1167,57 +1167,27 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
             node[0].eqNode(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, node[1],
                     NodeManager::currentNM()->mkNode(kind::MINUS, lent, lens), lens)));
     }
-  }else if(node.getKind() == kind::STRING_ITOS || node.getKind() == kind::STRING_U16TOS || node.getKind() == kind::STRING_U32TOS) {
+  }else if(node.getKind() == kind::STRING_ITOS) {
     if(node[0].isConst()) {
-      bool flag = false;
-      std::string stmp = node[0].getConst<Rational>().getNumerator().toString();
-      if(node.getKind() == kind::STRING_U16TOS) {
-        CVC4::Rational r1(UINT16_MAX);
-        CVC4::Rational r2 = node[0].getConst<Rational>();
-        if(r2>r1) {
-          flag = true;
-        }
-      } else if(node.getKind() == kind::STRING_U32TOS) {
-        CVC4::Rational r1(UINT32_MAX);
-        CVC4::Rational r2 = node[0].getConst<Rational>();
-        if(r2>r1) {
-          flag = true;
-        }
-      }
-      //std::string stmp = static_cast<std::ostringstream*>( &(std::ostringstream() << node[0]) )->str();
-      if(flag || stmp[0] == '-') {
+      if( node[0].getConst<Rational>().sgn()==-1 ){
         retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
-      } else {
+      }else{
+        std::string stmp = node[0].getConst<Rational>().getNumerator().toString();
+        Assert(stmp[0] != '-');
         retNode = NodeManager::currentNM()->mkConst( ::CVC4::String(stmp) );
       }
     }
-  }else if(node.getKind() == kind::STRING_STOI || node.getKind() == kind::STRING_STOU16 || node.getKind() == kind::STRING_STOU32) {
+  }else if(node.getKind() == kind::STRING_STOI) {
     if(node[0].isConst()) {
       CVC4::String s = node[0].getConst<String>();
       if(s.isNumber()) {
         std::string stmp = s.toString();
+        //TODO: leading zeros : when smt2 standard for strings is set, uncomment this if applicable
         //if(stmp[0] == '0' && stmp.size() != 1) {
-          //TODO: leading zeros
           //retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(-1));
         //} else {
-          bool flag = false;
           CVC4::Rational r2(stmp.c_str());
-          if(node.getKind() == kind::STRING_U16TOS) {
-            CVC4::Rational r1(UINT16_MAX);
-            if(r2>r1) {
-              flag = true;
-            }
-          } else if(node.getKind() == kind::STRING_U32TOS) {
-            CVC4::Rational r1(UINT32_MAX);
-            if(r2>r1) {
-              flag = true;
-            }
-          }
-          if(flag) {
-            retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(-1));
-          } else {
-            retNode = NodeManager::currentNM()->mkConst( r2 );
-          }
+          retNode = NodeManager::currentNM()->mkConst( r2 );
         //}
       } else {
         retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(-1));