mirror of
https://github.com/AdaCore/alt-ergo.git
synced 2026-02-12 12:39:26 -08:00
8617a1dbb2
* working examples for linear optimization feature * New option `--objectives-in-model` to show optimized expressions in 'model' If not set, a dedicated section '(objectives ...)' is added for that * reintroduce debug traces in satml * Theory.query: simple test to deactivate TCP for both FunSat and CDCL * begin-optim-alt: Frontend: new syntax for optimisation constraints, with their ordering. * Fix expr.ml: purify inside Optimize _ as well * prepare CS to return 'Unbounded' in case of optimization requests. * Infrastructure in theories for CS with optimized values * Detect optimization directives (predicates) in Theory and update env * IntervalCalculus: Produce optimized splits for LIA and LRA * update SMT2 model output with '(objectives ...)' section * UF: fix model_extraction: arguments of function may be interpreted Assertion used as invariant is not accurate * Models: re-introduce removed invariant check * Models: don't "assert false" when seeing an AC symbols in 'assign_next' Models gen for AC symbols in currently partial. See the comment in file ac.ml for more details. * Correctly handle Case-split backtrack when having Optimization constraints * Handling disjunctions in optimization * Translate minimize/maximize from psmt2-frontend to Alt-Ergo * Remove duplicate commands in psmt2 frontend * fix translate ordering in pstm2_to_alt_ergo * fix translate from SMT2 to AE * compute model of terms starting from the smallest one * Models: export the map of term |-> get-value(term) computed in UF * optim:re-set timelimit when trying to find a better min in other branches * Fix new options in output section in the manpage * Fix indentation in the legacy parser * Fix indentation in the legacy lexer * Apply suggestions from code review Co-authored-by: Pierrot <tiky.halbaroth@gmail.com> * Fix printer Remove eprintf calls introduced by OptimAE to replace them by Printer.print_dbg in order to print proper SMT-LIB comments. I also modify a bit print_dbg as it introduced newlines. A proper solution will be done in my future PR using headers from the library Logs. * Revert changes on print_dbg * Support optimize non-regression tests We cannot properly run non-regression tests with only a subset of the solvers defined in the main function of `gentest.ml`. I do a temporary ugly trick to prevent running optimize tests with inappropriate solvers. This should be revert as soon as Dolmen can parse a syntax for optimize constraints. * Add some tests for optimize feature * Split case_split handler into two parts Refactoring of the function `case_split`. OptimAE introduces a new kind of case_split: `optimized_split`. The previous code manages all the case splits in a single function even if AE processes optimized ones in a complete different way. This commit divides the function `case_split` into two functions: - `case_split` mostly as it was before OptimAE - `optimizing_split` which try to optimize one case split by call. We dispatch the call of `optimizing_split` in the `Relation` module based on the type of the split to optimize. * Removing useless function The function `partition_map` was only used by the case splits dispatcher of `Relation.ml`. We don't need this function anymore after refactoring this dispatcher. * Add comment about AC model-generation support * Too long lines * Give up if we try to optimize a strict inequality * Linter * Remove duplication of code in look_for_sat * Update src/lib/reasoners/sig_rel.mli Co-authored-by: Basile Clément <129742207+bclement-ocp@users.noreply.github.com> * Update src/lib/reasoners/shostak.ml Co-authored-by: Basile Clément <129742207+bclement-ocp@users.noreply.github.com> * Return `StrictBound` variant We return a new `StrictBound` variant when we try to optimize a strict bound with ocp-libsimplex. * Review changes * Temporary fix * Adding a test for optimization in SatML frontend The current implementation of the optimization feature is a bit complicated. In particular, the feature requires that the SAT solver keeps exploring other SAT branches of the problem to be sure to get an optimized model. This commit adds a nonregression test for the support of optimization in the frontend of SatML. * Documentation of analyze_unknown_for_objectives * Adding a test for strict bounds Adding a test that check optimization doesn't stop after failing to optimize a strict bound. * Rename arguments of look_for_sat The name used for the arguments of look_for_sat and make its semantic hard to understand. The meaning of the new arguments are: - `bad_last` is a variable used by a commented optimization. I plan to remove it in another PR but I kept its semantic here to keep a clear git history. - `sem_facts` are semantical facts produced by the function `assume_literals` of CC(X). By semantic facts, I mean fact using `Xliteral` as defined in `Th_util` module. Basically `sem_facts` is an imperative queue used to accumulate new facts discovered by CC(X) while propagating case-splits in `look_for_sat` to CC(X). - `acc_choices` is an accumulator of the choice made by the module Theory. Its initial value in the function `try_it` is just the current choices of the module. If the function `look_for_sat` succeeds, this argument is used to update the field `choices` of the environment of the module `Theory`. Basically, this field can be understand as a trail of the decision made by the module and `acc_choices` contains the future state of this trail. - `new_choices` contains a list of new choices to propagate to CC(X). * Add_explanation_to_split should act on split * Splitting look_for_sat The semantic of look_for_sat is quite complicated because we have to manage many different situations. I refactor it by splitting it in several functions: - `generate_choices` tries to produce new choices by calling the `case_split` primitive of the CC(X) algorithm. - `optimizing_split` attempts to optimize an objective. If it fails, it will stop the optimization in this branch of the SAT. If the flag `for_model` is set, it will continue to produce a model but without optimize this split anymore. - `propagate_choices` informs the environment `gamma_finite` of our new choices. - `aux` is a dispatcher function. It tries to optimize splits at much at possible. If there is no choice to propagate, it tries to produce new ones using `generate_choices`. Otherwise, it propagates all the new choices. * Documentation of look_for_sat and try_it * Update documentation of optimizing_split * Simplify the case split value for strict bounds * Removing `StrictBound` to use a separated ADT I remove the `StrictBound` case for the value of optimized_split. Instead, I use a separated ADT to recognize a, a+ and a-. * Rename the ADT epsilon to limit_kind * Simplify the optimized_split type * Remove deadcode optimization in `look_for_sat` The `look_for_sat` contains a commented case to process the input choice that isn't valid because the actual explanation doesn't contain the appropriate information. As we plan to refactor completely this part of the code, it doesn't make sense to keep it anymore. This commit remove completely this optimization and the flag `bad_case` used to activate it. * Simplify `mk_const_term` Removing the conversion to `string` of the input rational `c` in the function `mk_const_term`. The smart constructors `Expr.Reals.of_Q` and `Expr.Ints.of_Z` still do a round-trip through the type `string` but this commit reduces the number of locations in the codebase where we do this conversion. * Rename the constructors of the `limit_kind` type * Add a debugging flag for optimization * Improve the debugging messages for optimization * Refactoring the dispatcher of optimizing_split in `Relation` As Basile explained in the PR #861, there is nothing preventing us from having multiple relation theories on the same type. The previous dispatcher forbid such situations. * Simply `optimizing_split` in `look_for_sat` * Finite limits aren't propragate too As finite limits aren't propragate too, we should remove choices involving them while replaying choices above `gamma` in the function `try_it`. * Output post environment of `do_case_split_aux` * Review changes --------- Co-authored-by: iguer <iguer.pro@gmail.com> Co-authored-by: Albin Coquereau <6535385+ACoquereau@users.noreply.github.com> Co-authored-by: Basile Clément <129742207+bclement-ocp@users.noreply.github.com>
20 lines
372 B
Plaintext
20 lines
372 B
Plaintext
goal g1 :
|
|
forall x : int.
|
|
forall z : int.
|
|
maximize(x,1) ->
|
|
maximize(z,2) ->
|
|
2 * x <= 125 ->
|
|
0 <= z <= 10 ->
|
|
false
|
|
|
|
(* z is a "don't care" in this second example, because y is already
|
|
unbounded. (although y and z are independant *)
|
|
|
|
goal g :
|
|
forall y : int.
|
|
minimize(y,1) ->
|
|
3 * y <= 125 ->
|
|
forall z : int.
|
|
maximize(z,2) ->
|
|
0 <= z <= 10 ->
|
|
false |