GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/index_trie.h Lines: 9 9 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file index_trie.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mikolas Janota
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief Implementation of a trie that store subsets of tuples of term indices
13
 ** that are not yielding  useful instantiations. of quantifier instantiation.
14
 ** This is used in the term_tuple_enumerator.
15
 **/
16
#ifndef CVC4__THEORY__QUANTIFIERS__INDEX_TRIE_H
17
#define CVC4__THEORY__QUANTIFIERS__INDEX_TRIE_H
18
#include <algorithm>
19
#include <utility>
20
#include <vector>
21
22
#include "base/check.h"
23
24
namespace CVC4 {
25
namespace theory {
26
namespace quantifiers {
27
28
/** A single node of the IndexTrie. */
29
7826
struct IndexTrieNode
30
{
31
  std::vector<std::pair<size_t, IndexTrieNode*>> d_children;
32
  IndexTrieNode* d_blank = nullptr;
33
};
34
35
/** Trie of  sequences indices, used to check for subsequence membership.
36
 *
37
 * The  data structure stores tuples of indices where some elements may be
38
 * left blank. The objective is to enable checking whether a given, completely
39
 * filled in, tuple has a  sub-tuple  present in the data structure.  This is
40
 * used in the term tuple enumeration (term_tuple_enumerator.cpp) to store
41
 * combinations of terms that had yielded a useless instantiation  and therefore
42
 * should not be repeated.  Hence, we are always assuming that all tuples have
43
 * the same number of elements.
44
 *
45
 * So for instance, if the data structure contains (_, 1, _, 3),  any  given
46
 * tuple that contains 1 and 3 on second and forth position, respectively, would
47
 * match.
48
 *
49
 *  The data structure behaves essentially as a traditional trie. Each tuple
50
 * is treated as a sequence of integers with a special symbol for blank, which
51
 * is in fact stored  in a special  child (member d_blank).  As a small
52
 * optimization, a suffix containing only blanks is represented by  the empty
53
 * subtree, i.e., a null pointer.
54
 *
55
 */
56
class IndexTrie
57
{
58
 public:
59
  /*  Construct the trie,  if the argument ignoreFullySpecified is true,
60
   *  the data structure will  store only data structure containing at least
61
   *  one blank. */
62
1965
  IndexTrie(bool ignoreFullySpecified)
63
1965
      : d_ignoreFullySpecified(ignoreFullySpecified),
64
1965
        d_root(new IndexTrieNode())
65
  {
66
1965
  }
67
68
1965
  virtual ~IndexTrie() { freeRec(d_root); }
69
70
  /**  Add a tuple of values into the trie  masked by a bitmask, i.e.\ position
71
   * i is considered blank iff mask[i] is false. */
72
  void add(const std::vector<bool>& mask, const std::vector<size_t>& values);
73
74
  /** Check if the given set of indices is subsumed by something present in the
75
   * trie. If it is subsumed, give the maximum non-blank index. */
76
7751
  bool find(const std::vector<size_t>& members,
77
            /*out*/ size_t& nonBlankLength) const
78
  {
79
7751
    nonBlankLength = 0;
80
7751
    return findRec(d_root, 0, members, nonBlankLength);
81
  }
82
83
 private:
84
  /**  ignore tuples with no blanks in the add method */
85
  const bool d_ignoreFullySpecified;
86
  /**  the root of the trie, becomes null, if all tuples should match */
87
  IndexTrieNode* d_root;
88
89
  /** Auxiliary recursive function for cleanup. */
90
  void freeRec(IndexTrieNode* n);
91
92
  /** Auxiliary recursive function for finding  subsuming tuple. */
93
  bool findRec(const IndexTrieNode* n,
94
               size_t index,
95
               const std::vector<size_t>& members,
96
               size_t& nonBlankLength) const;
97
98
  /** Add master values  starting from index  to a given subtree. The
99
   * cardinality represents the number of non-blank elements left. */
100
  IndexTrieNode* addRec(IndexTrieNode* n,
101
                        size_t index,
102
                        size_t cardinality,
103
                        const std::vector<bool>& mask,
104
                        const std::vector<size_t>& values);
105
};
106
107
}  // namespace quantifiers
108
}  // namespace theory
109
}  // namespace CVC4
110
#endif /* THEORY__QUANTIFIERS__INDEX_TRIE_H */