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 |
1849 |
SygusTypeInfo::SygusTypeInfo() |
33 |
|
: d_hasIte(false), |
34 |
|
d_hasBoolConnective(false), |
35 |
|
d_min_term_size(0), |
36 |
|
d_sym_cons_any_constant(-1), |
37 |
1849 |
d_has_subterm_sym_cons(false) |
38 |
|
{ |
39 |
1849 |
} |
40 |
|
|
41 |
1849 |
void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn) |
42 |
|
{ |
43 |
1849 |
d_this = tn; |
44 |
1849 |
Assert(tn.isDatatype()); |
45 |
1849 |
const DType& dt = tn.getDType(); |
46 |
1849 |
Assert(dt.isSygus()); |
47 |
1849 |
Trace("sygus-db") << "Register type " << dt.getName() << "..." << std::endl; |
48 |
3698 |
TypeNode btn = dt.getSygusType(); |
49 |
1849 |
d_btype = btn; |
50 |
1849 |
Assert(!d_btype.isNull()); |
51 |
|
// get the sygus variable list |
52 |
3698 |
Node var_list = dt.getSygusVarList(); |
53 |
1849 |
if (!var_list.isNull()) |
54 |
|
{ |
55 |
4570 |
for (unsigned j = 0; j < var_list.getNumChildren(); j++) |
56 |
|
{ |
57 |
6590 |
Node sv = var_list[j]; |
58 |
|
SygusVarNumAttribute svna; |
59 |
3295 |
sv.setAttribute(svna, j); |
60 |
3295 |
d_var_list.push_back(sv); |
61 |
|
} |
62 |
|
} |
63 |
|
else |
64 |
|
{ |
65 |
|
// no arguments to synthesis functions |
66 |
574 |
d_var_list.clear(); |
67 |
|
} |
68 |
|
|
69 |
|
// compute min term size information: this must be computed before registering |
70 |
|
// subfield types |
71 |
1849 |
d_min_term_size = 1; |
72 |
12544 |
for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) |
73 |
|
{ |
74 |
10695 |
if (dt[i].getNumArgs() == 0) |
75 |
|
{ |
76 |
4574 |
d_min_term_size = 0; |
77 |
|
} |
78 |
|
} |
79 |
|
|
80 |
|
// register connected types |
81 |
12544 |
for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) |
82 |
|
{ |
83 |
22579 |
for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) |
84 |
|
{ |
85 |
23768 |
TypeNode ctn = dt[i].getArgType(j); |
86 |
11884 |
Trace("sygus-db") << " register subfield type " << ctn << std::endl; |
87 |
11884 |
if (tds->registerSygusType(ctn)) |
88 |
|
{ |
89 |
11840 |
SygusTypeInfo& stic = tds->getTypeInfo(ctn); |
90 |
|
// carry type attributes |
91 |
11840 |
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 |
12544 |
for (unsigned i = 0; i < dt.getNumConstructors(); i++) |
100 |
|
{ |
101 |
21390 |
Node sop = dt[i].getSygusOp(); |
102 |
10695 |
Assert(!sop.isNull()); |
103 |
10695 |
Trace("sygus-db") << " Operator #" << i << " : " << sop; |
104 |
10695 |
Kind builtinKind = UNDEFINED_KIND; |
105 |
10695 |
if (sop.getKind() == kind::BUILTIN) |
106 |
|
{ |
107 |
3883 |
builtinKind = NodeManager::operatorToKind(sop); |
108 |
3883 |
Trace("sygus-db") << ", kind = " << builtinKind; |
109 |
|
} |
110 |
6812 |
else if (sop.isConst() && dt[i].getNumArgs() == 0) |
111 |
|
{ |
112 |
3126 |
Trace("sygus-db") << ", constant"; |
113 |
3126 |
d_consts[sop] = i; |
114 |
3126 |
d_arg_const[i] = sop; |
115 |
|
} |
116 |
3686 |
else if (sop.getKind() == LAMBDA) |
117 |
|
{ |
118 |
|
// do type checking |
119 |
2114 |
Assert(sop[0].getNumChildren() == dt[i].getNumArgs()); |
120 |
6096 |
for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) |
121 |
|
{ |
122 |
7964 |
TypeNode ct = dt[i].getArgType(j); |
123 |
7964 |
TypeNode cbt = tds->sygusToBuiltinType(ct); |
124 |
7964 |
TypeNode lat = sop[0][j].getType(); |
125 |
7964 |
AlwaysAssert(cbt.isSubtypeOf(lat)) |
126 |
3982 |
<< "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 |
2114 |
if (sop[1].getMetaKind() != kind::metakind::PARAMETERIZED) |
133 |
|
{ |
134 |
1739 |
size_t nchild = sop[0].getNumChildren(); |
135 |
1739 |
if (nchild == sop[1].getNumChildren()) |
136 |
|
{ |
137 |
1640 |
builtinKind = sop[1].getKind(); |
138 |
4843 |
for (size_t j = 0; j < nchild; j++) |
139 |
|
{ |
140 |
3220 |
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 |
10695 |
if (builtinKind != UNDEFINED_KIND) |
151 |
|
{ |
152 |
5506 |
d_kinds[builtinKind] = i; |
153 |
5506 |
d_arg_kind[i] = builtinKind; |
154 |
|
} |
155 |
|
// symbolic constructors |
156 |
10695 |
if (sop.getAttribute(SygusAnyConstAttribute())) |
157 |
|
{ |
158 |
44 |
d_sym_cons_any_constant = i; |
159 |
44 |
d_has_subterm_sym_cons = true; |
160 |
|
} |
161 |
10695 |
d_ops[sop] = i; |
162 |
10695 |
d_arg_ops[i] = sop; |
163 |
10695 |
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 |
21390 |
Node g = tds->mkGeneric(dt, i); |
173 |
21390 |
TypeNode gtn = g.getType(); |
174 |
21390 |
AlwaysAssert(gtn.isSubtypeOf(btn)) |
175 |
10695 |
<< "Sygus datatype " << dt.getName() |
176 |
|
<< " encodes terms that are not of type " << btn << std::endl; |
177 |
10695 |
Trace("sygus-db") << "...done register Operator #" << i << std::endl; |
178 |
10695 |
Kind gk = g.getKind(); |
179 |
10695 |
if (gk == ITE) |
180 |
|
{ |
181 |
|
// mark that this type has an ITE |
182 |
721 |
d_hasIte = true; |
183 |
721 |
if (g.getType().isBoolean()) |
184 |
|
{ |
185 |
25 |
d_hasBoolConnective = true; |
186 |
|
} |
187 |
|
} |
188 |
19462 |
else if (gk == AND || gk == OR || gk == IMPLIES || gk == XOR |
189 |
18973 |
|| (gk == EQUAL && g[0].getType().isBoolean())) |
190 |
|
{ |
191 |
978 |
d_hasBoolConnective = true; |
192 |
|
} |
193 |
|
} |
194 |
|
// compute minimum type depth information |
195 |
1849 |
computeMinTypeDepthInternal(tn, 0); |
196 |
|
// compute minimum term size information |
197 |
1849 |
d_min_term_size = 1; |
198 |
12544 |
for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) |
199 |
|
{ |
200 |
10695 |
unsigned csize = 0; |
201 |
10695 |
if (dt[i].getNumArgs() > 0) |
202 |
|
{ |
203 |
6121 |
csize = 1; |
204 |
18005 |
for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) |
205 |
|
{ |
206 |
23768 |
TypeNode ct = dt[i].getArgType(j); |
207 |
11884 |
if (ct == tn) |
208 |
|
{ |
209 |
7735 |
csize += d_min_term_size; |
210 |
|
} |
211 |
4149 |
else if (tds->isRegistered(ct)) |
212 |
|
{ |
213 |
4105 |
SygusTypeInfo& stic = tds->getTypeInfo(ct); |
214 |
4105 |
csize += stic.getMinTermSize(); |
215 |
|
} |
216 |
|
else |
217 |
|
{ |
218 |
44 |
Assert(!ct.isDatatype() || !ct.getDType().isSygus()); |
219 |
|
} |
220 |
|
} |
221 |
|
} |
222 |
10695 |
d_min_cons_term_size[i] = csize; |
223 |
|
} |
224 |
3698 |
Trace("sygus-db") << "Register type " << dt.getName() << " finished" |
225 |
1849 |
<< std::endl; |
226 |
1849 |
} |
227 |
|
|
228 |
1 |
void SygusTypeInfo::initializeVarSubclasses() |
229 |
|
{ |
230 |
1 |
if (d_var_list.empty()) |
231 |
|
{ |
232 |
|
// no variables |
233 |
|
return; |
234 |
|
} |
235 |
1 |
if (!d_var_subclass_id.empty()) |
236 |
|
{ |
237 |
|
// already computed |
238 |
|
return; |
239 |
|
} |
240 |
|
// compute variable subclasses |
241 |
2 |
std::vector<TypeNode> sf_types; |
242 |
1 |
getSubfieldTypes(sf_types); |
243 |
|
// maps variables to the list of subfield types they occur in |
244 |
2 |
std::map<Node, std::vector<TypeNode> > type_occurs; |
245 |
3 |
for (const Node& v : d_var_list) |
246 |
|
{ |
247 |
2 |
type_occurs[v].clear(); |
248 |
|
} |
249 |
|
// for each type of subfield type of this enumerator |
250 |
2 |
for (unsigned i = 0, ntypes = sf_types.size(); i < ntypes; i++) |
251 |
|
{ |
252 |
2 |
std::vector<unsigned> rm_indices; |
253 |
2 |
TypeNode stn = sf_types[i]; |
254 |
1 |
Assert(stn.isDatatype()); |
255 |
1 |
const DType& dt = stn.getDType(); |
256 |
4 |
for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++) |
257 |
|
{ |
258 |
6 |
Node sopn = dt[j].getSygusOp(); |
259 |
3 |
Assert(!sopn.isNull()); |
260 |
3 |
if (type_occurs.find(sopn) != type_occurs.end()) |
261 |
|
{ |
262 |
|
// if it is a variable, store that it occurs in stn |
263 |
2 |
type_occurs[sopn].push_back(stn); |
264 |
|
} |
265 |
|
} |
266 |
|
} |
267 |
2 |
TypeNodeIdTrie tnit; |
268 |
3 |
for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs) |
269 |
|
{ |
270 |
2 |
tnit.add(to.first, to.second); |
271 |
|
} |
272 |
|
// 0 is reserved for "no type class id" |
273 |
1 |
unsigned typeIdCount = 1; |
274 |
1 |
tnit.assignIds(d_var_subclass_id, typeIdCount); |
275 |
|
// assign the list and reverse map to index |
276 |
3 |
for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs) |
277 |
|
{ |
278 |
4 |
Node v = to.first; |
279 |
2 |
unsigned sc = d_var_subclass_id[v]; |
280 |
2 |
Trace("sygus-db") << v << " has subclass id " << sc << std::endl; |
281 |
2 |
d_var_subclass_list_index[v] = d_var_subclass_list[sc].size(); |
282 |
2 |
d_var_subclass_list[sc].push_back(v); |
283 |
|
} |
284 |
|
} |
285 |
|
|
286 |
6713 |
TypeNode SygusTypeInfo::getBuiltinType() const { return d_btype; } |
287 |
|
|
288 |
129215 |
const std::vector<Node>& SygusTypeInfo::getVarList() const |
289 |
|
{ |
290 |
129215 |
return d_var_list; |
291 |
|
} |
292 |
|
|
293 |
36257 |
void SygusTypeInfo::computeMinTypeDepthInternal(TypeNode tn, |
294 |
|
unsigned type_depth) |
295 |
|
{ |
296 |
36257 |
std::map<TypeNode, unsigned>::iterator it = d_min_type_depth.find(tn); |
297 |
36257 |
if (it != d_min_type_depth.end() && type_depth >= it->second) |
298 |
|
{ |
299 |
|
// no new information |
300 |
62292 |
return; |
301 |
|
} |
302 |
5164 |
if (!tn.isDatatype()) |
303 |
|
{ |
304 |
|
// do not recurse to non-datatype types |
305 |
106 |
return; |
306 |
|
} |
307 |
5058 |
const DType& dt = tn.getDType(); |
308 |
5058 |
if (!dt.isSygus()) |
309 |
|
{ |
310 |
|
// do not recurse to non-sygus datatype types |
311 |
|
return; |
312 |
|
} |
313 |
5058 |
d_min_type_depth[tn] = type_depth; |
314 |
|
// compute for connected types |
315 |
34551 |
for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) |
316 |
|
{ |
317 |
63901 |
for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) |
318 |
|
{ |
319 |
68816 |
TypeNode at = dt[i].getArgType(j); |
320 |
34408 |
computeMinTypeDepthInternal(at, type_depth + 1); |
321 |
|
} |
322 |
|
} |
323 |
|
} |
324 |
|
|
325 |
|
unsigned SygusTypeInfo::getMinTypeDepth(TypeNode tn) const |
326 |
|
{ |
327 |
|
std::map<TypeNode, unsigned>::const_iterator it = d_min_type_depth.find(tn); |
328 |
|
if (it != d_min_type_depth.end()) |
329 |
|
{ |
330 |
|
Assert(false); |
331 |
|
return 0; |
332 |
|
} |
333 |
|
return it->second; |
334 |
|
} |
335 |
|
|
336 |
4105 |
unsigned SygusTypeInfo::getMinTermSize() const { return d_min_term_size; } |
337 |
|
|
338 |
|
unsigned SygusTypeInfo::getMinConsTermSize(unsigned cindex) |
339 |
|
{ |
340 |
|
std::map<unsigned, unsigned>::iterator it = d_min_cons_term_size.find(cindex); |
341 |
|
if (it != d_min_cons_term_size.end()) |
342 |
|
{ |
343 |
|
return it->second; |
344 |
|
} |
345 |
|
Assert(false); |
346 |
|
return 0; |
347 |
|
} |
348 |
|
|
349 |
486 |
void SygusTypeInfo::getSubfieldTypes(std::vector<TypeNode>& sf_types) const |
350 |
|
{ |
351 |
1528 |
for (const std::pair<const TypeNode, unsigned>& st : d_min_type_depth) |
352 |
|
{ |
353 |
1042 |
sf_types.push_back(st.first); |
354 |
|
} |
355 |
486 |
} |
356 |
|
|
357 |
15338 |
int SygusTypeInfo::getKindConsNum(Kind k) const |
358 |
|
{ |
359 |
15338 |
std::map<Kind, unsigned>::const_iterator it = d_kinds.find(k); |
360 |
15338 |
if (it != d_kinds.end()) |
361 |
|
{ |
362 |
15130 |
return static_cast<int>(it->second); |
363 |
|
} |
364 |
208 |
return -1; |
365 |
|
} |
366 |
|
|
367 |
180 |
int SygusTypeInfo::getConstConsNum(Node n) const |
368 |
|
{ |
369 |
180 |
std::map<Node, unsigned>::const_iterator it = d_consts.find(n); |
370 |
180 |
if (it != d_consts.end()) |
371 |
|
{ |
372 |
156 |
return static_cast<int>(it->second); |
373 |
|
} |
374 |
24 |
return -1; |
375 |
|
} |
376 |
|
|
377 |
6 |
int SygusTypeInfo::getOpConsNum(Node n) const |
378 |
|
{ |
379 |
6 |
std::map<Node, unsigned>::const_iterator it = d_ops.find(n); |
380 |
6 |
if (it != d_ops.end()) |
381 |
|
{ |
382 |
6 |
return static_cast<int>(it->second); |
383 |
|
} |
384 |
|
return -1; |
385 |
|
} |
386 |
|
|
387 |
6169 |
bool SygusTypeInfo::hasKind(Kind k) const { return getKindConsNum(k) != -1; } |
388 |
133 |
bool SygusTypeInfo::hasIte() const { return d_hasIte; } |
389 |
93 |
bool SygusTypeInfo::hasBoolConnective() const { return d_hasBoolConnective; } |
390 |
180 |
bool SygusTypeInfo::hasConst(Node n) const { return getConstConsNum(n) != -1; } |
391 |
|
bool SygusTypeInfo::hasOp(Node n) const { return getOpConsNum(n) != -1; } |
392 |
|
|
393 |
|
Node SygusTypeInfo::getConsNumOp(unsigned i) const |
394 |
|
{ |
395 |
|
std::map<unsigned, Node>::const_iterator itn = d_arg_ops.find(i); |
396 |
|
if (itn != d_arg_ops.end()) |
397 |
|
{ |
398 |
|
return itn->second; |
399 |
|
} |
400 |
|
return Node::null(); |
401 |
|
} |
402 |
|
|
403 |
2333 |
Node SygusTypeInfo::getConsNumConst(unsigned i) const |
404 |
|
{ |
405 |
2333 |
std::map<unsigned, Node>::const_iterator itn = d_arg_const.find(i); |
406 |
2333 |
if (itn != d_arg_const.end()) |
407 |
|
{ |
408 |
1238 |
return itn->second; |
409 |
|
} |
410 |
1095 |
return Node::null(); |
411 |
|
} |
412 |
|
|
413 |
7778 |
Kind SygusTypeInfo::getConsNumKind(unsigned i) const |
414 |
|
{ |
415 |
7778 |
std::map<unsigned, Kind>::const_iterator itk = d_arg_kind.find(i); |
416 |
7778 |
if (itk != d_arg_kind.end()) |
417 |
|
{ |
418 |
3869 |
return itk->second; |
419 |
|
} |
420 |
3909 |
return UNDEFINED_KIND; |
421 |
|
} |
422 |
|
|
423 |
|
bool SygusTypeInfo::isKindArg(unsigned i) const |
424 |
|
{ |
425 |
|
return getConsNumKind(i) != UNDEFINED_KIND; |
426 |
|
} |
427 |
|
|
428 |
|
bool SygusTypeInfo::isConstArg(unsigned i) const |
429 |
|
{ |
430 |
|
return d_arg_const.find(i) != d_arg_const.end(); |
431 |
|
} |
432 |
|
|
433 |
1739 |
int SygusTypeInfo::getAnyConstantConsNum() const |
434 |
|
{ |
435 |
1739 |
return d_sym_cons_any_constant; |
436 |
|
} |
437 |
|
|
438 |
10518 |
bool SygusTypeInfo::hasSubtermSymbolicCons() const |
439 |
|
{ |
440 |
10518 |
return d_has_subterm_sym_cons; |
441 |
|
} |
442 |
|
|
443 |
13 |
unsigned SygusTypeInfo::getSubclassForVar(Node n) const |
444 |
|
{ |
445 |
13 |
std::map<Node, unsigned>::const_iterator itcc = d_var_subclass_id.find(n); |
446 |
13 |
if (itcc == d_var_subclass_id.end()) |
447 |
|
{ |
448 |
|
Assert(false); |
449 |
|
return 0; |
450 |
|
} |
451 |
13 |
return itcc->second; |
452 |
|
} |
453 |
|
|
454 |
8 |
unsigned SygusTypeInfo::getNumSubclassVars(unsigned sc) const |
455 |
|
{ |
456 |
|
std::map<unsigned, std::vector<Node> >::const_iterator itvv = |
457 |
8 |
d_var_subclass_list.find(sc); |
458 |
8 |
if (itvv == d_var_subclass_list.end()) |
459 |
|
{ |
460 |
|
Assert(false); |
461 |
|
return 0; |
462 |
|
} |
463 |
8 |
return itvv->second.size(); |
464 |
|
} |
465 |
3 |
Node SygusTypeInfo::getVarSubclassIndex(unsigned sc, unsigned i) const |
466 |
|
{ |
467 |
|
std::map<unsigned, std::vector<Node> >::const_iterator itvv = |
468 |
3 |
d_var_subclass_list.find(sc); |
469 |
3 |
if (itvv == d_var_subclass_list.end() || i >= itvv->second.size()) |
470 |
|
{ |
471 |
|
Assert(false); |
472 |
|
return Node::null(); |
473 |
|
} |
474 |
3 |
return itvv->second[i]; |
475 |
|
} |
476 |
|
|
477 |
6 |
bool SygusTypeInfo::getIndexInSubclassForVar(Node v, unsigned& index) const |
478 |
|
{ |
479 |
|
std::map<Node, unsigned>::const_iterator itvv = |
480 |
6 |
d_var_subclass_list_index.find(v); |
481 |
6 |
if (itvv == d_var_subclass_list_index.end()) |
482 |
|
{ |
483 |
|
return false; |
484 |
|
} |
485 |
6 |
index = itvv->second; |
486 |
6 |
return true; |
487 |
|
} |
488 |
|
|
489 |
1 |
bool SygusTypeInfo::isSubclassVarTrivial() const |
490 |
|
{ |
491 |
|
for (const std::pair<const unsigned, std::vector<Node> >& p : |
492 |
1 |
d_var_subclass_list) |
493 |
|
{ |
494 |
1 |
if (p.second.size() > 1) |
495 |
|
{ |
496 |
1 |
return false; |
497 |
|
} |
498 |
|
} |
499 |
|
return true; |
500 |
|
} |
501 |
|
|
502 |
|
} // namespace quantifiers |
503 |
|
} // namespace theory |
504 |
29286 |
} // namespace cvc5 |