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 |
994 |
Node HoExtension::ppRewrite(Node node) |
44 |
|
{ |
45 |
|
// convert HO_APPLY to APPLY_UF if fully applied |
46 |
994 |
if (node.getKind() == HO_APPLY) |
47 |
|
{ |
48 |
294 |
if (node[0].getType().getNumChildren() == 2) |
49 |
|
{ |
50 |
115 |
Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl; |
51 |
230 |
Node ret = getApplyUfForHoApply(node); |
52 |
230 |
Trace("uf-ho") << "uf-ho : ppRewrite : " << node << " to " << ret |
53 |
115 |
<< std::endl; |
54 |
115 |
return ret; |
55 |
|
} |
56 |
|
} |
57 |
879 |
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 |
1870 |
while (curr.getKind() == HO_APPLY) |
89 |
|
{ |
90 |
574 |
children.push_back(curr[1]); |
91 |
574 |
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 |
115 |
Node HoExtension::getApplyUfForHoApply(Node node) |
125 |
|
{ |
126 |
115 |
Assert(node[0].getType().getNumChildren() == 2); |
127 |
230 |
std::vector<TNode> args; |
128 |
230 |
Node f = TheoryUfRewriter::decomposeHoApply(node, args, true); |
129 |
230 |
Node new_f = f; |
130 |
115 |
NodeManager* nm = NodeManager::currentNM(); |
131 |
115 |
SkolemManager* sm = nm->getSkolemManager(); |
132 |
115 |
if (!TheoryUfRewriter::canUseAsApplyUfOperator(f)) |
133 |
|
{ |
134 |
4 |
NodeNodeMap::const_iterator itus = d_uf_std_skolem.find(f); |
135 |
4 |
if (itus == d_uf_std_skolem.end()) |
136 |
|
{ |
137 |
8 |
std::unordered_set<Node> fvs; |
138 |
4 |
expr::getFreeVariables(f, fvs); |
139 |
8 |
Node lem; |
140 |
4 |
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 |
4 |
new_f = sm->mkDummySkolem("app_uf", f.getType()); |
174 |
4 |
lem = new_f.eqNode(f); |
175 |
|
} |
176 |
8 |
Trace("uf-ho-lemma") |
177 |
4 |
<< "uf-ho-lemma : Skolem definition for apply-conversion : " << lem |
178 |
4 |
<< std::endl; |
179 |
4 |
d_im.lemma(lem, InferenceId::UF_HO_APP_CONV_SKOLEM); |
180 |
4 |
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 |
4 |
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 |
115 |
Assert(TheoryUfRewriter::canUseAsApplyUfOperator(new_f)); |
195 |
115 |
args[0] = new_f; |
196 |
115 |
Node ret = nm->mkNode(APPLY_UF, args); |
197 |
115 |
Assert(ret.getType() == node.getType()); |
198 |
230 |
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 |
42119 |
while (!eqcs_i.isFinished()) |
217 |
|
{ |
218 |
40822 |
Node eqc = (*eqcs_i); |
219 |
40822 |
TypeNode tn = eqc.getType(); |
220 |
20411 |
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 |
20411 |
++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 |
|
Node deq = |
263 |
570 |
Rewriter::rewrite(itf->second[j].eqNode(itf->second[k]).negate()); |
264 |
|
// either add to model, or add lemma |
265 |
285 |
if (isCollectModel) |
266 |
|
{ |
267 |
|
// Add extentionality disequality to the model. |
268 |
|
// It is important that we construct new (unconstrained) variables |
269 |
|
// k here, so that we do not generate any inconsistencies. |
270 |
170 |
Node edeq = getExtensionalityDeq(deq, false); |
271 |
85 |
Assert(edeq.getKind() == NOT && edeq[0].getKind() == EQUAL); |
272 |
|
// introducing terms, must add required constraints, e.g. to |
273 |
|
// force equalities between APPLY_UF and HO_APPLY terms |
274 |
255 |
for (unsigned r = 0; r < 2; r++) |
275 |
|
{ |
276 |
170 |
if (!collectModelInfoHoTerm(edeq[0][r], m)) |
277 |
|
{ |
278 |
|
return 1; |
279 |
|
} |
280 |
|
} |
281 |
170 |
Trace("uf-ho-debug") |
282 |
85 |
<< "Add extensionality deq to model : " << edeq << std::endl; |
283 |
85 |
if (!m->assertEquality(edeq[0][0], edeq[0][1], false)) |
284 |
|
{ |
285 |
|
Node eq = edeq[0][0].eqNode(edeq[0][1]); |
286 |
|
Node lem = nm->mkNode(OR, deq.negate(), eq); |
287 |
|
Trace("uf-ho") << "HoExtension: cmi extensionality lemma " << lem |
288 |
|
<< std::endl; |
289 |
|
d_im.lemma(lem, InferenceId::UF_HO_MODEL_EXTENSIONALITY); |
290 |
|
return 1; |
291 |
|
} |
292 |
|
} |
293 |
|
else |
294 |
|
{ |
295 |
|
// apply extensionality lemma |
296 |
200 |
num_lemmas += applyExtensionality(deq); |
297 |
|
} |
298 |
|
} |
299 |
|
} |
300 |
|
} |
301 |
|
} |
302 |
1297 |
return num_lemmas; |
303 |
|
} |
304 |
|
|
305 |
682241 |
unsigned HoExtension::applyAppCompletion(TNode n) |
306 |
|
{ |
307 |
682241 |
Assert(n.getKind() == APPLY_UF); |
308 |
|
|
309 |
682241 |
eq::EqualityEngine* ee = d_state.getEqualityEngine(); |
310 |
|
// must expand into APPLY_HO version if not there already |
311 |
1364482 |
Node ret = TheoryUfRewriter::getHoApplyForApplyUf(n); |
312 |
682241 |
if (!ee->hasTerm(ret) || !ee->areEqual(ret, n)) |
313 |
|
{ |
314 |
25570 |
Node eq = n.eqNode(ret); |
315 |
25570 |
Trace("uf-ho-lemma") << "uf-ho-lemma : infer, by apply-expand : " << eq |
316 |
12785 |
<< std::endl; |
317 |
25570 |
d_im.assertInternalFact(eq, |
318 |
|
true, |
319 |
|
InferenceId::UF_HO_APP_ENCODE, |
320 |
|
PfRule::HO_APP_ENCODE, |
321 |
|
{}, |
322 |
12785 |
{n}); |
323 |
12785 |
return 1; |
324 |
|
} |
325 |
1338912 |
Trace("uf-ho-debug") << " ...already have " << ret << " == " << n << "." |
326 |
669456 |
<< std::endl; |
327 |
669456 |
return 0; |
328 |
|
} |
329 |
|
|
330 |
13717 |
unsigned HoExtension::checkAppCompletion() |
331 |
|
{ |
332 |
13717 |
Trace("uf-ho") << "HoExtension::checkApplyCompletion..." << std::endl; |
333 |
|
// compute the operators that are relevant (those for which an HO_APPLY exist) |
334 |
27434 |
std::set<TNode> rlvOp; |
335 |
13717 |
eq::EqualityEngine* ee = d_state.getEqualityEngine(); |
336 |
13717 |
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee); |
337 |
27434 |
std::map<TNode, std::vector<Node> > apply_uf; |
338 |
79275 |
while (!eqcs_i.isFinished()) |
339 |
|
{ |
340 |
78343 |
Node eqc = (*eqcs_i); |
341 |
91128 |
Trace("uf-ho-debug") << " apply completion : visit eqc " << eqc |
342 |
45564 |
<< std::endl; |
343 |
45564 |
eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee); |
344 |
5197198 |
while (!eqc_i.isFinished()) |
345 |
|
{ |
346 |
5164419 |
Node n = *eqc_i; |
347 |
2588602 |
if (n.getKind() == APPLY_UF || n.getKind() == HO_APPLY) |
348 |
|
{ |
349 |
1600566 |
int curr_sum = 0; |
350 |
3188347 |
std::map<TNode, bool> curr_rops; |
351 |
1600566 |
if (n.getKind() == APPLY_UF) |
352 |
|
{ |
353 |
1848941 |
TNode rop = ee->getRepresentative(n.getOperator()); |
354 |
928370 |
if (rlvOp.find(rop) != rlvOp.end()) |
355 |
|
{ |
356 |
|
// try if its operator is relevant |
357 |
370940 |
curr_sum = applyAppCompletion(n); |
358 |
370940 |
if (curr_sum > 0) |
359 |
|
{ |
360 |
7799 |
return curr_sum; |
361 |
|
} |
362 |
|
} |
363 |
|
else |
364 |
|
{ |
365 |
|
// add to pending list |
366 |
557430 |
apply_uf[rop].push_back(n); |
367 |
|
} |
368 |
|
// Arguments are also relevant operators. |
369 |
|
// It might be possible include fewer terms here, see #1115. |
370 |
2755505 |
for (unsigned k = 0; k < n.getNumChildren(); k++) |
371 |
|
{ |
372 |
1834934 |
if (n[k].getType().isFunction()) |
373 |
|
{ |
374 |
63706 |
TNode rop2 = ee->getRepresentative(n[k]); |
375 |
31853 |
curr_rops[rop2] = true; |
376 |
|
} |
377 |
|
} |
378 |
|
} |
379 |
|
else |
380 |
|
{ |
381 |
672196 |
Assert(n.getKind() == HO_APPLY); |
382 |
1344392 |
TNode rop = ee->getRepresentative(n[0]); |
383 |
672196 |
curr_rops[rop] = true; |
384 |
|
} |
385 |
2291758 |
for (std::map<TNode, bool>::iterator itc = curr_rops.begin(); |
386 |
2291758 |
itc != curr_rops.end(); |
387 |
|
++itc) |
388 |
|
{ |
389 |
1402968 |
TNode rop = itc->first; |
390 |
703977 |
if (rlvOp.find(rop) == rlvOp.end()) |
391 |
|
{ |
392 |
47040 |
rlvOp.insert(rop); |
393 |
|
// now, try each pending APPLY_UF for this operator |
394 |
|
std::map<TNode, std::vector<Node> >::iterator itu = |
395 |
47040 |
apply_uf.find(rop); |
396 |
47040 |
if (itu != apply_uf.end()) |
397 |
|
{ |
398 |
327783 |
for (unsigned j = 0, size = itu->second.size(); j < size; j++) |
399 |
|
{ |
400 |
311301 |
curr_sum = applyAppCompletion(itu->second[j]); |
401 |
311301 |
if (curr_sum > 0) |
402 |
|
{ |
403 |
4986 |
return curr_sum; |
404 |
|
} |
405 |
|
} |
406 |
|
} |
407 |
|
} |
408 |
|
} |
409 |
|
} |
410 |
2575817 |
++eqc_i; |
411 |
|
} |
412 |
32779 |
++eqcs_i; |
413 |
|
} |
414 |
932 |
return 0; |
415 |
|
} |
416 |
|
|
417 |
1071 |
unsigned HoExtension::check() |
418 |
|
{ |
419 |
1071 |
Trace("uf-ho") << "HoExtension::checkHigherOrder..." << std::endl; |
420 |
|
|
421 |
|
// infer new facts based on apply completion until fixed point |
422 |
|
unsigned num_facts; |
423 |
12646 |
do |
424 |
|
{ |
425 |
13717 |
num_facts = checkAppCompletion(); |
426 |
13717 |
if (d_state.isInConflict()) |
427 |
|
{ |
428 |
139 |
Trace("uf-ho") << "...conflict during app-completion." << std::endl; |
429 |
139 |
return 1; |
430 |
|
} |
431 |
13578 |
} while (num_facts > 0); |
432 |
|
|
433 |
932 |
unsigned num_lemmas = 0; |
434 |
|
|
435 |
932 |
num_lemmas = checkExtensionality(); |
436 |
932 |
if (num_lemmas > 0) |
437 |
|
{ |
438 |
74 |
Trace("uf-ho") << "...extensionality returned " << num_lemmas << " lemmas." |
439 |
37 |
<< std::endl; |
440 |
37 |
return num_lemmas; |
441 |
|
} |
442 |
|
|
443 |
895 |
Trace("uf-ho") << "...finished check higher order." << std::endl; |
444 |
|
|
445 |
895 |
return 0; |
446 |
|
} |
447 |
|
|
448 |
365 |
bool HoExtension::collectModelInfoHo(TheoryModel* m, |
449 |
|
const std::set<Node>& termSet) |
450 |
|
{ |
451 |
2603 |
for (std::set<Node>::iterator it = termSet.begin(); it != termSet.end(); ++it) |
452 |
|
{ |
453 |
4476 |
Node n = *it; |
454 |
|
// For model-building with higher-order, we require that APPLY_UF is always |
455 |
|
// expanded to HO_APPLY. That is, we always expand to a fully applicative |
456 |
|
// encoding during model construction. |
457 |
2238 |
if (!collectModelInfoHoTerm(n, m)) |
458 |
|
{ |
459 |
|
return false; |
460 |
|
} |
461 |
|
} |
462 |
|
// We apply an explicit extensionality technique for asserting |
463 |
|
// disequalities to the model to ensure that function values are distinct |
464 |
|
// in the curried HO_APPLY version of model construction. This is a |
465 |
|
// non-standard alternative to using a type enumerator over function |
466 |
|
// values to assign unique values. |
467 |
365 |
int addedLemmas = checkExtensionality(m); |
468 |
365 |
return addedLemmas == 0; |
469 |
|
} |
470 |
|
|
471 |
2408 |
bool HoExtension::collectModelInfoHoTerm(Node n, TheoryModel* m) |
472 |
|
{ |
473 |
2408 |
if (n.getKind() == APPLY_UF) |
474 |
|
{ |
475 |
2002 |
Node hn = TheoryUfRewriter::getHoApplyForApplyUf(n); |
476 |
1001 |
if (!m->assertEquality(n, hn, true)) |
477 |
|
{ |
478 |
|
Node eq = n.eqNode(hn); |
479 |
|
Trace("uf-ho") << "HoExtension: cmi app completion lemma " << eq |
480 |
|
<< std::endl; |
481 |
|
d_im.lemma(eq, InferenceId::UF_HO_MODEL_APP_ENCODE); |
482 |
|
return false; |
483 |
|
} |
484 |
|
} |
485 |
2408 |
return true; |
486 |
|
} |
487 |
|
|
488 |
|
} // namespace uf |
489 |
|
} // namespace theory |
490 |
31125 |
} // namespace cvc5 |