Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Andres Noetzli, Morgan Deters
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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 inst match trie class.
14 : : */
15 : :
16 : : #include "theory/quantifiers/inst_match_trie.h"
17 : :
18 : : using namespace cvc5::context;
19 : :
20 : : namespace cvc5::internal {
21 : : namespace theory {
22 : : namespace quantifiers {
23 : :
24 : 0 : bool InstMatchTrie::existsInstMatch(Node q,
25 : : const std::vector<Node>& m,
26 : : ImtIndexOrder* imtio,
27 : : unsigned index)
28 : : {
29 : 0 : return !addInstMatch(q, m, imtio, true, index);
30 : : }
31 : :
32 : 559141 : bool InstMatchTrie::addInstMatch(Node f,
33 : : const std::vector<Node>& m,
34 : : ImtIndexOrder* imtio,
35 : : bool onlyExist,
36 : : unsigned index)
37 : : {
38 [ + + ][ - - ]: 559141 : if (index == f[0].getNumChildren()
39 [ + + ][ + + ]: 559141 : || (imtio && index == imtio->d_order.size()))
[ + + ][ + - ]
40 : : {
41 : 162967 : return false;
42 : : }
43 [ + + ]: 396174 : unsigned i_index = imtio ? imtio->d_order[index] : index;
44 : 792348 : Node n = m[i_index];
45 : 396174 : std::map<Node, InstMatchTrie>::iterator it = d_data.find(n);
46 [ + + ]: 396174 : if (it != d_data.end())
47 : : {
48 : 200395 : bool ret = it->second.addInstMatch(f, m, imtio, onlyExist, index + 1);
49 [ - + ][ - - ]: 200395 : if (!onlyExist || !ret)
50 : : {
51 : 200395 : return ret;
52 : : }
53 : : }
54 [ + - ]: 195779 : if (!onlyExist)
55 : : {
56 : 195779 : d_data[n].addInstMatch(f, m, imtio, false, index + 1);
57 : : }
58 : 195779 : return true;
59 : : }
60 : :
61 : 0 : void InstMatchTrie::print(std::ostream& out,
62 : : Node q,
63 : : std::vector<TNode>& terms) const
64 : : {
65 [ - - ]: 0 : if (terms.size() == q[0].getNumChildren())
66 : : {
67 : 0 : out << " ( ";
68 [ - - ]: 0 : for (unsigned i = 0, size = terms.size(); i < size; i++)
69 : : {
70 [ - - ]: 0 : if (i > 0)
71 : : {
72 : 0 : out << ", ";
73 : : }
74 : 0 : out << terms[i];
75 : : }
76 : 0 : out << " )" << std::endl;
77 : : }
78 : : else
79 : : {
80 [ - - ]: 0 : for (const std::pair<const Node, InstMatchTrie>& d : d_data)
81 : : {
82 : 0 : terms.push_back(d.first);
83 : 0 : d.second.print(out, q, terms);
84 : 0 : terms.pop_back();
85 : : }
86 : : }
87 : 0 : }
88 : :
89 : 73 : void InstMatchTrie::getInstantiations(
90 : : Node q, std::vector<std::vector<Node>>& insts) const
91 : : {
92 : 73 : std::vector<Node> terms;
93 : 73 : getInstantiations(q, insts, terms);
94 : 73 : }
95 : :
96 : 773 : void InstMatchTrie::getInstantiations(Node q,
97 : : std::vector<std::vector<Node>>& insts,
98 : : std::vector<Node>& terms) const
99 : : {
100 [ + + ]: 773 : if (terms.size() == q[0].getNumChildren())
101 : : {
102 : 186 : insts.push_back(terms);
103 : : }
104 : : else
105 : : {
106 [ + + ]: 1287 : for (const std::pair<const Node, InstMatchTrie>& d : d_data)
107 : : {
108 : 700 : terms.push_back(d.first);
109 : 700 : d.second.getInstantiations(q, insts, terms);
110 : 700 : terms.pop_back();
111 : : }
112 : : }
113 : 773 : }
114 : :
115 : 0 : void InstMatchTrie::clear() { d_data.clear(); }
116 : :
117 : 0 : void InstMatchTrie::print(std::ostream& out, Node q) const
118 : : {
119 : 0 : std::vector<TNode> terms;
120 : 0 : print(out, q, terms);
121 : 0 : }
122 : :
123 : 10313 : CDInstMatchTrie::~CDInstMatchTrie()
124 : : {
125 [ + + ]: 19541 : for (std::pair<const Node, CDInstMatchTrie*>& d : d_data)
126 : : {
127 : 9228 : CDInstMatchTrie* current = d.second;
128 [ + - ]: 9228 : delete current;
129 : : }
130 : 10313 : d_data.clear();
131 : 10313 : }
132 : :
133 : 0 : bool CDInstMatchTrie::existsInstMatch(context::Context* context,
134 : : Node q,
135 : : const std::vector<Node>& m,
136 : : unsigned index)
137 : : {
138 : 0 : return !addInstMatch(context, q, m, index, true);
139 : : }
140 : :
141 : 23442 : bool CDInstMatchTrie::addInstMatch(context::Context* context,
142 : : Node f,
143 : : const std::vector<Node>& m,
144 : : unsigned index,
145 : : bool onlyExist)
146 : : {
147 : 23442 : bool reset = false;
148 [ + + ]: 23442 : if (!d_valid.get())
149 : : {
150 [ - + ]: 11510 : if (onlyExist)
151 : : {
152 : 0 : return true;
153 : : }
154 : : else
155 : : {
156 : 11510 : d_valid.set(true);
157 : 11510 : reset = true;
158 : : }
159 : : }
160 [ + + ]: 23442 : if (index == f[0].getNumChildren())
161 : : {
162 : 8123 : return reset;
163 : : }
164 : 30638 : Node n = m[index];
165 : 15319 : std::map<Node, CDInstMatchTrie*>::iterator it = d_data.find(n);
166 [ + + ]: 15319 : if (it != d_data.end())
167 : : {
168 : 6090 : bool ret = it->second->addInstMatch(context, f, m, index + 1, onlyExist);
169 [ - + ][ - - ]: 6090 : if (!onlyExist || !ret)
170 : : {
171 [ + + ][ + + ]: 6090 : return reset || ret;
172 : : }
173 : : }
174 [ + - ]: 9229 : if (!onlyExist)
175 : : {
176 : 9229 : CDInstMatchTrie* imt = new CDInstMatchTrie(context);
177 [ - + ][ - + ]: 9229 : Assert(d_data.find(n) == d_data.end());
[ - - ]
178 : 9229 : d_data[n] = imt;
179 : 9229 : imt->addInstMatch(context, f, m, index + 1, false);
180 : : }
181 : 9229 : return true;
182 : : }
183 : :
184 : 0 : void CDInstMatchTrie::print(std::ostream& out,
185 : : Node q,
186 : : std::vector<TNode>& terms) const
187 : : {
188 [ - - ]: 0 : if (d_valid.get())
189 : : {
190 [ - - ]: 0 : if (terms.size() == q[0].getNumChildren())
191 : : {
192 : 0 : out << " ( ";
193 [ - - ]: 0 : for (unsigned i = 0; i < terms.size(); i++)
194 : : {
195 [ - - ]: 0 : if (i > 0) out << " ";
196 : 0 : out << terms[i];
197 : : }
198 : 0 : out << " )" << std::endl;
199 : : }
200 : : else
201 : : {
202 [ - - ]: 0 : for (const std::pair<const Node, CDInstMatchTrie*>& d : d_data)
203 : : {
204 : 0 : terms.push_back(d.first);
205 : 0 : d.second->print(out, q, terms);
206 : 0 : terms.pop_back();
207 : : }
208 : : }
209 : : }
210 : 0 : }
211 : :
212 : 65 : void CDInstMatchTrie::getInstantiations(
213 : : Node q, std::vector<std::vector<Node>>& insts) const
214 : : {
215 : 65 : std::vector<Node> terms;
216 : 65 : getInstantiations(q, insts, terms);
217 : 65 : }
218 : :
219 : 132 : void CDInstMatchTrie::getInstantiations(Node q,
220 : : std::vector<std::vector<Node>>& insts,
221 : : std::vector<Node>& terms) const
222 : : {
223 [ + + ]: 132 : if (!d_valid.get())
224 : : {
225 : : // do nothing
226 : : }
227 [ + + ]: 130 : else if (terms.size() == q[0].getNumChildren())
228 : : {
229 : 65 : insts.push_back(terms);
230 : : }
231 : : else
232 : : {
233 [ + + ]: 132 : for (const std::pair<const Node, CDInstMatchTrie*>& d : d_data)
234 : : {
235 : 67 : terms.push_back(d.first);
236 : 67 : d.second->getInstantiations(q, insts, terms);
237 : 67 : terms.pop_back();
238 : : }
239 : : }
240 : 132 : }
241 : :
242 : 0 : void CDInstMatchTrie::print(std::ostream& out, Node q) const
243 : : {
244 : 0 : std::vector<TNode> terms;
245 : 0 : print(out, q, terms);
246 : 0 : }
247 : :
248 : 1742 : bool InstMatchTrieOrdered::addInstMatch(Node q, const std::vector<Node>& m)
249 : : {
250 : 1742 : return d_imt.addInstMatch(q, m, d_imtio);
251 : : }
252 : :
253 : 0 : bool InstMatchTrieOrdered::existsInstMatch(Node q, const std::vector<Node>& m)
254 : : {
255 : 0 : return d_imt.existsInstMatch(q, m, d_imtio);
256 : : }
257 : :
258 : : } // namespace quantifiers
259 : : } // namespace theory
260 : : } // namespace cvc5::internal
|
