src/expr/variadic_trie.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * Variadic trie utility
  14  */
  15
  16 #include "cvc5_private.h"
  17
  18 #ifndef CVC5__EXPR__VARIADIC_TRIE_H
  19 #define CVC5__EXPR__VARIADIC_TRIE_H
  20
  21 #include <map>
  22 #include <vector>
  23
  24 #include "expr/node.h"
  25
  26 namespace cvc5 {
  27
  28 /**
  29  * A trie that stores data at undetermined depth. Storing data at
  30  * undetermined depth is in contrast to the NodeTrie (expr/node_trie.h), which
  31  * assumes all data is stored at a fixed depth.
  32  *
  33  * Since data can be stored at any depth, we require both a d_children field
  34  * and a d_data field.
  35  */
  36 class VariadicTrie
  37 {
  38  public:
  39   /** the children of this node */
  40   std::map<Node, VariadicTrie> d_children;
  41   /** the data at this node */
  42   Node d_data;
  43   /**
  44    * Add data with identifier n indexed by i, return true if data is not already
  45    * stored at the node indexed by i.
  46    */
  47   bool add(Node n, const std::vector<Node>& i);
  48   /** Is there any data in this trie that is indexed by any subset of is? */
  49   bool hasSubset(const std::vector<Node>& is) const;
  50 };
  51
  52 }  // namespace cvc5
  53
  54 #endif /* CVC5__EXPR__VARIADIC_TRIE_H */