Add support for show statement in cat parser

[hernanponcedeleon]

No description provided.

[hernanponcedeleon]

These changes are need for eventual support of models like this one.

[ThomasHaas]

I wouldn't call this "support". The show (as) feature is essentially ignored and I think you should implement it like that (i.e., change nothing in the backend and just the parser skip it).
The reason is that you will need to implement it differently anyways, cause e.g. here shows three different variants, only one of which you "support":

show rf-reg // without renaming
show rf-mem as rf // with renaming
show co|fr as ca // can also show derived relations (even one that might not be relevant for the axioms)

[hernanponcedeleon]

The show in cat is used to enforce some edges to be displayed in the witness graphs. This will eventually be used in #732 thus I don't see why we should not already have this functionality implemented.

shows three different variants, only one of which you "support":

Now all 3 variants are supported.

Notice that for the last case, if we don't have a relation matching the term (as it is in the cat file you linked; co|fr neither exists in the included ctrl.cat), a new one will be created. Unless I am missing something, this will guarantee that a boolean variable for this term will exists in the solver if the eager encoding is used, and a graph with the definition will exists if the lazy method is used.

[ThomasHaas]

The show in cat is used to enforce some edges to be displayed in the witness graphs. This will eventually be used in #732 thus I don't see why we should not already have this functionality implemented.

Ok, but then the implementation should be proper. I think adding show-as properties directly to Relation is not the way to go. To me, it seems the show-as feature is akin to metadata, i.e., somehow stored externally/orthogonally.
In this case, I would prefer to have something like a mapping Map<Relation, ShowAsInfo> in Wmm that manages this fact. ShowAsInfo is a record/class with an optional display name and maybe other goodies like display color, arrow type (e.g. dashed) etc. (only added if/when needed of course).

Btw. looking up the relation by name/term is pointless. The parser already has the relation in hand and could directly use it instead of taking its name/term, discarding the relation, and then forcing a lookup by term/name again (which currently also forces the unnamed relations to (wrongly) get their term as name!)

Notice that for the last case, if we don't have a relation matching the term (as it is in the cat file you linked; co|fr neither exists in the included ctrl.cat), a new one will be created. Unless I am missing something, this will guarantee that a boolean variable for this term will exists in the solver if the eager encoding is used, and a graph with the definition will exists if the lazy method is used.

No, it does not because we have dead relation elimination that kills unused relations. While it is unlikely that you want to display a relation that is unused in the axioms, I think you still should account for this fact.
And even if the relation is not killed, active set computation may avoid encoding parts of it (or all of it if unused in axioms!).
I also don't think you want to slow down solving (whether eager or lazy) just because you force encoding of otherwise unused show-as relations. I also think this is unnecessary as you could compute the show-as relations only once when printing the graph, assuming that at least the base relations are sufficiently encoded (this is likely the case, but not necessarily).
That means adapting our dead relation elimination pass (not too bad), possibly the active set computation (this could be wild), and maybe even CAAT so as to not compute over irrelevant graphs for consistency checking.

[hernanponcedeleon]

I decided to refer the decision of what to do with the information coming from show statements to #732 and keep this PR to a minimum by just allowing to parse cat files making use of show statements, but simply ignoring them

[ThomasHaas]

Good idea :)