From a51d41f2a267df30c7ef24de5b753ce73e0ac479 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Tue, 18 Feb 2014 10:48:04 -0600 Subject: [PATCH] switch to total function str.to.int: maps invalid and non-digit strings to 0 --- src/printer/smt2/smt2_printer.cpp | 1 - src/smt/smt_engine.cpp | 55 ------------------- src/theory/strings/kinds | 4 +- src/theory/strings/theory_strings.cpp | 4 +- .../strings/theory_strings_preprocess.cpp | 7 ++- .../strings/theory_strings_rewriter.cpp | 2 +- 6 files changed, 8 insertions(+), 65 deletions(-) diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 5ac56e027..5dc3043af 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -287,7 +287,6 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::STRING_PREFIX: out << "str.prefixof "; break; case kind::STRING_SUFFIX: out << "str.suffixof "; break; case kind::STRING_ITOS: out << "int.to.str "; break; - case kind::STRING_STOI_TOTAL: case kind::STRING_STOI: out << "str.to.int "; break; case kind::STRING_TO_REGEXP: out << "str.to.re "; break; case kind::REGEXP_CONCAT: out << "re.++ "; break; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ac8e5bfe7..7ada9d350 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1613,61 +1613,6 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_mapmkNode( kind::ITE, cond, totalf, uf ); break; } - case kind::STRING_STOI: { - if(d_ufS2I.isNull()) { - std::vector< TypeNode > argTypes; - argTypes.push_back(NodeManager::currentNM()->stringType()); - d_ufS2I = NodeManager::currentNM()->mkSkolem("__ufS2I", - NodeManager::currentNM()->mkFunctionType( - argTypes, NodeManager::currentNM()->integerType()), - "uf str2int", - NodeManager::SKOLEM_EXACT_NAME); - } - Node cond; - if(n[0].isConst()) { - CVC4::String s = n[0].getConst(); - if(s.isNumber()) { - cond = NodeManager::currentNM()->mkConst( false ); - } else { - cond = NodeManager::currentNM()->mkConst( true ); - } - } else { - Node cc1 = n[0].eqNode(nm->mkConst(::CVC4::String(""))); - Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); - Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) ); - Node b1 = NodeManager::currentNM()->mkBoundVar("x", NodeManager::currentNM()->integerType()); - Node z1 = NodeManager::currentNM()->mkBoundVar("z1", NodeManager::currentNM()->stringType()); - Node z2 = NodeManager::currentNM()->mkBoundVar("z2", NodeManager::currentNM()->stringType()); - Node z3 = NodeManager::currentNM()->mkBoundVar("z3", NodeManager::currentNM()->stringType()); - Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1, z1, z2, z3); - std::vector< Node > vec_n; - Node g = NodeManager::currentNM()->mkNode(kind::GEQ, b1, zero); - vec_n.push_back(g); - g = NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, n[0]), b1); - vec_n.push_back(g); - g = b1.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, z1) ); - vec_n.push_back(g); - g = one.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, z2) ); - vec_n.push_back(g); - g = n[0].eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, z1, z2, z3) ); - vec_n.push_back(g); - for(unsigned i=0; i<=9; i++) { - char ch[2]; - ch[0] = i + '0'; ch[1] = '\0'; - std::string stmp(ch); - g = z2.eqNode( nm->mkConst(::CVC4::String(stmp)) ).negate(); - vec_n.push_back(g); - } - Node cc2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, vec_n)); - cc2 = NodeManager::currentNM()->mkNode(kind::EXISTS, b1v, cc2); - cond = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2)); - } - Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_STOI_TOTAL, n[0]); - Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufS2I, n[0]); - node = NodeManager::currentNM()->mkNode( kind::ITE, cond, uf, totalf ); - - break; - } case kind::DIVISION: { // partial function: division if(d_divByZero.isNull()) { diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 09f536b15..7fbefe251 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -22,8 +22,7 @@ operator STRING_STRREPL 3 "string replace" 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 (user symbol)" -operator STRING_STOI_TOTAL 1 "string to integer (internal symbol)" +operator STRING_STOI 1 "string to integer (total function)" #sort CHAR_TYPE \ # Cardinality::INTEGERS \ @@ -120,7 +119,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_STOI_TOTAL ::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 056cd9eb5..d8b20d890 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -57,7 +57,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_equalityEngine.addFunctionKind(kind::STRING_STRCTN); d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR_TOTAL); d_equalityEngine.addFunctionKind(kind::STRING_ITOS); - d_equalityEngine.addFunctionKind(kind::STRING_STOI_TOTAL); + d_equalityEngine.addFunctionKind(kind::STRING_STOI); d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); @@ -408,7 +408,7 @@ void TheoryStrings::preRegisterTerm(TNode n) { case kind::STRING_CONCAT: case kind::STRING_SUBSTR_TOTAL: case kind::STRING_ITOS: - case kind::STRING_STOI_TOTAL: + case kind::STRING_STOI: d_equalityEngine.addTerm(n); break; //case kind::STRING_ITOS: diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index d27dcfc9e..d5b5d9e55 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -319,7 +319,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { } else { throw LogicException("string int.to.str not supported in this release"); } - } else if( t.getKind() == kind::STRING_STOI_TOTAL ) { + } else if( t.getKind() == kind::STRING_STOI ) { if(options::stringExp()) { Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) ); Node nine = NodeManager::currentNM()->mkConst( ::CVC4::Rational(9) ); @@ -357,9 +357,10 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { vec_n.push_back(g); g = t[0].eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, z1, z2, z3) ); vec_n.push_back(g); + char ch[2]; + ch[1] = '\0'; for(unsigned i=0; i<=9; i++) { - char ch[2]; - ch[0] = i + '0'; ch[1] = '\0'; + ch[0] = i + '0'; std::string stmp(ch); g = z2.eqNode( NodeManager::currentNM()->mkConst(::CVC4::String(stmp)) ).negate(); vec_n.push_back(g); diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index c3f63f803..f0467507d 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -450,7 +450,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { std::string stmp = static_cast( &(std::ostringstream() << i) )->str(); retNode = NodeManager::currentNM()->mkConst( ::CVC4::String(stmp) ); } - } else if(node.getKind() == kind::STRING_STOI_TOTAL) { + } else if(node.getKind() == kind::STRING_STOI) { if(node[0].isConst()) { CVC4::String s = node[0].getConst(); int rt = s.toNumber(); -- 2.30.2