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

Jump to bottom

[Condition Based Refinement] Runtime Improvements #393

Closed
ebehner opened this issue Mar 4, 2024 · 2 comments · Fixed by #394
Closed

[Condition Based Refinement] Runtime Improvements #393

ebehner opened this issue Mar 4, 2024 · 2 comments · Fixed by #394
Assignees
@ebehner
Labels
feature-request New feature or request

Comments

@ebehner
Copy link
Collaborator

ebehner commented Mar 4, 2024

Proposal

The Condition Based refinement sometime takes 65% of the runtime (total time ~5 minutes) and sometimes only 11% (total time ~1minute) on the same sample. This should not happen. It seems that in the case this optimization need 65% of the time, that z3 does not fully simplify a condition, and we end up with computing 511 sub-expression. We should never compute this many sub-expression, but the stage should also be more independent of the success of the simplification of z3.

Approach

  1. Make the stage less dependent on the simplification of z3
  2. Make sure that we do not compute too many sub-expression, i.e., find a better way to only consider the sub-expression that make sense in the current content, and probably also not compute all at once, because we only use one, the first that fits.
@ebehner ebehner added the feature-request New feature or request label Mar 4, 2024
@ebehner ebehner self-assigned this Mar 4, 2024
@ebehner
Copy link
Collaborator Author

ebehner commented Mar 4, 2024

/cib

@github-actions GitHub Actions
Copy link
Contributor

github-actions bot commented Mar 4, 2024

Branch issue-393-_Condition_Based_Refinement_Runtime_Improvements created!

github-actions bot added a commit that referenced this issue Mar 4, 2024
@github-actions
Create draft PR for #393
03f2fcc
@github-actions github-actions bot mentioned this issue Mar 4, 2024
Merged
ebehner pushed a commit that referenced this issue Mar 13, 2024
@github-actions @ebehner
Create draft PR for #393
5902fa4
ebehner pushed a commit that referenced this issue Mar 28, 2024
@github-actions @ebehner
Create draft PR for #393
f52c557
0x6e62 added a commit that referenced this issue Apr 11, 2024
@github-actions @ebehner @0x6e62
[Condition Based Refinement] Runtime Improvements (#394)
d8d7671 
* Create draft PR for #393

* start with some tests for improving the runtime

* some remarks and changes

* some progress

* try to improve runtime

* update simplify and class for finding next subexpression

* minor remarks

* add version where we go in children order

* some cleanup and formatting

* try with graph to avoid unnecessary conditions

* some refactoring

* try something else

* another option

* some cleanup

* minor updates

* add docstrings

* try to add all information to the graph

* some refactroing to fulfill PR remarks

* some minor fixes

* fix imports

* update docstrings

* apply MR suggestions

---------

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: Eva-Maria Behner <[email protected]>
Co-authored-by: Niklas Bergmann <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@ebehner ebehner

Labels
feature-request New feature or request
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

[Condition Based Refinement] Runtime Improvements fkie-cad/dewolf
1 participant
@ebehner