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

[WIP] OptimAE #776

Closed
wants to merge 42 commits into from
Closed

[WIP] OptimAE #776

wants to merge 42 commits into from

Conversation

Halbaroth
Copy link
Collaborator

@Halbaroth Halbaroth commented Aug 9, 2023 •
edited
Loading

This PR is mostly a rebase of the branch optims: next...optims.
All the commits between e392d5b and c4b336c have been merged by the PR #530

Notice that I also ignored these commits:

@Halbaroth Halbaroth added this to the 2.6.0 milestone Aug 9, 2023
@Halbaroth Halbaroth force-pushed the cherry-pick-optimae branch from a6af670 to 80ace04 Compare August 29, 2023 08:42
@Halbaroth Halbaroth self-assigned this Aug 29, 2023
@bclement-ocp bclement-ocp mentioned this pull request Sep 4, 2023
Closed
@bclement-ocp
Copy link
Collaborator

This is a huge PR and it will take some time to properly review. Anything after "Add timeout-as-unknown option" (that seems to be the latest functionally-significant commit, at a glance) that is not necessary for the PR to compile and/or tests to pass should be split off into a separate PR to merge after the "main" PR if possible.

I removed in b745947 the why3 output format for models. AE will print only smtlib format for models.
I am not sure what was the purpose of this format.

This smells of Chesterton's fence. Did you check with the Why3 team and/or with MERCE (who I believe funded this work) that this is not a feature they need before removing it?

This was referenced Sep 5, 2023
Closed
Closed
@bclement-ocp bclement-ocp mentioned this pull request Sep 12, 2023
Closed
@Halbaroth Halbaroth force-pushed the cherry-pick-optimae branch 3 times, most recently from c213ee6 to 9f2449b Compare September 15, 2023 13:30
@iguerNL @Halbaroth
working examples for linear optimization feature
b26c5dd
@iguerNL @Halbaroth
New option --objectives-in-model to show optimized expressions in '…
7b97719 
…model'

If not set, a dedicated section '(objectives ...)' is added for that
@iguerNL @Halbaroth
Theory: harden 'compute_concrete_model' function
c299944
@iguerNL @Halbaroth
Push the test 'get_case_split_policy() == origin' into Theory.do_case…
e69d34e 
…_split
@iguerNL @Halbaroth
CS: functions return all the env instead of just 'gamma_finite'.
772a682
@iguerNL @Halbaroth
Refactoring to reduce "printing unbounded values" patch in uf.ml.
b4348e2
@iguerNL @Halbaroth
reintroduce debug traces in satml
3f778b2
@iguerNL @Halbaroth
Theory.query: simple test to deactivate TCP for both FunSat and CDCL
9c2263b
@iguerNL @Halbaroth
begin-optim-alt: Frontend: new syntax for optimisation constraints, w…
2bfa13c 
…ith their ordering.
@iguerNL @Halbaroth
Fix expr.ml: purify inside Optimize _ as well
28b8447
@iguerNL @Halbaroth
prepare CS to return 'Unbounded' in case of optimization requests.
0429b64
@iguerNL @Halbaroth
Infrastructure in theories for CS with optimized values
f5d8209
@iguerNL @Halbaroth
Detect optimization directives (predicates) in Theory and update env
ad9d782
@iguerNL @Halbaroth
IntervalCalculus: Produce optimized splits for LIA and LRA
1b740fe
@iguerNL @Halbaroth
update SMT2 model output with '(objectives ...)' section
3a8cdad
@iguerNL @Halbaroth
Fun_sat: refactor the way models are handled/printed
6b48f91 
- add a data-structure for models,
- save the strucutre in the SAT's env
- print the models in the Frontend module
@iguerNL @Halbaroth
satML: add missing case-split strategies
48cd803
@iguerNL @Halbaroth
satML: implement models generation.
73e400d
iguerNL and others added 24 commits September 15, 2023 15:31
@iguerNL @Halbaroth
UF: fix model_extraction: arguments of function may be interpreted
14b46b8 
Assertion used as invariant is not accurate
@iguerNL @Halbaroth
Print models of arrays (home made syntax)
9b9e110
@iguerNL @Halbaroth
Models: re-introduce removed invariant check
a06e01f
@iguerNL @Halbaroth
Models: don't "assert false" when seeing an AC symbols in 'assign_next'
296309c 
Models gen for AC symbols in currently partial. See the comment in
file ac.ml for more details.
@ACoquereau @Halbaroth
Fix printing of status when in interpretation mode and add clean fmt …
0325706 
…in the print_fmt function
@iguerNL @Halbaroth
Correctly handle Case-split backtrack when having Optimization constr…
12714f1 
…aints
@iguerNL @Halbaroth
Handling disjunctions in optimization
70e3514
@iguerNL @Halbaroth
Translate minimize/maximize from psmt2-frontend to Alt-Ergo
9e6e63c
@iguerNL @Halbaroth
fix translate ordering in pstm2_to_alt_ergo
230c928
@iguerNL @Halbaroth
fix translate from SMT2 to AE
a1698d0
@iguerNL @Halbaroth
re-implement all-models feature differently
f73a383 
all_models: reset last saved model before exploring other branches

all_models: re-set timelimit, which is inteded to be used per SAT branch/model in this case

print_status: Unknown instead of Timeout if get_interpretation && why3 output

continue models enumeration after a Timeout

avoid infinite loop in case no progression is made in all-models enumeration

do not support check-all-sat/all-models in Fun_SAT

add missing cases to GUI
@iguerNL @Halbaroth
compute model of terms starting from the smallest one
a7ad6b9
@iguerNL @Halbaroth
Models: export the map of term |-> get-value(term) computed in UF
4a0d2a7
@iguerNL @Halbaroth
optim:re-set timelimit when trying to find a better min in other bran…
3e679a2 
…ches
@ACoquereau @Halbaroth
Fix new options in output section in the manpage
105fa4a
@ACoquereau @Halbaroth
Add timeout-as-unknown option
9f8ed84
@Halbaroth
Don't run ocp-indent on mly files. See the issue
f437e21 
OCamlPro/ocp-indent#218
@Halbaroth
Fix indentation in the legacy parser
5272ea9
@Halbaroth
Fix indentation in the legacy lexer
61b7d1a
@Halbaroth
Print always smtlib comments in the models
3254796
@Halbaroth
Negative tests
9f2449b 
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
Fix the js worker
f9e74fe
@Halbaroth
Remove gui artefact
9f556cf
@Halbaroth
Rebase artefacts
19fa24a
@Halbaroth Halbaroth marked this pull request as ready for review September 20, 2023 14:10
@Halbaroth
Copy link
Collaborator Author

Halbaroth commented Sep 21, 2023 •
edited
Loading

I managed to split this PR into two parts. Please don't review it before I push the split ;)

@Halbaroth Halbaroth marked this pull request as draft September 21, 2023 09:26
@Halbaroth Halbaroth mentioned this pull request Sep 21, 2023
Closed
@Halbaroth
Copy link
Collaborator Author

I will try to extract the CheckSatAll feature from this PR also.

@Halbaroth Halbaroth closed this Oct 4, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees

@Halbaroth Halbaroth

Labels
enhancement
Projects
None yet
Milestone
2.6.0
Development

Successfully merging this pull request may close these issues.
4 participants
@Halbaroth @bclement-ocp @iguerNL @ACoquereau