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

7 files changed, 106 insertions, 39 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 518c30e81..f030d6de0 100644
--- 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 406319339..c25b8980f 100644
--- 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 67b60fdfe..48e9957d4 100644
--- 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 9ed52e94a..f2172071d 100644
--- 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 b2988d54a..3167734ee 100644
--- 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, lenp, 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 42962308d..8a603e6df 100644
--- 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 eef8f9805..d171c739d 100644
--- 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();
   }