Missing counterexamples?

Hi Vincent,

On this grammar:

$ cat /tmp/foo.y
%%
exp
: "if" exp "then" exp
| "if" exp "then" exp "else" exp
| exp "+" exp
| "num"

-Wcounterexamples shows three counterexamples:

> $ LC_ALL=C ∫ /tmp/foo.y -Wcou
> Shift/reduce conflict on token "+":
> 8:    3 exp: exp "+" exp .
> 8:    3 exp: exp . "+" exp
> Example              exp "+" exp • "+" exp
> First derivation     exp ::=[ exp ::=[ exp "+" exp • ] "+" exp ]
> Example              exp "+" exp • "+" exp
> Second derivation    exp ::=[ exp "+" exp ::=[ exp • "+" exp ] ]
> 
> Shift/reduce conflict on token "else":
> 9:    1 exp: "if" exp "then" exp .
> 9:    2 exp: "if" exp "then" exp . "else" exp
> Example              "if" exp "then" "if" exp "then" exp • "else" exp
> First derivation     exp ::=[ "if" exp "then" exp ::=[ "if" exp "then" exp • ] "else" exp ]
> Example              "if" exp "then" "if" exp "then" exp • "else" exp
> Second derivation    exp ::=[ "if" exp "then" exp ::=[ "if" exp "then" exp • "else" exp ] ]
> 
> Shift/reduce conflict on token "+":
> 11:    2 exp: "if" exp "then" exp "else" exp .
> 11:    3 exp: exp . "+" exp
> Example              "if" exp "then" exp "else" exp • "+" exp
> First derivation     exp ::=[ exp ::=[ "if" exp "then" exp "else" exp • ] "+" exp ]
> Example              "if" exp "then" exp "else" exp • "+" exp
> Second derivation    exp ::=[ "if" exp "then" exp "else" exp ::=[ exp • "+" exp ] ]
> 
> /tmp/foo.y: warning: 4 shift/reduce conflicts [-Wconflicts-sr]

There is nothing about the conflict between the if-then rule, and the + rule.  That's because/thanks to the "break" in report_state_counterexamples, whose purpose I guess is to reduce the number of counterexamples for similar situations.  For instance the ambiguous arithmetics with four operators has sixteen similar conflicts, we don't need that many counterexamples.

Declaring that rules are "alike" is non-trivial, but it would be interesting to explore.  The four arithmetic rules are definitely "alike", while in the case of the fourth missing counterexample here, I don't see that.  Alternatively we could have an additional flag asking for more extensive searches.

I checked in the original paper whether this trimming was reported, but I couldn't find anything about it.  The closest I found is in Section 6, "Constructing unifying counterexamples", which refers to a -extendedsearch options, but it's unrelated.

Is this documented somewhere?

Cheers!