1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Mathias Preiner, Aina Niemetz |
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 sygus type info class. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/quantifiers/sygus/type_info.h" |
17 |
|
|
18 |
|
#include "base/check.h" |
19 |
|
#include "expr/dtype.h" |
20 |
|
#include "expr/dtype_cons.h" |
21 |
|
#include "expr/sygus_datatype.h" |
22 |
|
#include "theory/datatypes/sygus_datatype_utils.h" |
23 |
|
#include "theory/quantifiers/sygus/term_database_sygus.h" |
24 |
|
#include "theory/quantifiers/sygus/type_node_id_trie.h" |
25 |
|
|
26 |
|
using namespace cvc5::kind; |
27 |
|
|
28 |
|
namespace cvc5 { |
29 |
|
namespace theory { |
30 |
|
namespace quantifiers { |
31 |
|
|
32 |
1767 |
SygusTypeInfo::SygusTypeInfo() |
33 |
|
: d_hasIte(false), |
34 |
|
d_hasBoolConnective(false), |
35 |
|
d_min_term_size(0), |
36 |
|
d_sym_cons_any_constant(-1), |
37 |
1767 |
d_has_subterm_sym_cons(false) |
38 |
|
{ |
39 |
1767 |
} |
40 |
|
|
41 |
1767 |
void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn) |
42 |
|
{ |
43 |
1767 |
d_this = tn; |
44 |
1767 |
Assert(tn.isDatatype()); |
45 |
1767 |
const DType& dt = tn.getDType(); |
46 |
1767 |
Assert(dt.isSygus()); |
47 |
1767 |
Trace("sygus-db") << "Register type " << dt.getName() << "..." << std::endl; |
48 |
3534 |
TypeNode btn = dt.getSygusType(); |
49 |
1767 |
d_btype = btn; |
50 |
1767 |
Assert(!d_btype.isNull()); |
51 |
|
// get the sygus variable list |
52 |
3534 |
Node var_list = dt.getSygusVarList(); |
53 |
1767 |
if (!var_list.isNull()) |
54 |
|
{ |
55 |
4984 |
for (unsigned j = 0; j < var_list.getNumChildren(); j++) |
56 |
|
{ |
57 |
7234 |
Node sv = var_list[j]; |
58 |
|
SygusVarNumAttribute svna; |
59 |
3617 |
sv.setAttribute(svna, j); |
60 |
3617 |
d_var_list.push_back(sv); |
61 |
|
} |
62 |
|
} |
63 |
|
else |
64 |
|
{ |
65 |
|
// no arguments to synthesis functions |
66 |
400 |
d_var_list.clear(); |
67 |
|
} |
68 |
|
|
69 |
|
// compute min term size information: this must be computed before registering |
70 |
|
// subfield types |
71 |
1767 |
d_min_term_size = 1; |
72 |
12302 |
for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) |
73 |
|
{ |
74 |
10535 |
if (dt[i].getNumArgs() == 0) |
75 |
|
{ |
76 |
4500 |
d_min_term_size = 0; |
77 |
|
} |
78 |
|
} |
79 |
|
|
80 |
|
// register connected types |
81 |
12302 |
for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) |
82 |
|
{ |
83 |
22229 |
for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) |
84 |
|
{ |
85 |
23388 |
TypeNode ctn = dt[i].getArgType(j); |
86 |
11694 |
Trace("sygus-db") << " register subfield type " << ctn << std::endl; |
87 |
11694 |
if (tds->registerSygusType(ctn)) |
88 |
|
{ |
89 |
11650 |
SygusTypeInfo& stic = tds->getTypeInfo(ctn); |
90 |
|
// carry type attributes |
91 |
11650 |
if (stic.d_has_subterm_sym_cons) |
92 |
|
{ |
93 |
222 |
d_has_subterm_sym_cons = true; |
94 |
|
} |
95 |
|
} |
96 |
|
} |
97 |
|
} |
98 |
|
// iterate over constructors |
99 |
12302 |
for (unsigned i = 0; i < dt.getNumConstructors(); i++) |
100 |
|
{ |
101 |
21070 |
Node sop = dt[i].getSygusOp(); |
102 |
10535 |
Assert(!sop.isNull()); |
103 |
10535 |
Trace("sygus-db") << " Operator #" << i << " : " << sop; |
104 |
10535 |
Kind builtinKind = UNDEFINED_KIND; |
105 |
10535 |
if (sop.getKind() == kind::BUILTIN) |
106 |
|
{ |
107 |
3812 |
builtinKind = NodeManager::operatorToKind(sop); |
108 |
3812 |
Trace("sygus-db") << ", kind = " << builtinKind; |
109 |
|
} |
110 |
6723 |
else if (sop.isConst() && dt[i].getNumArgs() == 0) |
111 |
|
{ |
112 |
2929 |
Trace("sygus-db") << ", constant"; |
113 |
2929 |
d_consts[sop] = i; |
114 |
2929 |
d_arg_const[i] = sop; |
115 |
|
} |
116 |
3794 |
else if (sop.getKind() == LAMBDA) |
117 |
|
{ |
118 |
|
// do type checking |
119 |
2064 |
Assert(sop[0].getNumChildren() == dt[i].getNumArgs()); |
120 |
5946 |
for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) |
121 |
|
{ |
122 |
7764 |
TypeNode ct = dt[i].getArgType(j); |
123 |
7764 |
TypeNode cbt = tds->sygusToBuiltinType(ct); |
124 |
7764 |
TypeNode lat = sop[0][j].getType(); |
125 |
7764 |
AlwaysAssert(cbt.isSubtypeOf(lat)) |
126 |
3882 |
<< "In sygus datatype " << dt.getName() |
127 |
|
<< ", argument to a lambda constructor is not " << lat << std::endl; |
128 |
|
} |
129 |
|
// See if it is a builtin kind, possible if the operator is of the form: |
130 |
|
// lambda x1 ... xn. f( x1, ..., xn ) and f is not a parameterized kind |
131 |
|
// (e.g. APPLY_UF is a parameterized kind). |
132 |
2064 |
if (sop[1].getMetaKind() != kind::metakind::PARAMETERIZED) |
133 |
|
{ |
134 |
1721 |
size_t nchild = sop[0].getNumChildren(); |
135 |
1721 |
if (nchild == sop[1].getNumChildren()) |
136 |
|
{ |
137 |
1622 |
builtinKind = sop[1].getKind(); |
138 |
4789 |
for (size_t j = 0; j < nchild; j++) |
139 |
|
{ |
140 |
3184 |
if (sop[0][j] != sop[1][j]) |
141 |
|
{ |
142 |
|
// arguments not in order |
143 |
17 |
builtinKind = UNDEFINED_KIND; |
144 |
17 |
break; |
145 |
|
} |
146 |
|
} |
147 |
|
} |
148 |
|
} |
149 |
|
} |
150 |
10535 |
if (builtinKind != UNDEFINED_KIND) |
151 |
|
{ |
152 |
5417 |
d_kinds[builtinKind] = i; |
153 |
5417 |
d_arg_kind[i] = builtinKind; |
154 |
|
} |
155 |
|
// symbolic constructors |
156 |
10535 |
if (sop.getAttribute(SygusAnyConstAttribute())) |
157 |
|
{ |
158 |
44 |
d_sym_cons_any_constant = i; |
159 |
44 |
d_has_subterm_sym_cons = true; |
160 |
|
} |
161 |
10535 |
d_ops[sop] = i; |
162 |
10535 |
d_arg_ops[i] = sop; |
163 |
10535 |
Trace("sygus-db") << std::endl; |
164 |
|
// We must properly catch type errors in sygus grammars for arguments of |
165 |
|
// builtin operators. The challenge is that we easily ask for expected |
166 |
|
// argument types of builtin operators e.g. PLUS. Hence we use a call to |
167 |
|
// mkGeneric below. This ensures that terms that this constructor encodes |
168 |
|
// are of the type specified in the datatype. This will fail if |
169 |
|
// e.g. bitvector-and is a constructor of an integer grammar. Our (version |
170 |
|
// 2) SyGuS parser ensures that sygus constructors are built from well-typed |
171 |
|
// terms, so the term created by mkGeneric will also be well-typed here. |
172 |
21070 |
Node g = tds->mkGeneric(dt, i); |
173 |
21070 |
TypeNode gtn = g.getType(); |
174 |
21070 |
AlwaysAssert(gtn.isSubtypeOf(btn)) |
175 |
10535 |
<< "Sygus datatype " << dt.getName() |
176 |
|
<< " encodes terms that are not of type " << btn << std::endl; |
177 |
10535 |
Trace("sygus-db") << "...done register Operator #" << i << std::endl; |
178 |
10535 |
Kind gk = g.getKind(); |
179 |
10535 |
if (gk == ITE) |
180 |
|
{ |
181 |
|
// mark that this type has an ITE |
182 |
730 |
d_hasIte = true; |
183 |
730 |
if (g.getType().isBoolean()) |
184 |
|
{ |
185 |
29 |
d_hasBoolConnective = true; |
186 |
|
} |
187 |
|
} |
188 |
19133 |
else if (gk == AND || gk == OR || gk == IMPLIES || gk == XOR |
189 |
18653 |
|| (gk == EQUAL && g[0].getType().isBoolean())) |
190 |
|
{ |
191 |
960 |
d_hasBoolConnective = true; |
192 |
|
} |
193 |
10535 |
if (Trace.isOn("sygus-db")) |
194 |
|
{ |
195 |
|
Node eop = datatypes::utils::getExpandedDefinitionForm(sop); |
196 |
|
Trace("sygus-db") << "Expanded form: "; |
197 |
|
if (eop == sop) |
198 |
|
{ |
199 |
|
Trace("sygus-db") << "same"; |
200 |
|
} |
201 |
|
else |
202 |
|
{ |
203 |
|
Trace("sygus-db") << eop; |
204 |
|
} |
205 |
|
Trace("sygus-db") << std::endl; |
206 |
|
} |
207 |
|
} |
208 |
|
// compute minimum type depth information |
209 |
1767 |
computeMinTypeDepthInternal(tn, 0); |
210 |
|
// compute minimum term size information |
211 |
1767 |
d_min_term_size = 1; |
212 |
12302 |
for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) |
213 |
|
{ |
214 |
10535 |
unsigned csize = 0; |
215 |
10535 |
if (dt[i].getNumArgs() > 0) |
216 |
|
{ |
217 |
6035 |
csize = 1; |
218 |
17729 |
for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) |
219 |
|
{ |
220 |
23388 |
TypeNode ct = dt[i].getArgType(j); |
221 |
11694 |
if (ct == tn) |
222 |
|
{ |
223 |
7600 |
csize += d_min_term_size; |
224 |
|
} |
225 |
4094 |
else if (tds->isRegistered(ct)) |
226 |
|
{ |
227 |
4050 |
SygusTypeInfo& stic = tds->getTypeInfo(ct); |
228 |
4050 |
csize += stic.getMinTermSize(); |
229 |
|
} |
230 |
|
else |
231 |
|
{ |
232 |
44 |
Assert(!ct.isDatatype() || !ct.getDType().isSygus()); |
233 |
|
} |
234 |
|
} |
235 |
|
} |
236 |
10535 |
d_min_cons_term_size[i] = csize; |
237 |
|
} |
238 |
3534 |
Trace("sygus-db") << "Register type " << dt.getName() << " finished" |
239 |
1767 |
<< std::endl; |
240 |
1767 |
} |
241 |
|
|
242 |
1 |
void SygusTypeInfo::initializeVarSubclasses() |
243 |
|
{ |
244 |
1 |
if (d_var_list.empty()) |
245 |
|
{ |
246 |
|
// no variables |
247 |
|
return; |
248 |
|
} |
249 |
1 |
if (!d_var_subclass_id.empty()) |
250 |
|
{ |
251 |
|
// already computed |
252 |
|
return; |
253 |
|
} |
254 |
|
// compute variable subclasses |
255 |
2 |
std::vector<TypeNode> sf_types; |
256 |
1 |
getSubfieldTypes(sf_types); |
257 |
|
// maps variables to the list of subfield types they occur in |
258 |
2 |
std::map<Node, std::vector<TypeNode> > type_occurs; |
259 |
3 |
for (const Node& v : d_var_list) |
260 |
|
{ |
261 |
2 |
type_occurs[v].clear(); |
262 |
|
} |
263 |
|
// for each type of subfield type of this enumerator |
264 |
2 |
for (unsigned i = 0, ntypes = sf_types.size(); i < ntypes; i++) |
265 |
|
{ |
266 |
2 |
std::vector<unsigned> rm_indices; |
267 |
2 |
TypeNode stn = sf_types[i]; |
268 |
1 |
Assert(stn.isDatatype()); |
269 |
1 |
const DType& dt = stn.getDType(); |
270 |
4 |
for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++) |
271 |
|
{ |
272 |
6 |
Node sopn = dt[j].getSygusOp(); |
273 |
3 |
Assert(!sopn.isNull()); |
274 |
3 |
if (type_occurs.find(sopn) != type_occurs.end()) |
275 |
|
{ |
276 |
|
// if it is a variable, store that it occurs in stn |
277 |
2 |
type_occurs[sopn].push_back(stn); |
278 |
|
} |
279 |
|
} |
280 |
|
} |
281 |
2 |
TypeNodeIdTrie tnit; |
282 |
3 |
for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs) |
283 |
|
{ |
284 |
2 |
tnit.add(to.first, to.second); |
285 |
|
} |
286 |
|
// 0 is reserved for "no type class id" |
287 |
1 |
unsigned typeIdCount = 1; |
288 |
1 |
tnit.assignIds(d_var_subclass_id, typeIdCount); |
289 |
|
// assign the list and reverse map to index |
290 |
3 |
for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs) |
291 |
|
{ |
292 |
4 |
Node v = to.first; |
293 |
2 |
unsigned sc = d_var_subclass_id[v]; |
294 |
2 |
Trace("sygus-db") << v << " has subclass id " << sc << std::endl; |
295 |
2 |
d_var_subclass_list_index[v] = d_var_subclass_list[sc].size(); |
296 |
2 |
d_var_subclass_list[sc].push_back(v); |
297 |
|
} |
298 |
|
} |
299 |
|
|
300 |
6664 |
TypeNode SygusTypeInfo::getBuiltinType() const { return d_btype; } |
301 |
|
|
302 |
129080 |
const std::vector<Node>& SygusTypeInfo::getVarList() const |
303 |
|
{ |
304 |
129080 |
return d_var_list; |
305 |
|
} |
306 |
|
|
307 |
37573 |
void SygusTypeInfo::computeMinTypeDepthInternal(TypeNode tn, |
308 |
|
unsigned type_depth) |
309 |
|
{ |
310 |
37573 |
std::map<TypeNode, unsigned>::iterator it = d_min_type_depth.find(tn); |
311 |
37573 |
if (it != d_min_type_depth.end() && type_depth >= it->second) |
312 |
|
{ |
313 |
|
// no new information |
314 |
64918 |
return; |
315 |
|
} |
316 |
5167 |
if (!tn.isDatatype()) |
317 |
|
{ |
318 |
|
// do not recurse to non-datatype types |
319 |
106 |
return; |
320 |
|
} |
321 |
5061 |
const DType& dt = tn.getDType(); |
322 |
5061 |
if (!dt.isSygus()) |
323 |
|
{ |
324 |
|
// do not recurse to non-sygus datatype types |
325 |
|
return; |
326 |
|
} |
327 |
5061 |
d_min_type_depth[tn] = type_depth; |
328 |
|
// compute for connected types |
329 |
35319 |
for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) |
330 |
|
{ |
331 |
66064 |
for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) |
332 |
|
{ |
333 |
71612 |
TypeNode at = dt[i].getArgType(j); |
334 |
35806 |
computeMinTypeDepthInternal(at, type_depth + 1); |
335 |
|
} |
336 |
|
} |
337 |
|
} |
338 |
|
|
339 |
|
unsigned SygusTypeInfo::getMinTypeDepth(TypeNode tn) const |
340 |
|
{ |
341 |
|
std::map<TypeNode, unsigned>::const_iterator it = d_min_type_depth.find(tn); |
342 |
|
if (it != d_min_type_depth.end()) |
343 |
|
{ |
344 |
|
Assert(false); |
345 |
|
return 0; |
346 |
|
} |
347 |
|
return it->second; |
348 |
|
} |
349 |
|
|
350 |
4050 |
unsigned SygusTypeInfo::getMinTermSize() const { return d_min_term_size; } |
351 |
|
|
352 |
|
unsigned SygusTypeInfo::getMinConsTermSize(unsigned cindex) |
353 |
|
{ |
354 |
|
std::map<unsigned, unsigned>::iterator it = d_min_cons_term_size.find(cindex); |
355 |
|
if (it != d_min_cons_term_size.end()) |
356 |
|
{ |
357 |
|
return it->second; |
358 |
|
} |
359 |
|
Assert(false); |
360 |
|
return 0; |
361 |
|
} |
362 |
|
|
363 |
412 |
void SygusTypeInfo::getSubfieldTypes(std::vector<TypeNode>& sf_types) const |
364 |
|
{ |
365 |
1298 |
for (const std::pair<const TypeNode, unsigned>& st : d_min_type_depth) |
366 |
|
{ |
367 |
886 |
sf_types.push_back(st.first); |
368 |
|
} |
369 |
412 |
} |
370 |
|
|
371 |
15299 |
int SygusTypeInfo::getKindConsNum(Kind k) const |
372 |
|
{ |
373 |
15299 |
std::map<Kind, unsigned>::const_iterator it = d_kinds.find(k); |
374 |
15299 |
if (it != d_kinds.end()) |
375 |
|
{ |
376 |
15090 |
return static_cast<int>(it->second); |
377 |
|
} |
378 |
209 |
return -1; |
379 |
|
} |
380 |
|
|
381 |
178 |
int SygusTypeInfo::getConstConsNum(Node n) const |
382 |
|
{ |
383 |
178 |
std::map<Node, unsigned>::const_iterator it = d_consts.find(n); |
384 |
178 |
if (it != d_consts.end()) |
385 |
|
{ |
386 |
155 |
return static_cast<int>(it->second); |
387 |
|
} |
388 |
23 |
return -1; |
389 |
|
} |
390 |
|
|
391 |
6 |
int SygusTypeInfo::getOpConsNum(Node n) const |
392 |
|
{ |
393 |
6 |
std::map<Node, unsigned>::const_iterator it = d_ops.find(n); |
394 |
6 |
if (it != d_ops.end()) |
395 |
|
{ |
396 |
6 |
return static_cast<int>(it->second); |
397 |
|
} |
398 |
|
return -1; |
399 |
|
} |
400 |
|
|
401 |
6151 |
bool SygusTypeInfo::hasKind(Kind k) const { return getKindConsNum(k) != -1; } |
402 |
134 |
bool SygusTypeInfo::hasIte() const { return d_hasIte; } |
403 |
91 |
bool SygusTypeInfo::hasBoolConnective() const { return d_hasBoolConnective; } |
404 |
178 |
bool SygusTypeInfo::hasConst(Node n) const { return getConstConsNum(n) != -1; } |
405 |
|
bool SygusTypeInfo::hasOp(Node n) const { return getOpConsNum(n) != -1; } |
406 |
|
|
407 |
|
Node SygusTypeInfo::getConsNumOp(unsigned i) const |
408 |
|
{ |
409 |
|
std::map<unsigned, Node>::const_iterator itn = d_arg_ops.find(i); |
410 |
|
if (itn != d_arg_ops.end()) |
411 |
|
{ |
412 |
|
return itn->second; |
413 |
|
} |
414 |
|
return Node::null(); |
415 |
|
} |
416 |
|
|
417 |
2262 |
Node SygusTypeInfo::getConsNumConst(unsigned i) const |
418 |
|
{ |
419 |
2262 |
std::map<unsigned, Node>::const_iterator itn = d_arg_const.find(i); |
420 |
2262 |
if (itn != d_arg_const.end()) |
421 |
|
{ |
422 |
1226 |
return itn->second; |
423 |
|
} |
424 |
1036 |
return Node::null(); |
425 |
|
} |
426 |
|
|
427 |
7297 |
Kind SygusTypeInfo::getConsNumKind(unsigned i) const |
428 |
|
{ |
429 |
7297 |
std::map<unsigned, Kind>::const_iterator itk = d_arg_kind.find(i); |
430 |
7297 |
if (itk != d_arg_kind.end()) |
431 |
|
{ |
432 |
3808 |
return itk->second; |
433 |
|
} |
434 |
3489 |
return UNDEFINED_KIND; |
435 |
|
} |
436 |
|
|
437 |
|
bool SygusTypeInfo::isKindArg(unsigned i) const |
438 |
|
{ |
439 |
|
return getConsNumKind(i) != UNDEFINED_KIND; |
440 |
|
} |
441 |
|
|
442 |
|
bool SygusTypeInfo::isConstArg(unsigned i) const |
443 |
|
{ |
444 |
|
return d_arg_const.find(i) != d_arg_const.end(); |
445 |
|
} |
446 |
|
|
447 |
1570 |
int SygusTypeInfo::getAnyConstantConsNum() const |
448 |
|
{ |
449 |
1570 |
return d_sym_cons_any_constant; |
450 |
|
} |
451 |
|
|
452 |
8550 |
bool SygusTypeInfo::hasSubtermSymbolicCons() const |
453 |
|
{ |
454 |
8550 |
return d_has_subterm_sym_cons; |
455 |
|
} |
456 |
|
|
457 |
13 |
unsigned SygusTypeInfo::getSubclassForVar(Node n) const |
458 |
|
{ |
459 |
13 |
std::map<Node, unsigned>::const_iterator itcc = d_var_subclass_id.find(n); |
460 |
13 |
if (itcc == d_var_subclass_id.end()) |
461 |
|
{ |
462 |
|
Assert(false); |
463 |
|
return 0; |
464 |
|
} |
465 |
13 |
return itcc->second; |
466 |
|
} |
467 |
|
|
468 |
8 |
unsigned SygusTypeInfo::getNumSubclassVars(unsigned sc) const |
469 |
|
{ |
470 |
|
std::map<unsigned, std::vector<Node> >::const_iterator itvv = |
471 |
8 |
d_var_subclass_list.find(sc); |
472 |
8 |
if (itvv == d_var_subclass_list.end()) |
473 |
|
{ |
474 |
|
Assert(false); |
475 |
|
return 0; |
476 |
|
} |
477 |
8 |
return itvv->second.size(); |
478 |
|
} |
479 |
3 |
Node SygusTypeInfo::getVarSubclassIndex(unsigned sc, unsigned i) const |
480 |
|
{ |
481 |
|
std::map<unsigned, std::vector<Node> >::const_iterator itvv = |
482 |
3 |
d_var_subclass_list.find(sc); |
483 |
3 |
if (itvv == d_var_subclass_list.end() || i >= itvv->second.size()) |
484 |
|
{ |
485 |
|
Assert(false); |
486 |
|
return Node::null(); |
487 |
|
} |
488 |
3 |
return itvv->second[i]; |
489 |
|
} |
490 |
|
|
491 |
6 |
bool SygusTypeInfo::getIndexInSubclassForVar(Node v, unsigned& index) const |
492 |
|
{ |
493 |
|
std::map<Node, unsigned>::const_iterator itvv = |
494 |
6 |
d_var_subclass_list_index.find(v); |
495 |
6 |
if (itvv == d_var_subclass_list_index.end()) |
496 |
|
{ |
497 |
|
return false; |
498 |
|
} |
499 |
6 |
index = itvv->second; |
500 |
6 |
return true; |
501 |
|
} |
502 |
|
|
503 |
1 |
bool SygusTypeInfo::isSubclassVarTrivial() const |
504 |
|
{ |
505 |
|
for (const std::pair<const unsigned, std::vector<Node> >& p : |
506 |
1 |
d_var_subclass_list) |
507 |
|
{ |
508 |
1 |
if (p.second.size() > 1) |
509 |
|
{ |
510 |
1 |
return false; |
511 |
|
} |
512 |
|
} |
513 |
|
return true; |
514 |
|
} |
515 |
|
|
516 |
|
} // namespace quantifiers |
517 |
|
} // namespace theory |
518 |
22755 |
} // namespace cvc5 |