Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Several changes to make sls terminate more often with length/extract operations #7498

Merged
merged 9 commits into from
Dec 30, 2024
Merged

Several changes to make sls terminate more often with length/extract operations #7498

Changes from 1 commit
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
602d97f
Fixed range regex
CEisenhofer Dec 30, 2024
30ffedd
Fix sls for str.at
CEisenhofer Dec 30, 2024
9f08f1f
Added case for str.at
CEisenhofer Dec 30, 2024
7c02410
Pad/Truncate string in sls extract/length to fit length constraints
CEisenhofer Dec 30, 2024
d54e545
Guarded index check
CEisenhofer Dec 30, 2024
0227ceb
Added missing progressing cases in extraction
CEisenhofer Dec 30, 2024
0cfaf5a
Merge remote-tracking branch 'microsoft/master' into eis-sls3
CEisenhofer Dec 30, 2024
8092672
Add padding if required
CEisenhofer Dec 30, 2024
c468ff4
Commented out debug output
CEisenhofer Dec 30, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Added case for str.at
  • Loading branch information
@CEisenhofer
CEisenhofer committed Dec 30, 2024
commit 9f08f1f2283edb93bea698272a5de9e7ade19f02
10 changes: 6 additions & 4 deletions src/ast/sls/sls_seq_plugin.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1222,16 +1222,13 @@ namespace sls {
expr* x, * y;
VERIFY(seq.str.is_at(e, x, y));
zstring se = strval0(e);
std::cout << "repair down at " << mk_pp(e, m) << " = " << se << std::endl;
if (se.length() > 1)
return false;
zstring sx = strval0(x);
std::cout << mk_pp(x, m) << " = " << sx << std::endl;
unsigned lenx = sx.length();
expr_ref idx = ctx.get_value(y);
rational r;
VERIFY(a.is_numeral(idx, r));
std::cout << mk_pp(y, m) << " = " << r << std::endl;

if (se.length() == 0) {
// index should be out of bounds of a.
Expand All @@ -1251,7 +1248,11 @@ namespace sls {
// index should be in bounds of a.
if (!is_value(x)) {
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 });
}
else {
Expand Down Expand Up @@ -1563,6 +1564,7 @@ namespace sls {


bool seq_plugin::apply_update() {
SASSERT(!m_str_updates.empty() || !m_int_updates.empty());
double sum_scores = 0;
for (auto const& [e, val, score] : m_str_updates)
sum_scores += score;
Expand Down