Skip to content

Conversation

@FelixKrayer
Copy link
Contributor

Copied from PR #1611 by @arkocal
The simplified warrowing solver

As to which solver we should keep as the simplified version, this one:

  1. Can be documented a little more for didactic purposes, but I find it to be very readable as is.
  2. We should find the paper most closely matching this solver.
  3. This one does not pass all tests due to narrowing.

I created this pullrequest so I can address comments and do changes.
Addressing comments by @sim642 :

  1. removed remove-wpoint option. Having this option is not necessary for this solver. However, I changed it to always remove wpoints, without checking the config, as this is the default setting in the config.
  2. solver data is no longer a record. There is no need for that
  3. moved query/side out. There is no real reason they were inside iterate, it was just the way it turned out after deleting
  4. TODO: decide if phases should be included. This solver does not have them, since the parallel solvers do not use them and it was created for comparison with those. However, for generalizing this solver I see the use of implementing the phases.

@michael-schwarz
Copy link
Member

@sim642 @arkocal: What is you take on phases or not?
I don't have a strong opinion here, but think we should move forward with merging this.

@arkocal
Copy link
Contributor

arkocal commented Dec 19, 2024

I am fine with either variant, so I would have a light preference to just proceed and merge. @sim642 had the point that the basic example should have a termination guarantee, which is reasonable, just not a deal breaker for me as I find warrowing a little more intuitive than phases.

tldr: I would keep it as is, but have no strong preference, so Simmo please feel free to override this if you do.

@FelixKrayer FelixKrayer marked this pull request as ready for review December 19, 2024 12:34
@sim642 sim642 added this to the v2.6.0 milestone Jan 3, 2025
@sim642 sim642 merged commit ef56bc7 into goblint:master Jan 3, 2025
11 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants