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