[PATCH 4/5] counterexample generation integration

[Vincent Imbimbo]

---
 src/complain.c  |  2 ++
 src/complain.h  |  2 ++
 src/conflicts.c | 67 +++++++++++++++++++++++++++++++++++++++++++++++++
 src/getargs.c   |  2 ++
 src/getargs.h   |  1 +
 src/local.mk    | 10 ++++++++
 src/main.c      |  3 +++
 7 files changed, 87 insertions(+)

diff --git a/src/complain.c b/src/complain.c
index 87563d59..e4037c5e 100644
--- a/src/complain.c
+++ b/src/complain.c
@@ -113,6 +113,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") },
   { "deprecated",       N_("obsolete constructs") },
   { "empty-rule",       N_("empty rules without %empty") },
   { "midrule-values",   N_("unset or unused midrule values") },
@@ -133,6 +134,7 @@ static const argmatch_warning_arg argmatch_warning_args[] =
   { "yacc",           Wyacc },
   { "conflicts-sr",   Wconflicts_sr },
   { "conflicts-rr",   Wconflicts_rr },
+  { "counterexample", Wcounterexample },
   { "deprecated",     Wdeprecated },
   { "empty-rule",     Wempty_rule },
   { "precedence",     Wprecedence },
diff --git a/src/complain.h b/src/complain.h
index 4b73d08d..dfe7bcc4 100644
--- a/src/complain.h
+++ b/src/complain.h
@@ -47,6 +47,7 @@ typedef enum
   {
     warning_conflicts_rr,
     warning_conflicts_sr,
+    warning_counterexample,
     warning_deprecated,
     warning_empty_rule,
     warning_midrule_values,
@@ -104,6 +105,7 @@ typedef enum
 
     Wconflicts_rr     = 1 << warning_conflicts_rr,
     Wconflicts_sr     = 1 << warning_conflicts_sr,
+    Wcounterexample   = 1 << warning_counterexample,
     Wdeprecated       = 1 << warning_deprecated,
     Wempty_rule       = 1 << warning_empty_rule,
     Wmidrule_values   = 1 << warning_midrule_values,
diff --git a/src/conflicts.c b/src/conflicts.c
index cfc729aa..01598049 100644
--- a/src/conflicts.c
+++ b/src/conflicts.c
@@ -34,6 +34,7 @@
 #include "reader.h"
 #include "state.h"
 #include "symtab.h"
+#include "counterexample.h"
 
 /* -1 stands for not specified. */
 int expected_sr_conflicts = -1;
@@ -628,6 +629,70 @@ conflicts_total_count (void)
 | Reporting per-rule conflicts. |
 `------------------------------*/
 
+static void
+report_counterexamples ()
+{
+  for (state_number sn = 0; sn < nstates; ++sn)
+    {
+      if (conflicts[sn])
+        {
+          state *s = states[sn];
+          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
 rule_conflicts_print (void)
 {
@@ -653,6 +718,8 @@ rule_conflicts_print (void)
                       r->user_number, rr, expected_rr);
         }
     }
+  if (warning_is_enabled (Wcounterexample))
+    report_counterexamples ();
 }
 
 /*---------------------------------.
diff --git a/src/getargs.c b/src/getargs.c
index bf4a938f..7544ec22 100644
--- a/src/getargs.c
+++ b/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},
 };
diff --git a/src/getargs.h b/src/getargs.h
index ab6af6c3..598fce4f 100644
--- a/src/getargs.h
+++ b/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.  */
diff --git a/src/local.mk b/src/local.mk
index ee8ec03b..8b28800f 100644
--- a/src/local.mk
+++ b/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                                  \
diff --git a/src/main.c b/src/main.c
index 258a6d1e..cbae8fbc 100644
--- a/src/main.c
+++ b/src/main.c
@@ -55,6 +55,7 @@
 #include "symtab.h"
 #include "tables.h"
 #include "uniqstr.h"
+#include "counterexample.h"
 
 
 int
@@ -144,6 +145,7 @@ main (int argc, char *argv[])
       conflicts_update_state_numbers (old_to_new, nstates_old);
       free (old_to_new);
     }
+  counterexample_init ();
   conflicts_print ();
   timevar_pop (tv_conflicts);
 
@@ -217,6 +219,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
-- 
2.20.1 (Apple Git-117)