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