diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 9048ac122..1b90bc9e3 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -945,6 +945,17 @@ void seq_util::str::get_concat(expr* e, expr_ref_vector& es) const { } } +void seq_util::str::get_concat(expr* e, ptr_vector& es) const { + expr* e1, * e2; + while (is_concat(e, e1, e2)) { + get_concat(e1, es); + e = e2; + } + if (!is_empty(e)) { + es.push_back(e); + } +} + /* Returns true if s is an expression of the form (l = |u|) |u|-k or (-k)+|u| or |u|+(-k). Also returns true and assigns k=0 and l=s if s is |u|. diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index c08ed6f7a..4a0b81c7b 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -424,6 +424,7 @@ public: MATCH_UNARY(is_unit); void get_concat(expr* e, expr_ref_vector& es) const; + void get_concat(expr* e, ptr_vector& es) const; void get_concat_units(expr* e, expr_ref_vector& es) const; expr* get_leftmost_concat(expr* e) const { expr* e1, *e2; while (is_concat(e, e1, e2)) e = e1; return e; } expr* get_rightmost_concat(expr* e) const { expr* e1, *e2; while (is_concat(e, e1, e2)) e = e2; return e; } diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp index 5d2a7e597..9745ed747 100644 --- a/src/ast/sls/sls_seq_plugin.cpp +++ b/src/ast/sls/sls_seq_plugin.cpp @@ -224,6 +224,23 @@ namespace sls { return m_values.get(id, nullptr); } + ptr_vector const& seq_plugin::lhs(expr* eq) { + auto& ev = get_eval(eq); + if (ev.lhs.empty()) { + expr* x, * y; + VERIFY(m.is_eq(eq, x, y)); + seq.str.get_concat(x, ev.lhs); + seq.str.get_concat(y, ev.rhs); + } + return ev.lhs; + } + + ptr_vector const& seq_plugin::rhs(expr* eq) { + lhs(eq); + auto& e = get_eval(eq); + return e.rhs; + } + zstring& seq_plugin::strval0(expr* e) { SASSERT(seq.is_string(e->get_sort())); return get_eval(e).val0.svalue; @@ -557,8 +574,10 @@ namespace sls { bool is_true = ctx.is_true(e); expr* x, * y; VERIFY(m.is_eq(e, x, y)); - verbose_stream() << is_true << ": " << mk_bounded_pp(e, m, 3) << "\n"; + IF_VERBOSE(3, verbose_stream() << is_true << ": " << mk_bounded_pp(e, m, 3) << "\n"); if (ctx.is_true(e)) { + if (ctx.rand(10) != 0) + return repair_down_str_eq_unify(e); if (!is_value(x)) m_str_updates.push_back({ x, strval1(y), 1 }); if (!is_value(y)) @@ -579,6 +598,81 @@ namespace sls { return apply_update(); } + bool seq_plugin::repair_down_str_eq_unify(app* eq) { + auto const& L = lhs(eq); + auto const& R = rhs(eq); + unsigned i = 0, j = 0; // position into current string + unsigned ni = 0, nj = 0; // current string in concatenation + double depth = 1.0; // priority of update. Doubled when depth of equal strings are increased. + while (ni < L.size() && nj < R.size()) { + auto const& xi = L[ni]; + auto const& yj = R[nj]; + auto const& vi = strval0(xi); + auto const& vj = strval0(yj); + IF_VERBOSE(4, + verbose_stream() << "unify: \"" << vi << "\" = \"" << vj << "\" incides " << i << " " << j << "\n"; + verbose_stream() << vi.length() << " " << vj.length() << "\n"); + if (vi.length() == i && vj.length() == j) { + depth *= 2; + if (nj + 1 < R.size() && !strval0(R[nj + 1]).empty()) + m_str_updates.push_back({ xi, vi + zstring(strval0(R[nj + 1])[0]), depth }); + if (ni + 1 < L.size() && !strval0(L[ni + 1]).empty()) + m_str_updates.push_back({ yj, vj + zstring(strval0(L[ni + 1])[0]), depth }); + i = 0; + j = 0; + ++ni; + ++nj; + continue; + } + if (vi.length() == i) { + // xi -> vi + vj[j] + SASSERT(j < vj.length()); + m_str_updates.push_back({ xi, vi + zstring(vj[j]), depth}); + depth *= 2; + i = 0; + ++ni; + continue; + } + if (vj.length() == j) { + // yj -> vj + vi[i] + SASSERT(i < vi.length()); + m_str_updates.push_back({ yj, vj + zstring(vi[i]), depth }); + depth *= 2; + j = 0; + ++nj; + continue; + } + SASSERT(i < vi.length()); + SASSERT(j < vj.length()); + if (is_value(xi) && is_value(yj)) { + ++i, ++j; + continue; + } + if (vi[i] == vj[j]) { + ++i, ++j; + continue; + } + if (!is_value(xi)) { + m_str_updates.push_back({ xi, vi.extract(0, i), depth }); + m_str_updates.push_back({ xi, vi.extract(0, i) + zstring(vj[j]), depth}); + } + if (!is_value(yj)) { + m_str_updates.push_back({ yj, vj.extract(0, j), depth }); + m_str_updates.push_back({ yj, vj.extract(0, j) + zstring(vi[i]), depth }); + } + break; + } + for (; ni < L.size(); ++ni) + if (!is_value(L[ni])) + m_str_updates.push_back({ L[ni], zstring(), depth }); + + for (; nj < R.size(); ++nj) + if (!is_value(R[nj])) + m_str_updates.push_back({ R[nj], zstring(), depth }); + + return apply_update(); + } + bool seq_plugin::repair_down_seq(app* e) { switch (e->get_decl_kind()) { case OP_SEQ_CONTAINS: @@ -1021,7 +1115,7 @@ namespace sls { auto [e, value, score] = m_str_updates[i]; if (update(e, value)) { - verbose_stream() << "set value " << mk_bounded_pp(e, m) << " := \"" << value << "\"\n"; + IF_VERBOSE(3, verbose_stream() << "set value " << mk_bounded_pp(e, m) << " := \"" << value << "\"\n"); m_str_updates.reset(); m_int_updates.reset(); return true; @@ -1034,7 +1128,7 @@ namespace sls { else { auto [e, value, score] = m_int_updates[i]; - verbose_stream() << "set value " << mk_bounded_pp(e, m) << " := " << value << "\n"; + IF_VERBOSE(3, verbose_stream() << "set value " << mk_bounded_pp(e, m) << " := " << value << "\n"); if (update(e, value)) { m_int_updates.reset(); diff --git a/src/ast/sls/sls_seq_plugin.h b/src/ast/sls/sls_seq_plugin.h index ea9566348..22363e21f 100644 --- a/src/ast/sls/sls_seq_plugin.h +++ b/src/ast/sls/sls_seq_plugin.h @@ -38,6 +38,7 @@ namespace sls { bool is_value = false; unsigned min_length = 0; unsigned max_length = UINT_MAX; + ptr_vector lhs, rhs; }; seq_util seq; @@ -69,6 +70,7 @@ namespace sls { bool repair_down_seq(app* e); bool repair_down_eq(app* e); + bool repair_down_str_eq_unify(app* e); bool repair_down_str_eq(app* e); bool repair_down_str_extract(app* e); bool repair_down_str_contains(expr* e); @@ -107,6 +109,8 @@ namespace sls { eval& get_eval(expr* e); eval* get_eval(expr* e) const; + ptr_vector const& lhs(expr* eq); + ptr_vector const& rhs(expr* eq); bool is_value(expr* e); public: