Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Gereon Kremer
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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/smt_engine_subsolver.h"
22 : : #include "theory/theory_model.h"
23 : : #include "theory/uf/function_const.h"
24 : : #include "theory/uf/lambda_lift.h"
25 : : #include "theory/uf/theory_uf_rewriter.h"
26 : : #include "util/rational.h"
27 : :
28 : : using namespace std;
29 : : using namespace cvc5::internal::kind;
30 : :
31 : : namespace cvc5::internal {
32 : : namespace theory {
33 : : namespace uf {
34 : :
35 : 1159 : HoExtension::HoExtension(Env& env,
36 : : TheoryState& state,
37 : : TheoryInferenceManager& im,
38 : 1159 : LambdaLift& ll)
39 : : : EnvObj(env),
40 : : d_state(state),
41 : : d_im(im),
42 : : d_ll(ll),
43 : 2318 : d_extensionality(userContext()),
44 : 2318 : d_cachedLemmas(userContext()),
45 : 2318 : d_uf_std_skolem(userContext()),
46 : 1159 : d_lamEqProcessed(userContext())
47 : : {
48 : 1159 : d_true = nodeManager()->mkConst(true);
49 : : // don't send true lemma
50 : 1159 : d_cachedLemmas.insert(d_true);
51 : 1159 : }
52 : :
53 : 40827 : TrustNode HoExtension::ppRewrite(Node node, std::vector<SkolemLemma>& lems)
54 : : {
55 : 40827 : Kind k = node.getKind();
56 [ + + ]: 40827 : if (k == Kind::HO_APPLY)
57 : : {
58 : : // convert HO_APPLY to APPLY_UF if fully applied
59 [ + + ]: 2266 : if (node[0].getType().getNumChildren() == 2)
60 : : {
61 [ + - ]: 1348 : Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl;
62 : 1348 : Node ret = getApplyUfForHoApply(node);
63 [ + - ]: 2696 : Trace("uf-ho") << "uf-ho : ppRewrite : " << node << " to " << ret
64 : 1348 : << std::endl;
65 : 1348 : return TrustNode::mkTrustRewrite(node, ret);
66 : : }
67 : : // partial beta reduction
68 : : // f ---> (lambda ((x Int) (y Int)) s[x, y]) then (@ f t) is preprocessed
69 : : // to (lambda ((y Int)) s[t, y]).
70 [ + - ]: 918 : if (options().uf.ufHoLazyLambdaLift)
71 : : {
72 : 918 : Node op = node[0];
73 : 918 : Node opl = d_ll.getLambdaFor(op);
74 [ - + ][ - - ]: 918 : if (!opl.isNull() && !d_ll.isLifted(opl))
[ - + ]
75 : : {
76 : 0 : NodeManager* nm = nodeManager();
77 : 0 : Node app = nm->mkNode(Kind::HO_APPLY, opl, node[1]);
78 : 0 : app = rewrite(app);
79 [ - - ]: 0 : Trace("uf-lazy-ll")
80 : 0 : << "Partial beta reduce: " << node << " -> " << app << std::endl;
81 : 0 : return TrustNode::mkTrustRewrite(node, app, nullptr);
82 : : }
83 : : }
84 : : }
85 [ + + ]: 38561 : else if (k == Kind::APPLY_UF)
86 : : {
87 : : // Say (lambda ((x Int)) t[x]) occurs in the input. We replace this
88 : : // by k during ppRewrite. In the following, if we see (k s), we replace
89 : : // it by t[s]. This maintains the invariant that the *only* occurrences
90 : : // of k are as arguments to other functions; k is not applied
91 : : // in any preprocessed constraints.
92 [ + + ]: 28524 : if (options().uf.ufHoLazyLambdaLift)
93 : : {
94 : : // if an application of the lambda lifted function, do beta reduction
95 : : // immediately
96 : 28392 : Node op = node.getOperator();
97 : 28392 : Node opl = d_ll.getLambdaFor(op);
98 [ + + ][ + + ]: 28392 : if (!opl.isNull() && !d_ll.isLifted(opl))
[ + + ]
99 : : {
100 [ - + ][ - + ]: 526 : Assert(opl.getKind() == Kind::LAMBDA);
[ - - ]
101 : 1052 : std::vector<Node> args(node.begin(), node.end());
102 : 526 : Node app = d_ll.betaReduce(opl, args);
103 [ + - ]: 1052 : Trace("uf-lazy-ll")
104 : 526 : << "Beta reduce: " << node << " -> " << app << std::endl;
105 : 526 : return TrustNode::mkTrustRewrite(node, app, nullptr);
106 : : }
107 : : // If an unlifted lambda occurs in an argument to APPLY_UF, it must be
108 : : // lifted. We do this only if the lambda needs lifting, i.e. it is one
109 : : // that may induce circular model dependencies.
110 [ + + ]: 72204 : for (const Node& nc : node)
111 : : {
112 [ + + ]: 44338 : if (nc.getType().isFunction())
113 : : {
114 : 6044 : Node lam = d_ll.getLambdaFor(nc);
115 [ + + ][ + + ]: 3022 : if (!lam.isNull() && d_ll.needsLift(lam))
[ + + ]
116 : : {
117 : 1884 : TrustNode trn = d_ll.lift(lam);
118 [ + + ]: 942 : if (!trn.isNull())
119 : : {
120 : 193 : lems.push_back(SkolemLemma(trn, nc));
121 : : }
122 : : }
123 : : }
124 : : }
125 : : }
126 : : }
127 [ + + ][ + + ]: 10037 : else if (k == Kind::LAMBDA || k == Kind::FUNCTION_ARRAY_CONST)
128 : : {
129 [ + - ]: 512 : Trace("uf-lazy-ll") << "Preprocess lambda: " << node << std::endl;
130 : 1024 : TrustNode skTrn = d_ll.ppRewrite(node, lems);
131 [ + - ][ - + ]: 512 : Trace("uf-lazy-ll") << "...return " << skTrn.getNode() << std::endl;
[ - - ]
132 : 512 : return skTrn;
133 : : }
134 : 38441 : return TrustNode::null();
135 : : }
136 : :
137 : 8076 : Node HoExtension::getExtensionalityDeq(TNode deq, bool isCached)
138 : : {
139 : 16152 : Assert(deq.getKind() == Kind::NOT && deq[0].getKind() == Kind::EQUAL);
140 [ - + ][ - + ]: 8076 : Assert(deq[0][0].getType().isFunction());
[ - - ]
141 [ + + ]: 8076 : if (isCached)
142 : : {
143 : 2746 : std::map<Node, Node>::iterator it = d_extensionality_deq.find(deq);
144 [ - + ]: 2746 : if (it != d_extensionality_deq.end())
145 : : {
146 : 0 : return it->second;
147 : : }
148 : : }
149 : 24228 : TypeNode tn = deq[0][0].getType();
150 : 16152 : std::vector<TypeNode> argTypes = tn.getArgTypes();
151 : 16152 : std::vector<Node> skolems;
152 : 8076 : NodeManager* nm = nodeManager();
153 : 8076 : SkolemManager* sm = nm->getSkolemManager();
154 : 16152 : std::vector<Node> cacheVals;
155 : 8076 : cacheVals.push_back(deq[0][0]);
156 : 8076 : cacheVals.push_back(deq[0][1]);
157 : 8076 : cacheVals.push_back(Node::null());
158 [ + + ]: 16236 : for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++)
159 : : {
160 : 8160 : cacheVals[2] = nm->mkConstInt(Rational(i));
161 : 16320 : Node k = sm->mkSkolemFunction(SkolemId::HO_DEQ_DIFF, cacheVals);
162 : 8160 : skolems.push_back(k);
163 : : }
164 [ + + ][ + + ]: 48456 : Node t[2];
[ - - ]
165 [ + + ]: 24228 : for (unsigned i = 0; i < 2; i++)
166 : : {
167 : 32304 : std::vector<Node> children;
168 : 32304 : Node curr = deq[0][i];
169 [ + + ]: 25656 : while (curr.getKind() == Kind::HO_APPLY)
170 : : {
171 : 9504 : children.push_back(curr[1]);
172 : 9504 : curr = curr[0];
173 : : }
174 : 16152 : children.push_back(curr);
175 : 16152 : std::reverse(children.begin(), children.end());
176 : 16152 : children.insert(children.end(), skolems.begin(), skolems.end());
177 : 16152 : t[i] = nm->mkNode(Kind::APPLY_UF, children);
178 : : }
179 : 16152 : Node conc = t[0].eqNode(t[1]).negate();
180 [ + + ]: 8076 : if (isCached)
181 : : {
182 : 2746 : d_extensionality_deq[deq] = conc;
183 : : }
184 : 8076 : return conc;
185 : : }
186 : :
187 : 15533 : unsigned HoExtension::applyExtensionality(TNode deq)
188 : : {
189 : 31066 : Assert(deq.getKind() == Kind::NOT && deq[0].getKind() == Kind::EQUAL);
190 [ - + ][ - + ]: 15533 : Assert(deq[0][0].getType().isFunction());
[ - - ]
191 : : // apply extensionality
192 [ + + ]: 15533 : if (d_extensionality.find(deq) == d_extensionality.end())
193 : : {
194 : 2746 : d_extensionality.insert(deq);
195 : 5492 : Node conc = getExtensionalityDeq(deq);
196 : 5492 : Node lem = nodeManager()->mkNode(Kind::OR, deq[0], conc);
197 [ + - ]: 5492 : Trace("uf-ho-lemma") << "uf-ho-lemma : extensionality : " << lem
198 : 2746 : << std::endl;
199 : 2746 : d_im.lemma(lem, InferenceId::UF_HO_EXTENSIONALITY);
200 : 2746 : return 1;
201 : : }
202 : 12787 : return 0;
203 : : }
204 : :
205 : 1348 : Node HoExtension::getApplyUfForHoApply(Node node)
206 : : {
207 [ - + ][ - + ]: 1348 : Assert(node[0].getType().getNumChildren() == 2);
[ - - ]
208 : 2696 : std::vector<TNode> args;
209 : 2696 : Node f = TheoryUfRewriter::decomposeHoApply(node, args, true);
210 : 2696 : Node new_f = f;
211 : 1348 : NodeManager* nm = nodeManager();
212 [ - + ]: 1348 : if (!TheoryUfRewriter::canUseAsApplyUfOperator(f))
213 : : {
214 : 0 : NodeNodeMap::const_iterator itus = d_uf_std_skolem.find(f);
215 [ - - ]: 0 : if (itus == d_uf_std_skolem.end())
216 : : {
217 : 0 : std::unordered_set<Node> fvs;
218 : 0 : expr::getFreeVariables(f, fvs);
219 : 0 : Node lem;
220 [ - - ]: 0 : if (!fvs.empty())
221 : : {
222 : 0 : std::vector<TypeNode> newTypes;
223 : 0 : std::vector<Node> vs;
224 : 0 : std::vector<Node> nvs;
225 [ - - ]: 0 : for (const Node& v : fvs)
226 : : {
227 : 0 : TypeNode vt = v.getType();
228 : 0 : newTypes.push_back(vt);
229 : 0 : Node nv = NodeManager::mkBoundVar(vt);
230 : 0 : vs.push_back(v);
231 : 0 : nvs.push_back(nv);
232 : : }
233 : 0 : TypeNode ft = f.getType();
234 : 0 : std::vector<TypeNode> argTypes = ft.getArgTypes();
235 : 0 : TypeNode rangeType = ft.getRangeType();
236 : :
237 : 0 : newTypes.insert(newTypes.end(), argTypes.begin(), argTypes.end());
238 : 0 : TypeNode nft = nm->mkFunctionType(newTypes, rangeType);
239 : 0 : new_f = NodeManager::mkDummySkolem("app_uf", nft);
240 [ - - ]: 0 : for (const Node& v : vs)
241 : : {
242 : 0 : new_f = nm->mkNode(Kind::HO_APPLY, new_f, v);
243 : : }
244 : 0 : Assert(new_f.getType() == f.getType());
245 : 0 : Node eq = new_f.eqNode(f);
246 : 0 : Node seq = eq.substitute(vs.begin(), vs.end(), nvs.begin(), nvs.end());
247 : 0 : lem = nm->mkNode(
248 : 0 : Kind::FORALL, nm->mkNode(Kind::BOUND_VAR_LIST, nvs), seq);
249 : : }
250 : : else
251 : : {
252 : : // introduce skolem to make a standard APPLY_UF
253 : 0 : new_f = NodeManager::mkDummySkolem("app_uf", f.getType());
254 : 0 : lem = new_f.eqNode(f);
255 : : }
256 [ - - ]: 0 : Trace("uf-ho-lemma")
257 : 0 : << "uf-ho-lemma : Skolem definition for apply-conversion : " << lem
258 : 0 : << std::endl;
259 : 0 : d_im.lemma(lem, InferenceId::UF_HO_APP_CONV_SKOLEM);
260 : 0 : d_uf_std_skolem[f] = new_f;
261 : : }
262 : : else
263 : : {
264 : 0 : new_f = (*itus).second;
265 : : }
266 : : // unroll the HO_APPLY, adding to the first argument position
267 : : // Note arguments in the vector args begin at position 1.
268 [ - - ]: 0 : while (new_f.getKind() == Kind::HO_APPLY)
269 : : {
270 : 0 : args.insert(args.begin() + 1, new_f[1]);
271 : 0 : new_f = new_f[0];
272 : : }
273 : : }
274 [ - + ][ - + ]: 1348 : Assert(TheoryUfRewriter::canUseAsApplyUfOperator(new_f));
[ - - ]
275 : 1348 : args[0] = new_f;
276 : 1348 : Node ret = nm->mkNode(Kind::APPLY_UF, args);
277 [ - + ][ - + ]: 1348 : Assert(ret.getType() == node.getType());
[ - - ]
278 : 2696 : return ret;
279 : : }
280 : :
281 : 5952 : unsigned HoExtension::checkExtensionality(TheoryModel* m)
282 : : {
283 : : // if we are in collect model info, we require looking at the model's
284 : : // equality engine, so that we only consider "relevant" (see
285 : : // Theory::computeRelevantTerms) function terms.
286 : : eq::EqualityEngine* ee =
287 [ + + ]: 5952 : m != nullptr ? m->getEqualityEngine() : d_state.getEqualityEngine();
288 : 5952 : NodeManager* nm = nodeManager();
289 : 5952 : unsigned num_lemmas = 0;
290 : 5952 : bool isCollectModel = (m != nullptr);
291 [ + - ]: 11904 : Trace("uf-ho") << "HoExtension::checkExtensionality, collectModel="
292 : 5952 : << isCollectModel << "..." << std::endl;
293 : 11904 : std::map<TypeNode, std::vector<Node> > func_eqcs;
294 : 5952 : eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
295 : 5952 : bool hasFunctions = false;
296 [ + + ]: 111380 : while (!eqcs_i.isFinished())
297 : : {
298 : 210856 : Node eqc = (*eqcs_i);
299 : 210856 : TypeNode tn = eqc.getType();
300 [ + + ][ + + ]: 105428 : if (tn.isFunction() && d_lambdaEqc.find(eqc) == d_lambdaEqc.end())
[ + + ]
301 : : {
302 : 18151 : hasFunctions = true;
303 : : // If during collect model, must have an infinite function type, since
304 : : // such function are not necessary to be handled during solving.
305 : : // If not during collect model, must have a finite function type, since
306 : : // such function symbols must be handled during solving.
307 [ + + ]: 18151 : if (d_env.isFiniteType(tn) != isCollectModel)
308 : : {
309 : 3097 : func_eqcs[tn].push_back(eqc);
310 [ + - ]: 6194 : Trace("uf-ho-debug")
311 : 3097 : << " func eqc : " << tn << " : " << eqc << std::endl;
312 : : }
313 : : }
314 : 105428 : ++eqcs_i;
315 : : }
316 [ - + ]: 5952 : if (!options().uf.ufHoExt)
317 : : {
318 : : // we are not applying extensionality, thus we are incomplete if functions
319 : : // are present
320 [ - - ]: 0 : if (hasFunctions)
321 : : {
322 : 0 : d_im.setModelUnsound(IncompleteId::UF_HO_EXT_DISABLED);
323 : : }
324 : 0 : return 0;
325 : : }
326 : :
327 : 7908 : for (std::map<TypeNode, std::vector<Node> >::iterator itf = func_eqcs.begin();
328 [ + + ]: 7908 : itf != func_eqcs.end();
329 : 1956 : ++itf)
330 : : {
331 [ + + ]: 5037 : for (unsigned j = 0, sizej = itf->second.size(); j < sizej; j++)
332 : : {
333 [ + + ]: 9008 : for (unsigned k = (j + 1), sizek = itf->second.size(); k < sizek; k++)
334 : : {
335 : : // if these equivalence classes are not explicitly disequal, do
336 : : // extensionality to ensure distinctness. Notice that we always use
337 : : // the (local) equality engine for this check via the state, since the
338 : : // model's equality engine does not store any disequalities. This is
339 : : // an optimization to introduce fewer equalities during model
340 : : // construction, since we know such disequalities have already been
341 : : // witness via assertions.
342 [ + + ]: 5935 : if (!d_state.areDisequal(itf->second[j], itf->second[k]))
343 : : {
344 : 10788 : Node deq = rewrite(itf->second[j].eqNode(itf->second[k]).negate());
345 : : // either add to model, or add lemma
346 [ + + ]: 5394 : if (isCollectModel)
347 : : {
348 : : // Add extentionality disequality to the model.
349 : : // It is important that we construct new (unconstrained) variables
350 : : // k here, so that we do not generate any inconsistencies.
351 : 5330 : Node edeq = getExtensionalityDeq(deq, false);
352 : 10660 : Assert(edeq.getKind() == Kind::NOT
353 : : && edeq[0].getKind() == Kind::EQUAL);
354 : : // introducing terms, must add required constraints, e.g. to
355 : : // force equalities between APPLY_UF and HO_APPLY terms
356 [ + + ]: 15990 : for (unsigned r = 0; r < 2; r++)
357 : : {
358 [ - + ]: 10660 : if (!collectModelInfoHoTerm(edeq[0][r], m))
359 : : {
360 : 0 : return 1;
361 : : }
362 : : }
363 : 5330 : bool success = false;
364 : 10660 : TypeNode tn = edeq[0][0].getType();
365 [ + - ]: 10660 : Trace("uf-ho-debug")
366 : 0 : << "Add extensionality deq to model for : " << edeq
367 : 5330 : << std::endl;
368 [ + + ]: 5330 : if (d_env.isFiniteType(tn))
369 : : {
370 : : // We are an infinite function type with a finite range sort.
371 : : // Model construction assigns the first value for all
372 : : // unconstrained variables for such sorts, which does not
373 : : // suffice in this context since we are trying to make the
374 : : // functions disequal. Thus, for such case we enumerate the first
375 : : // two values for this sort and set the extensionality index to
376 : : // be equal to these two distinct values. There must be at least
377 : : // two values since this is an infinite function sort.
378 : 7186 : TypeEnumerator te(tn);
379 : 7186 : Node v1 = *te;
380 : 3593 : te++;
381 : 3593 : Node v2 = *te;
382 [ + - ][ + - ]: 7186 : Assert(!v2.isNull() && v2 != v1);
[ - + ][ - - ]
383 : 7186 : success = m->assertEquality(edeq[0][0], v1, true)
384 : 7186 : && m->assertEquality(edeq[0][1], v2, true);
385 : : }
386 : : else
387 : : {
388 : 1737 : success = m->assertEquality(edeq[0][0], edeq[0][1], false);
389 : : }
390 [ + + ]: 5330 : if (!success)
391 : : {
392 : 24 : Node eq = edeq[0][0].eqNode(edeq[0][1]);
393 : 16 : Node lem = nm->mkNode(Kind::OR, deq.negate(), eq.negate());
394 [ + - ]: 16 : Trace("uf-ho") << "HoExtension: cmi extensionality lemma " << lem
395 : 8 : << std::endl;
396 : 8 : d_im.lemma(lem, InferenceId::UF_HO_MODEL_EXTENSIONALITY);
397 : 8 : return 1;
398 : : }
399 : : }
400 : : else
401 : : {
402 : : // apply extensionality lemma
403 : 64 : num_lemmas += applyExtensionality(deq);
404 : : }
405 : : }
406 : : }
407 : : }
408 : : }
409 : 5944 : return num_lemmas;
410 : : }
411 : :
412 : 2915480 : unsigned HoExtension::applyAppCompletion(TNode n)
413 : : {
414 [ - + ][ - + ]: 2915480 : Assert(n.getKind() == Kind::APPLY_UF);
[ - - ]
415 : :
416 : 2915480 : eq::EqualityEngine* ee = d_state.getEqualityEngine();
417 : : // must expand into APPLY_HO version if not there already
418 : 5830970 : Node ret = TheoryUfRewriter::getHoApplyForApplyUf(n);
419 : 2915480 : if (!ee->hasTerm(ret) || !ee->areEqual(ret, n))
420 : : {
421 : 29263 : Node eq = n.eqNode(ret);
422 [ + - ]: 58526 : Trace("uf-ho-lemma") << "uf-ho-lemma : infer, by apply-expand : " << eq
423 : 29263 : << std::endl;
424 : 58526 : d_im.assertInternalFact(eq,
425 : : true,
426 : : InferenceId::UF_HO_APP_ENCODE,
427 : : ProofRule::HO_APP_ENCODE,
428 : : {},
429 : 29263 : {n});
430 : 29263 : return 1;
431 : : }
432 [ + - ]: 5772440 : Trace("uf-ho-debug") << " ...already have " << ret << " == " << n << "."
433 : 2886220 : << std::endl;
434 : 2886220 : return 0;
435 : : }
436 : :
437 : 34349 : unsigned HoExtension::checkAppCompletion()
438 : : {
439 [ + - ]: 34349 : Trace("uf-ho") << "HoExtension::checkApplyCompletion..." << std::endl;
440 : : // compute the operators that are relevant (those for which an HO_APPLY exist)
441 : 68698 : std::set<TNode> rlvOp;
442 : 34349 : eq::EqualityEngine* ee = d_state.getEqualityEngine();
443 : 34349 : eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
444 : 68698 : std::map<TNode, std::vector<Node> > apply_uf;
445 [ + + ]: 659803 : while (!eqcs_i.isFinished())
446 : : {
447 : 654717 : Node eqc = (*eqcs_i);
448 [ + - ]: 1309430 : Trace("uf-ho-debug") << " apply completion : visit eqc " << eqc
449 : 654717 : << std::endl;
450 : 654717 : eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
451 [ + + ]: 11721900 : while (!eqc_i.isFinished())
452 : : {
453 : 11096400 : Node n = *eqc_i;
454 [ + + ][ + + ]: 11096400 : if (n.getKind() == Kind::APPLY_UF || n.getKind() == Kind::HO_APPLY)
[ + + ]
455 : : {
456 : 9104700 : int curr_sum = 0;
457 : 9104700 : std::map<TNode, bool> curr_rops;
458 [ + + ]: 9104700 : if (n.getKind() == Kind::APPLY_UF)
459 : : {
460 : 11529400 : TNode rop = ee->getRepresentative(n.getOperator());
461 [ + + ]: 5764720 : if (rlvOp.find(rop) != rlvOp.end())
462 : : {
463 : : // try if its operator is relevant
464 : 2693240 : curr_sum = applyAppCompletion(n);
465 [ + + ]: 2693240 : if (curr_sum > 0)
466 : : {
467 : 24590 : return curr_sum;
468 : : }
469 : : }
470 : : else
471 : : {
472 : : // add to pending list
473 : 3071480 : apply_uf[rop].push_back(n);
474 : : }
475 : : // Arguments are also relevant operators.
476 : : // It might be possible include fewer terms here, see #1115.
477 [ + + ]: 13771000 : for (unsigned k = 0; k < n.getNumChildren(); k++)
478 : : {
479 [ + + ]: 8030890 : if (n[k].getType().isFunction())
480 : : {
481 : 1190410 : TNode rop2 = ee->getRepresentative(n[k]);
482 : 595203 : curr_rops[rop2] = true;
483 : : }
484 : : }
485 : : }
486 : : else
487 : : {
488 [ - + ][ - + ]: 3339980 : Assert(n.getKind() == Kind::HO_APPLY);
[ - - ]
489 : 6679960 : TNode rop = ee->getRepresentative(n[0]);
490 : 3339980 : curr_rops[rop] = true;
491 : : }
492 : 13010600 : for (std::map<TNode, bool>::iterator itc = curr_rops.begin();
493 [ + + ]: 13010600 : itc != curr_rops.end();
494 : 3930480 : ++itc)
495 : : {
496 : 3935150 : TNode rop = itc->first;
497 [ + + ]: 3935150 : if (rlvOp.find(rop) == rlvOp.end())
498 : : {
499 : 168548 : rlvOp.insert(rop);
500 : : // now, try each pending APPLY_UF for this operator
501 : : std::map<TNode, std::vector<Node> >::iterator itu =
502 : 168548 : apply_uf.find(rop);
503 [ + + ]: 168548 : if (itu != apply_uf.end())
504 : : {
505 [ + + ]: 232319 : for (unsigned j = 0, size = itu->second.size(); j < size; j++)
506 : : {
507 : 222240 : curr_sum = applyAppCompletion(itu->second[j]);
508 [ + + ]: 222240 : if (curr_sum > 0)
509 : : {
510 : 4673 : return curr_sum;
511 : : }
512 : : }
513 : : }
514 : : }
515 : : }
516 : : }
517 : 11067200 : ++eqc_i;
518 : : }
519 : 625454 : ++eqcs_i;
520 : : }
521 : 5086 : return 0;
522 : : }
523 : :
524 : 5036 : unsigned HoExtension::checkLazyLambda()
525 : : {
526 [ + + ]: 5036 : if (!options().uf.ufHoLazyLambdaLift)
527 : : {
528 : : // no lambdas are lazily lifted
529 : 502 : return 0;
530 : : }
531 [ + - ]: 4534 : Trace("uf-ho") << "HoExtension::checkLazyLambda..." << std::endl;
532 : 4534 : NodeManager* nm = nodeManager();
533 : 4534 : unsigned numLemmas = 0;
534 : 4534 : d_lambdaEqc.clear();
535 : 4534 : eq::EqualityEngine* ee = d_state.getEqualityEngine();
536 : 4534 : eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
537 : : // normal functions equated to lambda functions
538 : 9068 : std::unordered_set<Node> normalEqFuns;
539 : : // mapping from functions to terms
540 [ + + ]: 95516 : while (!eqcs_i.isFinished())
541 : : {
542 : 90982 : Node eqc = (*eqcs_i);
543 : 90982 : ++eqcs_i;
544 [ + + ]: 90982 : if (!eqc.getType().isFunction())
545 : : {
546 : 70528 : continue;
547 : : }
548 : 20454 : eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
549 : 40908 : Node lamRep; // the first lambda function we encounter in the equivalence
550 : : // class
551 : 20454 : bool needsLift = false;
552 : 20454 : bool doLift = false;
553 : 40908 : Node lamRepLam;
554 : 40908 : std::unordered_set<Node> normalEqFunWait;
555 [ + + ]: 45922 : while (!eqc_i.isFinished())
556 : : {
557 : 25468 : Node n = *eqc_i;
558 : 25468 : ++eqc_i;
559 : 25468 : Node lam = d_ll.getLambdaFor(n);
560 [ + + ][ + + ]: 25468 : if (lam.isNull() || d_ll.isLifted(lam))
[ + + ]
561 : : {
562 [ + + ]: 19058 : if (!lamRep.isNull())
563 : : {
564 : : // if we are equal to a lambda function, we must beta-reduce
565 : : // applications of this
566 : 30 : normalEqFuns.insert(n);
567 : 30 : doLift = needsLift;
568 : : }
569 : : else
570 : : {
571 : : // waiting to see if there is a lambda function in this equivalence
572 : : // class
573 : 19028 : normalEqFunWait.insert(n);
574 : : }
575 : : }
576 [ + + ]: 6410 : else if (lamRep.isNull())
577 : : {
578 : : // there is a lambda function in this equivalence class
579 : 6368 : lamRep = n;
580 : 6368 : lamRepLam = lam;
581 [ + + ][ + - ]: 6368 : needsLift = d_ll.needsLift(lam) && !d_ll.isLifted(lam);
582 [ + + ][ + + ]: 6368 : doLift = needsLift && !normalEqFunWait.empty();
583 : : // must consider all normal functions we've seen so far
584 : 6368 : normalEqFuns.insert(normalEqFunWait.begin(), normalEqFunWait.end());
585 : 6368 : normalEqFunWait.clear();
586 : : }
587 : : else
588 : : {
589 : : // two lambda functions are in same equivalence class
590 [ + - ]: 42 : Node f = lamRep < n ? lamRep : n;
591 [ + - ]: 42 : Node g = lamRep < n ? n : lamRep;
592 : : // swap based on order
593 [ - + ]: 42 : if (g<f)
594 : : {
595 : 0 : Node tmp = f;
596 : 0 : f = g;
597 : 0 : g = tmp;
598 : : }
599 : 42 : Node fgEq = f.eqNode(g);
600 [ + + ]: 42 : if (d_lamEqProcessed.find(fgEq)!=d_lamEqProcessed.end())
601 : : {
602 : 20 : continue;
603 : : }
604 : 22 : d_lamEqProcessed.insert(fgEq);
605 : :
606 [ + - ]: 44 : Trace("uf-ho-debug") << " found equivalent lambda functions " << f
607 : 22 : << " and " << g << std::endl;
608 [ + - ]: 44 : Node flam = lamRep < n ? lamRepLam : lam;
609 [ + - ][ + - ]: 44 : Assert(!flam.isNull() && flam.getKind() == Kind::LAMBDA);
[ - + ][ - - ]
610 : 44 : Node lhs = flam[1];
611 [ + - ]: 44 : Node glam = lamRep < n ? lam : lamRepLam;
612 [ + - ]: 44 : Trace("uf-ho-debug")
613 : 22 : << " lambda are " << flam << " and " << glam << std::endl;
614 : 66 : std::vector<Node> args(flam[0].begin(), flam[0].end());
615 : 44 : Node rhs = d_ll.betaReduce(glam, args);
616 : 66 : Node univ = nm->mkNode(Kind::FORALL, flam[0], lhs.eqNode(rhs));
617 : : // do quantifier elimination if the option is set
618 : : // For example, say (= f1 f2) where f1 is (lambda ((x Int)) (< x a))
619 : : // and f2 is (lambda ((x Int)) (< x b)).
620 : : // By default, we would generate the inference
621 : : // (=> (= f1 f2) (forall ((x Int)) (= (< x a) (< x b))),
622 : : // where quantified reasoning is introduced into the main solving
623 : : // procedure.
624 : : // With --uf-lambda-qe, we use a subsolver to compute the quantifier
625 : : // elimination of:
626 : : // (forall ((x Int)) (= (< x a) (< x b)),
627 : : // which is (and (<= a b) (<= b a)). We instead generate the lemma
628 : : // (=> (= f1 f2) (and (<= a b) (<= b a)).
629 : : // The motivation for this is to reduce the complexity of constraints
630 : : // in the main solver. This is motivated by usages of set.filter where
631 : : // the lambdas are over a decidable theory that admits quantifier
632 : : // elimination, e.g. LIA or BV.
633 [ + + ]: 22 : if (options().uf.ufHoLambdaQe)
634 : : {
635 [ + - ]: 2 : Trace("uf-lambda-qe") << "Given " << flam << " == " << glam << std::endl;
636 [ + - ]: 2 : Trace("uf-lambda-qe") << "Run QE on " << univ << std::endl;
637 : 2 : std::unique_ptr<SolverEngine> lqe;
638 : : // initialize the subsolver using the standard method
639 : 2 : initializeSubsolver(lqe, d_env);
640 : 4 : Node univQe = lqe->getQuantifierElimination(univ, true);
641 [ + - ]: 2 : Trace("uf-lambda-qe") << "QE is " << univQe << std::endl;
642 [ - + ][ - + ]: 2 : Assert (!univQe.isNull());
[ - - ]
643 : : // Note that if quantifier elimination failed, then univQe will
644 : : // be equal to univ, in which case this above code has no effect.
645 : 2 : univ = univQe;
646 : : }
647 : : // f = g => forall x. reduce(lambda(f)(x)) = reduce(lambda(g)(x))
648 : : //
649 : : // For example, if f -> lambda z. z+1, g -> lambda y. y+3, this
650 : : // will infer: f = g => forall x. x+1 = x+3, which simplifies to
651 : : // f != g.
652 : 66 : Node lem = nm->mkNode(Kind::IMPLIES, fgEq, univ);
653 [ + - ]: 22 : if (cacheLemma(lem))
654 : : {
655 : 22 : d_im.lemma(lem, InferenceId::UF_HO_LAMBDA_UNIV_EQ);
656 : 22 : numLemmas++;
657 : : }
658 : : }
659 : : }
660 [ + + ]: 20454 : if (!lamRep.isNull())
661 : : {
662 : 6368 : d_lambdaEqc[eqc] = lamRep;
663 : : // Do the lambda lifting lemma if needed. This happens if a lambda
664 : : // needs lifting based on the symbols in its body and is equated to an
665 : : // ordinary function symbol. For example, this is what ensures we
666 : : // handle conflicts like f = (lambda ((x Int)) (+ 1 (f x))).
667 [ + + ]: 6368 : if (doLift)
668 : : {
669 : 88 : TrustNode tlift = d_ll.lift(lamRepLam);
670 [ - + ][ - + ]: 44 : Assert(!tlift.isNull());
[ - - ]
671 : 44 : d_im.trustedLemma(tlift, InferenceId::UF_HO_LAMBDA_LAZY_LIFT);
672 : : }
673 : : }
674 : : }
675 [ + - ]: 9068 : Trace("uf-ho-debug")
676 : 4534 : << " found " << normalEqFuns.size()
677 : 4534 : << " ordinary functions that are equal to lambda functions" << std::endl;
678 [ + + ]: 4534 : if (normalEqFuns.empty())
679 : : {
680 : 4465 : return numLemmas;
681 : : }
682 : : // if we have normal functions that are equal to lambda functions, go back
683 : : // and ensure they are mapped properly
684 : : // mapping from functions to terms
685 : 69 : eq::EqClassesIterator eqcs_i2 = eq::EqClassesIterator(ee);
686 [ + + ]: 4026 : while (!eqcs_i2.isFinished())
687 : : {
688 : 7914 : Node eqc = (*eqcs_i2);
689 : 3957 : ++eqcs_i2;
690 [ + - ]: 3957 : Trace("uf-ho-debug") << "Check equivalence class " << eqc << std::endl;
691 : 3957 : eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
692 [ + + ]: 18056 : while (!eqc_i.isFinished())
693 : : {
694 : 14099 : Node n = *eqc_i;
695 : 14099 : ++eqc_i;
696 [ + - ]: 14099 : Trace("uf-ho-debug") << "Check term " << n << std::endl;
697 : 14099 : Node op;
698 : 14099 : Kind k = n.getKind();
699 : 14099 : std::vector<Node> args;
700 [ + + ]: 14099 : if (k == Kind::APPLY_UF)
701 : : {
702 : 5592 : op = n.getOperator();
703 : 5592 : args.insert(args.end(), n.begin(), n.end());
704 : : }
705 [ + + ]: 8507 : else if (k == Kind::HO_APPLY)
706 : : {
707 : 3438 : op = n[0];
708 : 3438 : args.push_back(n[1]);
709 : : }
710 : : else
711 : : {
712 : 5069 : continue;
713 : : }
714 [ + + ]: 9030 : if (normalEqFuns.find(op) == normalEqFuns.end())
715 : : {
716 : 7544 : continue;
717 : : }
718 [ + - ]: 2972 : Trace("uf-ho-debug") << " found relevant ordinary application " << n
719 : 1486 : << std::endl;
720 [ - + ][ - + ]: 1486 : Assert(ee->hasTerm(op));
[ - - ]
721 : 4458 : Node r = ee->getRepresentative(op);
722 [ - + ][ - + ]: 1486 : Assert(d_lambdaEqc.find(r) != d_lambdaEqc.end());
[ - - ]
723 : 2972 : Node lf = d_lambdaEqc[r];
724 : 2972 : Node lam = d_ll.getLambdaFor(lf);
725 [ + - ][ + - ]: 2972 : Assert(!lam.isNull() && lam.getKind() == Kind::LAMBDA);
[ - + ][ - - ]
726 : : // a normal function g equal to a lambda, say f --> lambda(f)
727 : : // need to infer f = g => g(t) = f(t) for all terms g(t)
728 : : // that occur in the equality engine.
729 : 2972 : Node premise = op.eqNode(lf);
730 : 1486 : args.insert(args.begin(), lam);
731 : 2972 : Node rhs = nm->mkNode(n.getKind(), args);
732 : 1486 : rhs = rewrite(rhs);
733 : 2972 : Node conc = n.eqNode(rhs);
734 : 4458 : Node lem = nm->mkNode(Kind::IMPLIES, premise, conc);
735 [ + + ]: 1486 : if (cacheLemma(lem))
736 : : {
737 : 1454 : d_im.lemma(lem, InferenceId::UF_HO_LAMBDA_APP_REDUCE);
738 : 1454 : numLemmas++;
739 : : }
740 : : }
741 : : }
742 : 69 : return numLemmas;
743 : : }
744 : :
745 : 5213 : unsigned HoExtension::check()
746 : : {
747 [ + - ]: 5213 : Trace("uf-ho") << "HoExtension::checkHigherOrder..." << std::endl;
748 : :
749 : : // infer new facts based on apply completion until fixed point
750 : : unsigned num_facts;
751 : 29136 : do
752 : : {
753 : 34349 : num_facts = checkAppCompletion();
754 [ + + ]: 34349 : if (d_state.isInConflict())
755 : : {
756 [ + - ]: 127 : Trace("uf-ho") << "...conflict during app-completion." << std::endl;
757 : 127 : return 1;
758 : : }
759 [ + + ]: 34222 : } while (num_facts > 0);
760 : :
761 : : // Apply extensionality, lazy lambda schemas in order. We make lazy lambda
762 : : // handling come last as it may introduce quantifiers.
763 [ + + ]: 15091 : for (size_t i = 0; i < 2; i++)
764 : : {
765 : 10122 : unsigned num_lemmas = 0;
766 : : // apply the schema
767 [ + + ][ - ]: 10122 : switch (i)
768 : : {
769 : 5086 : case 0: num_lemmas = checkExtensionality(); break;
770 : 5036 : case 1: num_lemmas = checkLazyLambda(); break;
771 : 0 : default: break;
772 : : }
773 : : // finish if we added lemmas
774 [ + + ]: 10122 : if (num_lemmas > 0)
775 : : {
776 [ + - ]: 117 : Trace("uf-ho") << "...returned " << num_lemmas << " lemmas." << std::endl;
777 : 117 : return num_lemmas;
778 : : }
779 : : }
780 : :
781 [ + - ]: 4969 : Trace("uf-ho") << "...finished check higher order." << std::endl;
782 : :
783 : 4969 : return 0;
784 : : }
785 : :
786 : 866 : bool HoExtension::collectModelInfoHo(TheoryModel* m,
787 : : const std::set<Node>& termSet)
788 : : {
789 [ + + ]: 16669 : for (std::set<Node>::iterator it = termSet.begin(); it != termSet.end(); ++it)
790 : : {
791 : 15803 : Node n = *it;
792 : : // For model-building with higher-order, we require that APPLY_UF is always
793 : : // expanded to HO_APPLY. That is, we always expand to a fully applicative
794 : : // encoding during model construction.
795 [ - + ]: 15803 : if (!collectModelInfoHoTerm(n, m))
796 : : {
797 : 0 : return false;
798 : : }
799 : : }
800 : : // We apply an explicit extensionality technique for asserting
801 : : // disequalities to the model to ensure that function values are distinct
802 : : // in the curried HO_APPLY version of model construction. This is a
803 : : // non-standard alternative to using a type enumerator over function
804 : : // values to assign unique values.
805 : 866 : int addedLemmas = checkExtensionality(m);
806 : : // for equivalence classes that we know to assign a lambda directly
807 [ + + ]: 1238 : for (const std::pair<const Node, Node>& p : d_lambdaEqc)
808 : : {
809 : 372 : Node lam = d_ll.getLambdaFor(p.second);
810 : 372 : lam = rewrite(lam);
811 [ - + ][ - + ]: 372 : Assert(!lam.isNull());
[ - - ]
812 : 372 : m->assertEquality(p.second, lam, true);
813 : 372 : m->assertSkeleton(lam);
814 : : // we don't assign the function definition here, which is handled internally
815 : : // in the model builder.
816 : : }
817 : 866 : return addedLemmas == 0;
818 : : }
819 : :
820 : 26463 : bool HoExtension::collectModelInfoHoTerm(Node n, TheoryModel* m)
821 : : {
822 [ + + ]: 26463 : if (n.getKind() == Kind::APPLY_UF)
823 : : {
824 : 18499 : Node hn = TheoryUfRewriter::getHoApplyForApplyUf(n);
825 [ - + ]: 18499 : if (!m->assertEquality(n, hn, true))
826 : : {
827 : 0 : Node eq = n.eqNode(hn);
828 [ - - ]: 0 : Trace("uf-ho") << "HoExtension: cmi app completion lemma " << eq
829 : 0 : << std::endl;
830 : 0 : d_im.lemma(eq, InferenceId::UF_HO_MODEL_APP_ENCODE);
831 : 0 : return false;
832 : : }
833 : : }
834 : 26463 : return true;
835 : : }
836 : :
837 : 1508 : bool HoExtension::cacheLemma(TNode lem)
838 : : {
839 : 3016 : Node rewritten = rewrite(lem);
840 [ + + ]: 1508 : if (d_cachedLemmas.find(rewritten) != d_cachedLemmas.end())
841 : : {
842 : 32 : return false;
843 : : }
844 : 1476 : d_cachedLemmas.insert(rewritten);
845 : 1476 : return true;
846 : : }
847 : :
848 : : } // namespace uf
849 : : } // namespace theory
850 : : } // namespace cvc5::internal
|
