Fix model generation with SatML #832
Closed
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
- add a data-structure for models, - save the strucutre in the SAT's env - print the models in the Frontend module
Some tests about models failed in the OptimAE PR. This commit allows to tag tests in `tests/` with `fail` tag which means the test is supposed to fail.
Halbaroth
force-pushed
the
fix-model-generation-satml
branch
from
feea304
to
7ed39b7
Compare
I also remove the mention about the different kind of formats used to print models. Indeed, we use only the SMT-LIB format and the Why3 format is slightly different but probably outdated.
Halbaroth
force-pushed
the
fix-model-generation-satml
branch
from
1164290
to
c4c602c
Compare
As SatML supports model generation, we don't need to select the appropriate SAT solver while parsing the command line or the SMT-LIB statement `(set-option :produce-models true)`.
We should print constraints in models only if the appropriate flag is used in the command line.
Some cram tests are not valid anymore as we don't need to select the SAT solver Tableaux while generating models.
The dump-models option have been broken by the refactoring in OptimAE. I restore this feature.
Return the appropriate environment in the Frontend module to retrieve the model with `(get-model)` as we did in the PR OCamlPro#789.
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 PR restores the model generation tests.
The PR starts with the commit 2619445.
Please merge this PR just after #829 and before #776.