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

Fixed spurious counterexamples in seq-sls. Updates might not be identity mapping

Browse source
This commit is contained in:
CEisenhofer 2024-12-27 13:54:29 +01:00
parent 5eb71c3be6
commit 2a0c1dce18
5 changed files with 74 additions and 18 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();
m_min_sz = m_unsat.size(); // decrease the number of unsatisfied clauses found so far
}
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;
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<unsigned> m_models;
stopwatch m_stopwatch;
unsigned_vector m_num_models;

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

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

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

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

2
src/ast/sls/sls_seq_plugin.h
View file

@ -47,7 +47,7 @@ namespace sls {
seq_rewriter rw;
th_rewriter thrw;
scoped_ptr_vector<eval> 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 {