From 287785c8c2fe8031489bdf2d9f56506a8dfe3b48 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 5 Sep 2017 07:57:40 +0200 Subject: [PATCH] Remove support for conversions between uint32/uint16 and string. (#1069) * Remove support for conversions between uint32/uint16 and string. * Temporarily disable regression. --- src/parser/cvc/Cvc.g | 14 +----- src/parser/smt2/smt2.cpp | 4 -- src/printer/smt2/smt2_printer.cpp | 8 ---- src/theory/strings/kinds | 8 ---- src/theory/strings/theory_strings.cpp | 13 +----- .../strings/theory_strings_preprocess.cpp | 20 +------- .../strings/theory_strings_rewriter.cpp | 46 ++++--------------- test/regress/regress0/strings/Makefile.am | 2 +- test/regress/regress0/strings/type002.smt2 | 4 +- 9 files changed, 16 insertions(+), 103 deletions(-) diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index efdd328a4..6cc5c29a4 100644 --- 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 de3c9aa62..aeabdbac2 100644 --- 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 aa9c17e5a..2f2a6ff18 100644 --- 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 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().getNumerator().toString(); - if(node.getKind() == kind::STRING_U16TOS) { - CVC4::Rational r1(UINT16_MAX); - CVC4::Rational r2 = node[0].getConst(); - if(r2>r1) { - flag = true; - } - } else if(node.getKind() == kind::STRING_U32TOS) { - CVC4::Rational r1(UINT32_MAX); - CVC4::Rational r2 = node[0].getConst(); - if(r2>r1) { - flag = true; - } - } - //std::string stmp = static_cast( &(std::ostringstream() << node[0]) )->str(); - if(flag || stmp[0] == '-') { + if( node[0].getConst().sgn()==-1 ){ retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); - } else { + }else{ + std::string stmp = node[0].getConst().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(); 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 c47c10de0..8f4e3dc4b 100644 --- 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 296057a76..0df0f20b0 100644 --- 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) -- 2.30.2