add str to u16/u32, and u16/u32 to str

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 518c30e81e403ff3fb34e708def2b81cdc777776..f030d6de03febe83bb079e1a3ed12536a93483a8 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1337,6 +1337,10 @@ builtinOp[CVC4::Kind& kind]
   | STRSUFF_TOK    { $kind = CVC4::kind::STRING_SUFFIX; }
   | STRITOS_TOK    { $kind = CVC4::kind::STRING_ITOS; }
   | STRSTOI_TOK    { $kind = CVC4::kind::STRING_STOI; }
+  | STRU16TOS_TOK    { $kind = CVC4::kind::STRING_U16TOS; }
+  | STRSTOU16_TOK    { $kind = CVC4::kind::STRING_STOU16; }
+  | STRU32TOS_TOK    { $kind = CVC4::kind::STRING_U32TOS; }
+  | STRSTOU32_TOK    { $kind = CVC4::kind::STRING_STOU32; }
   | STRINRE_TOK    { $kind = CVC4::kind::STRING_IN_REGEXP; }
   | STRTORE_TOK    { $kind = CVC4::kind::STRING_TO_REGEXP; }
   | RECON_TOK      { $kind = CVC4::kind::REGEXP_CONCAT; }
@@ -1713,6 +1717,10 @@ STRPREF_TOK : 'str.prefixof' ;
 STRSUFF_TOK : 'str.suffixof' ;
 STRITOS_TOK : 'int.to.str' ;
 STRSTOI_TOK : 'str.to.int' ;
+STRU16TOS_TOK : 'u16.to.str' ;
+STRSTOU16_TOK : 'str.to.u16' ;
+STRU32TOS_TOK : 'u32.to.str' ;
+STRSTOU32_TOK : 'str.to.u32' ;
 STRINRE_TOK : 'str.in.re';
 STRTORE_TOK : 'str.to.re';
 RECON_TOK : 're.++';

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 4063193399f57c3c8e69c348451b60cfe19e3032..c25b8980f2f760d516dd547358c969b80c842b7d 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -339,6 +339,10 @@ 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;

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 67b60fdfea64c83f1034e6c8097ba345d1da7ede..48e9957d4f811da5f1a900df6bc7178958610c9a 100644 (file)
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -23,6 +23,10 @@ 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 \
@@ -106,6 +110,10 @@ 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 9ed52e94ad619f420dfde972f1c8617cbd0c78f2..f2172071de80a594319ac56274ed7626fc8ff558 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -72,6 +72,10 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
     d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR_TOTAL);
     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_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
     d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index b2988d54a920a6d2c818cd291539a4cf119c822f..6981a2a33754e3a7c6c41dda6e7061b1385b87a9 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -237,19 +237,28 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                } else {
                        throw LogicException("string indexof not supported in default mode, try --string-exp");
                }
-       } else if( t.getKind() == kind::STRING_ITOS ) {
+       } else if( t.getKind() == kind::STRING_ITOS || t.getKind() == kind::STRING_U16TOS || t.getKind() == kind::STRING_U32TOS ) {
                if(options::stringExp()) {
                        //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])));
                        Node num = t[0];
-                       Node pret = t;//NodeManager::currentNM()->mkNode(kind::STRING_ITOS, num);
+                       Node pret = NodeManager::currentNM()->mkNode(kind::STRING_ITOS, num);
                        Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, pret);
 
                        Node nonneg = NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero);
-                       Node lem = NodeManager::currentNM()->mkNode(kind::ITE, nonneg,
-                               NodeManager::currentNM()->mkNode(kind::GT, lenp, d_zero),
-                               t.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") ))//lenp.eqNode(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(65536) ), 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(4294967296) ), 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::IFF, nonneg.negate(),
+                               pret.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") ))//lenp.eqNode(d_zero)
                                );
                        new_nodes.push_back(lem);
 
@@ -338,13 +347,20 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                                                                NodeManager::currentNM()->mkConst(::CVC4::String("-")), pret))));
                        new_nodes.push_back( conc );*/
 
-                       d_cache[t] = t;
-                       retNode = t;
+                       d_cache[t] = pret;
+                       if(t != pret) {
+                               d_cache[pret] = pret;
+                       }
+                       retNode = pret;
                } else {
                        throw LogicException("string int.to.str not supported in default mode, try --string-exp");
                }
