Models, rebased #530
Merged
Models, rebased #530
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
Gbury
requested changes
Nov 9, 2022
Gbury
requested changes
Nov 16, 2022
Halbaroth
reviewed
Nov 16, 2022
Stevendeo
force-pushed
the
models
branch
2 times, most recently
from
2500665 to
d3eff1d
Compare
… instead of valid as a result
…ds to be well understood before making it work for every case
…int model and interpretation
…ions and not just constants
Gbury
approved these changes
Nov 18, 2022
Halbaroth
pushed a commit
to Halbaroth/alt-ergo
that referenced
this pull request
Jan 24, 2023
Add model generation to alt-ergo * examples and initial draft report * attempt to fix CI: Seq dep missing to compile lib_usage test file * change version to models * models generation: add some examples * parent f3ad875 author OCamlPro-mattiasdrp <mattias@ocamlpro.com> 1591793503 +0200 committer OCamlPro-mattiasdrp <mattias@ocamlpro.com> 1593523267 +0200 Rebase from next * check sat handled on the lowest possible level, need to work on unsat instead of valid as a result * first prototype for models in Why3, lots of hard coded stuff that needs to be well understood before making it work for every case * Change interpretation option, use mdl-formatter to compute but not print model and interpretation * Style check * Move the printing of counterexample from uf.ml to models.ml * Prototype of printer for records in smt format * Directly use rep of bool value for counterexamples * fix destr list rev * Clean choose_adequate_model for boolean constant * Add `fast` option that disable greedier instantiation phase * remove greedier and get_fast in fun_sat * Prototype to output constraint as model if output is set to why3 * Remove `why3-counter-example` option, use `-o why3` instead * Code cleaning and addition of functions printing with cascade of ite * fix compatibility for ocaml version < 4.07 * Fix printing of some type in smtlib2 output format * Add an example which test some ce * Add support for record constuctor use in model * Add option dummy-value for interpretation that output _ instead of dummy fresh value when no value is computed * Fix pp_term and assert output prototype * Add factorisation in ite when values or the same * reeplace dummy_value with use_underscore option * remove fast option, use `--instantiation-heuristic=normal` instead * Copy print expr code in models for better management of named expr * [models] add case-split on internal bool terms Useful when/if the SAT don't see/assign internal bool expression and/or SAT assignement is not propagated to theories (eg. because of CDCL(Tableaux) filtering) * Type Expr.view should remain "private" * fix intendation * Expr.get_infos returns the view: to avoid uesless tuple allocation * refactor the way model is output from fun_sat it now goes through Theory instead of calling directly Uf * Rename interpretation option values to None First Last and Every * Fix interpretation_timelimit initialisation * auto set option "fm_cross_limit = -1" (ie. infinity) if models-gen is set. * Fix use_underscore_interpretation option * Remove deadcode from models and mv models.ml in frontend * Add some documentation in options.ml for type model, instanciation_heuristic and interpretation * Fix no-term-like-pp option comment * Fix model options * remove unused models-generation code (all, complete and default models) * remove functions related to old model * clean unused code * fix linter * Fix frontend output in case of timeout * Clean models, remove old native output, and remove ref for records * Move profile module from Models module to structures * Fix printing of constraints in why3 output when constraints are functions and not just constants * Fix declare-fun command in models * Uses printer instead of format in models comments * Better command line arguments * Style fix * Adding simple model option * Rebase artifacts * Putting model option in the right option list * Poetry * Fix parse command * Poetry * Adding a proper exception for unsupported features and removing 'at_exit' instruction * Adding doc & some poetry * Consistent inlining annotations * Not updating instantiation heuristic in model option * New name for Profile module * Fix SMTLIB2 printer * Poetry * Rebase artifacts Co-authored-by: OCamlPro-mattiasdrp <mattias@ocamlpro.com> Co-authored-by: OriginLabs-Iguernlala <mohamed.iguernlala@origin-labs.com> Co-authored-by: Albin Coquereau <albin.coquereau@ocamlpro.com> Co-authored-by: Albin Coquereau <pro.acoquer@protonmail.com> Co-authored-by: Albin Coquereau <6535385+ACoquereau@users.noreply.github.com>
Merged
Closed
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.
No description provided.