From 9d7ce8e779d47082319a67dd8ae3d9d5db6e9a0e Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Fri, 27 Dec 2024 14:29:41 +0100 Subject: [PATCH] Removed debug code --- 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 | 42 ++++------------------------------ 4 files changed, 8 insertions(+), 48 deletions(-) diff --git a/src/ast/sls/sat_ddfw.cpp b/src/ast/sls/sat_ddfw.cpp index c7e134910..4a4c27159 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(); // decrease the number of unsatisfied clauses found so far + m_min_sz = m_unsat.size(); } unsigned h = value_hash(); diff --git a/src/ast/sls/sat_ddfw.h b/src/ast/sls/sat_ddfw.h index 62271cade..6f3386a05 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; // set of unsat clauses + indexed_uint_set m_unsat; 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; // the least number of unsatisfied clauses found so far + unsigned m_min_sz = UINT_MAX; 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 90a8faf51..b177bfb0c 100644 --- a/src/ast/sls/sls_context.cpp +++ b/src/ast/sls/sls_context.cpp @@ -196,9 +196,7 @@ 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()); @@ -212,10 +210,8 @@ 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) { - std::cout << "enforcing repair up: " << mk_pp(e, m) << std::endl; + if (p) p->repair_up(to_app(e)); - } } } } @@ -265,7 +261,6 @@ 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); } @@ -563,7 +558,6 @@ 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 42cdfddfa..86938c6f8 100644 --- a/src/ast/sls/sls_seq_plugin.cpp +++ b/src/ast/sls/sls_seq_plugin.cpp @@ -114,7 +114,6 @@ namespace sls { auto e = ctx.atom(lit.var()); if (!is_seq_predicate(e)) return; - std::cout << "propagate_literal: " << mk_pp(e, m) << std::endl; if (bval1(e) != lit.sign()) return; // Literal not currently satisfied => report back to context @@ -190,13 +189,10 @@ 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]); @@ -253,10 +249,6 @@ 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; } @@ -270,17 +262,11 @@ 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 + // Gets the currently 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; } @@ -300,7 +286,6 @@ 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)); @@ -315,7 +300,6 @@ 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()) { @@ -364,7 +348,6 @@ namespace sls { zstring const& seq_plugin::strval1(expr* 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; @@ -395,7 +378,6 @@ 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: { @@ -499,7 +481,6 @@ 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)) @@ -521,7 +502,6 @@ 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)) @@ -691,38 +671,30 @@ 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 }); - std::cout << "edit candidate: " << mk_pp(x, m) << " -> " << a + zstring(ch) << std::endl; - } - for (auto ch : chars) { + for (auto ch : chars) m_str_updates.push_back({ x, zstring(ch) + a, 1 }); - 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 - 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 - 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; } } } @@ -744,7 +716,6 @@ 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; @@ -977,8 +948,6 @@ 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); @@ -1517,8 +1486,6 @@ namespace sls { for (auto ch : value0) chars.insert(ch); - std::cout << "repair concat " << mk_pp(e, m) << " " << value << " " << value0 << std::endl; - add_edit_updates(es, value, value0, chars); unsigned diff = edit_distance(value, value0); @@ -1655,7 +1622,6 @@ 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))