mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

fixed redundant check

Browse source
This commit is contained in:
Thai Trinh 2017-12-08 17:20:30 +08:00
parent 7ece37f9a1
commit 6253faece7
1 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/smt/theory_seq.cpp
View file

@ -522,7 +522,7 @@ bool theory_seq::eq_unit(expr* const& l, expr* const &r) const {
return l == r || is_unit_nth(l) || is_unit_nth(r); return l == r || is_unit_nth(l) || is_unit_nth(r);
} }
// exists x, y, rs' s.t. (ls = x ++ rs' ++ y & rs = rs') || (ls = rs' ++ x && rs = y ++ rs') // exists x, y, rs' != empty s.t. (ls = x ++ rs' ++ y & rs = rs') || (ls = rs' ++ x && rs = y ++ rs')
unsigned_vector theory_seq::overlap(ptr_vector<expr> const& ls, ptr_vector<expr> const& rs) { unsigned_vector theory_seq::overlap(ptr_vector<expr> const& ls, ptr_vector<expr> const& rs) {
SASSERT(!ls.empty() && !rs.empty()); SASSERT(!ls.empty() && !rs.empty());
unsigned_vector res; unsigned_vector res;
@ -554,7 +554,7 @@ unsigned_vector theory_seq::overlap(ptr_vector<expr> const& ls, ptr_vector<expr>
return result; return result;
} }
// exists x, y, rs' s.t. (ls = x ++ rs' ++ y & rs = rs') || (ls = x ++ rs' && rs = rs' ++ y) // exists x, y, rs' != empty s.t. (ls = x ++ rs' ++ y & rs = rs') || (ls = x ++ rs' && rs = rs' ++ y)
unsigned_vector theory_seq::overlap2(ptr_vector<expr> const& ls, ptr_vector<expr> const& rs) { unsigned_vector theory_seq::overlap2(ptr_vector<expr> const& ls, ptr_vector<expr> const& rs) {
SASSERT(!ls.empty() && !rs.empty()); SASSERT(!ls.empty() && !rs.empty());
unsigned_vector res; unsigned_vector res;
@ -568,11 +568,13 @@ unsigned_vector theory_seq::overlap2(ptr_vector<expr> const& ls, ptr_vector<expr
for (unsigned i = 0; i < ls.size(); ++i) { for (unsigned i = 0; i < ls.size(); ++i) {
if (eq_unit(ls[i],rs[0])) { if (eq_unit(ls[i],rs[0])) {
bool same = true; bool same = true;
for (unsigned j = i; j<ls.size() && j-i<rs.size(); ++j) { unsigned j = i+1;
while (j<ls.size() && j-i<rs.size()) {
if (!eq_unit(ls[j], rs[j-i])) { if (!eq_unit(ls[j], rs[j-i])) {
same = false; same = false;
break; break;
} }
++j;
} }
if (same) if (same)
result.push_back(i); result.push_back(i);