1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Gereon Kremer, 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 |
|
* Implementation of the higher-order extension of TheoryUF. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/uf/ho_extension.h" |
17 |
|
|
18 |
|
#include "expr/node_algorithm.h" |
19 |
|
#include "expr/skolem_manager.h" |
20 |
|
#include "options/uf_options.h" |
21 |
|
#include "theory/theory_model.h" |
22 |
|
#include "theory/uf/theory_uf_rewriter.h" |
23 |
|
|
24 |
|
using namespace std; |
25 |
|
using namespace cvc5::kind; |
26 |
|
|
27 |
|
namespace cvc5 { |
28 |
|
namespace theory { |
29 |
|
namespace uf { |
30 |
|
|
31 |
238 |
HoExtension::HoExtension(Env& env, |
32 |
|
TheoryState& state, |
33 |
238 |
TheoryInferenceManager& im) |
34 |
|
: EnvObj(env), |
35 |
|
d_state(state), |
36 |
|
d_im(im), |
37 |
238 |
d_extensionality(userContext()), |
38 |
476 |
d_uf_std_skolem(userContext()) |
39 |
|
{ |
40 |
238 |
d_true = NodeManager::currentNM()->mkConst(true); |
41 |
238 |
} |
42 |
|
|
43 |
744 |
Node HoExtension::ppRewrite(Node node) |
44 |
|
{ |
45 |
|
// convert HO_APPLY to APPLY_UF if fully applied |
46 |
744 |
if (node.getKind() == HO_APPLY) |
47 |
|
{ |
48 |
328 |
if (node[0].getType().getNumChildren() == 2) |
49 |
|
{ |
50 |
119 |
Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl; |
51 |
238 |
Node ret = getApplyUfForHoApply(node); |
52 |
238 |
Trace("uf-ho") << "uf-ho : ppRewrite : " << node << " to " << ret |
53 |
119 |
<< std::endl; |
54 |
119 |
return ret; |
55 |
|
} |
56 |
|
} |
57 |
625 |
return node; |
58 |
|
} |
59 |
|
|
60 |
361 |
Node HoExtension::getExtensionalityDeq(TNode deq, bool isCached) |
61 |
|
{ |
62 |
361 |
Assert(deq.getKind() == NOT && deq[0].getKind() == EQUAL); |
63 |
361 |
Assert(deq[0][0].getType().isFunction()); |
64 |
361 |
if (isCached) |
65 |
|
{ |
66 |
276 |
std::map<Node, Node>::iterator it = d_extensionality_deq.find(deq); |
67 |
276 |
if (it != d_extensionality_deq.end()) |
68 |
|
{ |
69 |
|
return it->second; |
70 |
|
} |
71 |
|
} |
72 |
722 |
TypeNode tn = deq[0][0].getType(); |
73 |
722 |
std::vector<TypeNode> argTypes = tn.getArgTypes(); |
74 |
722 |
std::vector<Node> skolems; |
75 |
361 |
NodeManager* nm = NodeManager::currentNM(); |
76 |
361 |
SkolemManager* sm = nm->getSkolemManager(); |
77 |
770 |
for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++) |
78 |
|
{ |
79 |
|
Node k = sm->mkDummySkolem( |
80 |
818 |
"k", argTypes[i], "skolem created for extensionality."); |
81 |
409 |
skolems.push_back(k); |
82 |
|
} |
83 |
722 |
Node t[2]; |
84 |
1083 |
for (unsigned i = 0; i < 2; i++) |
85 |
|
{ |
86 |
1444 |
std::vector<Node> children; |
87 |
1444 |
Node curr = deq[0][i]; |
88 |
1868 |
while (curr.getKind() == HO_APPLY) |
89 |
|
{ |
90 |
573 |
children.push_back(curr[1]); |
91 |
573 |
curr = curr[0]; |
92 |
|
} |
93 |
722 |
children.push_back(curr); |
94 |
722 |
std::reverse(children.begin(), children.end()); |
95 |
722 |
children.insert(children.end(), skolems.begin(), skolems.end()); |
96 |
722 |
t[i] = nm->mkNode(APPLY_UF, children); |
97 |
|
} |
98 |
722 |
Node conc = t[0].eqNode(t[1]).negate(); |
99 |
361 |
if (isCached) |
100 |
|
{ |
101 |
276 |
d_extensionality_deq[deq] = conc; |
102 |
|
} |
103 |
361 |
return conc; |
104 |
|
} |
105 |
|
|
106 |
3829 |
unsigned HoExtension::applyExtensionality(TNode deq) |
107 |
|
{ |
108 |
3829 |
Assert(deq.getKind() == NOT && deq[0].getKind() == EQUAL); |
109 |
3829 |
Assert(deq[0][0].getType().isFunction()); |
110 |
|
// apply extensionality |
111 |
3829 |
if (d_extensionality.find(deq) == d_extensionality.end()) |
112 |
|
{ |
113 |
276 |
d_extensionality.insert(deq); |
114 |
552 |
Node conc = getExtensionalityDeq(deq); |
115 |
552 |
Node lem = NodeManager::currentNM()->mkNode(OR, deq[0], conc); |
116 |
552 |
Trace("uf-ho-lemma") << "uf-ho-lemma : extensionality : " << lem |
117 |
276 |
<< std::endl; |
118 |
276 |
d_im.lemma(lem, InferenceId::UF_HO_EXTENSIONALITY); |
119 |
276 |
return 1; |
120 |
|
} |
121 |
3553 |
return 0; |
122 |
|
} |
123 |
|
|
124 |
119 |
Node HoExtension::getApplyUfForHoApply(Node node) |
125 |
|
{ |
126 |
119 |
Assert(node[0].getType().getNumChildren() == 2); |
127 |
238 |
std::vector<TNode> args; |
128 |
238 |
Node f = TheoryUfRewriter::decomposeHoApply(node, args, true); |
129 |
238 |
Node new_f = f; |
130 |
119 |
NodeManager* nm = NodeManager::currentNM(); |
131 |
119 |
SkolemManager* sm = nm->getSkolemManager(); |
132 |
119 |
if (!TheoryUfRewriter::canUseAsApplyUfOperator(f)) |
133 |
|
{ |
134 |
|
NodeNodeMap::const_iterator itus = d_uf_std_skolem.find(f); |
135 |
|
if (itus == d_uf_std_skolem.end()) |
136 |
|
{ |
137 |
|
std::unordered_set<Node> fvs; |
138 |
|
expr::getFreeVariables(f, fvs); |
139 |
|
Node lem; |
140 |
|
if (!fvs.empty()) |
141 |
|
{ |
142 |
|
std::vector<TypeNode> newTypes; |
143 |
|
std::vector<Node> vs; |
144 |
|
std::vector<Node> nvs; |
145 |
|
for (const Node& v : fvs) |
146 |
|
{ |
147 |
|
TypeNode vt = v.getType(); |
148 |
|
newTypes.push_back(vt); |
149 |
|
Node nv = nm->mkBoundVar(vt); |
150 |
|
vs.push_back(v); |
151 |
|
nvs.push_back(nv); |
152 |
|
} |
153 |
|
TypeNode ft = f.getType(); |
154 |
|
std::vector<TypeNode> argTypes = ft.getArgTypes(); |
155 |
|
TypeNode rangeType = ft.getRangeType(); |
156 |
|
|
157 |
|
newTypes.insert(newTypes.end(), argTypes.begin(), argTypes.end()); |
158 |
|
TypeNode nft = nm->mkFunctionType(newTypes, rangeType); |
159 |
|
new_f = sm->mkDummySkolem("app_uf", nft); |
160 |
|
for (const Node& v : vs) |
161 |
|
{ |
162 |
|
new_f = nm->mkNode(HO_APPLY, new_f, v); |
163 |
|
} |
164 |
|
Assert(new_f.getType() == f.getType()); |
165 |
|
Node eq = new_f.eqNode(f); |
166 |
|
Node seq = eq.substitute(vs.begin(), vs.end(), nvs.begin(), nvs.end()); |
167 |
|
lem = nm->mkNode( |
168 |
|
FORALL, nm->mkNode(BOUND_VAR_LIST, nvs), seq); |
169 |
|
} |
170 |
|
else |
171 |
|
{ |
172 |
|
// introduce skolem to make a standard APPLY_UF |
173 |
|
new_f = sm->mkDummySkolem("app_uf", f.getType()); |
174 |
|
lem = new_f.eqNode(f); |
175 |
|
} |
176 |
|
Trace("uf-ho-lemma") |
177 |
|
<< "uf-ho-lemma : Skolem definition for apply-conversion : " << lem |
178 |
|
<< std::endl; |
179 |
|
d_im.lemma(lem, InferenceId::UF_HO_APP_CONV_SKOLEM); |
180 |
|
d_uf_std_skolem[f] = new_f; |
181 |
|
} |
182 |
|
else |
183 |
|
{ |
184 |
|
new_f = (*itus).second; |
185 |
|
} |
186 |
|
// unroll the HO_APPLY, adding to the first argument position |
187 |
|
// Note arguments in the vector args begin at position 1. |
188 |
|
while (new_f.getKind() == HO_APPLY) |
189 |
|
{ |
190 |
|
args.insert(args.begin() + 1, new_f[1]); |
191 |
|
new_f = new_f[0]; |
192 |
|
} |
193 |
|
} |
194 |
119 |
Assert(TheoryUfRewriter::canUseAsApplyUfOperator(new_f)); |
195 |
119 |
args[0] = new_f; |
196 |
119 |
Node ret = nm->mkNode(APPLY_UF, args); |
197 |
119 |
Assert(ret.getType() == node.getType()); |
198 |
238 |
return ret; |
199 |
|
} |
200 |
|
|
201 |
1297 |
unsigned HoExtension::checkExtensionality(TheoryModel* m) |
202 |
|
{ |
203 |
|
// if we are in collect model info, we require looking at the model's |
204 |
|
// equality engine, so that we only consider "relevant" (see |
205 |
|
// Theory::computeRelevantTerms) function terms. |
206 |
|
eq::EqualityEngine* ee = |
207 |
1297 |
m != nullptr ? m->getEqualityEngine() : d_state.getEqualityEngine(); |
208 |
1297 |
NodeManager* nm = NodeManager::currentNM(); |
209 |
1297 |
unsigned num_lemmas = 0; |
210 |
1297 |
bool isCollectModel = (m != nullptr); |
211 |
2594 |
Trace("uf-ho") << "HoExtension::checkExtensionality, collectModel=" |
212 |
1297 |
<< isCollectModel << "..." << std::endl; |
213 |
2594 |
std::map<TypeNode, std::vector<Node> > func_eqcs; |
214 |
1297 |
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee); |
215 |
1297 |
bool hasFunctions = false; |
216 |
42113 |
while (!eqcs_i.isFinished()) |
217 |
|
{ |
218 |
40816 |
Node eqc = (*eqcs_i); |
219 |
40816 |
TypeNode tn = eqc.getType(); |
220 |
20408 |
if (tn.isFunction()) |
221 |
|
{ |
222 |
3164 |
hasFunctions = true; |
223 |
|
// if during collect model, must have an infinite type |
224 |
|
// if not during collect model, must have a finite type |
225 |
3164 |
if (d_env.isFiniteType(tn) != isCollectModel) |
226 |
|
{ |
227 |
1481 |
func_eqcs[tn].push_back(eqc); |
228 |
2962 |
Trace("uf-ho-debug") |
229 |
1481 |
<< " func eqc : " << tn << " : " << eqc << std::endl; |
230 |
|
} |
231 |
|
} |
232 |
20408 |
++eqcs_i; |
233 |
|
} |
234 |
1297 |
if (!options::ufHoExt()) |
235 |
|
{ |
236 |
|
// we are not applying extensionality, thus we are incomplete if functions |
237 |
|
// are present |
238 |
|
if (hasFunctions) |
239 |
|
{ |
240 |
|
d_im.setIncomplete(IncompleteId::UF_HO_EXT_DISABLED); |
241 |
|
} |
242 |
|
return 0; |
243 |
|
} |
244 |
|
|
245 |
2389 |
for (std::map<TypeNode, std::vector<Node> >::iterator itf = func_eqcs.begin(); |
246 |
2389 |
itf != func_eqcs.end(); |
247 |
|
++itf) |
248 |
|
{ |
249 |
2573 |
for (unsigned j = 0, sizej = itf->second.size(); j < sizej; j++) |
250 |
|
{ |
251 |
2370 |
for (unsigned k = (j + 1), sizek = itf->second.size(); k < sizek; k++) |
252 |
|
{ |
253 |
|
// if these equivalence classes are not explicitly disequal, do |
254 |
|
// extensionality to ensure distinctness. Notice that we always use |
255 |
|
// the (local) equality engine for this check via the state, since the |
256 |
|
// model's equality engine does not store any disequalities. This is |
257 |
|
// an optimization to introduce fewer equalities during model |
258 |
|
// construction, since we know such disequalities have already been |
259 |
|
// witness via assertions. |
260 |
889 |
if (!d_state.areDisequal(itf->second[j], itf->second[k])) |
261 |
|
{ |
262 |
570 |
Node deq = rewrite(itf->second[j].eqNode(itf->second[k]).negate()); |
263 |
|
// either add to model, or add lemma |
264 |
285 |
if (isCollectModel) |
265 |
|
{ |
266 |
|
// Add extentionality disequality to the model. |
267 |
|
// It is important that we construct new (unconstrained) variables |
268 |
|
// k here, so that we do not generate any inconsistencies. |
269 |
170 |
Node edeq = getExtensionalityDeq(deq, false); |
270 |
85 |
Assert(edeq.getKind() == NOT && edeq[0].getKind() == EQUAL); |
271 |
|
// introducing terms, must add required constraints, e.g. to |
272 |
|
// force equalities between APPLY_UF and HO_APPLY terms |
273 |
255 |
for (unsigned r = 0; r < 2; r++) |
274 |
|
{ |
275 |
170 |
if (!collectModelInfoHoTerm(edeq[0][r], m)) |
276 |
|
{ |
277 |
|
return 1; |
278 |
|
} |
279 |
|
} |
280 |
170 |
Trace("uf-ho-debug") |
281 |
85 |
<< "Add extensionality deq to model : " << edeq << std::endl; |
282 |
85 |
if (!m->assertEquality(edeq[0][0], edeq[0][1], false)) |
283 |
|
{ |
284 |
|
Node eq = edeq[0][0].eqNode(edeq[0][1]); |
285 |
|
Node lem = nm->mkNode(OR, deq.negate(), eq); |
286 |
|
Trace("uf-ho") << "HoExtension: cmi extensionality lemma " << lem |
287 |
|
<< std::endl; |
288 |
|
d_im.lemma(lem, InferenceId::UF_HO_MODEL_EXTENSIONALITY); |
289 |
|
return 1; |
290 |
|
} |
291 |
|
} |
292 |
|
else |
293 |
|
{ |
294 |
|
// apply extensionality lemma |
295 |
200 |
num_lemmas += applyExtensionality(deq); |
296 |
|
} |
297 |
|
} |
298 |
|
} |
299 |
|
} |
300 |
|
} |
301 |
1297 |
return num_lemmas; |
302 |
|
} |
303 |
|
|
304 |
682239 |
unsigned HoExtension::applyAppCompletion(TNode n) |
305 |
|
{ |
306 |
682239 |
Assert(n.getKind() == APPLY_UF); |
307 |
|
|
308 |
682239 |
eq::EqualityEngine* ee = d_state.getEqualityEngine(); |
309 |
|
// must expand into APPLY_HO version if not there already |
310 |
1364478 |
Node ret = TheoryUfRewriter::getHoApplyForApplyUf(n); |
311 |
682239 |
if (!ee->hasTerm(ret) || !ee->areEqual(ret, n)) |
312 |
|
{ |
313 |
25570 |
Node eq = n.eqNode(ret); |
314 |
25570 |
Trace("uf-ho-lemma") << "uf-ho-lemma : infer, by apply-expand : " << eq |
315 |
12785 |
<< std::endl; |
316 |
25570 |
d_im.assertInternalFact(eq, |
317 |
|
true, |
318 |
|
InferenceId::UF_HO_APP_ENCODE, |
319 |
|
PfRule::HO_APP_ENCODE, |
320 |
|
{}, |
321 |
12785 |
{n}); |
322 |
12785 |
return 1; |
323 |
|
} |
324 |
1338908 |
Trace("uf-ho-debug") << " ...already have " << ret << " == " << n << "." |
325 |
669454 |
<< std::endl; |
326 |
669454 |
return 0; |
327 |
|
} |
328 |
|
|
329 |
13717 |
unsigned HoExtension::checkAppCompletion() |
330 |
|
{ |
331 |
13717 |
Trace("uf-ho") << "HoExtension::checkApplyCompletion..." << std::endl; |
332 |
|
// compute the operators that are relevant (those for which an HO_APPLY exist) |
333 |
27434 |
std::set<TNode> rlvOp; |
334 |
13717 |
eq::EqualityEngine* ee = d_state.getEqualityEngine(); |
335 |
13717 |
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee); |
336 |
27434 |
std::map<TNode, std::vector<Node> > apply_uf; |
337 |
79037 |
while (!eqcs_i.isFinished()) |
338 |
|
{ |
339 |
78105 |
Node eqc = (*eqcs_i); |
340 |
90890 |
Trace("uf-ho-debug") << " apply completion : visit eqc " << eqc |
341 |
45445 |
<< std::endl; |
342 |
45445 |
eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee); |
343 |
5197007 |
while (!eqc_i.isFinished()) |
344 |
|
{ |
345 |
5164347 |
Node n = *eqc_i; |
346 |
2588566 |
if (n.getKind() == APPLY_UF || n.getKind() == HO_APPLY) |
347 |
|
{ |
348 |
1600524 |
int curr_sum = 0; |
349 |
3188263 |
std::map<TNode, bool> curr_rops; |
350 |
1600524 |
if (n.getKind() == APPLY_UF) |
351 |
|
{ |
352 |
1848877 |
TNode rop = ee->getRepresentative(n.getOperator()); |
353 |
928336 |
if (rlvOp.find(rop) != rlvOp.end()) |
354 |
|
{ |
355 |
|
// try if its operator is relevant |
356 |
370912 |
curr_sum = applyAppCompletion(n); |
357 |
370912 |
if (curr_sum > 0) |
358 |
|
{ |
359 |
7795 |
return curr_sum; |
360 |
|
} |
361 |
|
} |
362 |
|
else |
363 |
|
{ |
364 |
|
// add to pending list |
365 |
557424 |
apply_uf[rop].push_back(n); |
366 |
|
} |
367 |
|
// Arguments are also relevant operators. |
368 |
|
// It might be possible include fewer terms here, see #1115. |
369 |
2755431 |
for (unsigned k = 0; k < n.getNumChildren(); k++) |
370 |
|
{ |
371 |
1834890 |
if (n[k].getType().isFunction()) |
372 |
|
{ |
373 |
63706 |
TNode rop2 = ee->getRepresentative(n[k]); |
374 |
31853 |
curr_rops[rop2] = true; |
375 |
|
} |
376 |
|
} |
377 |
|
} |
378 |
|
else |
379 |
|
{ |
380 |
672188 |
Assert(n.getKind() == HO_APPLY); |
381 |
1344376 |
TNode rop = ee->getRepresentative(n[0]); |
382 |
672188 |
curr_rops[rop] = true; |
383 |
|
} |
384 |
2291708 |
for (std::map<TNode, bool>::iterator itc = curr_rops.begin(); |
385 |
2291708 |
itc != curr_rops.end(); |
386 |
|
++itc) |
387 |
|
{ |
388 |
1402948 |
TNode rop = itc->first; |
389 |
703969 |
if (rlvOp.find(rop) == rlvOp.end()) |
390 |
|
{ |
391 |
47036 |
rlvOp.insert(rop); |
392 |
|
// now, try each pending APPLY_UF for this operator |
393 |
|
std::map<TNode, std::vector<Node> >::iterator itu = |
394 |
47036 |
apply_uf.find(rop); |
395 |
47036 |
if (itu != apply_uf.end()) |
396 |
|
{ |
397 |
327823 |
for (unsigned j = 0, size = itu->second.size(); j < size; j++) |
398 |
|
{ |
399 |
311327 |
curr_sum = applyAppCompletion(itu->second[j]); |
400 |
311327 |
if (curr_sum > 0) |
401 |
|
{ |
402 |
4990 |
return curr_sum; |
403 |
|
} |
404 |
|
} |
405 |
|
} |
406 |
|
} |
407 |
|
} |
408 |
|
} |
409 |
2575781 |
++eqc_i; |
410 |
|
} |
411 |
32660 |
++eqcs_i; |
412 |
|
} |
413 |
932 |
return 0; |
414 |
|
} |
415 |
|
|
416 |
1071 |
unsigned HoExtension::check() |
417 |
|
{ |
418 |
1071 |
Trace("uf-ho") << "HoExtension::checkHigherOrder..." << std::endl; |
419 |
|
|
420 |
|
// infer new facts based on apply completion until fixed point |
421 |
|
unsigned num_facts; |
422 |
12646 |
do |
423 |
|
{ |
424 |
13717 |
num_facts = checkAppCompletion(); |
425 |
13717 |
if (d_state.isInConflict()) |
426 |
|
{ |
427 |
139 |
Trace("uf-ho") << "...conflict during app-completion." << std::endl; |
428 |
139 |
return 1; |
429 |
|
} |
430 |
13578 |
} while (num_facts > 0); |
431 |
|
|
432 |
932 |
unsigned num_lemmas = 0; |
433 |
|
|
434 |
932 |
num_lemmas = checkExtensionality(); |
435 |
932 |
if (num_lemmas > 0) |
436 |
|
{ |
437 |
74 |
Trace("uf-ho") << "...extensionality returned " << num_lemmas << " lemmas." |
438 |
37 |
<< std::endl; |
439 |
37 |
return num_lemmas; |
440 |
|
} |
441 |
|
|
442 |
895 |
Trace("uf-ho") << "...finished check higher order." << std::endl; |
443 |
|
|
444 |
895 |
return 0; |
445 |
|
} |
446 |
|
|
447 |
365 |
bool HoExtension::collectModelInfoHo(TheoryModel* m, |
448 |
|
const std::set<Node>& termSet) |
449 |
|
{ |
450 |
2601 |
for (std::set<Node>::iterator it = termSet.begin(); it != termSet.end(); ++it) |
451 |
|
{ |
452 |
4472 |
Node n = *it; |
453 |
|
// For model-building with higher-order, we require that APPLY_UF is always |
454 |
|
// expanded to HO_APPLY. That is, we always expand to a fully applicative |
455 |
|
// encoding during model construction. |
456 |
2236 |
if (!collectModelInfoHoTerm(n, m)) |
457 |
|
{ |
458 |
|
return false; |
459 |
|
} |
460 |
|
} |
461 |
|
// We apply an explicit extensionality technique for asserting |
462 |
|
// disequalities to the model to ensure that function values are distinct |
463 |
|
// in the curried HO_APPLY version of model construction. This is a |
464 |
|
// non-standard alternative to using a type enumerator over function |
465 |
|
// values to assign unique values. |
466 |
365 |
int addedLemmas = checkExtensionality(m); |
467 |
365 |
return addedLemmas == 0; |
468 |
|
} |
469 |
|
|
470 |
2406 |
bool HoExtension::collectModelInfoHoTerm(Node n, TheoryModel* m) |
471 |
|
{ |
472 |
2406 |
if (n.getKind() == APPLY_UF) |
473 |
|
{ |
474 |
2002 |
Node hn = TheoryUfRewriter::getHoApplyForApplyUf(n); |
475 |
1001 |
if (!m->assertEquality(n, hn, true)) |
476 |
|
{ |
477 |
|
Node eq = n.eqNode(hn); |
478 |
|
Trace("uf-ho") << "HoExtension: cmi app completion lemma " << eq |
479 |
|
<< std::endl; |
480 |
|
d_im.lemma(eq, InferenceId::UF_HO_MODEL_APP_ENCODE); |
481 |
|
return false; |
482 |
|
} |
483 |
|
} |
484 |
2406 |
return true; |
485 |
|
} |
486 |
|
|
487 |
|
} // namespace uf |
488 |
|
} // namespace theory |
489 |
31137 |
} // namespace cvc5 |