Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Mathias Preiner
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 higher-order trigger class.
14 : : */
15 : :
16 : : #include "theory/quantifiers/ematching/ho_trigger.h"
17 : :
18 : : #include <stack>
19 : :
20 : : #include "theory/quantifiers/ho_term_database.h"
21 : : #include "theory/quantifiers/instantiate.h"
22 : : #include "theory/quantifiers/quantifiers_inference_manager.h"
23 : : #include "theory/quantifiers/quantifiers_registry.h"
24 : : #include "theory/quantifiers/quantifiers_state.h"
25 : : #include "theory/quantifiers/term_registry.h"
26 : : #include "theory/quantifiers/term_util.h"
27 : : #include "theory/uf/theory_uf_rewriter.h"
28 : : #include "util/hash.h"
29 : :
30 : : using namespace cvc5::internal::kind;
31 : :
32 : : namespace cvc5::internal {
33 : : namespace theory {
34 : : namespace quantifiers {
35 : : namespace inst {
36 : :
37 : 230 : HigherOrderTrigger::HigherOrderTrigger(
38 : : Env& env,
39 : : QuantifiersState& qs,
40 : : QuantifiersInferenceManager& qim,
41 : : QuantifiersRegistry& qr,
42 : : TermRegistry& tr,
43 : : Node q,
44 : : std::vector<Node>& nodes,
45 : : std::map<Node, std::vector<Node> >& ho_apps,
46 : 230 : bool isUser)
47 : 230 : : Trigger(env, qs, qim, qr, tr, q, nodes, isUser), d_ho_var_apps(ho_apps)
48 : : {
49 : 230 : NodeManager* nm = nodeManager();
50 : : // process the higher-order variable applications
51 [ + + ]: 468 : for (std::pair<const Node, std::vector<Node> >& as : d_ho_var_apps)
52 : : {
53 : 476 : Node n = as.first;
54 : 238 : d_ho_var_list.push_back(n);
55 : 476 : TypeNode tn = n.getType();
56 [ - + ][ - + ]: 238 : Assert(tn.isFunction());
[ - - ]
57 [ - + ]: 238 : if (TraceIsOn("ho-quant-trigger"))
58 : : {
59 [ - - ]: 0 : Trace("ho-quant-trigger") << " have " << as.second.size();
60 [ - - ]: 0 : Trace("ho-quant-trigger") << " patterns with variable operator " << n
61 : 0 : << ":" << std::endl;
62 [ - - ]: 0 : for (unsigned j = 0; j < as.second.size(); j++)
63 : : {
64 [ - - ]: 0 : Trace("ho-quant-trigger") << " " << as.second[j] << std::endl;
65 : : }
66 : : }
67 [ + - ]: 238 : if (d_ho_var_types.find(tn) == d_ho_var_types.end())
68 : : {
69 [ + - ]: 476 : Trace("ho-quant-trigger") << " type " << tn
70 : 238 : << " needs higher-order matching." << std::endl;
71 : 238 : d_ho_var_types.insert(tn);
72 : : }
73 : : // make the bound variable lists
74 : 238 : d_ho_var_bvl[n] = nm->getBoundVarListForFunctionType(tn);
75 [ + + ]: 522 : for (const Node& nc : d_ho_var_bvl[n])
76 : : {
77 : 284 : d_ho_var_bvs[n].push_back(nc);
78 : : }
79 : : }
80 : 230 : }
81 : :
82 : 460 : HigherOrderTrigger::~HigherOrderTrigger() {}
83 : 0 : void HigherOrderTrigger::collectHoVarApplyTerms(
84 : : Node q, Node& n, std::map<Node, std::vector<Node> >& apps)
85 : : {
86 : 0 : std::vector<Node> ns;
87 : 0 : ns.push_back(n);
88 : 0 : collectHoVarApplyTerms(q, ns, apps);
89 : 0 : Assert(ns.size() == 1);
90 : 0 : n = ns[0];
91 : 0 : }
92 : :
93 : 42883 : void HigherOrderTrigger::collectHoVarApplyTerms(
94 : : Node q, std::vector<Node>& ns, std::map<Node, std::vector<Node> >& apps)
95 : : {
96 : 85766 : std::unordered_map<TNode, Node> visited;
97 : 42883 : std::unordered_map<TNode, Node>::iterator it;
98 : : // whether the visited node is a child of a HO_APPLY chain
99 : 85766 : std::unordered_map<TNode, bool> withinApply;
100 : 85766 : std::vector<TNode> visit;
101 : 85766 : TNode cur;
102 [ + + ]: 89607 : for (unsigned i = 0, size = ns.size(); i < size; i++)
103 : : {
104 : 46724 : visit.push_back(ns[i]);
105 : 46724 : withinApply[ns[i]] = false;
106 : 484927 : do
107 : : {
108 : 531651 : cur = visit.back();
109 : 531651 : visit.pop_back();
110 : :
111 : 531651 : it = visited.find(cur);
112 [ + + ]: 531651 : if (it == visited.end())
113 : : {
114 : : // do not look in nested quantifiers
115 [ - + ]: 261117 : if (cur.getKind() == Kind::FORALL)
116 : : {
117 : 0 : visited[cur] = cur;
118 : : }
119 : : else
120 : : {
121 : 261117 : bool curWithinApply = withinApply[cur];
122 : 261117 : visited[cur] = Node::null();
123 : 261117 : visit.push_back(cur);
124 [ + + ]: 484927 : for (unsigned j = 0, sizec = cur.getNumChildren(); j < sizec; j++)
125 : : {
126 [ - + ][ - - ]: 223810 : withinApply[cur[j]] = curWithinApply && j == 0;
127 : 223810 : visit.push_back(cur[j]);
128 : : }
129 : : }
130 : : }
131 [ + + ]: 270534 : else if (it->second.isNull())
132 : : {
133 : : // carry the conversion
134 : 522234 : Node ret = cur;
135 : 261117 : bool childChanged = false;
136 : 522234 : std::vector<Node> children;
137 [ + + ]: 261117 : if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
138 : : {
139 : 100519 : children.push_back(cur.getOperator());
140 : : }
141 [ + + ]: 484927 : for (const Node& nc : cur)
142 : : {
143 : 223810 : it = visited.find(nc);
144 [ - + ][ - + ]: 223810 : Assert(it != visited.end());
[ - - ]
145 [ - + ][ - + ]: 223810 : Assert(!it->second.isNull());
[ - - ]
146 [ + + ][ + + ]: 223810 : childChanged = childChanged || nc != it->second;
147 : 223810 : children.push_back(it->second);
148 : : }
149 [ + + ]: 261117 : if (childChanged)
150 : : {
151 : 336 : ret = NodeManager::currentNM()->mkNode(cur.getKind(), children);
152 : : }
153 : : // now, convert and store the application
154 [ + - ]: 261117 : if (!withinApply[cur])
155 : : {
156 : 522234 : TNode op;
157 [ + + ]: 261117 : if (ret.getKind() == Kind::APPLY_UF)
158 : : {
159 : : // could be a fully applied function variable
160 : 92576 : op = ret.getOperator();
161 : : }
162 [ + + ]: 168541 : else if (ret.getKind() == Kind::HO_APPLY)
163 : : {
164 : 116 : op = ret;
165 [ + + ]: 232 : while (op.getKind() == Kind::HO_APPLY)
166 : : {
167 : 116 : op = op[0];
168 : : }
169 : : }
170 [ + + ]: 261117 : if (!op.isNull())
171 : : {
172 [ + + ]: 92692 : if (op.getKind() == Kind::INST_CONSTANT)
173 : : {
174 [ - + ][ - + ]: 238 : Assert(TermUtil::getInstConstAttr(ret) == q);
[ - - ]
175 [ + - ]: 476 : Trace("ho-quant-trigger-debug")
176 : 0 : << "Ho variable apply term : " << ret << " with head " << op
177 : 238 : << std::endl;
178 [ + + ]: 238 : if (ret.getKind() == Kind::APPLY_UF)
179 : : {
180 : 230 : Node prev = ret;
181 : : // for consistency, convert to HO_APPLY if fully applied
182 : 230 : ret = uf::TheoryUfRewriter::getHoApplyForApplyUf(ret);
183 : : }
184 : 238 : apps[op].push_back(ret);
185 : : }
186 : : }
187 : : }
188 : 261117 : visited[cur] = ret;
189 : : }
190 [ + + ]: 531651 : } while (!visit.empty());
191 : :
192 : : // store the conversion
193 [ - + ][ - + ]: 46724 : Assert(visited.find(ns[i]) != visited.end());
[ - - ]
194 : 46724 : ns[i] = visited[ns[i]];
195 : : }
196 : 42883 : }
197 : :
198 : 642 : uint64_t HigherOrderTrigger::addInstantiations()
199 : : {
200 : : // call the base class implementation
201 : 642 : uint64_t addedFoLemmas = Trigger::addInstantiations();
202 : : // also adds predicate lemms to force app completion
203 : 642 : uint64_t addedHoLemmas = addHoTypeMatchPredicateLemmas();
204 : 642 : return addedHoLemmas + addedFoLemmas;
205 : : }
206 : :
207 : 1816 : bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
208 : : {
209 [ + + ]: 1816 : if (options().quantifiers.hoMatching)
210 : : {
211 : : // get substitution corresponding to m
212 : 2976 : std::vector<TNode> vars;
213 : 2976 : std::vector<TNode> subs;
214 [ + + ]: 4740 : for (unsigned i = 0, size = d_quant[0].getNumChildren(); i < size; i++)
215 : : {
216 : 3252 : subs.push_back(m[i]);
217 : 3252 : vars.push_back(d_qreg.getInstantiationConstant(d_quant, i));
218 : : }
219 : :
220 [ + - ]: 1488 : Trace("ho-unif-debug") << "Run higher-order unification..." << std::endl;
221 : :
222 : : // get the substituted form of all variable-operator ho application terms
223 : 1488 : std::map<TNode, std::vector<Node> > ho_var_apps_subs;
224 [ + + ]: 2984 : for (std::pair<const Node, std::vector<Node> >& ha : d_ho_var_apps)
225 : : {
226 : 2992 : TNode var = ha.first;
227 [ + + ]: 2992 : for (unsigned j = 0, size = ha.second.size(); j < size; j++)
228 : : {
229 : 2992 : TNode app = ha.second[j];
230 : : Node sapp =
231 : 1496 : app.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
232 : 1496 : ho_var_apps_subs[var].push_back(sapp);
233 [ + - ]: 2992 : Trace("ho-unif-debug") << " app[" << var << "] : " << app << " -> "
234 : 1496 : << sapp << std::endl;
235 : : }
236 : : }
237 : :
238 : : // compute argument vectors for each variable
239 : 1488 : d_lchildren.clear();
240 : 1488 : d_arg_to_arg_rep.clear();
241 : 1488 : d_arg_vector.clear();
242 : 1488 : EntailmentCheck* echeck = d_treg.getEntailmentCheck();
243 [ + + ]: 2984 : for (std::pair<const TNode, std::vector<Node> >& ha : ho_var_apps_subs)
244 : : {
245 : 2992 : TNode var = ha.first;
246 : 1496 : unsigned vnum = var.getAttribute(InstVarNumAttribute());
247 : 2992 : TNode value = m[vnum];
248 [ + - ]: 1496 : Trace("ho-unif-debug") << " val[" << var << "] = " << value << std::endl;
249 : :
250 [ + - ]: 2992 : Trace("ho-unif-debug2") << "initialize lambda information..."
251 : 1496 : << std::endl;
252 : : // initialize the lambda children
253 : 1496 : d_lchildren[vnum].push_back(value);
254 : : std::map<TNode, std::vector<Node> >::iterator ithb =
255 : 1496 : d_ho_var_bvs.find(var);
256 [ - + ][ - + ]: 1496 : Assert(ithb != d_ho_var_bvs.end());
[ - - ]
257 : 1496 : d_lchildren[vnum].insert(
258 : 1496 : d_lchildren[vnum].end(), ithb->second.begin(), ithb->second.end());
259 : :
260 [ + - ]: 1496 : Trace("ho-unif-debug2") << "compute fixed arguments..." << std::endl;
261 : : // compute for each argument if it is only applied to a fixed value modulo
262 : : // equality
263 : 2992 : std::map<unsigned, Node> fixed_vals;
264 [ + + ]: 2992 : for (unsigned i = 0; i < ha.second.size(); i++)
265 : : {
266 : 2992 : std::vector<TNode> args;
267 : : // must substitute the operator we matched with the original
268 : : // higher-order variable (var) that matched it. This ensures that the
269 : : // argument vector (args) below is of the proper length. This handles,
270 : : // for example, matches like:
271 : : // (@ x y) with (@ (@ k1 k2) k3)
272 : : // where k3 but not k2 should be an argument of the match.
273 : 2992 : Node hmatch = ha.second[i];
274 [ + - ]: 1496 : Trace("ho-unif-debug2") << "Match is " << hmatch << std::endl;
275 : 1496 : hmatch = hmatch.substitute(value, var);
276 [ + - ]: 1496 : Trace("ho-unif-debug2") << "Pre-subs match is " << hmatch << std::endl;
277 : 2992 : Node f = uf::TheoryUfRewriter::decomposeHoApply(hmatch, args);
278 : : // Assert( f==value );
279 [ + + ]: 3308 : for (unsigned k = 0, size = args.size(); k < size; k++)
280 : : {
281 : : // must now subsitute back, to handle cases like
282 : : // (@ x y) matching (@ t (@ t s))
283 : : // where the above substitution would produce (@ x (@ x s)),
284 : : // but the argument should be (@ t s).
285 : 1812 : args[k] = args[k].substitute(var, value);
286 : 3624 : Node val = args[k];
287 : 1812 : std::map<unsigned, Node>::iterator itf = fixed_vals.find(k);
288 [ + - ]: 1812 : if (itf == fixed_vals.end())
289 : : {
290 : 1812 : fixed_vals[k] = val;
291 : : }
292 [ - - ]: 0 : else if (!itf->second.isNull())
293 : : {
294 [ - - ]: 0 : if (!d_qstate.areEqual(itf->second, args[k]))
295 : : {
296 [ - - ]: 0 : if (!echeck->isEntailed(itf->second.eqNode(args[k]), true))
297 : : {
298 : 0 : fixed_vals[k] = Node::null();
299 : : }
300 : : }
301 : : }
302 : : }
303 : : }
304 [ - + ]: 1496 : if (TraceIsOn("ho-unif-debug"))
305 : : {
306 : 0 : for (std::map<unsigned, Node>::iterator itf = fixed_vals.begin();
307 [ - - ]: 0 : itf != fixed_vals.end();
308 : 0 : ++itf)
309 : : {
310 [ - - ]: 0 : Trace("ho-unif-debug") << " arg[" << var << "][" << itf->first
311 : 0 : << "] : " << itf->second << std::endl;
312 : : }
313 : : }
314 : :
315 : : // now construct argument vectors
316 [ + - ]: 1496 : Trace("ho-unif-debug2") << "compute argument vectors..." << std::endl;
317 : 1496 : std::map<Node, unsigned> arg_to_rep;
318 [ + + ]: 3316 : for (unsigned index = 0, size = ithb->second.size(); index < size;
319 : : index++)
320 : : {
321 : 3640 : Node bv_at_index = ithb->second[index];
322 : 1820 : std::map<unsigned, Node>::iterator itf = fixed_vals.find(index);
323 [ + - ]: 1820 : Trace("ho-unif-debug") << " * arg[" << var << "][" << index << "]";
324 [ + + ]: 1820 : if (itf != fixed_vals.end())
325 : : {
326 [ + - ]: 1812 : if (!itf->second.isNull())
327 : : {
328 : 5436 : Node r = d_qstate.getRepresentative(itf->second);
329 : 1812 : std::map<Node, unsigned>::iterator itfr = arg_to_rep.find(r);
330 [ + + ]: 1812 : if (itfr != arg_to_rep.end())
331 : : {
332 : 130 : d_arg_to_arg_rep[vnum][index] = itfr->second;
333 : : // function applied to equivalent values at multiple arguments,
334 : : // can permute variables
335 : 130 : d_arg_vector[vnum][itfr->second].push_back(bv_at_index);
336 [ + - ]: 260 : Trace("ho-unif-debug") << " = { self } ++ arg[" << var << "]["
337 : 130 : << itfr->second << "]" << std::endl;
338 : : }
339 : : else
340 : : {
341 : 1682 : arg_to_rep[r] = index;
342 : : // function applied to single value, can either use variable or
343 : : // value at this argument position. We give priority to variables,
344 : : // although this order could be changed.
345 : 1682 : d_arg_vector[vnum][index].push_back(bv_at_index);
346 : 1682 : d_arg_vector[vnum][index].push_back(itf->second);
347 [ + - ]: 3364 : Trace("ho-unif-debug") << " = { self, " << itf->second << " } "
348 : 1682 : << std::endl;
349 : : }
350 : : }
351 : : else
352 : : {
353 : : // function is applied to disequal values, can only use variable at
354 : : // this argument position
355 : 0 : d_arg_vector[vnum][index].push_back(bv_at_index);
356 [ - - ]: 0 : Trace("ho-unif-debug") << " = { self } (disequal)" << std::endl;
357 : : }
358 : : }
359 : : else
360 : : {
361 : : // argument is irrelevant to matching, assume identity variable
362 : 8 : d_arg_vector[vnum][index].push_back(bv_at_index);
363 [ + - ]: 8 : Trace("ho-unif-debug") << " = { self } (irrelevant)" << std::endl;
364 : : }
365 : : }
366 [ + - ]: 1496 : Trace("ho-unif-debug2") << "finished." << std::endl;
367 : : }
368 : :
369 : 1488 : bool ret = sendInstantiation(m, 0);
370 [ + - ]: 1488 : Trace("ho-unif-debug") << "Finished, success = " << ret << std::endl;
371 : 1488 : return ret;
372 : : }
373 : : else
374 : : {
375 : : // do not run higher-order matching
376 : 328 : return d_qim.getInstantiate()->addInstantiation(d_quant, m, id);
377 : : }
378 : : }
379 : :
380 : : // recursion depth limited by number of arguments of higher order variables
381 : : // occurring as pattern operators (very small)
382 : 4082 : bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m,
383 : : size_t var_index)
384 : : {
385 [ + - ]: 8164 : Trace("ho-unif-debug2") << "send inst " << var_index << " / "
386 : 4082 : << d_ho_var_list.size() << std::endl;
387 [ + + ]: 4082 : if (var_index == d_ho_var_list.size())
388 : : {
389 : : // we now have an instantiation to try
390 : 7758 : return d_qim.getInstantiate()->addInstantiation(
391 : 5172 : d_quant, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_HO);
392 : : }
393 : : else
394 : : {
395 : 2992 : Node var = d_ho_var_list[var_index];
396 : 1496 : unsigned vnum = var.getAttribute(InstVarNumAttribute());
397 [ - + ][ - + ]: 1496 : Assert(vnum < m.size());
[ - - ]
398 : 1496 : Node value = m[vnum];
399 [ - + ][ - + ]: 1496 : Assert(d_lchildren[vnum][0] == value);
[ - - ]
400 [ - + ][ - + ]: 1496 : Assert(d_ho_var_bvl.find(var) != d_ho_var_bvl.end());
[ - - ]
401 : :
402 : : // now, recurse on arguments to enumerate equivalent matching lambda
403 : : // expressions
404 : : bool ret =
405 : 1496 : sendInstantiationArg(m, var_index, vnum, 0, d_ho_var_bvl[var], false);
406 : :
407 : : // reset the value
408 : 1496 : m[vnum] = value;
409 : :
410 : 1496 : return ret;
411 : : }
412 : : }
413 : :
414 : 4584 : bool HigherOrderTrigger::sendInstantiationArg(std::vector<Node>& m,
415 : : unsigned var_index,
416 : : unsigned vnum,
417 : : unsigned arg_index,
418 : : Node lbvl,
419 : : bool arg_changed)
420 : : {
421 [ + - ]: 9168 : Trace("ho-unif-debug2") << "send inst arg " << arg_index << " / "
422 : 4584 : << lbvl.getNumChildren() << std::endl;
423 [ + + ]: 4584 : if (arg_index == lbvl.getNumChildren())
424 : : {
425 : : // construct the lambda
426 [ + + ]: 2594 : if (arg_changed)
427 : : {
428 [ + - ]: 2344 : Trace("ho-unif-debug2")
429 : 1172 : << " make lambda from children: " << d_lchildren[vnum] << std::endl;
430 : : Node body =
431 : 2344 : NodeManager::currentNM()->mkNode(Kind::APPLY_UF, d_lchildren[vnum]);
432 [ + - ]: 1172 : Trace("ho-unif-debug2") << " got " << body << std::endl;
433 : 2344 : Node lam = NodeManager::mkNode(Kind::LAMBDA, lbvl, body);
434 : 1172 : m[vnum] = lam;
435 [ + - ]: 1172 : Trace("ho-unif-debug2") << " try " << vnum << " -> " << lam << std::endl;
436 : : }
437 : 2594 : return sendInstantiation(m, var_index + 1);
438 : : }
439 : : else
440 : : {
441 : : std::map<unsigned, unsigned>::iterator itr =
442 : 1990 : d_arg_to_arg_rep[vnum].find(arg_index);
443 : : unsigned rindex =
444 [ + + ]: 1990 : itr != d_arg_to_arg_rep[vnum].end() ? itr->second : arg_index;
445 : : std::map<unsigned, std::vector<Node> >::iterator itv =
446 : 1990 : d_arg_vector[vnum].find(rindex);
447 [ - + ][ - + ]: 1990 : Assert(itv != d_arg_vector[vnum].end());
[ - - ]
448 : 1990 : Node prev = lbvl[arg_index];
449 : 1990 : bool ret = false;
450 : : // try each argument in the vector
451 [ + + ]: 3598 : for (unsigned i = 0, size = itv->second.size(); i < size; i++)
452 : : {
453 [ + + ][ + + ]: 3088 : bool new_arg_changed = arg_changed || prev != itv->second[i];
454 : 3088 : d_lchildren[vnum][arg_index + 1] = itv->second[i];
455 [ + + ]: 3088 : if (sendInstantiationArg(
456 : : m, var_index, vnum, arg_index + 1, lbvl, new_arg_changed))
457 : : {
458 : 1480 : ret = true;
459 : 1480 : break;
460 : : }
461 : : }
462 : : // clean up
463 : 1990 : d_lchildren[vnum][arg_index + 1] = prev;
464 : 1990 : return ret;
465 : : }
466 : : }
467 : :
468 : 642 : uint64_t HigherOrderTrigger::addHoTypeMatchPredicateLemmas()
469 : : {
470 [ - + ]: 642 : if (d_ho_var_types.empty())
471 : : {
472 : 0 : return 0;
473 : : }
474 [ + - ]: 642 : Trace("ho-quant-trigger") << "addHoTypeMatchPredicateLemmas..." << std::endl;
475 : 642 : uint64_t numLemmas = 0;
476 : : // this forces expansion of APPLY_UF terms to curried HO_APPLY chains
477 : 642 : TermDb* tdb = d_treg.getTermDatabase();
478 : 642 : unsigned size = tdb->getNumOperators();
479 : 642 : NodeManager* nm = NodeManager::currentNM();
480 [ + + ]: 6266 : for (unsigned j = 0; j < size; j++)
481 : : {
482 : 11248 : Node f = tdb->getOperator(j);
483 [ + + ]: 5624 : if (f.isVar())
484 : : {
485 : 9312 : TypeNode tn = f.getType();
486 [ + - ]: 4656 : if (tn.isFunction())
487 : : {
488 : 9312 : std::vector<TypeNode> argTypes = tn.getArgTypes();
489 [ - + ][ - + ]: 4656 : Assert(argTypes.size() > 0);
[ - - ]
490 : 9312 : TypeNode range = tn.getRangeType();
491 : : // for each function type suffix of the type of f, for example if
492 : : // f : (Int -> (Int -> Int))
493 : : // we iterate with stn = (Int -> (Int -> Int)) and (Int -> Int)
494 [ + + ]: 9800 : for (unsigned a = 0, arg_size = argTypes.size(); a < arg_size; a++)
495 : : {
496 : 10288 : std::vector<TypeNode> sargts;
497 : 5144 : sargts.insert(sargts.begin(), argTypes.begin() + a, argTypes.end());
498 [ - + ][ - + ]: 5144 : Assert(sargts.size() > 0);
[ - - ]
499 : 10288 : TypeNode stn = nm->mkFunctionType(sargts, range);
500 [ + - ]: 10288 : Trace("ho-quant-trigger-debug")
501 : 5144 : << "For " << f << ", check " << stn << "..." << std::endl;
502 : : // if a variable of this type occurs in this trigger
503 [ + + ]: 5144 : if (d_ho_var_types.find(stn) != d_ho_var_types.end())
504 : : {
505 : 6280 : Node u = HoTermDb::getHoTypeMatchPredicate(tn);
506 : 9420 : Node au = NodeManager::mkNode(Kind::APPLY_UF, u, f);
507 [ + + ]: 3140 : if (d_qim.addPendingLemma(au,
508 : : InferenceId::QUANTIFIERS_HO_MATCH_PRED))
509 : : {
510 : : // this forces f to be a first-class member of the quantifier-free
511 : : // equality engine, which in turn forces the quantifier-free
512 : : // theory solver to expand it to an HO_APPLY chain.
513 [ + - ]: 1292 : Trace("ho-quant")
514 : 646 : << "Added ho match predicate lemma : " << au << std::endl;
515 : 646 : numLemmas++;
516 : : }
517 : : }
518 : : }
519 : : }
520 : : }
521 : : }
522 : :
523 : 642 : return numLemmas;
524 : : }
525 : :
526 : : } // namespace inst
527 : : } // namespace quantifiers
528 : : } // namespace theory
529 : : } // namespace cvc5::internal
|
