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

Add padding if required

Browse source
This commit is contained in:
CEisenhofer 2024-12-30 19:25:06 +01:00
parent 0cfaf5ad92
commit 809267258d
1 changed files with 25 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -518,6 +518,8 @@ namespace sls {
return true;
if (seq.is_string(e->get_sort()) && strval0(e) == strval1(e))
return true;
SASSERT(!seq.is_string(e->get_sort()) || strval0(e).length() >= get_eval(e).min_length);
SASSERT(!seq.is_string(e->get_sort()) || strval0(e).length() <= get_eval(e).max_length);
if (e->get_family_id() == m_fid)
return repair_down_seq(e);
if (m.is_eq(e))
@ -1314,7 +1316,7 @@ namespace sls {
zstring new_x = sx;
while (new_x.length() < r)
new_x += zstring(!m_chars.empty() ? m_chars[ctx.rand(m_chars.size())] : zstring("a"));
new_x += se;
new_x = trunc_pad_to_fit(get_eval(x).min_length, get_eval(x).max_length, new_x + se);
m_str_updates.push_back({ x, new_x, 1 });
}
}
@ -1512,6 +1514,7 @@ namespace sls {
bool seq_plugin::repair_down_str_extract(app* e) {
expr* x, * offset, * len;
VERIFY(seq.str.is_extract(e, x, offset, len));
SASSERT(strval0(e) != strval1(e));
zstring v = strval0(e);
zstring r = strval0(x);
expr_ref offset_e = ctx.get_value(offset);
@ -1519,34 +1522,36 @@ namespace sls {
rational offset_val, len_val;
VERIFY(a.is_numeral(offset_e, offset_val));
VERIFY(a.is_numeral(len_e, len_val));
if (v.empty() && (offset_val.is_neg() || !len_val.is_pos()))
return true;
// std::cout << "repair extract " << mk_bounded_pp(e, m) << " := \"" << v << "\"" << std::endl;
// std::cout << "Args: \"" << r << "\" " << offset_val << " " << len_val << std::endl;
unsigned offset_u = offset_val.is_unsigned() ? offset_val.get_unsigned() : 0;
unsigned len_u = len_val.is_unsigned() ? len_val.get_unsigned() : 0;
bool has_empty = false;
if (offset_val.is_neg() || offset_val.get_unsigned() >= r.length()) {
m_str_updates.push_back({ e, zstring(), 1 });
has_empty = true;
for (unsigned i = 0; i < r.length(); i++)
m_int_updates.push_back({ offset, rational(i), 1 });
}
if (!len_val.is_pos()) {
m_str_updates.push_back({ e, zstring(), 1 });
for (unsigned i = 1; i < r.length() - offset_val.get_unsigned(); i++)
has_empty = true;
for (unsigned i = 1; i + offset_u < r.length(); i++)
m_int_updates.push_back({ len, rational(i), 1 });
}
if (offset_val.is_unsigned() && len_val.is_unsigned() && v == r.extract(offset_val.get_unsigned(), len_val.get_unsigned()))
return true;
SASSERT(offset_val.is_unsigned());
SASSERT(len_val.is_unsigned());
unsigned offset_u = offset_val.get_unsigned();
unsigned len_u = len_val.get_unsigned();
if (has_empty)
m_str_updates.push_back({ e, zstring(), 1 });
zstring prefix = r.extract(0, offset_u);
zstring suffix = r.extract(offset_u + len_u, r.length());
zstring new_r = prefix + v + suffix;
new_r = trunc_pad_to_fit(get_eval(x).min_length, get_eval(x).max_length, new_r);
if (new_r == r)
if (new_r != r)
m_str_updates.push_back({ x, new_r, 1 });
return apply_update();
@ -1672,7 +1677,9 @@ namespace sls {
if (is_str_update) {
auto [e, value, score] = m_str_updates[i];
// std::cout << "Trying str-update: " << mk_pp(e, m) << " := \"" << value << "\"" << std::endl;
if (update(e, value)) {
// std::cout << "Success" << std::endl;
IF_VERBOSE(3, verbose_stream() << "set value " << mk_bounded_pp(e, m) << " := \"" << value << "\"\n");
m_str_updates.reset();
m_int_updates.reset();
@ -1688,7 +1695,9 @@ namespace sls {
IF_VERBOSE(3, verbose_stream() << "set value " << mk_bounded_pp(e, m) << " := " << value << "\n");
// std::cout << "Trying int-update: " << mk_pp(e, m) << " := " << value << std::endl;
if (update(e, value)) {
// std::cout << "Success" << std::endl;
m_int_updates.reset();
m_str_updates.reset();
return true;
@ -1699,12 +1708,13 @@ namespace sls {
}
}
std::cout << "No candidate found" << std::endl;
return false;
}
bool seq_plugin::update(expr* e, zstring const& value) {
SASSERT(value != strval0(e));
std::cout << "update " << mk_pp(e, m) << " := \"" << value << "\" [\"" << strval0(e) << "\"]" << std::endl;
// std::cout << "str-update " << mk_pp(e, m) << " := \"" << value << "\" [\"" << strval0(e) << "\"]" << std::endl;
// if (value == strval0(e))
// return true;
if (is_value(e))