Refactor goblint.constraint dune library#1745
Merged
sim642 merged 11 commits intogoblint:masterfrom May 16, 2025
Merged
Conversation
Since this is the simplest case that other (semantically) built upon, it is easier to understand when its first read
arkocal
commented
May 15, 2025
arkocal
commented
May 15, 2025
arkocal
commented
May 15, 2025
arkocal
commented
May 15, 2025
Contributor
Author
|
I have unwrapped the module, as it was marked as TODO in the dune file. Now I see there are also other modules that have this. Should we still proceed with that. I think it with submodules it becomes a bit more important to not pollute the global namespace. If so, what is the right way to go about the documentation here? ps. Since most things defined here are types anyway, I did not create |
Member
I did some fixes to the wrapped |
goblint.constraint dune library
michael-schwarz
approved these changes
May 16, 2025
sim642
approved these changes
May 16, 2025
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR should implement what is already in #1743 , while also providing lifters so that not all solvers must be modified. It should also make sure this is in line with the work on
createnodes for concurrent solvers.While going through the complete file to make sure everything is done at the right place, I have realized that some complexity has grown here and it would make sense to remove some complexity before introducing some, so I will keep this running as a draft, but feel free to drop comments if you disagree with any of the changes or want to discuss anything.
Every commit should be more or less self contained.