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

Added case for str.at

Browse source
This commit is contained in:
CEisenhofer 2024-12-30 14:20:18 +01:00
parent 30ffedd46a
commit 9f08f1f228
1 changed files with 6 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1222,16 +1222,13 @@ 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);
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.
@ -1251,7 +1248,11 @@ namespace sls {
// index should be in bounds of a. // index should be in bounds of a.
if (!is_value(x)) { if (!is_value(x)) {
if (lenx > r && r >= 0) { if (lenx > r && r >= 0) {
zstring new_x = sx.extract(0, r.get_unsigned()) + se + sx.extract(r.get_unsigned() + 1, lenx); // insert or replace the desired character
zstring p = sx.extract(0, r.get_unsigned()) + se;
zstring new_x = p + sx.extract(r.get_unsigned() + 1, lenx - (r.get_unsigned() + 1));
m_str_updates.push_back({ x, new_x, 1 });
new_x = p + sx.extract(r.get_unsigned(), lenx - r.get_unsigned());
m_str_updates.push_back({ x, new_x, 1 }); m_str_updates.push_back({ x, new_x, 1 });
} }
else { else {
@ -1563,6 +1564,7 @@ namespace sls {
bool seq_plugin::apply_update() { bool seq_plugin::apply_update() {
SASSERT(!m_str_updates.empty() || !m_int_updates.empty());
double sum_scores = 0; double sum_scores = 0;
for (auto const& [e, val, score] : m_str_updates) for (auto const& [e, val, score] : m_str_updates)
sum_scores += score; sum_scores += score;