[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: cex: unifying counterexamples that are not unified
From: |
Vincent Imbimbo |
Subject: |
Re: cex: unifying counterexamples that are not unified |
Date: |
Sun, 21 Jun 2020 11:08:08 -0400 |
Hey Akim,
I think the problem here is the extra A was derived to be null during the
search. Either the derivation tree is missing information, or there's
something wrong with the printing code. I'm looking into it.
~Vincent
On Fri, Jun 19, 2020 at 2:10 AM Akim Demaille <akim.demaille@gmail.com>
wrote:
> 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!