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  
      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
      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  // rule_num is the number of the rule SYM -> CHILDREN.
      58  derivation *
      59  derivation_new (symbol_number sym, derivation_list children,
      60                  const rule *r);
      61  
      62  static inline derivation *derivation_new_leaf (symbol_number sym)
      63  {
      64    return derivation_new (sym, NULL, NULL);
      65  }
      66  
      67  // Number of symbols.
      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);
      73  
      74  // A derivation denoting the position of the dot.
      75  derivation *derivation_dot (void);
      76  
      77  #endif /* DERIVATION_H */