[Why3-club] Module names in files for external provers

Stefan Berghofer berghofe at in.tum.de
Fri Mar 7 11:38:10 CET 2014


On 03/06/2014 10:43 AM, Guillaume Melquiond wrote:
> On 05/03/2014 10:59, Stefan Berghofer wrote:
>> Is there some function in the Why3 API that maps an identifier to the name of
>> the module / theory in which it was introduced?
>
> (Disclaimer: I am no expert on that part of the code, so take my answer with a grain of salt.)
>
> Yes and no. I don't think there is a such function already. But the code at the start of printers supporting realizations (including Isabelle) already does it, though only for realized theories. By lifting this restriction, it should be possible to achieve what you want.

Hi Guillaume,

thanks for your reply. It seems that applying Task.used_symbols to the result of Task.used_theories
yields exactly the mapping that I was looking for. I was a bit confused by the comment appearing
before the declaration of these functions in task.mli, which said something like "realization utilities",
but as you pointed out, these functions need not necessarily be used for dealing with realized theories.

Greetings,
Stefan



More information about the Why3-club mailing list