diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-18 11:08:20 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-18 11:08:20 -0600 |
| commit | 4d5387554a084e7da29a170c2851830f5fe55199 (patch) | |
| tree | 06bed2e06af7d1e61e174736c7b3d4419bcc92d8 /src/theory/strings | |
| parent | a51d41f2a267df30c7ef24de5b753ce73e0ac479 (diff) | |
str.to.int(INVALID) = -1
Diffstat (limited to 'src/theory/strings')
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 13 |
1 files 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); |