cex: bind counterexample generation

* src/complain.h, src/complain.c: Add support for -Wcounterexample.
* src/conflicts.c (report_counterexamples): New.
(rule_conflicts_print): Use it when -Wcounterexample is given.
* src/getargs.h, src/getargs.c: Add support for --trace=cex.
* src/main.c (main): Init and deinit counterexample generation.

src/complain.c

@@ -114,6 +114,7 @@ static const argmatch_warning_doc argmatch_warning_docs[] =
 {
   { "conflicts-sr",     N_("S/R conflicts (enabled by default)") },
   { "conflicts-rr",     N_("R/R conflicts (enabled by default)") },
+  { "counterexample",   N_("Conflict counter examples") },
   { "dangling-alias",   N_("string aliases not attached to a symbol") },
   { "deprecated",       N_("obsolete constructs") },
   { "empty-rule",       N_("empty rules without %empty") },
@@ -133,6 +134,7 @@ static const argmatch_warning_arg argmatch_warning_args[] =
   { "all",            Wall },
   { "conflicts-rr",   Wconflicts_rr },
   { "conflicts-sr",   Wconflicts_sr },
+  { "counterexample", Wcounterexample },
   { "dangling-alias", Wdangling_alias },
   { "deprecated",     Wdeprecated },
   { "empty-rule",     Wempty_rule },

src/complain.h

@@ -46,6 +46,7 @@ typedef enum
   {
     warning_conflicts_rr,
     warning_conflicts_sr,
+    warning_counterexample,
     warning_dangling_alias,
     warning_deprecated,
     warning_empty_rule,
@@ -106,6 +107,7 @@ typedef enum
 
     Wconflicts_rr     = 1 << warning_conflicts_rr,
     Wconflicts_sr     = 1 << warning_conflicts_sr,
+    Wcounterexample   = 1 << warning_counterexample,
     Wdangling_alias   = 1 << warning_dangling_alias,
     Wdeprecated       = 1 << warning_deprecated,
     Wempty_rule       = 1 << warning_empty_rule,
@@ -122,7 +124,7 @@ typedef enum
 
     /**< All above warnings.  */
     Weverything       = ~complaint & ~fatal & ~silent,
-    Wall              = Weverything & ~Wdangling_alias & ~Wyacc
+    Wall              = Weverything & ~Wcounterexample & ~Wdangling_alias & ~Wyacc
   } warnings;
 
 /** Whether the warnings of \a flags are all unset.

src/conflicts.c

@@ -25,6 +25,7 @@
 
 #include "complain.h"
 #include "conflicts.h"
+#include "counterexample.h"
 #include "files.h"
 #include "getargs.h"
 #include "gram.h"
@@ -624,6 +625,72 @@ conflicts_total_count (void)
   return count_sr_conflicts () + count_rr_conflicts ();
 }
 
+static void
+report_state_counterexamples (const state *s)
+{
+  const state_number sn = s->number;
+  const reductions *reds = s->reductions;
+  for (int i = 0; i < reds->num; ++i)
+    {
+      rule *r1 = reds->rules[i];
+      state_item_number c1;
+      for (int j = state_item_map[sn];
+           j < state_item_map[sn + 1]; ++j)
+        {
+          if (item_number_as_rule_number (*state_items[j].item) == r1->number)
+            {
+              c1 = j;
+              break;
+            }
+        }
+
+      for (int j = state_item_map[sn];
+           j < state_item_map[sn + 1]; ++j)
+        {
+          if (SI_DISABLED (j))
+            continue;
+          state_item *si = state_items + j;
+          item_number conf = *si->item;
+          if (item_number_is_symbol_number (conf) &&
+              bitset_test (reds->lookahead_tokens[i], conf))
+            {
+              counterexample_report_shift_reduce (c1, j, conf);
+              break;
+            }
+        }
+      for (int j = i+1; j < reds->num; ++j)
+        {
+          bitset conf = bitset_create (ntokens, BITSET_FIXED);
+          bitset_intersection (conf,
+                               reds->lookahead_tokens[i],
+                               reds->lookahead_tokens[j]);
+          if (!bitset_empty_p (conf))
+            {
+              rule *r2 = reds->rules[j];
+              for (int k = state_item_map[sn];
+                   k < state_item_map[sn + 1]; ++k)
+                {
+                  state_item *si = state_items + k;
+                  const rule *r = item_rule (si->item);
+                  if (r == r2)
+                    {
+                      counterexample_report_reduce_reduce (c1, k, conf);
+                      break;
+                    }
+                }
+            }
+        }
+    }
+}
+
+static void
+report_counterexamples (void)
+{
+  for (state_number sn = 0; sn < nstates; ++sn)
+    if (conflicts[sn])
+      report_state_counterexamples (states[sn]);
+}
+
 /*------------------------------.
 | Reporting per-rule conflicts. |
 `------------------------------*/
@@ -653,6 +720,8 @@ rule_conflicts_print (void)
                       r->user_number, rr, expected_rr);
         }
     }
