From b143a954c5d98e0c85292ab4d579835b4d48c8e7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 25 Nov 2024 13:46:16 -0800 Subject: [PATCH] add notes and additional functions to sls-seq Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_arith_base.cpp | 2 + src/ast/sls/sls_seq_plugin.cpp | 130 ++++++++++++++++++++++++++------- src/ast/sls/sls_seq_plugin.h | 4 + src/smt/theory_sls.cpp | 14 +++- src/smt/theory_sls.h | 2 + 5 files changed, 125 insertions(+), 27 deletions(-) diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp index 93025909f..0fb9b4d6e 100644 --- a/src/ast/sls/sls_arith_base.cpp +++ b/src/ast/sls/sls_arith_base.cpp @@ -1952,6 +1952,8 @@ namespace sls { for (unsigned j = i + 1; j < args.get_num_args(); ++j) { auto v1 = mk_term(args.get_arg(i)); auto v2 = mk_term(args.get_arg(j)); + verbose_stream() << "repair " << v1 << " " << v2 << " " + << value(v1) << " " << value(v2) << "\n"; if (value(v1) == value(v2)) { auto new_value = value(v1) + num_t(1); if (new_value == value(v2)) diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp index 3f435328b..563a0a6b0 100644 --- a/src/ast/sls/sls_seq_plugin.cpp +++ b/src/ast/sls/sls_seq_plugin.cpp @@ -72,6 +72,19 @@ Alternate to lookahead strategy: Revert bias on long strings: - give preference to reset leaves that are assigned to long strings - bake in bias for shorter strings into equation solving? + +Equality solving using stochastic Nelson. +- Given equality where current assignment does not satisfy it: + - Xw = v: + - let X' range over prefixes of X that matches v. + - non-deterministic set X <- strval0(X') + - non-deterministic set X <- strval0(X') + 'a' where strval0(X') + 'a' matches prefix of strval0(v), and X' is longest prefix of X that matches v. + - If X fully matches a prefix of v, then, in addition to the rules above: + - consume constant character from strval0(X)w = v + - reveal the next variable to solve for. + + - What scores make sense to use for partial solutions? + --*/ #include "ast/sls/sls_seq_plugin.h" @@ -411,6 +424,22 @@ namespace sls { if (m.is_bool(e)) return; + if (seq.str.is_itos(e)) { + repair_up_str_itos(e); + return; + } + if (seq.str.is_stoi(e)) { + repair_up_str_stoi(e); + return; + } + if (seq.str.is_length(e)) { + repair_up_str_length(e); + return; + } + if (seq.str.is_index(e)) { + repair_up_str_indexof(e); + return; + } if (seq.is_string(e->get_sort())) { if (is_value(e)) return; @@ -419,16 +448,6 @@ namespace sls { return; } - if (seq.str.is_length(e)) { - repair_up_str_length(e); - return; - } - - if (seq.str.is_index(e)) { - repair_up_str_indexof(e); - return; - } - verbose_stream() << "repair up nyi: " << mk_bounded_pp(e, m) << "\n"; } @@ -471,6 +490,35 @@ namespace sls { return apply_update(); } + void seq_plugin::repair_up_str_stoi(app* e) { + expr* x; + VERIFY(seq.str.is_stoi(e, x)); + + rational val_e; + rational val_x(strval0(x).encode().c_str()); + VERIFY(a.is_numeral(ctx.get_value(e), val_e)); + if (val_e.is_unsigned() && val_e == val_x) + return; + if (val_x < 0) + update(e, rational(0)); + else + update(e, val_x); + } + + void seq_plugin::repair_up_str_itos(app* e) { + expr* x; + VERIFY(seq.str.is_itos(e, x)); + rational val_x; + VERIFY(a.is_numeral(ctx.get_value(x), val_x)); + rational val_e(strval0(e).encode().c_str()); + if (val_x.is_unsigned() && val_x == val_e) + return; + if (val_x < 0) + update(e, zstring()); + else + update(e, zstring(val_x.to_string())); + } + void seq_plugin::repair_up_str_length(app* e) { expr* x; VERIFY(seq.str.is_length(e, x)); @@ -566,21 +614,33 @@ namespace sls { if (seq.is_string(to_app(e)->get_arg(0)->get_sort())) return repair_down_str_indexof(e); break; + case OP_STRING_CONST: + UNREACHABLE(); + break; + case OP_STRING_ITOS: + return repair_down_str_itos(e); + case OP_STRING_STOI: + return repair_down_str_stoi(e); + case OP_STRING_UBVTOS: + case OP_STRING_SBVTOS: + case OP_STRING_TO_CODE: + case OP_STRING_FROM_CODE: case OP_SEQ_UNIT: - case OP_SEQ_REPLACE: case OP_SEQ_NTH: case OP_SEQ_NTH_I: case OP_SEQ_NTH_U: - case OP_SEQ_LAST_INDEX: - case OP_SEQ_TO_RE: - case OP_SEQ_IN_RE: + case OP_SEQ_REPLACE: case OP_SEQ_REPLACE_RE_ALL: case OP_SEQ_REPLACE_RE: case OP_SEQ_REPLACE_ALL: case OP_SEQ_MAP: case OP_SEQ_MAPI: case OP_SEQ_FOLDL: - case OP_SEQ_FOLDLI: + case OP_SEQ_FOLDLI: + + case OP_SEQ_TO_RE: + case OP_SEQ_IN_RE: + case OP_RE_PLUS: case OP_RE_STAR: case OP_RE_OPTION: @@ -598,23 +658,43 @@ namespace sls { case OP_RE_OF_PRED: case OP_RE_REVERSE: case OP_RE_DERIVATIVE: - case OP_STRING_CONST: - case OP_STRING_ITOS: - case OP_STRING_STOI: - case OP_STRING_UBVTOS: - case OP_STRING_SBVTOS: case OP_STRING_LT: case OP_STRING_LE: - case OP_STRING_IS_DIGIT: - case OP_STRING_TO_CODE: - case OP_STRING_FROM_CODE: - default: - break; + case OP_STRING_IS_DIGIT: + break; + default: + verbose_stream() << "unexpected repair down " << mk_bounded_pp(e, m) << "\n"; + UNREACHABLE(); } verbose_stream() << "nyi repair down " << mk_bounded_pp(e, m) << "\n"; return false; } + bool seq_plugin::repair_down_str_itos(app* e) { + expr* x; + VERIFY(seq.str.is_itos(e, x)); + zstring se = strval0(e); + rational r(se.encode().c_str()); + if (r.is_int()) + m_int_updates.push_back({ x, r, 1 }); + else + m_int_updates.push_back({ x, rational(-1 - ctx.rand(10)), 1 }); + + return apply_update(); + } + + bool seq_plugin::repair_down_str_stoi(app* e) { + expr* x; + rational r; + VERIFY(seq.str.is_stoi(e, x)); + VERIFY(a.is_numeral(ctx.get_value(e), r) && r.is_int()); + if (r < 0) + return false; + zstring r_val(r.to_string()); + m_str_updates.push_back({ x, r_val, 1 }); + return apply_update(); + } + bool seq_plugin::repair_down_str_at(app* e) { expr* x, * y; VERIFY(seq.str.is_at(e, x, y)); diff --git a/src/ast/sls/sls_seq_plugin.h b/src/ast/sls/sls_seq_plugin.h index 2afc087fd..7648a9193 100644 --- a/src/ast/sls/sls_seq_plugin.h +++ b/src/ast/sls/sls_seq_plugin.h @@ -79,9 +79,13 @@ namespace sls { bool repair_down_str_replace(app* e); bool repair_down_str_prefixof(app* e); bool repair_down_str_suffixof(app* e); + bool repair_down_str_itos(app* e); + bool repair_down_str_stoi(app* e); void repair_up_str_length(app* e); void repair_up_str_indexof(app* e); + void repair_up_str_itos(app* e); + void repair_up_str_stoi(app* e); bool is_seq_predicate(expr* e); diff --git a/src/smt/theory_sls.cpp b/src/smt/theory_sls.cpp index f9234f75d..2737c6ee9 100644 --- a/src/smt/theory_sls.cpp +++ b/src/smt/theory_sls.cpp @@ -76,6 +76,10 @@ namespace smt { return ctx.get_num_bool_vars(); } + void theory_sls::init_search_eh() { + m_init_search = true; + } + void theory_sls::finalize() { if (!m_smt_plugin) return; @@ -84,11 +88,14 @@ namespace smt { m_smt_plugin->finalize(m_model); m_model = nullptr; m_smt_plugin = nullptr; + m_init_search = false; } void theory_sls::propagate() { - if (!m_smt_plugin) + if (!m_init_search) return; + if (!m_smt_plugin) + m_smt_plugin = alloc(sls::smt_plugin, * this); if (!m_checking) { expr_ref_vector fmls(m); for (unsigned i = 0; i < ctx.get_num_asserted_formulas(); ++i) @@ -104,6 +111,7 @@ namespace smt { m_smt_plugin->collect_statistics(m_st); m_smt_plugin->finalize(m_model); m_smt_plugin = nullptr; + m_init_search = false; } } @@ -183,8 +191,9 @@ namespace smt { finalize(); smt_params p(ctx.get_fparams()); m_parallel_mode = p.m_sls_parallel; - m_smt_plugin = alloc(sls::smt_plugin, *this); + m_smt_plugin = nullptr; m_checking = false; + m_init_search = false; } void theory_sls::collect_statistics(::statistics& st) const { @@ -216,6 +225,7 @@ namespace smt { m_smt_plugin->collect_statistics(m_st); m_smt_plugin->finalize(m_model); m_smt_plugin = nullptr; + m_init_search = false; } } diff --git a/src/smt/theory_sls.h b/src/smt/theory_sls.h index f58510522..187d8a124 100644 --- a/src/smt/theory_sls.h +++ b/src/smt/theory_sls.h @@ -72,6 +72,7 @@ namespace smt { unsigned m_after_resolve_decide_count = 0; unsigned m_resolve_count = 0; unsigned m_resolve_gap = 0; + bool m_init_search = false; ::statistics m_st; vector m_shared_clauses; @@ -125,6 +126,7 @@ namespace smt { void inc_activity(sat::bool_var v, double inc) override; bool parallel_mode() const override { return m_parallel_mode; } bool get_smt_value(expr* v, expr_ref& value) override; + void init_search_eh() override; };