cex: also include in the report on --report=counterexamples

And let --report=all include the counterexamples.

* src/getargs.h, src/getargs.c (report_cex): New.
* src/main.c: Compute counterexamples when -rcex is specified.
* src/print.c: Include the counterexamples when -rcex is specified.

* tests/conflicts.at, tests/existing.at, tests/local.at: Adjust.
This commit is contained in:
Akim Demaille
2020-06-14 08:18:37 +02:00
parent d4f854e5b2
commit c35e829a76
8 changed files with 71 additions and 16 deletions

View File

@@ -206,23 +206,26 @@ ARGMATCH_DEFINE_GROUP (report, enum report)
static const argmatch_report_doc argmatch_report_docs[] =
{
{ "states", N_("describe the states") },
{ "itemsets", N_("complete the core item sets with their closure") },
{ "lookaheads", N_("explicitly associate lookahead tokens to items") },
{ "solved", N_("describe shift/reduce conflicts solving") },
{ "all", N_("include all the above information") },
{ "none", N_("disable the report") },
{ "states", N_("describe the states") },
{ "itemsets", N_("complete the core item sets with their closure") },
{ "lookaheads", N_("explicitly associate lookahead tokens to items") },
{ "solved", N_("describe shift/reduce conflicts solving") },
{ "counterexamples", N_("generate conflict counterexamples") },
{ "all", N_("include all the above information") },
{ "none", N_("disable the report") },
{ NULL, NULL },
};
static const argmatch_report_arg argmatch_report_args[] =
{
{ "none", report_none },
{ "states", report_states },
{ "itemsets", report_states | report_itemsets },
{ "lookaheads", report_states | report_lookahead_tokens },
{ "solved", report_states | report_solved_conflicts },
{ "all", report_all },
{ "none", report_none },
{ "states", report_states },
{ "itemsets", report_states | report_itemsets },
{ "lookaheads", report_states | report_lookahead_tokens },
{ "solved", report_states | report_solved_conflicts },
{ "counterexamples", report_cex },
{ "cex", report_cex },
{ "all", report_all },
{ NULL, report_none },
};

View File

@@ -79,6 +79,7 @@ enum report
report_itemsets = 1 << 1,
report_lookahead_tokens = 1 << 2,
report_solved_conflicts = 1 << 3,
report_cex = 1 << 4,
report_all = ~0
};
/** What appears in the *.output file. */

View File

@@ -146,7 +146,8 @@ main (int argc, char *argv[])
conflicts_update_state_numbers (old_to_new, nstates_old);
free (old_to_new);
}
if (warning_is_enabled (Wcounterexamples))
if (report_flag & report_cex
|| warning_is_enabled (Wcounterexamples))
counterexample_init ();
conflicts_print ();
timevar_pop (tv_conflicts);

View File

@@ -356,7 +356,9 @@ print_state (FILE *out, const state *s)
fputc ('\n', out);
fputs (s->solved_conflicts, out);
}
if (warning_is_enabled (Wcounterexamples) && has_conflicts (s))
if (has_conflicts (s)
&& (report_flag & report_cex
|| warning_is_enabled (Wcounterexamples)))
{
fputc ('\n', out);
counterexample_report_state (s, out, " ");