Missing counterexamples?

[Akim Demaille]

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!