Refactoring models invocation #614
Conversation
…reproducible-resource-limit
Halbaroth
force-pushed
the
refactoring-models-invocation
branch
from
13f95f9 to
1aeea7a
Compare
…n :produce-models
|
It is ready |
|
AE still displays the status after printing the model, even if you use the native language. |
| (* The command line option overrides the behavior of the get-model | ||
| commands. *) |
There was a problem hiding this comment.
I believe we discussed this multiple times and agreed that command line options should not override the behavior of in-band commands. If you use the option to get a model on each check_sat / check-sat, you should get that. If you also use get-model, you should get two models (or more, depending on the number of times get-model is called).
There was a problem hiding this comment.
I believe that comment should now be removed?
There was a problem hiding this comment.
Don't worry :) I didn't forget it
There was a problem hiding this comment.
Apologies for misunderstanding, i thought you were done!
There was a problem hiding this comment.
You didn't forget but you still merged with the comment in there…
I assume you mean before printing the model? But that's good, thanks for checking! |
Alas, I didn't. As I explained on Zulip, AE prints its models in a exception handler. After printing it, the exception is raised again and a second handler prints the status. |
|
I think we can fix the issue with the order between the status and the model in another PR. Modifying the way AE catches exceptions can be tricky :) |
|
I don't think we need to modify the way we catch exceptions, we should get away with simply adding the model as payload to But I agree, this should be a separate PR. |
Sounds good :) I will do it quickly :D |
| @@ -212,6 +212,9 @@ val set_input_format : input_format -> unit | |||
| *) | |||
| val set_interpretation : interpretation -> unit | |||
|
|
|||
| (** [all_interpretations] accessible with {!val:get_all_interpretations}. *) | |||
There was a problem hiding this comment.
Docstring was not updated
There was a problem hiding this comment.
This was merged without updating the docstring.
This PR adds the support for the instruction
get-model.The command is only supported through the new frontend Dolmen. It means you cannot use the statement
get-modelwithout the option--frontend dolmen.There is no support for the
get-modelstatement in the native language of AE.