[PATCH 5/5] counterexample test suite

[Vincent Imbimbo]

---
 tests/counterexample.at | 357 ++++++++++++++++++++++++++++++++++++++++
 tests/testsuite.at      |   3 +
 2 files changed, 360 insertions(+)
 create mode 100644 tests/counterexample.at

diff --git a/tests/counterexample.at b/tests/counterexample.at
new file mode 100644
index 00000000..a42ea013
--- /dev/null
+++ b/tests/counterexample.at
@@ -0,0 +1,357 @@
+# Exercising Bison on conflicts.                         -*- Autotest -*-
+
+# Copyright (C) 2020 Free Software
+# Foundation, Inc.
+
+# This program is free software: you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation, either version 3 of the License, or
+# (at your option) any later version.
+#
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+AT_BANNER([[Counterexamples.]])
+
+## --------------------- ##
+## Simple Unifying S/R.  ##
+## --------------------- ##
+
+AT_SETUP([Unifying S/R])
+
+AT_DATA([[input.y]],
+[[%token A B C
+%%
+s: a x | y c;
+a: A;
+c: C;
+x: B | B C;
+y: A | A B;
+]])
+
+AT_BISON_CHECK([-Wcounterexample input.y], 0, [],
+[[
+]])
+
+AT_CLEANUP
+
+## ------------------- ##
+## Deep Unifying S/R.  ##
+## ------------------- ##
+
+AT_SETUP([Deep Unifying S/R])
+
+AT_DATA([[input.y]],
+[[%token A B C
+%%
+s: ac | a bc;
+ac: A ac C | b;
+b: B | B b;
+a: A | A a;
+bc: B bc C | B C;
+]])
+
+AT_BISON_CHECK([-Wcounterexample input.y], 0, [],
+[[
+]])
+
+AT_CLEANUP
+
+## ------------------------------------ ##
+## S/R Conflict with Nullable Symbols.  ##
+## ------------------------------------ ##
+
+AT_SETUP([S/R Conflict with Nullable Symbols])
+
+AT_DATA([[input.y]],
+[[%token A B X Y
+%%
+s: ax by | A xby;
+ax: A x;
+x: %empty | X x;
+by: B y;
+y: %empty | Y y;
+xby: B | X xby Y;
+]])
+
+AT_BISON_CHECK([-Wcounterexample input.y], 0, [],
+[[
+]])
+
+AT_CLEANUP
+
+## ---------------------------- ##
+## Non-unifying Ambiguous S/R.  ##
+## ---------------------------- ##
+
+AT_SETUP([Non-unifying Ambiguous S/R])
+
+AT_DATA([[input.y]],
+[[%token A B C D E
+%%
+g: s | x;
+s: A x E | A x D E;
+x: b cd | bc;
+b: B;
+cd: C D;
+bc: B C;
+]])
+
+AT_BISON_CHECK([-Wcounterexample input.y], 0, [],
+[[
+]])
+
+AT_CLEANUP
+
+## ------------------------------ ##
+## Non-unifying Unambiguous S/R.  ##
+## ------------------------------ ##
+
+AT_SETUP([Non-unifying Unambiguous S/R])
+
+AT_DATA([[input.y]],
+[[%token A B
+%%
+s: t | s t;
+t: x | y;
+x: A;
+y: A A B;
+]])
+
+AT_BISON_CHECK([-Wcounterexample input.y], 0, [],
+[[
+]])
+
+AT_CLEANUP
+
+## ----------------------- ##
+## S/R after first token.  ##
+## ----------------------- ##
+
+AT_SETUP([S/R after first token])
+
+AT_DATA([[input.y]],
+[[%token A B X Y
+%%
+a: r t | s;
+r: b;
+b: B;
+t: A xx | A x xy;
+s: b A xx y;
+x: X;
+xx: X X;
+xy: X Y;
+y: Y;
+]])
+
+AT_BISON_CHECK([-Wcounterexample input.y], 0, [],
+[[
+]])
+
+AT_CLEANUP
+
+## ----------------------------- ##
+## Unifying R/R counterexample.  ##
+## ----------------------------- ##
+
+AT_SETUP([Unifying R/R counterexample])
+
+AT_DATA([[input.y]],
+[[%token A
+%%
+a : A b ;
+b : A | b;
+]])
+
+AT_BISON_CHECK([-Wcounterexample input.y], 0, [],
+[[
+]])
+
+AT_CLEANUP
+
+## ------------------------------- ##
+## Non-unifying R/R lr1 conflict.  ##
+## ------------------------------- ##
+
+AT_SETUP([Non-unifying R/R lr1 conflict])
+
+AT_DATA([[input.y]],
+[[%token A B C D
+%%
+s: a A | B a C | b C | B b A;
+a: D;
+b: D;
+]])
+
+AT_BISON_CHECK([-Wcounterexample input.y], 0, [],
+[[
+]])
+
+AT_CLEANUP
+
+## ------------------------------- ##
+## Non-unifying R/R lr2 conflict.  ##
+## ------------------------------- ##
+
+AT_SETUP([Non-unifying R/R lr2 conflict])
+
+AT_DATA([[input.y]],
+[[%token H J K X
+%%
+s: a J;
+a: H i;
+i: X | i J K;
+]])
+
+AT_BISON_CHECK([-Wcounterexample input.y], 0, [],
+[[
+]])
+
+AT_CLEANUP
+
+## -------------------- ##
+## Cex Search Prepend.  ##
+## -------------------- ##
+
+# Tests prepend steps in uniying counterexample
+# graph search
+
+AT_SETUP([Cex Search Prepend])
+
+AT_DATA([[input.y]],
+[[%token N A B C D
+%%
+s: n | n C;
+n: N n D | N n C | N a B | N b;
+a: A;
+b: A B C | A B D;
+]])
+
+AT_BISON_CHECK([-Wcounterexample input.y], 0, [],
+[[
+]])
+
+AT_CLEANUP
+
+## ------------------- ##
+## R/R cex with prec.  ##
+## ------------------- ##
+
+# Tests that counterexamples containing rules using
+# precedence/associativity directives work.
+
+AT_SETUP([R/R cex with prec])
+
+AT_DATA([[input.y]],
+[[%left b
+%right c
+%%
+S: B C | C B;
+A : B  | C  | %empty;
+B : A b A;
+C : A c A;
+]])
+
+AT_BISON_CHECK([-Wcounterexample input.y], 0, [],
+[[
+]])
+
+AT_CLEANUP
+
+## ------------------- ##
+## Null nonterminals.  ##
+## ------------------- ##
+
+AT_SETUP([Null nonterminals])
+
+AT_DATA([[input.y]],
+[[%token A
+%%
+a : b d | c d ;
+b : ;
+c : ;
+d : a | c A | d;
+]])
+
+AT_BISON_CHECK([-Wcounterexample input.y], 0, [],
+[[
+]])
+
+AT_CLEANUP
+
+## --------------------------- ##
+## Non-unifying Prefix Share.  ##
+## --------------------------- ##
+
+AT_SETUP([Non-unifying Prefix Share])
+
+# Tests for a counterexample which should start its derivation
+# at a shared symbol rather than the start symbol.
+
+AT_DATA([[input.y]],
+[[%token H J
+%%
+s: a | a J;
+a: H i J J
+i: %empty | i J;
+]])
+
+AT_BISON_CHECK([-Wcounterexample input.y], 0, [],
+[[
+]])
+
+AT_CLEANUP
+
+## -------------------- ##
+## Deep Null Unifying.  ##
+## ---------------------##
+
+# Tests that nested nullable nonterminals
+# are derived correctly.
+
+AT_SETUP([Deep Null Unifying])
+
+AT_DATA([[input.y]],
+[[%token a d
+%%
+S: a A D | a A A D;
+A: B;
+B: C
+C: %empty
+D: d;
+]])
+
+AT_BISON_CHECK([-Wcounterexample input.y], 0, [],
+[[
+]])
+
+AT_CLEANUP
+
+## ------------------------ ##
+## Deep Null Non-unifying.  ##
+## -------------------------##
+
+# Tests that expand_to_conflict works with nullable sybols
+
+AT_SETUP([Deep Null Non-unifying])
+
+AT_DATA([[input.y]],
+[[%token a d e
+%%
+S: a A D | a A A D e;
+A: B;
+B: C
+C: %empty
+D: d;
+]])
+
+AT_BISON_CHECK([-Wcounterexample input.y], 0, [],
+[[
+]])
+
+AT_CLEANUP
\ No newline at end of file
diff --git a/tests/testsuite.at b/tests/testsuite.at
index 4ccbfd1e..f8d87639 100644
--- a/tests/testsuite.at
+++ b/tests/testsuite.at
@@ -44,6 +44,9 @@ m4_include([report.at])
 # Conflicts detection and resolution.
 m4_include([conflicts.at])
 
+# Counterexaple generation.
+m4_include([counterexample.at])
+
 # Support for #lines.
 m4_include([synclines.at])
 
-- 
2.20.1 (Apple Git-117)