diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-19 12:20:44 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-19 12:20:44 -0600 |
| commit | 6ea4417a0c859190d39f1e94c724d27a96cb717d (patch) | |
| tree | 18c519470dad57bf643e279bf6c2231b8651145c /src/theory/strings | |
| parent | 0aa0a9e616e6d8fc4db19b908b81c2c1a525dcd3 (diff) | |
add negative int2str
Diffstat (limited to 'src/theory/strings')
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 43e7829bb..6520f5517 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -232,7 +232,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { } } else if( t.getKind() == kind::STRING_ITOS ) { if(options::stringExp()) { - Node num = t[0];//NodeManager::currentNM()->mkNode(kind::ABS, t[0]); + Node num = NodeManager::currentNM()->mkNode(kind::ABS, t[0]); Node pret = NodeManager::currentNM()->mkNode(kind::STRING_ITOS, num); Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, pret); @@ -306,13 +306,13 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, g1, conc ); conc = NodeManager::currentNM()->mkNode( kind::FORALL, b1v, conc ); new_nodes.push_back( conc ); - /* + Node sign = NodeManager::currentNM()->mkNode(kind::ITE, NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero), NodeManager::currentNM()->mkConst(::CVC4::String("")), NodeManager::currentNM()->mkConst(::CVC4::String("-"))); conc = t.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sign, pret) ); - new_nodes.push_back( conc );*/ + new_nodes.push_back( conc ); d_cache[t] = t; retNode = t; |