doc: cex documentation

* NEWS, doc/bison.texi: Add documentation for conflict counterexample
generation.
This commit is contained in:
Vincent Imbimbo
2020-06-28 15:30:17 -04:00
committed by Akim Demaille
parent ed9a821caa
commit 1247d94ba6
2 changed files with 99 additions and 8 deletions

24
NEWS
View File

@@ -4,6 +4,30 @@ GNU Bison NEWS
** New features
*** Counterexample Generation
When given `--report=counterexamples` or `-Wcounterexamples`, bison will
now output counterexamples for conflicts in the grammar. These are
strings in the grammar which can be parsed in two ways due to the
conflict. For example:
Example exp '+' exp • '/' exp
First derivation exp ::=[ exp ::=[ exp '+' exp • ] '/' exp ]
Second derivation exp ::=[ exp '+' exp ::=[ exp • '/' exp ] ]
This is a shift/reduce conflict caused by none of the operators having
precedence, so the example can be parsed in the two ways shown. When
bison cannot find an example that can be derived in two ways, it instead
generates two examples that are the same up until the dot:
First example expr • ID $end
First derivation $accept ::=[ s ::=[ a ::=[ expr • ] ID ] $end ]
Second example expr • ID ',' ID $end
Second derivation $accept ::=[ s ::=[ a ::=[ expr ::=[ expr • ID ',' ] ] ID ] $end ]
In these cases, the parser usually doesn't have enough lookahead to
differentiate the two given examples.
*** File prefix mapping
Bison learned a new argument, `--file-prefix-map OLD=NEW`. Any file path