1 files changed, 110 insertions, 0 deletions
diff --git a/src/theory/quantifiers/index_trie.h b/src/theory/quantifiers/index_trie.h
new file mode 100644
index 000000000..b77095181
--- /dev/null
+++ b/src/theory/quantifiers/index_trie.h
@@ -0,0 +1,110 @@
+/*********************                                                        */
+/*! \file index_trie.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Mikolas Janota
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of a trie that store subsets of tuples of term indices
+ ** that are not yielding  useful instantiations. of quantifier instantiation.
+ ** This is used in the term_tuple_enumerator.
+ **/
+#ifndef CVC4__THEORY__QUANTIFIERS__INDEX_TRIE_H
+#define CVC4__THEORY__QUANTIFIERS__INDEX_TRIE_H
+#include <algorithm>
+#include <utility>
+#include <vector>
+
+#include "base/check.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** A single node of the IndexTrie. */
+struct IndexTrieNode
+{
+  std::vector<std::pair<size_t, IndexTrieNode*>> d_children;
+  IndexTrieNode* d_blank = nullptr;
+};
+
+/** Trie of  sequences indices, used to check for subsequence membership.
+ *
+ * The  data structure stores tuples of indices where some elements may be
+ * left blank. The objective is to enable checking whether a given, completely
+ * filled in, tuple has a  sub-tuple  present in the data structure.  This is
+ * used in the term tuple enumeration (term_tuple_enumerator.cpp) to store
+ * combinations of terms that had yielded a useless instantiation  and therefore
+ * should not be repeated.  Hence, we are always assuming that all tuples have
+ * the same number of elements.
+ *
+ * So for instance, if the data structure contains (_, 1, _, 3),  any  given
+ * tuple that contains 1 and 3 on second and forth position, respectively, would
+ * match.
+ *
+ *  The data structure behaves essentially as a traditional trie. Each tuple
+ * is treated as a sequence of integers with a special symbol for blank, which
+ * is in fact stored  in a special  child (member d_blank).  As a small
+ * optimization, a suffix containing only blanks is represented by  the empty
+ * subtree, i.e., a null pointer.
+ *
+ */
+class IndexTrie
+{
+ public:
+  /*  Construct the trie,  if the argument ignoreFullySpecified is true,
+   *  the data structure will  store only data structure containing at least
+   *  one blank. */
+  IndexTrie(bool ignoreFullySpecified)
+      : d_ignoreFullySpecified(ignoreFullySpecified),
+        d_root(new IndexTrieNode())
+  {
+  }
+
+  virtual ~IndexTrie() { freeRec(d_root); }
+
+  /**  Add a tuple of values into the trie  masked by a bitmask, i.e.\ position
+   * i is considered blank iff mask[i] is false. */
+  void add(const std::vector<bool>& mask, const std::vector<size_t>& values);
+
+  /** Check if the given set of indices is subsumed by something present in the
+   * trie. If it is subsumed, give the maximum non-blank index. */
+  bool find(const std::vector<size_t>& members,
+            /*out*/ size_t& nonBlankLength) const
+  {
+    nonBlankLength = 0;
+    return findRec(d_root, 0, members, nonBlankLength);
+  }
+
+ private:
+  /**  ignore tuples with no blanks in the add method */
+  const bool d_ignoreFullySpecified;
+  /**  the root of the trie, becomes null, if all tuples should match */
+  IndexTrieNode* d_root;
+
+  /** Auxiliary recursive function for cleanup. */
+  void freeRec(IndexTrieNode* n);
+
+  /** Auxiliary recursive function for finding  subsuming tuple. */
+  bool findRec(const IndexTrieNode* n,
+               size_t index,
+               const std::vector<size_t>& members,
+               size_t& nonBlankLength) const;
+
+  /** Add master values  starting from index  to a given subtree. The
+   * cardinality represents the number of non-blank elements left. */
+  IndexTrieNode* addRec(IndexTrieNode* n,
+                        size_t index,
+                        size_t cardinality,
+                        const std::vector<bool>& mask,
+                        const std::vector<size_t>& values);
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+#endif /* THEORY__QUANTIFIERS__INDEX_TRIE_H */