[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
cex: unifying counterexamples that are not unified
From: |
Akim Demaille |
Subject: |
cex: unifying counterexamples that are not unified |
Date: |
Fri, 19 Jun 2020 08:10:45 +0200 |
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!
- cex: unifying counterexamples that are not unified,
Akim Demaille <=