Remove get_first_interpretation adn get_every_interpretation #1299
Conversation
As noticed by Basile, this feature is broken in presence of optimization and no one used it. This PR removes these options. I kept the cli option but it is now a no-op.
src/bin/common/parse_command.ml
Outdated
| let doc = | ||
| Fmt.str | ||
| "This option allowed choosing when the model generation occurs. \ | ||
| It have been removed in Alt-Ergo 2.7.0. If model generation is \ |
There was a problem hiding this comment.
| It have been removed in Alt-Ergo 2.7.0. If model generation is \ | |
| It has been removed in Alt-Ergo 2.7.0. If model generation is \ |
src/bin/common/parse_command.ml
Outdated
| match interpretation with | ||
| | INone when produce_models || dump_models -> ILast | ||
| | interpretation -> interpretation | ||
| let mk_interpretation _interpretation produce_models dump_models = |
There was a problem hiding this comment.
| let mk_interpretation _interpretation produce_models dump_models = | |
| let mk_model_generation _interpretation produce_models dump_models = |
src/bin/common/parse_command.ml
Outdated
| const mk_interpretation $ interpretation $ | ||
| produce_models $ dump_models | ||
| ), | ||
| const mk_interpretation $ interpretation $ produce_models $ dump_models), |
There was a problem hiding this comment.
| const mk_interpretation $ interpretation $ produce_models $ dump_models), | |
| const mk_model_generation $ interpretation $ produce_models $ dump_models), |
src/lib/reasoners/satml_frontend.ml
Outdated
| if not updated then ( | ||
| if Options.get_model_generation () then update_model env; | ||
| Options.Time.unset_timeout (); | ||
| (* may becomes ModelGen *) |
There was a problem hiding this comment.
I don't think it can become ModelGen anymore — if the unknown-reason becomes ModelGen it should be set by update_model, not i_dont_know.
src/lib/util/options.mli
Outdated
| (** Set [produce_models] accessible with {!val:get_produce_models} *) | ||
| val set_model_generation : bool -> unit |
There was a problem hiding this comment.
Either the comment should be updated to say model_generation and get_model_generation, or the code should be updated to be called set_produce_models and get_produce_models (I think the second option makes more sense --- might as well standardise on the SMT-LIB names).
There was a problem hiding this comment.
I named it set_produce_models first, I have no strong opinion on its name.
There was a problem hiding this comment.
When in doubt about naming and there is an appropriate name for the SMT-LIB standard we should pick that one I think, so let's go with set_produce_models even if that is a slightly awkward name.
| env.last_saved_objectives <- Some objectives; | ||
| with | ||
| | Ex.Inconsistent (_expl, _classes) as e -> raise e | ||
| | Util.Timeout -> i_dont_know env (Timeout ModelGen) |
There was a problem hiding this comment.
I believe this line was removed because if we raise I_dont_know here the solver ends up in an inconsistent state and performing further commands can lead to incorrect output or crashes — is there a reason to add it back?
There was a problem hiding this comment.
On next, if Timeout is raised during model generation, we catch it in unsat_rec and raise I_dont_know with Timeout ProofSearch as unknown reason, so the solver already ends up in an inconsistent state.
There was a problem hiding this comment.
Ah, that is true — we actually check for timeout outside of the solver, from the frontend (which is a design wart we should fix someday, but it does mean this line is OK).
There was a problem hiding this comment.
I added it because you pointed out that we cannot change the unknown reason as suggested by Steven. I don't understand what is wrong here.
There was a problem hiding this comment.
uhm, I see. It is because of the lazy value again...
As noticed by Basile, this feature is broken in presence of optimization and no one used it. This PR removes these options.
I kept the cli option but it is now a no-op.