1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
|
/******************************************************************************
* Top contributors (to current version):
* Andrew Reynolds, Morgan Deters, Mathias Preiner
*
* This file is part of the cvc5 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.
* ****************************************************************************
*
* Inst match trie class.
*/
#include "cvc5_private.h"
#ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H
#define CVC5__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H
#include <map>
#include "context/cdlist.h"
#include "context/cdo.h"
#include "expr/node.h"
namespace cvc5 {
namespace theory {
namespace quantifiers {
class QuantifiersState;
/** trie for InstMatch objects
*
* This class is used for storing instantiations of a quantified formula q.
* It is a trie data structure for which entries can be added and removed.
* This class has interfaces for adding instantiations that are either
* represented by std::vectors or InstMatch objects (see inst_match.h).
*/
class InstMatchTrie
{
public:
/** index ordering */
class ImtIndexOrder
{
public:
std::vector<unsigned> d_order;
};
public:
InstMatchTrie() {}
~InstMatchTrie() {}
/** exists inst match
*
* This method considers the entry given by m, starting at the given index.
* The domain of m is the bound variables of quantified formula q.
* It returns true if (the suffix) of m exists in this trie.
* If modEq is true, we check for duplication modulo equality the current
* equalities in the equality engine of qs.
*/
bool existsInstMatch(QuantifiersState& qs,
Node q,
const std::vector<Node>& m,
bool modEq = false,
ImtIndexOrder* imtio = nullptr,
unsigned index = 0);
/** add inst match
*
* This method adds (the suffix of) m starting at the given index to this
* trie, and returns true if and only if m did not already occur in this trie.
* The domain of m is the bound variables of quantified formula q.
* If modEq is true, we check for duplication modulo equality the current
* equalities in the equality engine of qs.
*/
bool addInstMatch(QuantifiersState& qs,
Node f,
const std::vector<Node>& m,
bool modEq = false,
ImtIndexOrder* imtio = nullptr,
bool onlyExist = false,
unsigned index = 0);
/** remove inst match
*
* This removes (the suffix of) m starting at the given index from this trie.
* It returns true if and only if this entry existed in this trie.
* The domain of m is the bound variables of quantified formula q.
*/
bool removeInstMatch(Node f,
const std::vector<Node>& m,
ImtIndexOrder* imtio = nullptr,
unsigned index = 0);
/**
* Adds the instantiations for q into insts.
*/
void getInstantiations(Node q, std::vector<std::vector<Node>>& insts) const;
/** clear the data of this class */
void clear();
/** print this class */
void print(std::ostream& out, Node q) const;
/** the data */
std::map<Node, InstMatchTrie> d_data;
private:
/** Helper for getInstantiations.*/
void getInstantiations(Node q,
std::vector<std::vector<Node>>& insts,
std::vector<Node>& terms) const;
/** helper for print
* terms accumulates the path we are on in the trie.
*/
void print(std::ostream& out, Node q, std::vector<TNode>& terms) const;
};
/** trie for InstMatch objects
*
* This is a context-dependent version of the above class.
*/
class CDInstMatchTrie
{
public:
CDInstMatchTrie(context::Context* c) : d_valid(c, false) {}
~CDInstMatchTrie();
/** exists inst match
*
* This method considers the entry given by m, starting at the given index.
* The domain of m is the bound variables of quantified formula q.
* It returns true if (the suffix) of m exists in this trie.
* If modEq is true, we check for duplication modulo equality the current
* equalities in the equality engine of qs.
* It additionally takes a context c, for which the entry is valid in.
*/
bool existsInstMatch(QuantifiersState& qs,
Node q,
const std::vector<Node>& m,
bool modEq = false,
unsigned index = 0);
/** add inst match
*
* This method adds (the suffix of) m starting at the given index to this
* trie, and returns true if and only if m did not already occur in this trie.
* The domain of m is the bound variables of quantified formula q.
* If modEq is true, we check for duplication modulo equality the current
* equalities in the equality engine of qs.
* It additionally takes a context c, for which the entry is valid in.
*/
bool addInstMatch(QuantifiersState& qs,
Node q,
const std::vector<Node>& m,
bool modEq = false,
unsigned index = 0,
bool onlyExist = false);
/** remove inst match
*
* This removes (the suffix of) m starting at the given index from this trie.
* It returns true if and only if this entry existed in this trie.
* The domain of m is the bound variables of quantified formula q.
*/
bool removeInstMatch(Node q, const std::vector<Node>& m, unsigned index = 0);
/**
* Adds the instantiations for q into insts.
*/
void getInstantiations(Node q, std::vector<std::vector<Node>>& insts) const;
/** print this class */
void print(std::ostream& out, Node q) const;
private:
/** Helper for getInstantiations.*/
void getInstantiations(Node q,
std::vector<std::vector<Node>>& insts,
std::vector<Node>& terms) const;
/** helper for print
* terms accumulates the path we are on in the trie.
*/
void print(std::ostream& out, Node q, std::vector<TNode>& terms) const;
/** the data */
std::map<Node, CDInstMatchTrie*> d_data;
/** is valid */
context::CDO<bool> d_valid;
};
/** inst match trie ordered
*
* This is an ordered version of the context-independent instantiation match
* trie. It stores a variable order and a base InstMatchTrie.
*/
class InstMatchTrieOrdered
{
public:
InstMatchTrieOrdered(InstMatchTrie::ImtIndexOrder* imtio) : d_imtio(imtio) {}
~InstMatchTrieOrdered() {}
/** get the ordering */
InstMatchTrie::ImtIndexOrder* getOrdering() { return d_imtio; }
/** get the trie data */
InstMatchTrie* getTrie() { return &d_imt; }
/** add match m for quantified formula q
*
* This method returns true if the match m was not previously added to this
* class. If modEq is true, we consider duplicates modulo the current
* equalities stored in the equality engine of qs.
*/
bool addInstMatch(QuantifiersState& qs,
Node q,
const std::vector<Node>& m,
bool modEq = false);
/** returns true if this trie contains m
*
* This method returns true if the match m exists in this
* class. If modEq is true, we consider duplicates modulo the current
* equalities stored in the equality engine of qs.
*/
bool existsInstMatch(QuantifiersState& qs,
Node q,
const std::vector<Node>& m,
bool modEq = false);
private:
/** the ordering */
InstMatchTrie::ImtIndexOrder* d_imtio;
/** the data of this class */
InstMatchTrie d_imt;
};
} // namespace quantifiers
} // namespace theory
} // namespace cvc5
#endif /* CVC5__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H */
|
