My use case is a meta-interpreter that solves queries according to an alternate resolution procedure. I think it generalizes to any meta-interpreter that must take over the final reporting rather than hand it back to the top-level.
In my case, there are two reasons for this. 1) The query is solved as a BDD over all of the possible models (ASP style, though with the traditional least Herbrand model semantics). The user’s query variables will only have bindings at top-level if they happen to be bound in the last model, which is incorrect because it suggests that they have this binding in all of the models. 2) The BDD is written to an SVG dot file rather than displayed. It would be large and not very useful to read. The written BDD relates the variables on internal nodes back to the query variables via Skolem functions over those variables. I need the user’s original names for this to be meaningful.
While I’m at it, is there a way to suppress the top-level display of bindings and constraints (since these will be misleading and not very informative)? Just success or ‘false’ will do.