mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-20 23:56:37 +00:00
Code Activity

Removed debug code

Browse source
This commit is contained in:
CEisenhofer 2024-12-27 14:29:41 +01:00
parent 2a0c1dce18
commit 9d7ce8e779
4 changed files with 8 additions and 48 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/sls/sat_ddfw.cpp
View file

@ -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();

4
src/ast/sls/sat_ddfw.h
View file

@ -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<unsigned> m_models;
stopwatch m_stopwatch;
unsigned_vector m_num_models;

8
src/ast/sls/sls_context.cpp
View file

@ -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);

42
src/ast/sls/sls_seq_plugin.cpp
View file

@ -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<expr> 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))