A reporter that prints on the appropriate output (regular or
diagnostic) according to the source.
As explained in #785, we cannot do really better without breaking the API of Printer
This PR is rebased on #1204
See #1207 for an example using sources introduced here.
Notice that I create two sources for theories with a Shostak and Relation modules. An alternative implementation consists in prefixing all the messages in *_rel.ml by [Rel] as it does in the legacy code. I have no strong opinion on this choice.
I did not create a bijection between debug flags and sources because it is more flexible to use two different lists.
For instance, it could be useful to create flags that set different sources (and actually, --dd adt for instance set adt and adt_rel sources).
This PR adds:
Logsas a new dependency;As explained in #785, we cannot do really better without breaking the API of
PrinterThis PR is rebased on #1204
See #1207 for an example using sources introduced here.
Notice that I create two sources for theories with a Shostak and Relation modules. An alternative implementation consists in prefixing all the messages in
*_rel.mlby[Rel]as it does in the legacy code. I have no strong opinion on this choice.I did not create a bijection between debug flags and sources because it is more flexible to use two different lists. For instance, it could be useful to create flags that set different sources (and actually,
--dd adtfor instance setadtandadt_relsources).