Fixes several model printing bugs (and more) #584
Merged
Conversation
This file contains 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
…(in terms of the internal domain constants)
…e monotonicity information back to FiniteModelBuilder
…Functions, we now also pass the result back to FiniteModelBuilder
…full solution will come later
…me into play) fixes (hopefully fully) issue #477
…into bool, let's prevent this for the future by making the SATSolver enums classes
…offset computed for it
quickbeam123
force-pushed
the
martin-fix-fmb
branch
from
fab203b
to
65a3a4e
Compare
quickbeam123
force-pushed
the
martin-fix-fmb
branch
from
65a3a4e
to
5a8aa15
Compare
MichaelRawson
approved these changes
Aug 5, 2024
|
I've mostly just asked for some explanatory comments...once you've done what you are willing to do go ahead and merge. |
This was
linked to
issues
Aug 5, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Quite a few changes in FiniteModelBuilder and around with the ultimate aim of Vampire being able to correctly model-check all finite models it generates.
This PR achieves this goal for inputs in CNF and under
fde=none:erd=off:updr=off:bce=off- (This means we verify models we output, but so far only for strategies which don't manipulate the signature or eliminate things.)The next step will be to support undoing these elimination operations and making the model work for the original input (and to do the corresponding operations also for saturations, where we will simply dump the definitions of the eliminated symbols to document how one could recover a model, if they had one.)