mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

added assertions

Browse source
This commit is contained in:
Thai Trinh 2017-12-08 17:10:28 +08:00
parent 034e72572f
commit 7ece37f9a1
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_seq.cpp
View file

@ -522,8 +522,9 @@ bool theory_seq::eq_unit(expr* const& l, expr* const &r) const {
return l == r || is_unit_nth(l) || is_unit_nth(r);
}
// exists y s.t. ls and rs ++ y have the same suffix
// exists x, y, rs' 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) {
SASSERT(!ls.empty() && !rs.empty());
unsigned_vector res;
expr* l = m_util.str.mk_concat(ls.size(),ls.c_ptr());
expr* r = m_util.str.mk_concat(rs.size(),rs.c_ptr());
@ -553,8 +554,9 @@ unsigned_vector theory_seq::overlap(ptr_vector<expr> const& ls, ptr_vector<expr>
return result;
}
// exists x s.t. x ++ ls and rs have the same prefix
// exists x, y, rs' 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) {
SASSERT(!ls.empty() && !rs.empty());
unsigned_vector res;
expr* l = m_util.str.mk_concat(ls.size(),ls.c_ptr());
expr* r = m_util.str.mk_concat(rs.size(),rs.c_ptr());