1 /* Counterexample derivation trees
2
3 Copyright (C) 2020-2021 Free Software Foundation, Inc.
4
5 This file is part of Bison, the GNU Compiler Compiler.
6
7 This program is free software: you can redistribute it and/or modify
8 it under the terms of the GNU General Public License as published by
9 the Free Software Foundation, either version 3 of the License, or
10 (at your option) any later version.
11
12 This program is distributed in the hope that it will be useful,
13 but WITHOUT ANY WARRANTY; without even the implied warranty of
14 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 GNU General Public License for more details.
16
17 You should have received a copy of the GNU General Public License
18 along with this program. If not, see <https://www.gnu.org/licenses/>. */
19
20 #ifndef DERIVATION_H
21 # define DERIVATION_H
22
23 # include <gl_linked_list.h>
24 # include <gl_xlist.h>
25
26 # include "gram.h"
27
28 /* Derivations are trees of symbols such that each nonterminal's
29 children are symbols that produce that nonterminal if they are
30 relevant to the counterexample. The leaves of a derivation form a
31 counterexample when printed. */
32
33 typedef gl_list_t derivation_list;
34 typedef struct derivation derivation;
35
derivation_list_new(void)36 static inline derivation_list derivation_list_new (void)
37 {
38 return gl_list_create_empty (GL_LINKED_LIST, NULL, NULL, NULL, true);
39 }
40
41 static inline bool
derivation_list_next(gl_list_iterator_t * it,derivation ** d)42 derivation_list_next (gl_list_iterator_t *it, derivation **d)
43 {
44 const void *p = NULL;
45 bool res = gl_list_iterator_next (it, &p, NULL);
46 if (res)
47 *d = (derivation *) p;
48 else
49 gl_list_iterator_free (it);
50 return res;
51 }
52
53 void derivation_list_append (derivation_list dl, derivation *d);
54 void derivation_list_prepend (derivation_list dl, derivation *d);
55 void derivation_list_free (derivation_list dl);
56
57 derivation *derivation_new (symbol_number sym, derivation_list children);
58
derivation_new_leaf(symbol_number sym)59 static inline derivation *derivation_new_leaf (symbol_number sym)
60 {
61 return derivation_new (sym, NULL);
62 }
63
64 // Number of symbols.
65 size_t derivation_size (const derivation *deriv);
66 void derivation_print (const derivation *deriv, FILE *out, const char *prefix);
67 void derivation_print_leaves (const derivation *deriv, FILE *out);
68 void derivation_free (derivation *deriv);
69 void derivation_retain (derivation *deriv);
70
71 // A derivation denoting the position of the dot.
72 derivation *derivation_dot (void);
73
74 #endif /* DERIVATION_H */
75