[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Missing counterexamples?
From: |
Akim Demaille |
Subject: |
Missing counterexamples? |
Date: |
Mon, 8 Jun 2020 07:38:07 +0200 |
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!
[Prev in Thread] |
Current Thread |
[Next in Thread] |
- Missing counterexamples?,
Akim Demaille <=