Support get-value statement
#1032
Open
Commits on Aug 16, 2024
-
Keep partial models in with a separate key
We keep the last consistent SAT environment with the Dolmen key `partial_model` in `Solving_loop`. This solution isn't sufficient to implement correctly `get-value`. Indeed, we need to ensure `get-model` statements located after some `get-value` statements will still print the same model. To obtain this behaviour, now we keep the last model and the last unknown reason after a `check-sat` in a separate key. Support `get-value` in Solving_loop Add support for the SMT-LIB statement `get-value` in `Solving_loop`. With the current implementation of the solver, it's not easy to keep a consistent environment of the SAT solver without reassuming all the formulas as we do in `Solving_loop`. Instead, we save the last consistent environment obtained after a `check-sat` statement in the Dolmen state and we have to keep the last model and unknown reason with different keys. Indeed, after using `get-value`, the `get-model` statement has to output the same model. Create a new type name in `Symbols` Refactoring `get-value` support This commit adds a better support of `get-value` and `get-assignment`. These features are implemented using a new wrapper functor on the top of the SAT solvers of Alt-Ergo. - Values for bool expressions are computed by the SAT solver; - Before launching the solver to compute some model terms, we check if there aren't already available in the boolean or first-order models; - Thanks to the wrapper functor, the feature works well with the legacy solver FunSAT; We also test our generated models by non-regression tests using the `get-value`. Add option `--verify-models` This option will be useful to check our models with the new `get-value` command. Adding `--verify-models` turns on the model generation (as we did with the `--produce-models` option). If our best-effort model checker doesn't find a contradiction, we don't print anything. fix documentation Add the location for get-value À la C Use first-class module instead of functor Add Expr.Core.of_bool Reinit GetValue cpt spelling Documentation of the module Graph Derive comparison function of name_space Restore the documentation of `name` Remove the joke :( Remove the joke :( New exception for wrong model We raise a new exception `Wrong_model` in `get_value` in order to clarify the API. Rebase artefacts Removing get-value statements to check models Add a new SMT option for the CLI option `--verify-models` Use `Stdcompat.Either` for OCaml 4.08 Reset decisions only for get-value statements We need to reset the decision level of SatML after calling the `unsat` function as the decision level of this solver isn't necessary zero. This hotfix is only necessary for SatML. Add a new function `reset_decisions` in the SAT API. Saved the boolean model before resetting decisions The call `SAT.reset_decisions` may erase part of the boolean models in `get_value`. For sake of efficiency, we save the boolean model before resetting decisions. Add tests Add a link to issue 1063 Address partially review
-
-
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.