From b19aa753e376cd02f750ced25c842fe20869ef8a Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Mon, 31 Mar 2014 15:55:45 -0500 Subject: [PATCH] add str to u16/u32, and u16/u32 to str --- src/parser/smt2/Smt2.g | 8 +++ src/printer/smt2/smt2_printer.cpp | 4 ++ src/theory/strings/kinds | 8 +++ src/theory/strings/theory_strings.cpp | 4 ++ .../strings/theory_strings_preprocess.cpp | 63 ++++++++++++++----- .../strings/theory_strings_rewriter.cpp | 39 ++++++++++-- .../strings/theory_strings_type_rules.h | 19 ------ test/regress/regress0/strings/type002.smt2 | 2 +- 8 files changed, 107 insertions(+), 40 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().getNumerator().toString(); + if(node.getKind() == kind::STRING_U16TOS) { + CVC4::Rational r1(65536); + CVC4::Rational r2 = node[0].getConst(); + if(r2>r1) { + flag = true; + } + } else if(node.getKind() == kind::STRING_U32TOS) { + CVC4::Rational r1(4294967296); + CVC4::Rational r2 = node[0].getConst(); + if(r2>r1) { + flag = true; + } + } //std::string stmp = static_cast( &(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(); 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(); } diff --git a/test/regress/regress0/strings/type002.smt2 b/test/regress/regress0/strings/type002.smt2 index ac4d9ab8a..cbad2226a 100644 --- a/test/regress/regress0/strings/type002.smt2 +++ b/test/regress/regress0/strings/type002.smt2 @@ -8,7 +8,7 @@ (declare-fun i () Int) (assert (>= i 420)) -(assert (= x (int.to.str i))) +(assert (= x (u16.to.str i))) (assert (= x (str.++ y "0" z))) (assert (not (= y ""))) (assert (not (= z ""))) -- 2.30.2