diff options
| -rw-r--r-- | src/counterexample.h | 10 | ||||
| -rw-r--r-- | src/derivation.c | 46 | ||||
| -rw-r--r-- | src/derivation.h | 3 |
3 files changed, 34 insertions, 25 deletions
diff --git a/src/counterexample.h b/src/counterexample.h index c251d319..735828fa 100644 --- a/src/counterexample.h +++ b/src/counterexample.h @@ -20,11 +20,17 @@ #ifndef COUNTEREXAMPLE_H # define COUNTEREXAMPLE_H -# include "state-item.h" +# include "state.h" +// Init/deinit this module. void counterexample_init (void); void counterexample_free (void); -void counterexample_report_state (const state *s, FILE *out, const char *prefix); +// Print the counterexamples for the conflicts of state S. +// +// Used both for the warnings on the terminal (OUT = stderr, PREFIX = +// ""), and for the reports (OUT != stderr, PREFIX != ""). +void +counterexample_report_state (const state *s, FILE *out, const char *prefix); #endif /* COUNTEREXAMPLE_H */ diff --git a/src/derivation.c b/src/derivation.c index da5649fc..39f66211 100644 --- a/src/derivation.c +++ b/src/derivation.c @@ -29,7 +29,7 @@ struct derivation { symbol_number sym; - gl_list_t children; + derivation_list children; int reference_count; }; @@ -129,7 +129,7 @@ derivation_size (const derivation *deriv) /* Print DERIV, colored according to COUNTER. Return false if nothing is printed. */ static bool -derivation_print_impl (const derivation *deriv, FILE *f, +derivation_print_impl (const derivation *deriv, FILE *out, bool leaves_only, int *counter, const char *prefix) { @@ -139,16 +139,16 @@ derivation_print_impl (const derivation *deriv, FILE *f, char style[20]; snprintf (style, 20, "cex-%d", *counter); ++*counter; - begin_use_class (style, f); + begin_use_class (style, out); if (!leaves_only) { - fputs (prefix, f); - begin_use_class ("cex-step", f); - fprintf (f, "%s ", sym->tag); - print_arrow (f); - fprintf (f, " [ "); - end_use_class ("cex-step", f); + fputs (prefix, out); + begin_use_class ("cex-step", out); + fprintf (out, "%s ", sym->tag); + print_arrow (out); + fprintf (out, " [ "); + end_use_class ("cex-step", out); prefix = ""; } bool res = false; @@ -157,7 +157,7 @@ derivation_print_impl (const derivation *deriv, FILE *f, derivation_list_next (&it, &child); ) { - if (derivation_print_impl (child, f, leaves_only, counter, prefix)) + if (derivation_print_impl (child, out, leaves_only, counter, prefix)) { prefix = " "; res = true; @@ -167,30 +167,30 @@ derivation_print_impl (const derivation *deriv, FILE *f, } if (!leaves_only) { - begin_use_class ("cex-step", f); + begin_use_class ("cex-step", out); if (res) - fputs (" ]", f); + fputs (" ]", out); else - fputs ("]", f); - end_use_class ("cex-step", f); + fputs ("]", out); + end_use_class ("cex-step", out); } - end_use_class (style, f); + end_use_class (style, out); return res; } else if (deriv == &d_dot) { - fputs (prefix, f); - begin_use_class ("cex-dot", f); - print_dot (f); - end_use_class ("cex-dot", f); + fputs (prefix, out); + begin_use_class ("cex-dot", out); + print_dot (out); + end_use_class ("cex-dot", out); } else // leaf. { - fputs (prefix, f); + fputs (prefix, out); const symbol *sym = symbols[deriv->sym]; - begin_use_class ("cex-leaf", f); - fprintf (f, "%s", sym->tag); - end_use_class ("cex-leaf", f); + begin_use_class ("cex-leaf", out); + fprintf (out, "%s", sym->tag); + end_use_class ("cex-leaf", out); } return true; } diff --git a/src/derivation.h b/src/derivation.h index 9f015df2..62676368 100644 --- a/src/derivation.h +++ b/src/derivation.h @@ -60,12 +60,15 @@ static inline derivation *derivation_new_leaf (symbol_number sym) { return derivation_new (sym, NULL); } + +// Number of symbols. size_t derivation_size (const derivation *deriv); void derivation_print (const derivation *deriv, FILE *out, const char *prefix); void derivation_print_leaves (const derivation *deriv, FILE *out, const char *prefix); void derivation_free (derivation *deriv); void derivation_retain (derivation *deriv); +// A derivation denoting the position of the dot. derivation *derivation_dot (void); #endif /* DERIVATION_H */ |