Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix model generation with SatML #832

Closed
wants to merge 22 commits into from
Closed

Fix model generation with SatML #832

wants to merge 22 commits into from

Commits on Sep 22, 2023

  1. Theory: harden 'compute_concrete_model' function

    @iguerNL @Halbaroth
    iguerNL authored and Halbaroth committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    631749b View commit details
    Browse the repository at this point in the history

  2. Push the test 'get_case_split_policy() == origin' into Theory.do_case… 

    …_split
    @iguerNL @Halbaroth
    iguerNL authored and Halbaroth committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    68595c8 View commit details
    Browse the repository at this point in the history

  3. CS: functions return all the env instead of just 'gamma_finite'.

    @iguerNL @Halbaroth
    iguerNL authored and Halbaroth committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    fad35b2 View commit details
    Browse the repository at this point in the history

  4. Fun_sat: refactor the way models are handled/printed 

    - add a data-structure for models,
- save the strucutre in the SAT's env
- print the models in the Frontend module
    @iguerNL @Halbaroth
    iguerNL authored and Halbaroth committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    227b393 View commit details
    Browse the repository at this point in the history

  5. satML: add missing case-split strategies

    @iguerNL @Halbaroth
    iguerNL authored and Halbaroth committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    e29fd5a View commit details
    Browse the repository at this point in the history

  6. satML: implement models generation.

    @iguerNL @Halbaroth
    iguerNL authored and Halbaroth committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    d033751 View commit details
    Browse the repository at this point in the history

  7. Make model tests negative 

    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
    Halbaroth committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    8d619a4 View commit details
    Browse the repository at this point in the history

  8. Reindent

    @Halbaroth
    Halbaroth committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    500870a View commit details
    Browse the repository at this point in the history

  9. Update documentation about output_concrete_model 

    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
    Halbaroth committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    5dcd64d View commit details
    Browse the repository at this point in the history

  10. Document the timeout_reason ADT

    @Halbaroth
    Halbaroth committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    d2422fd View commit details
    Browse the repository at this point in the history

  11. poetry

    @Halbaroth
    Halbaroth committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    d99addb View commit details
    Browse the repository at this point in the history

  12. Restore the comment about reinit_cpt

    @Halbaroth
    Halbaroth committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    6dc2fa5 View commit details
    Browse the repository at this point in the history

  13. Fix spelling

    @Halbaroth
    Halbaroth committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    d26bb62 View commit details
    Browse the repository at this point in the history

  14. Remainder to the issue 834

    @Halbaroth
    Halbaroth committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    ee53ad7 View commit details
    Browse the repository at this point in the history

  15. Simplify get-model processing

    @Halbaroth
    Halbaroth committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    8a00a07 View commit details
    Browse the repository at this point in the history

  16. Remove SAT solver choices while model generating 

    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)`.
    @Halbaroth
    Halbaroth committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    be61e56 View commit details
    Browse the repository at this point in the history

  17. Fix model output 

    We should print constraints in models only if the appropriate flag is
used in the command line.
    @Halbaroth
    Halbaroth committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    1140a2b View commit details
    Browse the repository at this point in the history

  18. All the model tests are positive

    @Halbaroth
    Halbaroth committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    95eb40d View commit details
    Browse the repository at this point in the history

  19. Remove deprecated cram tests 

    Some cram tests are not valid anymore as we don't need to select the SAT
solver Tableaux while generating models.
    @Halbaroth
    Halbaroth committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    fe6bead View commit details
    Browse the repository at this point in the history

  20. Test models with all the SAT solvers

    @Halbaroth
    Halbaroth committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    c4c602c View commit details
    Browse the repository at this point in the history

  21. Restoring dump-models option 

    The dump-models option have been broken by the refactoring in OptimAE.
I restore this feature.
    @Halbaroth
    Halbaroth committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    8db76ae View commit details
    Browse the repository at this point in the history

  22. Use the right post-solve SAT environment for models 

    Return the appropriate environment in the Frontend module to
retrieve the model with `(get-model)` as we did in the PR OCamlPro#789.
    @Halbaroth
    Halbaroth committed Sep 22, 2023
    Configuration menu
    Copy the full SHA
    028bb58 View commit details
    Browse the repository at this point in the history