Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Utility for processing single invocation synthesis conjectures.
11 : : */
12 : : #include "theory/quantifiers/single_inv_partition.h"
13 : :
14 : : #include <sstream>
15 : :
16 : : #include "expr/node_algorithm.h"
17 : : #include "expr/skolem_manager.h"
18 : : #include "theory/quantifiers/term_util.h"
19 : :
20 : : using namespace cvc5::internal;
21 : : using namespace cvc5::internal::kind;
22 : : using namespace std;
23 : :
24 : : namespace cvc5::internal {
25 : : namespace theory {
26 : : namespace quantifiers {
27 : :
28 : 6329 : SingleInvocationPartition::SingleInvocationPartition(Env& env)
29 [ + + ]: 31645 : : EnvObj(env), d_has_input_funcs(false)
30 : : {
31 : 6329 : }
32 : :
33 : 0 : bool SingleInvocationPartition::init(Node n)
34 : : {
35 : : // first, get types of arguments for functions
36 : 0 : std::vector<TypeNode> typs;
37 : 0 : std::map<Node, bool> visited;
38 : 0 : std::vector<Node> funcs;
39 [ - - ]: 0 : if (inferArgTypes(n, typs, visited))
40 : : {
41 : 0 : return init(funcs, typs, n, false);
42 : : }
43 : : else
44 : : {
45 [ - - ]: 0 : Trace("si-prt") << "Could not infer argument types." << std::endl;
46 : 0 : return false;
47 : : }
48 : 0 : }
49 : :
50 : 126 : Node SingleInvocationPartition::getFirstOrderVariableForFunction(Node f) const
51 : : {
52 : 126 : std::map<Node, Node>::const_iterator it = d_func_fo_var.find(f);
53 [ + - ]: 126 : if (it != d_func_fo_var.end())
54 : : {
55 : 126 : return it->second;
56 : : }
57 : 0 : return Node::null();
58 : : }
59 : :
60 : 0 : Node SingleInvocationPartition::getFunctionForFirstOrderVariable(Node v) const
61 : : {
62 : 0 : std::map<Node, Node>::const_iterator it = d_fo_var_to_func.find(v);
63 [ - - ]: 0 : if (it != d_fo_var_to_func.end())
64 : : {
65 : 0 : return it->second;
66 : : }
67 : 0 : return Node::null();
68 : : }
69 : :
70 : 126 : Node SingleInvocationPartition::getFunctionInvocationFor(Node f) const
71 : : {
72 : 126 : std::map<Node, Node>::const_iterator it = d_func_inv.find(f);
73 [ + - ]: 126 : if (it != d_func_inv.end())
74 : : {
75 : 126 : return it->second;
76 : : }
77 : 0 : return Node::null();
78 : : }
79 : :
80 : 157 : void SingleInvocationPartition::getFunctionVariables(
81 : : std::vector<Node>& fvars) const
82 : : {
83 : 157 : fvars.insert(fvars.end(), d_func_vars.begin(), d_func_vars.end());
84 : 157 : }
85 : :
86 : 946 : void SingleInvocationPartition::getFunctions(std::vector<Node>& fs) const
87 : : {
88 : 946 : fs.insert(fs.end(), d_all_funcs.begin(), d_all_funcs.end());
89 : 946 : }
90 : :
91 : 162 : void SingleInvocationPartition::getSingleInvocationVariables(
92 : : std::vector<Node>& sivars) const
93 : : {
94 : 162 : sivars.insert(sivars.end(), d_si_vars.begin(), d_si_vars.end());
95 : 162 : }
96 : :
97 : 5 : void SingleInvocationPartition::getAllVariables(std::vector<Node>& vars) const
98 : : {
99 : 5 : vars.insert(vars.end(), d_all_vars.begin(), d_all_vars.end());
100 : 5 : }
101 : :
102 : : // gets the argument type list for the first APPLY_UF we see
103 : 0 : bool SingleInvocationPartition::inferArgTypes(Node n,
104 : : std::vector<TypeNode>& typs,
105 : : std::map<Node, bool>& visited)
106 : : {
107 [ - - ]: 0 : if (visited.find(n) == visited.end())
108 : : {
109 : 0 : visited[n] = true;
110 [ - - ]: 0 : if (n.getKind() != Kind::FORALL)
111 : : {
112 [ - - ]: 0 : if (n.getKind() == Kind::APPLY_UF)
113 : : {
114 [ - - ]: 0 : for (unsigned i = 0; i < n.getNumChildren(); i++)
115 : : {
116 : 0 : typs.push_back(n[i].getType());
117 : : }
118 : 0 : return true;
119 : : }
120 : : else
121 : : {
122 [ - - ]: 0 : for (unsigned i = 0; i < n.getNumChildren(); i++)
123 : : {
124 [ - - ]: 0 : if (inferArgTypes(n[i], typs, visited))
125 : : {
126 : 0 : return true;
127 : : }
128 : : }
129 : : }
130 : : }
131 : : }
132 : 0 : return false;
133 : : }
134 : :
135 : 977 : bool SingleInvocationPartition::init(std::vector<Node>& funcs, Node n)
136 : : {
137 [ + - ]: 1954 : Trace("si-prt") << "Initialize with " << funcs.size() << " input functions ("
138 : 977 : << funcs << ")..." << std::endl;
139 : 977 : std::vector<TypeNode> typs;
140 [ + - ]: 977 : if (!funcs.empty())
141 : : {
142 : 977 : TypeNode tn0 = funcs[0].getType();
143 [ + + ]: 977 : if (tn0.isFunction())
144 : : {
145 [ + + ]: 2138 : for (unsigned i = 0, nargs = tn0.getNumChildren() - 1; i < nargs; i++)
146 : : {
147 : 1399 : typs.push_back(tn0[i]);
148 : : }
149 : : }
150 [ + + ]: 1397 : for (unsigned i = 1, size = funcs.size(); i < size; i++)
151 : : {
152 : 447 : TypeNode tni = funcs[i].getType();
153 [ + + ]: 447 : if (tni.getNumChildren() != tn0.getNumChildren())
154 : : {
155 : : // can't anti-skolemize functions of different sort
156 [ + - ]: 27 : Trace("si-prt") << "...type mismatch" << std::endl;
157 : 27 : return false;
158 : : }
159 [ + + ]: 420 : else if (tni.isFunction())
160 : : {
161 [ + + ]: 1414 : for (unsigned j = 0, nargs = tni.getNumChildren() - 1; j < nargs; j++)
162 : : {
163 [ - + ]: 1050 : if (tni[j] != typs[j])
164 : : {
165 [ - - ]: 0 : Trace("si-prt") << "...argument type mismatch" << std::endl;
166 : 0 : return false;
167 : : }
168 : : }
169 : : }
170 [ + + ]: 447 : }
171 [ + + ]: 977 : }
172 [ + - ]: 950 : Trace("si-prt") << "#types = " << typs.size() << std::endl;
173 : 950 : return init(funcs, typs, n, true);
174 : 977 : }
175 : :
176 : 950 : bool SingleInvocationPartition::init(std::vector<Node>& funcs,
177 : : std::vector<TypeNode>& typs,
178 : : Node n,
179 : : bool has_funcs)
180 : : {
181 [ - + ][ - + ]: 950 : Assert(d_arg_types.empty());
[ - - ]
182 [ - + ][ - + ]: 950 : Assert(d_input_funcs.empty());
[ - - ]
183 [ - + ][ - + ]: 950 : Assert(d_si_vars.empty());
[ - - ]
184 : 950 : NodeManager* nm = nodeManager();
185 : 950 : d_has_input_funcs = has_funcs;
186 : 950 : d_arg_types.insert(d_arg_types.end(), typs.begin(), typs.end());
187 : 950 : d_input_funcs.insert(d_input_funcs.end(), funcs.begin(), funcs.end());
188 [ + - ]: 950 : Trace("si-prt") << "Initialize..." << std::endl;
189 [ + + ]: 2337 : for (unsigned j = 0; j < d_arg_types.size(); j++)
190 : : {
191 : 1387 : std::stringstream ss;
192 : 1387 : ss << "s_" << j;
193 : 1387 : Node si_v = NodeManager::mkBoundVar(ss.str(), d_arg_types[j]);
194 : 1387 : d_si_vars.push_back(si_v);
195 : 1387 : }
196 [ - + ][ - + ]: 950 : Assert(d_si_vars.size() == d_arg_types.size());
[ - - ]
197 [ + + ]: 2308 : for (const Node& inf : d_input_funcs)
198 : : {
199 : 2716 : Node sk = NodeManager::mkDummySkolem("_sik", inf.getType());
200 : 1358 : d_input_func_sks.push_back(sk);
201 : 1358 : }
202 [ + - ]: 950 : Trace("si-prt") << "SingleInvocationPartition::process " << n << std::endl;
203 [ + - ]: 950 : Trace("si-prt") << "Get conjuncts..." << std::endl;
204 : 950 : std::vector<Node> conj;
205 [ + + ]: 950 : if (collectConjuncts(n, true, conj))
206 : : {
207 [ + - ]: 946 : Trace("si-prt") << "...success." << std::endl;
208 [ + + ]: 3083 : for (unsigned i = 0; i < conj.size(); i++)
209 : : {
210 : 2137 : std::vector<Node> si_terms;
211 : 2137 : std::vector<Node> si_subs;
212 [ + - ]: 2137 : Trace("si-prt") << "Process conjunct : " << conj[i] << std::endl;
213 : : // do DER on conjunct
214 : : // Must avoid eliminating the first-order input functions in the
215 : : // getQuantSimplify step below. We use a substitution to avoid this.
216 : : // This makes it so that e.g. the synthesis conjecture:
217 : : // exists f. f!=0 ^ P
218 : : // is not rewritten to exists f. (f=0 => false) ^ P and subsquently
219 : : // rewritten to exists f. false ^ P by the elimination f -> 0.
220 : 2137 : Node cr = conj[i].substitute(d_input_funcs.begin(),
221 : : d_input_funcs.end(),
222 : : d_input_func_sks.begin(),
223 : 2137 : d_input_func_sks.end());
224 : 2137 : cr = getQuantSimplify(cr);
225 : 4274 : cr = cr.substitute(d_input_func_sks.begin(),
226 : : d_input_func_sks.end(),
227 : : d_input_funcs.begin(),
228 : 2137 : d_input_funcs.end());
229 [ + + ]: 2137 : if (cr != conj[i])
230 : : {
231 [ + - ]: 625 : Trace("si-prt-debug") << "...rewritten to " << cr << std::endl;
232 : : }
233 : 2137 : std::map<Node, bool> visited;
234 : : // functions to arguments
235 : 2137 : std::vector<Node> args;
236 : 2137 : Subs sb;
237 : 2137 : bool singleInvocation = true;
238 : 2137 : bool ngroundSingleInvocation = false;
239 [ + + ]: 2137 : if (processConjunct(cr, visited, args, sb))
240 : : {
241 [ + + ]: 4414 : for (size_t j = 0, vsize = sb.d_vars.size(); j < vsize; j++)
242 : : {
243 : 2372 : Node s = sb.d_subs[j];
244 : 2372 : si_terms.push_back(s);
245 [ + + ]: 2372 : Node op = s.hasOperator() ? s.getOperator() : s;
246 [ - + ][ - + ]: 2372 : Assert(d_func_fo_var.find(op) != d_func_fo_var.end());
[ - - ]
247 : 2372 : si_subs.push_back(d_func_fo_var[op]);
248 : 2372 : }
249 : 2042 : std::map<Node, Node> subs_map;
250 : 2042 : std::map<Node, Node> subs_map_rev;
251 : : // normalize the invocations
252 [ + + ]: 2042 : if (!sb.empty())
253 : : {
254 : 1971 : cr = sb.apply(cr);
255 : : }
256 : 2042 : std::vector<Node> children;
257 : 2042 : children.push_back(cr);
258 : 2042 : sb.clear();
259 [ + - ]: 4084 : Trace("si-prt") << "...single invocation, with arguments: "
260 : 2042 : << std::endl;
261 [ + + ]: 5329 : for (unsigned j = 0; j < args.size(); j++)
262 : : {
263 [ + - ]: 3287 : Trace("si-prt") << args[j] << " ";
264 : 3287 : if (args[j].getKind() == Kind::BOUND_VARIABLE
265 [ + + ][ + + ]: 6574 : && !sb.contains(args[j]))
[ + + ][ + + ]
[ - - ]
266 : : {
267 : 1717 : sb.add(args[j], d_si_vars[j]);
268 : : }
269 : : else
270 : : {
271 : 1570 : children.push_back(d_si_vars[j].eqNode(args[j]).negate());
272 : : }
273 : : }
274 [ + - ]: 2042 : Trace("si-prt") << std::endl;
275 : 2042 : cr = nm->mkOr(children);
276 : 2042 : cr = sb.apply(cr);
277 [ + - ]: 4084 : Trace("si-prt-debug")
278 : 2042 : << "...normalized invocations to " << cr << std::endl;
279 : : // now must check if it has other bound variables
280 : 2042 : std::unordered_set<Node> fvs;
281 : 2042 : expr::getFreeVariables(cr, fvs);
282 : : // bound variables must be contained in the single invocation variables
283 [ + + ]: 8156 : for (const Node& bv : fvs)
284 : : {
285 : 6114 : if (std::find(d_si_vars.begin(), d_si_vars.end(), bv)
286 [ + + ]: 12228 : == d_si_vars.end())
287 : : {
288 : : // getFreeVariables also collects functions in the rare case that
289 : : // we are synthesizing a function with 0 arguments, take this into
290 : : // account here.
291 : 2827 : if (std::find(d_input_funcs.begin(), d_input_funcs.end(), bv)
292 [ + + ]: 5654 : == d_input_funcs.end())
293 : : {
294 [ + - ]: 910 : Trace("si-prt")
295 : 455 : << "...not ground single invocation." << std::endl;
296 : 455 : ngroundSingleInvocation = true;
297 : 455 : singleInvocation = false;
298 : : }
299 : : }
300 : : }
301 [ + + ]: 2042 : if (singleInvocation)
302 : : {
303 [ + - ]: 1616 : Trace("si-prt") << "...ground single invocation" << std::endl;
304 : : }
305 : 2042 : }
306 : : else
307 : : {
308 [ + - ]: 95 : Trace("si-prt") << "...not single invocation." << std::endl;
309 : 95 : singleInvocation = false;
310 : : // rename bound variables with maximal overlap with si_vars
311 : 95 : std::unordered_set<Node> fvs;
312 : 95 : expr::getFreeVariables(cr, fvs);
313 : 95 : std::vector<Node> termsNs;
314 : 95 : std::vector<Node> subsNs;
315 [ + + ]: 616 : for (const Node& v : fvs)
316 : : {
317 : 521 : TypeNode tn = v.getType();
318 [ + - ]: 1042 : Trace("si-prt-debug")
319 : 521 : << "Fit bound var: " << v << " with si." << std::endl;
320 [ + + ]: 3533 : for (unsigned k = 0; k < d_si_vars.size(); k++)
321 : : {
322 [ + + ]: 3303 : if (tn == d_arg_types[k])
323 : : {
324 : 2066 : if (std::find(subsNs.begin(), subsNs.end(), d_si_vars[k])
325 [ + + ]: 4132 : == subsNs.end())
326 : : {
327 : 291 : termsNs.push_back(v);
328 : 291 : subsNs.push_back(d_si_vars[k]);
329 [ + - ]: 582 : Trace("si-prt-debug")
330 : 291 : << " ...use " << d_si_vars[k] << std::endl;
331 : 291 : break;
332 : : }
333 : : }
334 : : }
335 : 521 : }
336 [ - + ][ - + ]: 95 : Assert(termsNs.size() == subsNs.size());
[ - - ]
337 : 190 : cr = cr.substitute(
338 : 95 : termsNs.begin(), termsNs.end(), subsNs.begin(), subsNs.end());
339 : 95 : }
340 [ + - ]: 4274 : Trace("si-prt") << ".....got si=" << singleInvocation
341 : 2137 : << ", result : " << cr << std::endl;
342 : 2137 : d_conjuncts[2].push_back(cr);
343 : 2137 : std::unordered_set<Node> fvs;
344 : 2137 : expr::getFreeVariables(cr, fvs);
345 : 2137 : d_all_vars.insert(fvs.begin(), fvs.end());
346 [ + + ]: 2137 : if (singleInvocation)
347 : : {
348 : : // replace with single invocation formulation
349 [ - + ][ - + ]: 1616 : Assert(si_terms.size() == si_subs.size());
[ - - ]
350 : 3232 : cr = cr.substitute(
351 : 1616 : si_terms.begin(), si_terms.end(), si_subs.begin(), si_subs.end());
352 [ + - ]: 1616 : Trace("si-prt") << ".....si version=" << cr << std::endl;
353 : 1616 : d_conjuncts[0].push_back(cr);
354 : : }
355 : : else
356 : : {
357 : 521 : d_conjuncts[1].push_back(cr);
358 [ + + ]: 521 : if (ngroundSingleInvocation)
359 : : {
360 : 426 : d_conjuncts[3].push_back(cr);
361 : : }
362 : : }
363 : 2137 : }
364 : : }
365 : : else
366 : : {
367 [ + - ]: 4 : Trace("si-prt") << "...failed." << std::endl;
368 : 4 : return false;
369 : : }
370 : 946 : return true;
371 : 950 : }
372 : :
373 : 2714 : bool SingleInvocationPartition::collectConjuncts(Node n,
374 : : bool pol,
375 : : std::vector<Node>& conj)
376 : : {
377 [ + + ][ + - ]: 2714 : if ((!pol && n.getKind() == Kind::OR) || (pol && n.getKind() == Kind::AND))
[ + + ][ + + ]
[ + + ]
378 : : {
379 [ + + ]: 2088 : for (unsigned i = 0; i < n.getNumChildren(); i++)
380 : : {
381 [ + + ]: 1641 : if (!collectConjuncts(n[i], pol, conj))
382 : : {
383 : 3 : return false;
384 : : }
385 : : }
386 : : }
387 [ + + ]: 2264 : else if (n.getKind() == Kind::NOT)
388 : : {
389 : 123 : return collectConjuncts(n[0], !pol, conj);
390 : : }
391 [ + + ]: 2141 : else if (n.getKind() == Kind::FORALL)
392 : : {
393 : 4 : return false;
394 : : }
395 : : else
396 : : {
397 [ + + ]: 2137 : if (!pol)
398 : : {
399 : 120 : n = TermUtil::simpleNegate(n);
400 : : }
401 [ + - ]: 2137 : Trace("si-prt") << "Conjunct : " << n << std::endl;
402 : 2137 : conj.push_back(n);
403 : : }
404 : 2584 : return true;
405 : : }
406 : :
407 : 30873 : bool SingleInvocationPartition::processConjunct(Node n,
408 : : std::map<Node, bool>& visited,
409 : : std::vector<Node>& args,
410 : : Subs& sb)
411 : : {
412 : 30873 : std::map<Node, bool>::iterator it = visited.find(n);
413 [ + + ]: 30873 : if (it != visited.end())
414 : : {
415 : 10345 : return true;
416 : : }
417 : : else
418 : : {
419 : 20528 : bool ret = true;
420 [ + + ]: 49264 : for (unsigned i = 0; i < n.getNumChildren(); i++)
421 : : {
422 [ + + ]: 28736 : if (!processConjunct(n[i], visited, args, sb))
423 : : {
424 : 215 : ret = false;
425 : : }
426 : : }
427 [ + + ]: 20528 : if (ret)
428 : : {
429 : 20327 : Node f;
430 : 20327 : bool success = false;
431 [ + - ]: 20327 : if (d_has_input_funcs)
432 : : {
433 [ + + ]: 20327 : f = n.hasOperator() ? n.getOperator() : n;
434 : 20327 : if (std::find(d_input_funcs.begin(), d_input_funcs.end(), f)
435 [ + + ]: 40654 : != d_input_funcs.end())
436 : : {
437 : : // If n is an application of a function-to-synthesize f, or is
438 : : // itself a function-to-synthesize, then n must be fully applied.
439 : : // This catches cases where n is a function-to-synthesize that occurs
440 : : // in a higher-order context.
441 : : // If the type of n is functional, then it is not fully applied.
442 [ + + ]: 2572 : if (n.getType().isFunction())
443 : : {
444 : 4 : ret = false;
445 : 4 : success = false;
446 : : }
447 : : else
448 : : {
449 : 2568 : success = true;
450 : : }
451 : : }
452 : : }
453 : : else
454 : : {
455 [ - - ]: 0 : if (n.getKind() == Kind::APPLY_UF)
456 : : {
457 : 0 : f = n.getOperator();
458 : 0 : success = true;
459 : : }
460 : : }
461 [ + + ]: 20327 : if (success)
462 : : {
463 [ + - ]: 2568 : Trace("si-prt-debug") << "Process " << n << std::endl;
464 [ + - ]: 2568 : if (!sb.contains(n))
465 : : {
466 : : // check if it matches the type requirement
467 [ + + ]: 2568 : if (isAntiSkolemizableType(f))
468 : : {
469 [ + + ]: 2556 : if (args.empty())
470 : : {
471 : : // record arguments
472 [ + + ]: 5689 : for (unsigned i = 0; i < n.getNumChildren(); i++)
473 : : {
474 : 3590 : args.push_back(n[i]);
475 : : }
476 : : }
477 : : else
478 : : {
479 : : // arguments must be the same as those already recorded
480 [ + + ]: 1523 : for (unsigned i = 0; i < n.getNumChildren(); i++)
481 : : {
482 [ + + ]: 1159 : if (args[i] != n[i])
483 : : {
484 [ + - ]: 186 : Trace("si-prt-debug") << "...bad invocation : " << n
485 : 93 : << " at arg " << i << "." << std::endl;
486 : 93 : ret = false;
487 : 93 : break;
488 : : }
489 : : }
490 : : }
491 [ + + ]: 2556 : if (ret)
492 : : {
493 : 2463 : sb.add(n, d_func_inv[f]);
494 : : }
495 : : }
496 : : else
497 : : {
498 [ + - ]: 24 : Trace("si-prt-debug")
499 : 12 : << "... " << f << " is a bad operator." << std::endl;
500 : 12 : ret = false;
501 : : }
502 : : }
503 : : }
504 : 20327 : }
505 : 20528 : visited[n] = ret;
506 : 20528 : return ret;
507 : : }
508 : : }
509 : :
510 : 2568 : bool SingleInvocationPartition::isAntiSkolemizableType(Node f)
511 : : {
512 : 2568 : std::map<Node, bool>::iterator it = d_funcs.find(f);
513 [ + + ]: 2568 : if (it != d_funcs.end())
514 : : {
515 : 1288 : return it->second;
516 : : }
517 : : else
518 : : {
519 : 1280 : TypeNode tn = f.getType();
520 : 1280 : bool ret = false;
521 [ - + ]: 2350 : if (((tn.isFunction() && tn.getNumChildren() == d_arg_types.size() + 1)
522 [ + + ][ + - ]: 2350 : || (d_arg_types.empty() && tn.getNumChildren() == 0)))
[ + + ][ + + ]
523 : : {
524 : 1268 : ret = true;
525 : 1268 : std::vector<Node> children;
526 : 1268 : children.push_back(f);
527 : : // TODO: permutations of arguments
528 [ + + ]: 3676 : for (unsigned i = 0; i < d_arg_types.size(); i++)
529 : : {
530 : 2408 : children.push_back(d_si_vars[i]);
531 [ - + ]: 2408 : if (tn[i] != d_arg_types[i])
532 : : {
533 : 0 : ret = false;
534 : 0 : break;
535 : : }
536 : : }
537 [ + - ]: 1268 : if (ret)
538 : : {
539 : 1268 : Node t;
540 [ + + ]: 1268 : if (children.size() > 1)
541 : : {
542 : 1070 : t = nodeManager()->mkNode(Kind::APPLY_UF, children);
543 : : }
544 : : else
545 : : {
546 : 198 : t = children[0];
547 : : }
548 : 1268 : d_func_inv[f] = t;
549 : 1268 : std::stringstream ss;
550 : 1268 : ss << "F_" << f;
551 : 1268 : TypeNode rt;
552 [ + + ]: 1268 : if (d_arg_types.empty())
553 : : {
554 : 198 : rt = tn;
555 : : }
556 : : else
557 : : {
558 : 1070 : rt = tn.getRangeType();
559 : : }
560 : 1268 : Node v = nodeManager()->mkBoundVar(ss.str(), rt);
561 : 1268 : d_func_fo_var[f] = v;
562 : 1268 : d_fo_var_to_func[v] = f;
563 : 1268 : d_func_vars.push_back(v);
564 : 1268 : d_all_funcs.push_back(f);
565 : 1268 : }
566 : 1268 : }
567 : 1280 : d_funcs[f] = ret;
568 : 1280 : return ret;
569 : 1280 : }
570 : : }
571 : :
572 : 162 : Node SingleInvocationPartition::getConjunct(int index)
573 : : {
574 : 162 : return d_conjuncts[index].empty()
575 : 162 : ? nodeManager()->mkConst(true)
576 : 162 : : (d_conjuncts[index].size() == 1
577 : 103 : ? d_conjuncts[index][0]
578 [ - + ][ + + ]: 589 : : nodeManager()->mkNode(Kind::AND, d_conjuncts[index]));
579 : : }
580 : :
581 : 946 : void SingleInvocationPartition::debugPrint(CVC5_UNUSED const char* c)
582 : : {
583 [ + - ]: 946 : Trace(c) << "Single invocation variables : ";
584 [ + + ]: 2328 : for (unsigned i = 0; i < d_si_vars.size(); i++)
585 : : {
586 [ + - ]: 1382 : Trace(c) << d_si_vars[i] << " ";
587 : : }
588 [ + - ]: 946 : Trace(c) << std::endl;
589 [ + - ]: 946 : Trace(c) << "Functions : " << std::endl;
590 [ + + ]: 2226 : for (std::map<Node, bool>::iterator it = d_funcs.begin(); it != d_funcs.end();
591 : 1280 : ++it)
592 : : {
593 [ + - ]: 1280 : Trace(c) << " " << it->first << " : ";
594 [ + + ]: 1280 : if (it->second)
595 : : {
596 [ + - ]: 2536 : Trace(c) << d_func_inv[it->first] << " " << d_func_fo_var[it->first]
597 : 1268 : << std::endl;
598 : : }
599 : : else
600 : : {
601 [ + - ]: 12 : Trace(c) << "not incorporated." << std::endl;
602 : : }
603 : : }
604 [ + + ]: 4730 : for (unsigned i = 0; i < 4; i++)
605 : : {
606 [ + - ][ - - ]: 7568 : Trace(c) << (i == 0 ? "Single invocation"
607 [ - - ]: 0 : : (i == 1 ? "Non-single invocation"
608 [ - - ]: 0 : : (i == 2 ? "All"
609 : 3784 : : "Non-ground single invocation")));
610 [ + - ]: 3784 : Trace(c) << " conjuncts: " << std::endl;
611 [ + + ]: 8484 : for (unsigned j = 0; j < d_conjuncts[i].size(); j++)
612 : : {
613 [ + - ]: 4700 : Trace(c) << " " << (j + 1) << " : " << d_conjuncts[i][j] << std::endl;
614 : : }
615 : : }
616 [ + - ]: 946 : Trace(c) << std::endl;
617 : 946 : }
618 : :
619 : 2137 : Node SingleInvocationPartition::getQuantSimplify(TNode n) const
620 : : {
621 : 2137 : std::unordered_set<Node> fvs;
622 : 2137 : expr::getFreeVariables(n, fvs);
623 [ + + ]: 2137 : if (fvs.empty())
624 : : {
625 : 1065 : return rewrite(n);
626 : : }
627 : 1072 : std::vector<Node> bvs(fvs.begin(), fvs.end());
628 : 1072 : NodeManager* nm = nodeManager();
629 : 2144 : Node q = nm->mkNode(Kind::FORALL, nm->mkNode(Kind::BOUND_VAR_LIST, bvs), n);
630 : 1072 : q = rewrite(q);
631 : 1072 : return TermUtil::getRemoveQuantifiers(q);
632 : 2137 : }
633 : :
634 : : } // namespace quantifiers
635 : : } // namespace theory
636 : : } // namespace cvc5::internal
|
