diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-20 17:03:24 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-20 17:03:24 -0600 |
| commit | 7f0f26da448a22fd111041f1c33194040ef4dc25 (patch) | |
| tree | ffd4f2a4de506a791890395233b79ea9b23fd27c /src/theory/strings | |
| parent | fa797d425d7a75711a1dd885be3f97f22e30a7dc (diff) | |
| parent | b12a68cf8df41e941ca0834006f5a4d68b48c05a (diff) | |
Merge branch 'master' of github.com:tiliang/CVC4
Conflicts:
src/theory/strings/theory_strings_preprocess.cpp
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 04e7a06cc..1df79ccff 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -238,10 +238,10 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node pret = NodeManager::currentNM()->mkNode(kind::STRING_ITOS, num); Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, pret); - Node lem = NodeManager::currentNM()->mkNode(kind::IFF, + /*Node lem = NodeManager::currentNM()->mkNode(kind::IFF, t.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("0"))), t[0].eqNode(d_zero)); - new_nodes.push_back(lem); + new_nodes.push_back(lem);*/ Node b1 = NodeManager::currentNM()->mkBoundVar("x", NodeManager::currentNM()->integerType()); Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1); @@ -277,7 +277,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node cc2 = ufx.eqNode(ufMx); cc2 = NodeManager::currentNM()->mkNode(kind::IMPLIES, lstx, cc2); // leading zero - Node cl = NodeManager::currentNM()->mkNode(kind::AND, lstx, d_zero.eqNode(t[0]).negate()); + Node cl = NodeManager::currentNM()->mkNode(kind::AND, lstx, d_zero.eqNode(b1).negate()); Node cc21 = NodeManager::currentNM()->mkNode(kind::IMPLIES, cl, NodeManager::currentNM()->mkNode(kind::GT, ufMx, d_zero)); //cc3 Node cc3 = NodeManager::currentNM()->mkNode(kind::GEQ, ufMx, d_zero); |