+  if (warning_is_enabled (Wcounterexample))
+    report_counterexamples ();
 }
 
 /*---------------------------------.

src/getargs.c

@@ -261,6 +261,7 @@ static const argmatch_trace_doc argmatch_trace_docs[] =
   { "skeleton",   "skeleton postprocessing" },
   { "time",       "time consumption" },
   { "ielr",       "IELR conversion" },
+  { "cex",        "counterexample generation"},
   { "all",        "all of the above" },
   { NULL, NULL},
 };
@@ -283,6 +284,7 @@ static const argmatch_trace_arg argmatch_trace_args[] =
   { "skeleton",  trace_skeleton },
   { "time",      trace_time },
   { "ielr",      trace_ielr },
+  { "cex",       trace_cex },
   { "all",       trace_all },
   { NULL,        trace_none},
 };

src/getargs.h

@@ -105,6 +105,7 @@ enum trace
     trace_ielr      = 1 << 12, /**< IELR conversion. */
     trace_closure   = 1 << 13, /**< Input/output of closure(). */
     trace_locations = 1 << 14, /**< Full display of locations. */
+    trace_cex       = 1 << 15, /**< Counterexample generation */
     trace_all       = ~0       /**< All of the above.  */
   };
 /** What debug items bison displays during its run.  */

src/local.mk

@@ -40,6 +40,10 @@ src_bison_SOURCES =                             \
   src/complain.h                                \
   src/conflicts.c                               \
   src/conflicts.h                               \
+  src/counterexample.c                          \
+  src/counterexample.h                          \
+  src/derivation.c                              \
+  src/derivation.h                              \
   src/derives.c                                 \
   src/derives.h                                 \
   src/files.c                                   \
@@ -61,6 +65,8 @@ src_bison_SOURCES =                             \
   src/location.h                                \
   src/lr0.c                                     \
   src/lr0.h                                     \
+  src/lssi.c                                    \
+  src/lssi.h                                    \
   src/main.c                                    \
   src/muscle-tab.c                              \
   src/muscle-tab.h                              \
@@ -71,6 +77,8 @@ src_bison_SOURCES =                             \
   src/output.c                                  \
   src/output.h                                  \
   src/parse-gram.y                              \
+  src/parse-simulation.c                        \
+  src/parse-simulation.h                        \
   src/print-graph.c                             \
   src/print-graph.h                             \
   src/print-xml.c                               \
@@ -91,6 +99,8 @@ src_bison_SOURCES =                             \
   src/scan-skel.h                               \
   src/state.c                                   \
   src/state.h                                   \
+  src/state-item.c                              \
+  src/state-item.h                              \
   src/symlist.c                                 \
   src/symlist.h                                 \
   src/symtab.c                                  \

src/main.c

@@ -33,6 +33,7 @@
 
 #include "complain.h"
 #include "conflicts.h"
+#include "counterexample.h"
 #include "derives.h"
 #include "files.h"
 #include "fixits.h"
@@ -144,6 +145,8 @@ main (int argc, char *argv[])
       conflicts_update_state_numbers (old_to_new, nstates_old);
       free (old_to_new);
     }
+  if (warning_is_enabled (Wcounterexample))
+    counterexample_init ();
   conflicts_print ();
   timevar_pop (tv_conflicts);
 
@@ -217,6 +220,7 @@ main (int argc, char *argv[])
   reduce_free ();
   conflicts_free ();
   grammar_free ();
+  counterexample_free ();
   output_file_names_free ();
 
   /* The scanner memory cannot be released right after parsing, as it