[models] Add tests for model generation #703
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
|
Uh, looks like some of the expected files are empty, not sure what's going on |
This updates the [gentest] tool to be able to add tests for model generation.
bclement-ocp
force-pushed
the
model_tests
branch
from
f8d32ee
to
f712cc7
Compare
There are regressions otherwise, see OCamlPro#704
|
Did you promote them with |
|
No I just messed up a rule in |
Halbaroth
approved these changes
Jun 27, 2023
Merged
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.
This updates the [gentest] tool to be able to add tests for model generation.
Note that while writing this I noticed:
check_satin the Alt-Ergo language (the models are not printed, unless--dump-modelis provided)check_satwith Alt-Ergo or(check-sat-assuming)for smtlib2, we are not actually taking into consideration the assumptions when printing the model and print the pre-solve model. Or something similar (the gist of it is thatprocess_decldiscards the generated model). I will make separate PRs for these.