diff --git a/src/ast/rewriter/seq_skolem.cpp b/src/ast/rewriter/seq_skolem.cpp index c2e948216..96b3df3ed 100644 --- a/src/ast/rewriter/seq_skolem.cpp +++ b/src/ast/rewriter/seq_skolem.cpp @@ -26,10 +26,14 @@ skolem::skolem(ast_manager& m, th_rewriter& rw): m_suffix = "seq.s.prefix"; m_accept = "aut.accept"; m_tail = "seq.tail"; + m_left = "seq.left"; + m_right = "seq.right"; m_seq_first = "seq.first"; m_seq_last = "seq.last"; m_indexof_left = "seq.idx.l"; m_indexof_right = "seq.idx.r"; + m_lindexof_left = "seq.lidx.l"; + m_lindexof_right = "seq.lidx.r"; m_aut_step = "aut.step"; m_pre = "seq.pre"; // (seq.pre s l): prefix of string s of length l m_post = "seq.post"; // (seq.post s l): suffix of string s of length k, based on extract starting at index i of length l @@ -155,6 +159,20 @@ bool skolem::is_tail(expr* e, expr*& s, expr*& idx) const { return is_tail(e) && (s = to_app(e)->get_arg(0), idx = to_app(e)->get_arg(1), true); } +bool skolem::is_left_or_right(expr* e, expr*& x, expr*& y, expr*& z) { + if (!is_skolem(m_left, e) && !is_skolem(m_right, e)) + return false; + x = nullptr; + y = nullptr; + z = nullptr; + unsigned sz = to_app(e)->get_num_args(); + if (sz > 0) x = to_app(e)->get_arg(0); + if (sz > 1) y = to_app(e)->get_arg(1); + if (sz > 2) z = to_app(e)->get_arg(2); + return true; +} + + bool skolem::is_eq(expr* e, expr*& a, expr*& b) const { return is_skolem(m_eq, e) && (a = to_app(e)->get_arg(0), b = to_app(e)->get_arg(1), true); } diff --git a/src/ast/rewriter/seq_skolem.h b/src/ast/rewriter/seq_skolem.h index 088a00eeb..4b828abf6 100644 --- a/src/ast/rewriter/seq_skolem.h +++ b/src/ast/rewriter/seq_skolem.h @@ -32,8 +32,10 @@ namespace seq { symbol m_prefix, m_suffix; symbol m_tail; + symbol m_left, m_right; symbol m_seq_first, m_seq_last; - symbol m_indexof_left, m_indexof_right; // inverse of indexof: (indexof_left s t) + s + (indexof_right s t) = t, for s in t. + symbol m_indexof_left, m_indexof_right; // inverse of indexof: (indexof_left s t) + s + (indexof_right s t) = t, for s in t. + symbol m_lindexof_left, m_lindexof_right; // inverse of indexof: (indexof_left s t) + s + (indexof_right s t) = t, for s in t. symbol m_aut_step; // regex unfolding state symbol m_accept; // regex symbol m_is_empty; // regex emptiness check @@ -81,8 +83,8 @@ namespace seq { expr_ref mk_indexof_right(expr* t, expr* s, expr* offset = nullptr) { return mk(m_indexof_right, t, s, offset); } expr_ref mk_contains_left(expr* t, expr* s, expr* offset = nullptr) { return mk("seq.cnt.l", t, s, offset); } expr_ref mk_contains_right(expr* t, expr* s, expr* offset = nullptr) { return mk("seq.cnt.r", t, s, offset); } - expr_ref mk_last_indexof_left(expr* t, expr* s, expr* offset = nullptr) { return mk("seq.lidx.l", t, s, offset); } - expr_ref mk_last_indexof_right(expr* t, expr* s, expr* offset = nullptr) { return mk("seq.lidx.r", t, s, offset); } + expr_ref mk_last_indexof_left(expr* t, expr* s, expr* offset = nullptr) { return mk(m_lindexof_left, t, s, offset); } + expr_ref mk_last_indexof_right(expr* t, expr* s, expr* offset = nullptr) { return mk(m_lindexof_right, t, s, offset); } expr_ref mk_tail(expr* s, expr* i) { return mk(m_tail, s, i); } expr_ref mk_post(expr* s, expr* i) { return mk(m_post, s, i); } @@ -100,8 +102,8 @@ namespace seq { expr_ref mk_digit2int(expr* ch) { return mk(symbol("seq.digit2int"), ch, nullptr, nullptr, nullptr, a.mk_int()); } expr_ref mk_digit2bv(expr* ch, sort* bv_sort); expr_ref mk_ubv2ch(expr* b) { return mk(symbol("seq.ubv2ch"), b, nullptr, nullptr, nullptr, seq.mk_char_sort()); } - expr_ref mk_left(expr* x, expr* y, expr* z = nullptr) { return mk("seq.left", x, y, z); } - expr_ref mk_right(expr* x, expr* y, expr* z = nullptr) { return mk("seq.right", x, y, z); } + expr_ref mk_left(expr* x, expr* y, expr* z = nullptr) { return mk(m_left, x, y, z); } + expr_ref mk_right(expr* x, expr* y, expr* z = nullptr) { return mk(m_right, x, y, z); } expr_ref mk_max_unfolding_depth(unsigned d); expr_ref mk_length_limit(expr* e, unsigned d); @@ -117,6 +119,8 @@ namespace seq { bool is_seq_first(expr* e) const { return is_skolem(m_seq_first, e); } bool is_indexof_left(expr* e) const { return is_skolem(m_indexof_left, e); } bool is_indexof_right(expr* e) const { return is_skolem(m_indexof_right, e); } + bool is_last_indexof_left(expr* e) const { return is_skolem(m_lindexof_left, e); } + bool is_last_indexof_right(expr* e) const { return is_skolem(m_lindexof_right, e); } bool is_indexof_left(expr* e, expr*& x, expr*& y) const { return is_indexof_left(e) && (x = to_app(e)->get_arg(0), y = to_app(e)->get_arg(1), true); } @@ -124,6 +128,7 @@ namespace seq { return is_indexof_right(e) && (x = to_app(e)->get_arg(0), y = to_app(e)->get_arg(1), true); } + bool is_left_or_right(expr* e, expr*& x, expr*& y, expr*& z); bool is_step(expr* e) const { return is_skolem(m_aut_step, e); } bool is_step(expr* e, expr*& s, expr*& idx, expr*& re, expr*& i, expr*& j, expr*& t) const; bool is_accept(expr* acc) const { return is_skolem(m_accept, acc); } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 5712d1d41..7b0955518 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1538,10 +1538,23 @@ void theory_seq::add_length(expr* l) { Add length limit restrictions to sequence s. */ void theory_seq::add_length_limit(expr* s, unsigned k, bool is_searching) { - if (m_sk.is_indexof_left(s)) + if (m_util.str.is_concat(s)) { + for (expr* e : *to_app(s)) + add_length_limit(e, k, is_searching); return; - if (m_sk.is_indexof_right(s)) + } + if (m_util.str.is_unit(s)) return; + if (m_util.str.is_empty(s)) + return; + + if (m_sk.is_skolem(s)) { + for (expr* e : *to_app(s)) + if (m_util.is_seq(e) || m_sk.is_skolem(e)) + add_length_limit(e, k, is_searching); + return; + } + expr_ref lim_e = m_ax.add_length_limit(s, k); unsigned k0 = 0; if (m_length_limit_map.find(s, k0)) {