Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Implementation of a trie that store subsets of tuples of term indices
11 : : * that are not yielding useful instantiations. of quantifier instantiation.
12 : : * This is used in the term_tuple_enumerator.
13 : : */
14 : : #ifndef CVC5__THEORY__QUANTIFIERS__INDEX_TRIE_H
15 : : #define CVC5__THEORY__QUANTIFIERS__INDEX_TRIE_H
16 : :
17 : : #include <algorithm>
18 : : #include <utility>
19 : : #include <vector>
20 : :
21 : : #include "base/check.h"
22 : : #include "expr/node.h"
23 : :
24 : : namespace cvc5::internal {
25 : : namespace theory {
26 : : namespace quantifiers {
27 : :
28 : : /** A single node of the IndexTrie. */
29 : : struct IndexTrieNode
30 : : {
31 : : std::vector<std::pair<Node, IndexTrieNode*>> d_children;
32 : : IndexTrieNode* d_blank = nullptr;
33 : : };
34 : :
35 : : /** Trie of Nodes, 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 : : * Additionally, this class accepts membership queries involving null nodes,
56 : : * which are interpreted as requiring that all possible values of the node at
57 : : * that position are contained. For example, writing `_` for null:
58 : : * (_, 1, 2, 3) is contained in (_, 1, _, 3)
59 : : * (1, 1, _, 3) is contained in (_, 1, _, 3)
60 : : * (_, 2, _, _) is not contained in (_, 1, _, 3)
61 : : * (_, 1, 2, 3) is not contained in (0, 1, _, 3)
62 : : */
63 : : class IndexTrie
64 : : {
65 : : public:
66 : : /* Construct the trie, if the argument ignoreFullySpecified is true,
67 : : * the data structure will store only data structure containing at least
68 : : * one blank. */
69 : 9508 : IndexTrie(bool ignoreFullySpecified = true)
70 : 9508 : : d_ignoreFullySpecified(ignoreFullySpecified),
71 : 9508 : d_root(new IndexTrieNode())
72 : : {
73 : 9508 : }
74 : :
75 : 14662 : virtual ~IndexTrie() { freeRec(d_root); }
76 : :
77 : : /** Add a tuple of values into the trie masked by a bitmask, i.e.\ position
78 : : * i is considered blank iff mask[i] is false. */
79 : : void add(const std::vector<bool>& mask, const std::vector<Node>& values);
80 : :
81 : : /** Check if the given set of indices is subsumed by something present in the
82 : : * trie. If it is subsumed, give the maximum non-blank index. */
83 : 150354 : bool find(const std::vector<Node>& members,
84 : : /*out*/ size_t& nonBlankLength) const
85 : : {
86 : 150354 : nonBlankLength = 0;
87 : 150354 : return findRec(d_root, 0, members, nonBlankLength);
88 : : }
89 : :
90 : : private:
91 : : /** ignore tuples with no blanks in the add method */
92 : : const bool d_ignoreFullySpecified;
93 : : /** the root of the trie, becomes null, if all tuples should match */
94 : : IndexTrieNode* d_root;
95 : :
96 : : /** Auxiliary recursive function for cleanup. */
97 : : void freeRec(IndexTrieNode* n);
98 : :
99 : : /** Auxiliary recursive function for finding subsuming tuple. */
100 : : bool findRec(const IndexTrieNode* n,
101 : : size_t index,
102 : : const std::vector<Node>& members,
103 : : size_t& nonBlankLength) const;
104 : :
105 : : /** Add master values starting from index to a given subtree. The
106 : : * cardinality represents the number of non-blank elements left. */
107 : : IndexTrieNode* addRec(IndexTrieNode* n,
108 : : size_t index,
109 : : size_t cardinality,
110 : : const std::vector<bool>& mask,
111 : : const std::vector<Node>& values);
112 : : };
113 : :
114 : : } // namespace quantifiers
115 : : } // namespace theory
116 : : } // namespace cvc5::internal
117 : : #endif /* THEORY__QUANTIFIERS__INDEX_TRIE_H */
|
