From 2a0c1dce188163e83db6c2847a610978dc1e1980 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Fri, 27 Dec 2024 13:54:29 +0100 Subject: [PATCH] Fixed spurious counterexamples in seq-sls. Updates might not be identity mapping --- src/ast/sls/sat_ddfw.cpp | 2 +- src/ast/sls/sat_ddfw.h | 4 +- src/ast/sls/sls_context.cpp | 8 +++- src/ast/sls/sls_seq_plugin.cpp | 76 ++++++++++++++++++++++++++++------ src/ast/sls/sls_seq_plugin.h | 2 +- 5 files changed, 74 insertions(+), 18 deletions(-) diff --git a/src/ast/sls/sat_ddfw.cpp b/src/ast/sls/sat_ddfw.cpp index 4a4c27159..c7e134910 100644 --- a/src/ast/sls/sat_ddfw.cpp +++ b/src/ast/sls/sat_ddfw.cpp @@ -419,7 +419,7 @@ namespace sat { if (m_unsat.size() < m_min_sz) { m_models.reset(); - m_min_sz = m_unsat.size(); + m_min_sz = m_unsat.size(); // decrease the number of unsatisfied clauses found so far } unsigned h = value_hash(); diff --git a/src/ast/sls/sat_ddfw.h b/src/ast/sls/sat_ddfw.h index 6f3386a05..62271cade 100644 --- a/src/ast/sls/sat_ddfw.h +++ b/src/ast/sls/sat_ddfw.h @@ -92,7 +92,7 @@ namespace sat { unsigned m_use_list_vars = 0, m_use_list_clauses = 0; lbool m_last_result = l_true; - indexed_uint_set m_unsat; + indexed_uint_set m_unsat; // set of unsat clauses indexed_uint_set m_unsat_vars; // set of variables that are in unsat clauses random_gen m_rand; uint64_t m_last_flips_for_shift = 0; @@ -100,7 +100,7 @@ namespace sat { unsigned m_restart_count = 0, m_reinit_count = 0; uint64_t m_restart_next = 0, m_reinit_next = 0; uint64_t m_flips = 0, m_last_flips = 0, m_shifts = 0; - unsigned m_min_sz = UINT_MAX; + unsigned m_min_sz = UINT_MAX; // the least number of unsatisfied clauses found so far u_map m_models; stopwatch m_stopwatch; unsigned_vector m_num_models; diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp index b177bfb0c..90a8faf51 100644 --- a/src/ast/sls/sls_context.cpp +++ b/src/ast/sls/sls_context.cpp @@ -196,7 +196,9 @@ namespace sls { if (is_app(e)) { auto p = m_plugins.get(get_fid(e), nullptr); ++m_stats.m_num_repair_down; + std::cout << "enforcing repair down: " << mk_pp(e, m) << std::endl; if (p && !p->repair_down(to_app(e)) && !m_repair_up.contains(e->get_id())) { + std::cout << "revert repair down: " << mk_pp(e, m) << std::endl; IF_VERBOSE(3, verbose_stream() << "revert repair: " << mk_bounded_pp(e, m) << "\n"); TRACE("sls", tout << "revert repair: " << mk_bounded_pp(e, m) << "\n"); m_repair_up.insert(e->get_id()); @@ -210,8 +212,10 @@ namespace sls { TRACE("sls", tout << "repair up " << mk_bounded_pp(e, m) << "\n"); if (is_app(e)) { auto p = m_plugins.get(get_fid(e), nullptr); - if (p) + if (p) { + std::cout << "enforcing repair up: " << mk_pp(e, m) << std::endl; p->repair_up(to_app(e)); + } } } } @@ -261,6 +265,7 @@ namespace sls { return; family_id fid = get_fid(a); auto p = m_plugins.get(fid, nullptr); + std::cout << "Propagating literal: " << mk_pp(a, m) << std::endl; if (p) p->propagate_literal(lit); } @@ -558,6 +563,7 @@ namespace sls { } void context::new_value_eh(expr* e) { + std::cout << "new_value: " << mk_pp(e, m) << std::endl; DEBUG_CODE( if (m.is_bool(e)) { auto v = m_atom2bool_var.get(e->get_id(), sat::null_bool_var); diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp index 9ed98d467..42cdfddfa 100644 --- a/src/ast/sls/sls_seq_plugin.cpp +++ b/src/ast/sls/sls_seq_plugin.cpp @@ -114,10 +114,11 @@ namespace sls { auto e = ctx.atom(lit.var()); if (!is_seq_predicate(e)) return; - auto a = to_app(e); + std::cout << "propagate_literal: " << mk_pp(e, m) << std::endl; if (bval1(e) != lit.sign()) return; - ctx.new_value_eh(e); + // Literal not currently satisfied => report back to context + ctx.new_value_eh(e); } expr_ref seq_plugin::get_value(expr* e) { @@ -189,10 +190,13 @@ namespace sls { } return true; } - + void seq_plugin::register_term(expr* e) { + std::cout << "register_term: " << mk_pp(e, m) << std::endl; if (seq.is_string(e->get_sort())) { + // assign the terms assumed value based on the evaluation of its arguments strval0(e) = strval1(e); + // store all characters introduced in the term for (unsigned i = 0; i < strval0(e).length(); ++i) m_chars.insert(strval0(e)[i]); @@ -249,6 +253,10 @@ namespace sls { seq.str.get_concat(x, ev.lhs); seq.str.get_concat(y, ev.rhs); } + // std::cout << "lhs(" << mk_pp(eq, m) << ") = "; + // for (int i = 0; i < ev.lhs.size(); i++) + // std::cout << mk_pp(ev.lhs[i], m) << " "; + // std::cout << std::endl; return ev.lhs; } @@ -262,10 +270,17 @@ namespace sls { ptr_vector const& seq_plugin::rhs(expr* eq) { lhs(eq); auto& e = get_eval(eq); + // std::cout << "rhs(" << mk_pp(eq, m) << ") = "; + // for (int i = 0; i < e.rhs.size(); i++) + // std::cout << mk_pp(e.rhs[i], m) << " "; + // std::cout << std::endl; return e.rhs; } + // Gets the assumed value for e zstring& seq_plugin::strval0(expr* e) { + if (!get_eval(e).is_value) + std::cout << "strval0(" << mk_pp(e, m) << ") = " << get_eval(e).val0.svalue << std::endl; SASSERT(seq.is_string(e->get_sort())); return get_eval(e).val0.svalue; } @@ -285,6 +300,7 @@ namespace sls { bool seq_plugin::bval1(expr* e) { + // std::cout << "bval1(" << mk_pp(e, m) << ")" << std::endl; SASSERT(is_app(e)); if (to_app(e)->get_family_id() == seq.get_family_id()) return bval1_seq(to_app(e)); @@ -299,6 +315,7 @@ namespace sls { } bool seq_plugin::bval1_seq(app* e) { + std::cout << "bval1_seq(" << mk_pp(e, m) << ")" << std::endl; expr* a, *b; SASSERT(e->get_family_id() == seq.get_family_id()); switch (e->get_decl_kind()) { @@ -343,10 +360,11 @@ namespace sls { return false; } + // Evaluate e using the assumed values of its arguments and cache + return the result zstring const& seq_plugin::strval1(expr* e) { - SASSERT(is_app(e)); SASSERT(seq.is_string(e->get_sort())); auto & ev = get_eval(e); + std::cout << "strval1(" << mk_pp(e, m) << ")" << std::endl; if (ev.is_value) return ev.val0.svalue; @@ -377,6 +395,7 @@ namespace sls { for (auto arg : *to_app(e)) r = r + strval0(arg); ev.val1.svalue = r; + std::cout << "strval1(" << mk_pp(e, m) << ") = " << ev.val1.svalue << std::endl; return ev.val1.svalue; } case OP_SEQ_EXTRACT: { @@ -480,6 +499,7 @@ namespace sls { } void seq_plugin::repair_up(app* e) { + std::cout << "repair_up(" << mk_pp(e, m) << ")" << std::endl; if (m.is_bool(e)) return; if (is_value(e)) @@ -501,6 +521,7 @@ namespace sls { } bool seq_plugin::repair_down(app* e) { + std::cout << "repair_down(" << mk_pp(e, m) << ")" << std::endl; if (m.is_bool(e) && bval1(e) == ctx.is_true(e)) return true; if (seq.is_string(e->get_sort()) && strval0(e) == strval1(e)) @@ -608,6 +629,7 @@ namespace sls { VERIFY(m.is_eq(e, x, y)); IF_VERBOSE(3, verbose_stream() << is_true << ": " << mk_bounded_pp(e, m, 3) << "\n"); if (ctx.is_true(e)) { + // equality if (false && ctx.rand(2) != 0 && repair_down_str_eq_edit_distance_incremental(e)) return true; if (ctx.rand(2) != 0 && repair_down_str_eq_edit_distance(e)) @@ -620,6 +642,7 @@ namespace sls { m_str_updates.push_back({ y, strval1(x), 1 }); } else { + // disequality if (!is_value(x) && !m_chars.empty()) { zstring ch(m_chars[ctx.rand(m_chars.size())]); m_str_updates.push_back({ x, strval1(y) + ch, 1 }); @@ -668,19 +691,40 @@ namespace sls { if (is_value(x)) continue; zstring const & a = strval0(x); - for (auto ch : chars) + for (auto ch : chars) { m_str_updates.push_back({ x, a + zstring(ch), 1 }); - for (auto ch : chars) + std::cout << "edit candidate: " << mk_pp(x, m) << " -> " << a + zstring(ch) << std::endl; + } + for (auto ch : chars) { m_str_updates.push_back({ x, zstring(ch) + a, 1 }); - if (a.length() > 0) { + std::cout << "edit candidate: " << mk_pp(x, m) << " -> " << zstring(ch) + a << std::endl; + } + if (!a.empty()) { zstring b = a.extract(0, a.length() - 1); + unsigned remC = a[a.length() - 1]; m_str_updates.push_back({ x, b, 1 }); // truncate a - for (auto ch : chars) + std::cout << "edit candidate: " << mk_pp(x, m) << " -> " << b << std::endl; + for (auto ch : chars) { + if (ch == remC) + // We would end up with the initial string + // => this "no-op" could be spuriously considered a solution (also it does not help) + continue; m_str_updates.push_back({ x, b + zstring(ch), 1 }); // replace last character in a by ch - b = a.extract(1, a.length() - 1); - m_str_updates.push_back({ x, b, 1 }); // truncate a - for (auto ch : chars) - m_str_updates.push_back({ x, zstring(ch) + b, 1 }); // replace first character in a by ch + std::cout << "edit candidate: " << mk_pp(x, m) << " -> " << b + zstring(ch) << std::endl; + } + if (a.length() > 1) { + // Otw. we just get the same set of candidates another time + b = a.extract(1, a.length() - 1); + remC = a[0]; + m_str_updates.push_back({ x, b, 1 }); // truncate a + std::cout << "edit candidate: " << mk_pp(x, m) << " -> " << b << std::endl; + for (auto ch : chars) { + if (ch == remC) + continue; + m_str_updates.push_back({ x, zstring(ch) + b, 1 }); // replace first character in a by ch + std::cout << "edit candidate: " << mk_pp(x, m) << " -> " << zstring(ch) + b << std::endl; + } + } } } unsigned first_diff = UINT_MAX; @@ -700,6 +744,7 @@ namespace sls { break; auto new_val = val_x.extract(0, first_diff) + zstring(val_other[first_diff]) + val_x.extract(first_diff + 1, val_x.length()); m_str_updates.push_back({ x, new_val, 1 }); + std::cout << "edit candidate: " << mk_pp(x, m) << " -> " << new_val << std::endl; break; } index -= len_x; @@ -932,6 +977,8 @@ namespace sls { b_chars.insert(ch); b += strval0(y); } + std::cout << "L: " << mk_pp_vec(L.size(), (ast**)L.data(), m) << " = " << "R: " << mk_pp_vec(R.size(), (ast**)R.data(), m) << std::endl; + std::cout << "a: " << a << " = " << "b: " << b << std::endl; if (a == b) return update(eq->get_arg(0), a) && update(eq->get_arg(1), b); @@ -1468,7 +1515,9 @@ namespace sls { uint_set chars; for (auto ch : value0) - chars.insert(ch); + chars.insert(ch); + + std::cout << "repair concat " << mk_pp(e, m) << " " << value << " " << value0 << std::endl; add_edit_updates(es, value, value0, chars); @@ -1606,6 +1655,7 @@ namespace sls { } bool seq_plugin::update(expr* e, zstring const& value) { + std::cout << "Update: " << mk_pp(e, m) << " := " << value << std::endl; if (value == strval0(e)) return true; if (is_value(e)) diff --git a/src/ast/sls/sls_seq_plugin.h b/src/ast/sls/sls_seq_plugin.h index cabfa6d9a..bd34b3449 100644 --- a/src/ast/sls/sls_seq_plugin.h +++ b/src/ast/sls/sls_seq_plugin.h @@ -47,7 +47,7 @@ namespace sls { seq_rewriter rw; th_rewriter thrw; scoped_ptr_vector m_values; - indexed_uint_set m_chars; + indexed_uint_set m_chars; // set of characters in the problem bool m_initialized = false; struct str_update {