diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-01-02 11:43:00 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-01-02 11:43:00 -0600 |
commit | ac73ef6098ccdbf59623171bcd4837ddd0afc38f (patch) | |
tree | dc81b6270df046417a275fa2ad229c29ce0f5b7d /src/theory/quantifiers/extended_rewrite.cpp | |
parent | dc2f9914f49076d56cdb18e14971df67fbe567bb (diff) |
Improve rewriter for string equality (#1427)
Diffstat (limited to 'src/theory/quantifiers/extended_rewrite.cpp')
-rw-r--r-- | src/theory/quantifiers/extended_rewrite.cpp | 41 |
1 files changed, 0 insertions, 41 deletions
diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index b463a319a..956822303 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -118,47 +118,6 @@ Node ExtendedRewriter::extendedRewrite(Node n) Node new_ret; if (ret.getKind() == kind::EQUAL) { - // string equalities with disequal prefix or suffix - if (ret[0].getType().isString()) - { - std::vector<Node> c[2]; - for (unsigned i = 0; i < 2; i++) - { - strings::TheoryStringsRewriter::getConcat(ret[i], c[i]); - } - if (c[0].empty() == c[1].empty()) - { - if (!c[0].empty()) - { - for (unsigned i = 0; i < 2; i++) - { - unsigned index1 = i == 0 ? 0 : c[0].size() - 1; - unsigned index2 = i == 0 ? 0 : c[1].size() - 1; - if (c[0][index1].isConst() && c[1][index2].isConst()) - { - CVC4::String s = c[0][index1].getConst<String>(); - CVC4::String t = c[1][index2].getConst<String>(); - unsigned len_short = s.size() <= t.size() ? s.size() : t.size(); - bool isSameFix = - i == 1 ? s.rstrncmp(t, len_short) : s.strncmp(t, len_short); - if (!isSameFix) - { - Trace("q-ext-rewrite") << "sygus-extr : " << ret - << " rewrites to false due to " - "disequal string prefix/suffix." - << std::endl; - new_ret = d_false; - break; - } - } - } - } - } - else - { - new_ret = d_false; - } - } if (new_ret.isNull()) { // simple ITE pulling |