Show statements rework

[MaxOstrowski]

Quite often we encounter encodings where people use output formatting (show statements, additional calculation in the encoding). This can lead to serious performance degradation, especially in the presence of aggregates.
Given the following example:

{foo(1..100)}.
#show bar(Y) : Y = #sum {1,X : foo(X)}.

clingo (clasp) introduces variables and constraints for the show statement. We have a nice separation between instance and encoding, and I would like to think about a similar separation of solving and output. Show statements shouldn't effect the search process, so users can use these more freely.
Do you think it would be possible/is worth to:

1. remove the additional constraints (and variables) from the solving process and just check the conditions once an answer set is found
2. remove the grounding of the show statements and lazily evaluate the first order show statement in the presence of a model

I think that these changes would make ASP more accessible for the average user that does not might expect that show statements have an impact on the performance of a system.

[daveraja]

This sounds like a really nice feature. There are many occasions where this would have helped me avoid needing to use python to post-process the model.

It would be non-trivial to implement efficiently, as the show syntax would basically be an SQL-like query language. But, if it were to be added it would also be useful to have an API call to control whether to process the shows for a given model.

[rkaminsk]

In principle one could ground the show statements individually for each model but this would only be possible in clingo.

This is nothing that can easily be added to the current system that is designed to also provide grounder and solver separately.

However, one could write a system based on the clingo API that offers a feature like this.

[MaxOstrowski]

I guess it would be very easy to provide a python executable that works exactly like clingo, that first filters out any show statements, then does all the solving, and in the end uses the show statement to print solutions.
Using another control object to ground the show statement wrt. the found model would make implementation even easier. Lets start with this. The question is how performant this will be and how it would influence the API (or the gringo/clasp separation).

[sthiele]

I have a further remark related to #show statements that came up lately.
Currently, #show statements can have influence on the solving process. Because under some conditions, they are interpreted like #project directives. In a future implementation, it would be nice if these two concerns were separated.

[rkaminsk]

The --project option already put's you in full control. I am also not sure that we can improve much here. Projecting on the shown atoms often makes sense. Especially, in simple examples. The #project directive is a more advanced language construct.

[rkaminsk]

What would be the behavior you would like to have?

[sthiele]

The feedback I got why it is confusing is as follows:

• In normal mode, projection on shown atoms is not the default, one must enable the feature with --project=show.

• With brave reasoning mode, suddenly projection on shown atoms is the default behavior and can only disable it by removing the show statement or doing it proper with a #project statement.

The following behavior would be more consistent:

• Projection on show is per default off in all modes.
• If one wants to do projection, one can use the #project statement.
• If one wants to do projection on shown atoms, use --project=show.
• I think one could remove the option --project=project and --project=auto.
• A new option --project=ignore to turn off projection if #project statements are present could be useful.

[rkaminsk]

* In normal mode, projection on shown atoms is not the default, one must enable the feature with `--project=show`.

Passing --project is enough. If there is a #project directive, --project=project will be used and --project=show, otherwise.

The following behavior would be more consistent:

* Projection on show is per default off in all modes.

This might be something for a major solver version update. It sounds like a change that would have to be discussed in a larger group.

From a user's perspective one could also set the projection mode to auto by default to always project. The downside would be additional effort when enumerating solutions.