| /* Counterexample derivation trees |
| |
| Copyright (C) 2020-2021 Free Software Foundation, Inc. |
| |
| This file is part of Bison, the GNU Compiler Compiler. |
| |
| 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 <https://www.gnu.org/licenses/>. */ |
| |
| #ifndef DERIVATION_H |
| # define DERIVATION_H |
| |
| # include <gl_linked_list.h> |
| # include <gl_xlist.h> |
| |
| # include "gram.h" |
| |
| /* Derivations are trees of symbols such that each nonterminal's |
| children are symbols that produce that nonterminal if they are |
| relevant to the counterexample. The leaves of a derivation form a |
| counterexample when printed. */ |
| |
| typedef gl_list_t derivation_list; |
| typedef struct derivation derivation; |
| |
| static inline derivation_list derivation_list_new (void) |
| { |
| return gl_list_create_empty (GL_LINKED_LIST, NULL, NULL, NULL, true); |
| } |
| |
| static inline bool |
| derivation_list_next (gl_list_iterator_t *it, derivation **d) |
| { |
| const void *p = NULL; |
| bool res = gl_list_iterator_next (it, &p, NULL); |
| if (res) |
| *d = (derivation *) p; |
| else |
| gl_list_iterator_free (it); |
| return res; |
| } |
| |
| void derivation_list_append (derivation_list dl, derivation *d); |
| void derivation_list_prepend (derivation_list dl, derivation *d); |
| void derivation_list_free (derivation_list dl); |
| |
| // rule_num is the number of the rule SYM -> CHILDREN. |
| derivation * |
| derivation_new (symbol_number sym, derivation_list children, |
| const rule *r); |
| |
| static inline derivation *derivation_new_leaf (symbol_number sym) |
| { |
| return derivation_new (sym, NULL, 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); |
| 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 */ |