From 7ece37f9a1e13902df439e00644ea7cd79994b11 Mon Sep 17 00:00:00 2001 From: Thai Trinh Date: Fri, 8 Dec 2017 17:10:28 +0800 Subject: [PATCH] added assertions --- src/smt/theory_seq.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index b412870aa..754e2b84c 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -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 const& ls, ptr_vector 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 const& ls, ptr_vector 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 const& ls, ptr_vector 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());