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