cex: unifying counterexamples that are not unified

Akim Demaille <[email protected]>
Newsgroups gmane.comp.parsers.bison.patches
Message-ID <[email protected]>
Hi Vincent,

There is something not quite right in the current implementation.  On the following grammar, taken from the test suite:

$ cat bar.y
%left b
%right c
%%
S: B C | C B;
A: B  | C  | %empty;
B: A b A;
C: A c A;

bison thinks it found two unifying examples, but the derivations actually yield two different sentential forms:

$ bison bar.y -Wcex
bar.y: avertissement: 4 conflits par réduction/réduction [-Wconflicts-rr]
Reduce/reduce conflict on tokens b, c:
  Example              B • b A A c A
  First derivation     S ::=[ B ::=[ A ::=[ B • ] b A ] C ::=[ A c A ] ]
  Example              B • b A c A
  Second derivation    S ::=[ B C ::=[ A ::=[ B ::=[ A ::=[ • ] b A ] ] c A ] ]

Reduce/reduce conflict on tokens b, c:
  Example              C • c A A b A
  First derivation     S ::=[ C ::=[ A ::=[ C • ] c A ] B ::=[ A b A ] ]
  Example              C • c A b A
  Second derivation    S ::=[ C B ::=[ A ::=[ C ::=[ A ::=[ • ] c A ] ] b A ] ]

The derivations are difficult to read.  They look as follows (hoping nothing will wreck the indentation):

> S
> |
> B       C
> |       |
> A b A   A c A
> |
> B •



> S
> |
> B  C
>    |
>    A c A
>    |
>    B
>    |
>    A b A
>    |
>    •
> 



The code appears to believe the example is unifying because both derivations share the same prefix up to the dot, and both comply with parse_state_derivation_completed, whose meaning is unclear to me (could you please add comments to these routines?).

But here it seems insufficient to dub this as unifying.

Cheers!
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.