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.

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

Clean up destabilize_vs #1434

Merged
merged 1 commit into from
Jun 3, 2024
Merged

Conversation

Red-Panda64
Copy link
Contributor

Problem

See #1433

Proposed Fix

Remove destabilize_vs. To replace its functionality, add an optional callback to all destabilize functions, allowing the caller to perform the check whether the global destabilized a stable start variable or a called variable when needed without a dedicated destabilize implementation. This way, the additional overhead of going through the start variables check only occurs in side with the "cycle" strategy, just as before.

@sim642 sim642 self-requested a review April 25, 2024 09:26
@sim642 sim642 added the cleanup label Apr 25, 2024
@sim642 sim642 linked an issue Apr 25, 2024 that may be closed by this pull request
@sim642 sim642 changed the title clean up destabilize_vs Clean up destabilize_vs Apr 25, 2024
Copy link
Member

@michael-schwarz michael-schwarz left a comment

Choose a reason for hiding this comment

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

Nice! This is definitely an improvement over the state before where we risked things going out of sync frequently.

@@ -496,16 +489,19 @@ module Base =
(* solve x Widen *)
in

let rec destabilize_normal x =
let rec destabilize_normal ?(notify_destabilized = fun _ _ _ -> ()) x =
Copy link
Member

Choose a reason for hiding this comment

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

Since the fun argument does not change between invocations it might make sense to have an inner recursive function that does not have this parameters but uses the one from the outside scope.

Copy link
Member

@sim642 sim642 left a comment

Choose a reason for hiding this comment

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

This seems a bit premature to me. It's not clear whether the original reasons for separating this are no longer valid or not.

src/solver/td3.ml Outdated Show resolved Hide resolved
src/solver/td3.ml Outdated Show resolved Hide resolved
@michael-schwarz
Copy link
Member

We should add the hook & simplify the control flow and then we can merge it. The other change we do not want to merge for now.

@Red-Panda64
Copy link
Contributor Author

Apologies, I had forgotten this was still open. It is now reduced to unwrapping the obscured control flow around || and the hook call.

@sim642 sim642 added this to the v2.4.0 milestone Jun 3, 2024
@sim642 sim642 merged commit 06a2fa7 into goblint:master Jun 3, 2024
11 of 12 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.

Dubious code duplication in destabilize_vs
3 participants