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