Seeing given clauses during the search

[mccune]

In the next round of updates for the GUI, I'm thinking of adding the
following feature. When a Prover9 job is running, show some of the
given clauses that have been used.

An old Otter GUI showed the all of the output as it was being generated,
and it consisted mostly of the given clauses (all of them). Why not
do this in the Prover9-Mace4 GUI? Because it slows things too much.

I assume in most cases, the user will be interested in only the
lowest weight clauses.

So every few seconds, the GUI will look through the new given clauses
and update the display with any new light ones. Two ways to do it are:

(1) Each time the display is updated, only show the lightest n given
clauses (n is the number of lines that fits into the available space).
If any clauses are too long, you can scroll horizontally.

(2) Only show clauses with weight <= than some limit.
Each time the display is updated, add any clauses <= the limit.
With vertical and horizontal scrolling. The user can set/change
the limit (dynamically.

With either method, the clauses can be ordered by weight, by age,
or by selection order. However, the user will be annoyed if the
list is updated while he's looking at a clause; the only way I see
to prevent that is to use method (2) and order by selection order.

Any opinions on these ideas?

Bill

[mkinyon]

Rather than come up with some kind of filter, wouldn't it be easier just to allow the user to click and look at all the current output up to when the click occurs, but don't auto-refresh it? Or at most, auto-refresh after a full minute or so? I don't really need auto-refresh every few seconds.

[mccune]

I think you're right that auto-refresh is not necessary (and it may be annoying). But I like the idea
of filters. So the user will have the option of seeing the whole output or just some of the given clauses.

[mkinyon]

Oh, I thought you meant these filters would be the default. But you're going to give the option of seeing the whole thing. In that case, sure!