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

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

* Temporarily disable regression.

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index efdd328a4db66203d3da419856de568028579006..6cc5c29a40e04dc18fa054a7dcfdd24c4df58cda 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -226,10 +226,6 @@ tokens {
   STRING_SUFFIXOF_TOK = 'SUFFIXOF';
   STRING_STOI_TOK = 'STRING_TO_INTEGER';
   STRING_ITOS_TOK = 'INTEGER_TO_STRING';
-  STRING_U16TOS_TOK = 'UINT16_TO_STRING';
-  STRING_STOU16_TOK = 'STRING_TO_UINT16';
-  STRING_U32TOS_TOK = 'UINT32_TO_STRING';
-  STRING_STOU32_TOK = 'STRING_TO_UINT32';
   //Regular expressions (TODO)
   //STRING_IN_REGEXP_TOK
   //STRING_TO_REGEXP_TOK
@@ -1990,15 +1986,7 @@ stringTerm[CVC4::Expr& f]
   | STRING_STOI_TOK LPAREN formula[f] RPAREN
     { f = MK_EXPR(CVC4::kind::STRING_STOI, f); }
   | STRING_ITOS_TOK LPAREN formula[f] RPAREN
-    { f = MK_EXPR(CVC4::kind::STRING_ITOS, f); }
-  | STRING_U16TOS_TOK LPAREN formula[f] RPAREN
-    { f = MK_EXPR(CVC4::kind::STRING_U16TOS, f); }
-  | STRING_STOU16_TOK LPAREN formula[f] RPAREN
-    { f = MK_EXPR(CVC4::kind::STRING_STOU16, f); }
-  | STRING_U32TOS_TOK LPAREN formula[f] RPAREN
-    { f = MK_EXPR(CVC4::kind::STRING_U32TOS, f); }
-  | STRING_STOU32_TOK LPAREN formula[f] RPAREN
-    { f = MK_EXPR(CVC4::kind::STRING_STOU32, f); }    
+    { f = MK_EXPR(CVC4::kind::STRING_ITOS, f); }   
 
     /* string literal */
   | str[s]

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index de3c9aa627e0d952055eb6033ba4a51377ef4f54..aeabdbac26580536b3c25420d1e11eb9b9c1581c 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -120,10 +120,6 @@ void Smt2::addStringOperators() {
   addOperator(kind::STRING_SUFFIX, "str.suffixof" );
   addOperator(kind::STRING_ITOS, "int.to.str" );
   addOperator(kind::STRING_STOI, "str.to.int" );
-  addOperator(kind::STRING_U16TOS, "u16.to.str" );
-  addOperator(kind::STRING_STOU16, "str.to.u16" );
-  addOperator(kind::STRING_U32TOS, "u32.to.str" );
-  addOperator(kind::STRING_STOU32, "str.to.u32" );
   addOperator(kind::STRING_IN_REGEXP, "str.in.re");
   addOperator(kind::STRING_TO_REGEXP, "str.to.re");
   addOperator(kind::REGEXP_CONCAT, "re.++");

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index aa9c17e5a13eac1bccc035c24802db8d2b0f5a7e..2f2a6ff18a0859b6d4cf85f208fbd5ce6e469882 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -451,10 +451,6 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::STRING_SUFFIX: out << "str.suffixof "; break;
   case kind::STRING_ITOS: out << "int.to.str "; break;
   case kind::STRING_STOI: out << "str.to.int "; break;
-  case kind::STRING_U16TOS: out << "u16.to.str "; break;
-  case kind::STRING_STOU16: out << "str.to.u16 "; break;
-  case kind::STRING_U32TOS: out << "u32.to.str "; break;
-  case kind::STRING_STOU32: out << "str.to.u32 "; break;
   case kind::STRING_TO_REGEXP: out << "str.to.re "; break;
   case kind::REGEXP_CONCAT: out << "re.++ "; break;
   case kind::REGEXP_UNION: out << "re.union "; break;
@@ -939,10 +935,6 @@ static string smtKindString(Kind k) throw() {
   case kind::STRING_SUFFIX: return "str.suffixof" ;
   case kind::STRING_ITOS: return "int.to.str" ;
   case kind::STRING_STOI: return "str.to.int" ;
-  case kind::STRING_U16TOS: return "u16.to.str" ;
-  case kind::STRING_STOU16: return "str.to.u16" ;
-  case kind::STRING_U32TOS: return "u32.to.str" ;
-  case kind::STRING_STOU32: return "str.to.u32" ;
   case kind::STRING_IN_REGEXP: return "str.in.re";
   case kind::STRING_TO_REGEXP: return "str.to.re";
   case kind::REGEXP_CONCAT: return "re.++";

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 3cdff9cbaf810c4e9f5f6fde06deafa9dcd5d4a7..3a5fd59e9d0cb82e11cc10bc60b80763bb04b3b5 100644 (file)
--- 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 babf77a74fd712ed85fdc97a34939c16bd5b3840..412cc727d71b88e66f4af09d70710cdf9f5e791a 100644 (file)
--- 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 ca49727ef5a55a0d8955c3d9425f76a0f19dddb7..1a61cb44933edca29e92e5c9d8753b746b4e1a22 100644 (file)
--- 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 de9b60d87e5cd0c8a93b05ca09014d87c0d004a0..d475305fb73965b714cf679c034699bdad75c4ea 100644 (file)
--- 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));

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index c47c10de0c930d7f993bc68b82783733c92f69e6..8f4e3dc4b677f4a24317c1075166fa70f049cf7b 100644 (file)
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -72,7 +72,6 @@ TESTS = \
   bug686dd.smt2 \
   idof-handg.smt2 \
   fmf001.smt2 \
-  type002.smt2 \
   crash-1019.smt2 \
   norn-31.smt2 \
   strings-native-simple.cvc \
@@ -100,6 +99,7 @@ EXTRA_DIST +=
 
 #norn-dis-0707-3.smt2
 #norn-ab.smt2
+#type002.smt2
 
 # synonyms for "check"
 .PHONY: regress regress0 test

diff --git a/test/regress/regress0/strings/type002.smt2 b/test/regress/regress0/strings/type002.smt2
index 296057a76ea861b902701746285e3b539997be32..0df0f20b0cd2fa7bc83d773eb55fcd8f55ea728e 100644 (file)
--- a/test/regress/regress0/strings/type002.smt2
+++ b/test/regress/regress0/strings/type002.smt2
@@ -8,11 +8,11 @@
 (declare-fun i () Int)
 
 (assert (>= i 420))
-(assert (= x (u16.to.str i)))
+(assert (= x (int.to.str i)))
 (assert (= x (str.++ y "0" z)))
 (assert (not (= y "")))
 (assert (not (= z "")))
 
 
 
-(check-sat)
\ No newline at end of file
+(check-sat)