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
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.
Currently the
solve()method on theIDESolvercannot 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,nextandfinalize. They are being called according to the below flow-chart:In addition to these basic APIs there are convenience functions like
solveUntil,solveWithTimeout, etc. that build upon this model. The originalsolvemethod 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.