mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-23 19:47:52 +00:00
Code Activity

Fix sls for str.at

Browse source
This commit is contained in:
CEisenhofer 2024-12-30 14:03:37 +01:00
parent 602d97f29e
commit 30ffedd46a
1 changed files with 8 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1222,14 +1222,16 @@ namespace sls {
expr* x, * y; expr* x, * y;
VERIFY(seq.str.is_at(e, x, y)); VERIFY(seq.str.is_at(e, x, y));
zstring se = strval0(e); zstring se = strval0(e);
verbose_stream() << "repair down at " << mk_pp(e, m) << " " << se << "\n"; std::cout << "repair down at " << mk_pp(e, m) << " = " << se << std::endl;
if (se.length() > 1) if (se.length() > 1)
return false; return false;
zstring sx = strval0(x); zstring sx = strval0(x);
std::cout << mk_pp(x, m) << " = " << sx << std::endl;
unsigned lenx = sx.length(); unsigned lenx = sx.length();
expr_ref idx = ctx.get_value(y); expr_ref idx = ctx.get_value(y);
rational r; rational r;
VERIFY(a.is_numeral(idx, r)); VERIFY(a.is_numeral(idx, r));
std::cout << mk_pp(y, m) << " = " << r << std::endl;
if (se.length() == 0) { if (se.length() == 0) {
// index should be out of bounds of a. // index should be out of bounds of a.
@ -1252,8 +1254,11 @@ namespace sls {
zstring new_x = sx.extract(0, r.get_unsigned()) + se + sx.extract(r.get_unsigned() + 1, lenx); zstring new_x = sx.extract(0, r.get_unsigned()) + se + sx.extract(r.get_unsigned() + 1, lenx);
m_str_updates.push_back({ x, new_x, 1 }); m_str_updates.push_back({ x, new_x, 1 });
} }
if (lenx <= r) { else {
zstring new_x = sx + se; zstring new_x = sx;
while (new_x.length() < r)
new_x += zstring(m_chars[ctx.rand(m_chars.size())]);
new_x += se;
m_str_updates.push_back({ x, new_x, 1 }); m_str_updates.push_back({ x, new_x, 1 });
} }
} }