-       } else if( t.getKind() == kind::STRING_STOI ) {
+       } else if( t.getKind() == kind::STRING_STOI || t.getKind() == kind::STRING_STOU16 || t.getKind() == kind::STRING_STOU32 ) {
                if(options::stringExp()) {
+                       Node str = t[0];
+                       Node pret = NodeManager::currentNM()->mkNode(kind::STRING_STOI, str);
+                       Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, str);
+
                        Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
                        Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
                        Node nine = NodeManager::currentNM()->mkConst( ::CVC4::Rational(9) );
@@ -361,24 +377,35 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                                                                "uf type conv M");
 
                        Node ufP0 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, d_zero);
-                       new_nodes.push_back(t.eqNode(ufP0));
+                       new_nodes.push_back(pret.eqNode(ufP0));
                        //lemma
                        Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES,
-                               t[0].eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(""))),
-                               t.eqNode(negone));
+                               str.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(""))),
+                               pret.eqNode(negone));
                        new_nodes.push_back(lem);
                        /*lem = NodeManager::currentNM()->mkNode(kind::IFF,
                                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::IMPLIES,
+                               NodeManager::currentNM()->mkNode(kind::GEQ, lenp, NodeManager::currentNM()->mkConst(::CVC4::String("5"))),
+                               pret.eqNode(negone));
+                               new_nodes.push_back(lem);
+                       } else if(t.getKind()==kind::STRING_U32TOS) {
+                               lem = NodeManager::currentNM()->mkNode(kind::IMPLIES,
+                               NodeManager::currentNM()->mkNode(kind::GEQ, lenp, NodeManager::currentNM()->mkConst(::CVC4::String("10"))),
+                               pret.eqNode(negone));
+                               new_nodes.push_back(lem);
+                       }
                        //cc1
                        Node cc1 = t[0].eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("")));
                        //cc1 = NodeManager::currentNM()->mkNode(kind::AND, ufP0.eqNode(negone), cc1);
                        //cc2
                        std::vector< Node > vec_n;
                        Node z1 = NodeManager::currentNM()->mkSkolem("z1_$$", NodeManager::currentNM()->stringType());
-                       Node z2 = NodeManager::currentNM()->mkSkolem("z1_$$", NodeManager::currentNM()->stringType());
-                       Node z3 = NodeManager::currentNM()->mkSkolem("z1_$$", NodeManager::currentNM()->stringType());
+                       Node z2 = NodeManager::currentNM()->mkSkolem("z2_$$", NodeManager::currentNM()->stringType());
+                       Node z3 = NodeManager::currentNM()->mkSkolem("z3_$$", NodeManager::currentNM()->stringType());
                        Node g = one.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, z2) );
                        vec_n.push_back(g);
                        g = t[0].eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, z1, z2, z3) );
@@ -397,7 +424,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                        Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2);
                        Node g2 = NodeManager::currentNM()->mkNode(kind::AND,
                                                NodeManager::currentNM()->mkNode(kind::GEQ, b2, d_zero),
-                                               NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, t[0]), b2));
+                                               NodeManager::currentNM()->mkNode(kind::GT, pret, b2));
                        Node ufx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, b2);
                        Node ufx1 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, NodeManager::currentNM()->mkNode(kind::MINUS,b2,one));
                        Node ufMx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, b2);
@@ -457,8 +484,12 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                        Node conc = NodeManager::currentNM()->mkNode(kind::ITE, ufP0.eqNode(negone),
                                                        NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2), cc3);
                        new_nodes.push_back( conc );
-                       d_cache[t] = t;
-                       retNode = t;
+
+                       d_cache[t] = pret;
+                       if(t != pret) {
+                               d_cache[pret] = pret;
+                       }
+                       retNode = pret;
                } else {
                        throw LogicException("string int.to.str not supported in default mode, try --string-exp");
                }

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 42962308d925b2d3eca80fd380ddb604ad87b3e4..8a603e6df62962b72e2b2da30d8fe859cf436a0c 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -476,17 +476,31 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
                                                node[0].eqNode(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[1],
                                                                                NodeManager::currentNM()->mkNode(kind::MINUS, lent, lens), lens)));
                }
-       } else if(node.getKind() == kind::STRING_ITOS) {
+       } else if(node.getKind() == kind::STRING_ITOS || node.getKind() == kind::STRING_U16TOS || node.getKind() == kind::STRING_U32TOS) {
                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(65536);
+                               CVC4::Rational r2 = node[0].getConst<Rational>();
+                               if(r2>r1) {
+                                       flag = true;
+                               }
+                       } else if(node.getKind() == kind::STRING_U32TOS) {
+                               CVC4::Rational r1(4294967296);
+                               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(stmp[0] == '-') {
+                       if(flag || stmp[0] == '-') {
                                retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
                        } else {
                                retNode = NodeManager::currentNM()->mkConst( ::CVC4::String(stmp) );
                        }
                }
-       } else if(node.getKind() == kind::STRING_STOI) {
+       } else if(node.getKind() == kind::STRING_STOI || node.getKind() == kind::STRING_STOU16 || node.getKind() == kind::STRING_STOU32) {
                if(node[0].isConst()) {
                        CVC4::String s = node[0].getConst<String>();
                        if(s.isNumber()) {
@@ -495,7 +509,24 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
                                        //TODO: leading zeros
                                        retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(-1));
                                } else {
-                                       retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(stmp.c_str()));
+                                       bool flag = false;
+                                       CVC4::Rational r2(stmp.c_str());
+                                       if(node.getKind() == kind::STRING_U16TOS) {
+                                               CVC4::Rational r1(65536);
+                                               if(r2>r1) {
+                                                       flag = true;
+                                               }
+                                       } else if(node.getKind() == kind::STRING_U32TOS) {
+                                               CVC4::Rational r1(4294967296);
+                                               if(r2>r1) {
+                                                       flag = true;
+                                               }
+                                       }
+                                       if(flag) {
+                                               retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(-1));
+                                       } else {
+                                               retNode = NodeManager::currentNM()->mkConst( r2 );
+                                       }
                                }
                        } else {
                                retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(-1));

diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index eef8f980571bfd3357e709057fd23bee5d932bcb..d171c739dbc9e0440b802963654178d3feba8ad0 100644 (file)
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -312,9 +312,6 @@ public:
                if (!t.isRegExp()) {
                  throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
                }
-               if(++it != it_end) {
-                 throw TypeCheckingExceptionPrivate(n, "too many regexp");
-               }
        }
     return nodeManager->regexpType();
   }
@@ -331,9 +328,6 @@ public:
                if (!t.isRegExp()) {
                  throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
                }
-               if(++it != it_end) {
-                 throw TypeCheckingExceptionPrivate(n, "too many regexp");
-               }
        }
     return nodeManager->regexpType();
   }
@@ -350,9 +344,6 @@ public:
                if (!t.isRegExp()) {
                  throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
                }
-               if(++it != it_end) {
-                 throw TypeCheckingExceptionPrivate(n, "too many regexp");
-               }
        }
     return nodeManager->regexpType();
   }
@@ -384,10 +375,6 @@ public:
                if(ch[0] > ch[1]) {
                        throw TypeCheckingExceptionPrivate(n, "expecting the first constant is less or equal to the second one in regexp range");
                }
-
-               if( it != it_end ) {
-                 throw TypeCheckingExceptionPrivate(n, "too many terms in regexp range");
-               }
        }
     return nodeManager->regexpType();
   }
@@ -443,9 +430,6 @@ public:
                //if( (*it).getKind() != kind::CONST_STRING ) {
                //  throw TypeCheckingExceptionPrivate(n, "expecting constant string terms");
                //}
-               if(++it != it_end) {
-                 throw TypeCheckingExceptionPrivate(n, "too many terms");
-               }
        }
     return nodeManager->regexpType();
   }
@@ -467,9 +451,6 @@ public:
                if (!t.isRegExp()) {
                  throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
                }
-               if(++it != it_end) {
-                 throw TypeCheckingExceptionPrivate(n, "too many terms");
-               }
        }
     return nodeManager->booleanType();
   }

diff --git a/test/regress/regress0/strings/type002.smt2 b/test/regress/regress0/strings/type002.smt2
index ac4d9ab8a61f14f9b0c57a7fa93cfb98029ccfed..cbad2226a4b1399668a01181556e1be117f7b92b 100644 (file)
--- a/test/regress/regress0/strings/type002.smt2
+++ b/test/regress/regress0/strings/type002.smt2
@@ -8,7 +8,7 @@
 (declare-fun i () Int)\r
 \r
 (assert (>= i 420))\r
-(assert (= x (int.to.str i)))\r
+(assert (= x (u16.to.str i)))\r
 (assert (= x (str.++ y "0" z)))\r
 (assert (not (= y "")))\r
 (assert (not (= z "")))\r