mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-23 11:37:54 +00:00
Code Activity

Added missing progressing cases in extraction

Browse source
This commit is contained in:
CEisenhofer 2024-12-30 17:56:43 +01:00
parent d54e54580d
commit 0227cebee4
1 changed files with 7 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1484,16 +1484,14 @@ namespace sls {
m_str_updates.push_back({ e, zstring(), 1 }); m_str_updates.push_back({ e, zstring(), 1 });
for (unsigned i = 0; i < r.length(); i++) for (unsigned i = 0; i < r.length(); i++)
m_int_updates.push_back({ offset, rational(i), 1 }); m_int_updates.push_back({ offset, rational(i), 1 });
return apply_update();
} }
if (!len_val.is_pos()) { if (!len_val.is_pos()) {
m_str_updates.push_back({ e, zstring(), 1 }); m_str_updates.push_back({ e, zstring(), 1 });
for (unsigned i = 0; i < r.length() - offset_val.get_unsigned(); i++) for (unsigned i = 1; i < r.length() - offset_val.get_unsigned(); i++)
m_int_updates.push_back({ len, rational(i), 1 }); m_int_updates.push_back({ len, rational(i), 1 });
return apply_update();
} }
if (v == r.extract(offset_val.get_unsigned(), len_val.get_unsigned())) if (offset_val.is_unsigned() && len_val.is_unsigned() && v == r.extract(offset_val.get_unsigned(), len_val.get_unsigned()))
return true; return true;
SASSERT(offset_val.is_unsigned()); SASSERT(offset_val.is_unsigned());
@ -1504,14 +1502,12 @@ namespace sls {
zstring prefix = r.extract(0, offset_u); zstring prefix = r.extract(0, offset_u);
zstring suffix = r.extract(offset_u + len_u, r.length()); zstring suffix = r.extract(offset_u + len_u, r.length());
zstring new_r = prefix + v + suffix; zstring new_r = prefix + v + suffix;
std::cout << "repair extract " << mk_bounded_pp(e, m) << " \"" << v << "\"" << std::endl;
std::cout << "\"" << r << "\" " << offset_val << " " << len_val << std::endl;
new_r = trunc_pad_to_fit(get_eval(x).min_length, get_eval(x).max_length, new_r); new_r = trunc_pad_to_fit(get_eval(x).min_length, get_eval(x).max_length, new_r);
std::cout << new_r << std::endl; if (new_r == r)
m_str_updates.push_back({ x, new_r, 1 }); m_str_updates.push_back({ x, new_r, 1 });
return apply_update(); return apply_update();
} }
@ -1667,6 +1663,7 @@ namespace sls {
bool seq_plugin::update(expr* e, zstring const& value) { bool seq_plugin::update(expr* e, zstring const& value) {
SASSERT(value != strval0(e)); SASSERT(value != strval0(e));
std::cout << "update " << mk_pp(e, m) << " := \"" << value << "\" [\"" << strval0(e) << "\"]" << std::endl;
// if (value == strval0(e)) // if (value == strval0(e))
// return true; // return true;
if (is_value(e)) if (is_value(e))