1 /* Counterexample derivation trees
3 Copyright (C) 2020-2021 Free Software Foundation, Inc.
5 This file is part of Bison, the GNU Compiler Compiler.
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.
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.
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/>. */
23 # include <gl_linked_list.h>
24 # include <gl_xlist.h>
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. */
33 typedef gl_list_t derivation_list
;
34 typedef struct derivation derivation
;
36 static inline derivation_list
derivation_list_new (void)
38 return gl_list_create_empty (GL_LINKED_LIST
, NULL
, NULL
, NULL
, true);
42 derivation_list_next (gl_list_iterator_t
*it
, derivation
**d
)
45 bool res
= gl_list_iterator_next (it
, &p
, NULL
);
47 *d
= (derivation
*) p
;
49 gl_list_iterator_free (it
);
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
);
57 // rule_num is the number of the rule SYM -> CHILDREN.
59 derivation_new (symbol_number sym
, derivation_list children
,
62 static inline derivation
*derivation_new_leaf (symbol_number sym
)
64 return derivation_new (sym
, NULL
, NULL
);
68 size_t derivation_size (const derivation
*deriv
);
69 void derivation_print (const derivation
*deriv
, FILE *out
, const char *prefix
);
70 void derivation_print_leaves (const derivation
*deriv
, FILE *out
);
71 void derivation_free (derivation
*deriv
);
72 void derivation_retain (derivation
*deriv
);
74 // A derivation denoting the position of the dot.
75 derivation
*derivation_dot (void);
77 #endif /* DERIVATION_H */