From 4d5387554a084e7da29a170c2851830f5fe55199 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Tue, 18 Feb 2014 11:08:20 -0600 Subject: [PATCH] str.to.int(INVALID) = -1 --- src/theory/strings/theory_strings_preprocess.cpp | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index d5b5d9e55..43e7829bb 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -321,6 +321,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { } } else if( t.getKind() == kind::STRING_STOI ) { if(options::stringExp()) { + Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) ); Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) ); Node nine = NodeManager::currentNM()->mkConst( ::CVC4::Rational(9) ); Node ten = NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) ); @@ -339,7 +340,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { new_nodes.push_back(t.eqNode(ufP0)); //cc1 Node cc1 = t[0].eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(""))); - cc1 = NodeManager::currentNM()->mkNode(kind::AND, ufP0.eqNode(d_zero), cc1); + cc1 = NodeManager::currentNM()->mkNode(kind::AND, ufP0.eqNode(negone), cc1); //cc2 Node b1 = NodeManager::currentNM()->mkBoundVar("x", NodeManager::currentNM()->integerType()); Node z1 = NodeManager::currentNM()->mkBoundVar("z1", NodeManager::currentNM()->stringType()); @@ -357,17 +358,17 @@ 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'; + char chtmp[2]; + chtmp[1] = '\0'; for(unsigned i=0; i<=9; i++) { - ch[0] = i + '0'; - std::string stmp(ch); + chtmp[0] = i + '0'; + std::string stmp(chtmp); g = z2.eqNode( NodeManager::currentNM()->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); - cc2 = NodeManager::currentNM()->mkNode(kind::AND, ufP0.eqNode(d_zero), cc2); + cc2 = NodeManager::currentNM()->mkNode(kind::AND, ufP0.eqNode(negone), cc2); //cc3 Node b2 = NodeManager::currentNM()->mkBoundVar("y", NodeManager::currentNM()->integerType()); Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2); -- 2.30.2