Skip to content

Conversation

@fabianbs96
Copy link
Member

@fabianbs96 fabianbs96 commented Jun 28, 2023

Currently the solve() method on the IDESolver cannot be interrupted once started. This is not problem for analyzing small target programs, but is unacceptable for larger analyses that may run for days.

This PR adds fine-grained control over the solving process while still abstracting the solver internals.

The abstraction consists of three basic functions: initialize, next and finalize.
They are being called according to the below flow-chart:

flowchart LR
  initialize-->|true| next
  initialize-->|false| finalize
  next-->|true| next
  next -->|false|finalize
Loading

In addition to these basic APIs there are convenience functions like solveUntil, solveWithTimeout, etc. that build upon this model.
The original solve method has been rewritten and makes use of this model as well while keeping its original semantics.

Further, the solving methods (including finalize) now return a view into the solver results (or owning solver-results when called with an rvalue-reference) for allowing to be used in a more fluent way.

@fabianbs96 fabianbs96 added the enhancement New feature or request label Jun 28, 2023
@fabianbs96 fabianbs96 requested a review from MMory as a code owner June 28, 2023 16:58
@fabianbs96 fabianbs96 self-assigned this Jun 28, 2023
Copy link
Member

@MMory MMory left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

lgtm, it is good to have this, thank you!

@MMory MMory merged commit c6417d9 into development Jun 29, 2023
@MMory MMory deleted the f-InteractiveIDESolver branch June 29, 2023 11:54
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

enhancement New feature or request

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants