1 /********************* */
2 /*! \file sygus_process_conj.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Andrew Reynolds
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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.\endverbatim
11 **
12 ** \brief Implementation of techniqures for static preprocessing and analysis
13 ** of sygus conjectures.
14 **/
15 #include "theory/quantifiers/sygus/sygus_process_conj.h"
16
17 #include <stack>
18
19 #include "expr/datatype.h"
20 #include "options/quantifiers_options.h"
21 #include "theory/datatypes/datatypes_rewriter.h"
22 #include "theory/quantifiers/sygus/term_database_sygus.h"
23 #include "theory/quantifiers/term_util.h"
24
25 using namespace CVC4::kind;
26 using namespace std;
27
28 namespace CVC4 {
29 namespace theory {
30 namespace quantifiers {
31
init(Node f)32 void SynthConjectureProcessFun::init(Node f)
33 {
34 d_synth_fun = f;
35 Assert(f.getType().isFunction());
36
37 // initialize the arguments
38 std::unordered_map<TypeNode, unsigned, TypeNodeHashFunction>
39 type_to_init_deq_id;
40 std::vector<Type> argTypes =
41 static_cast<FunctionType>(f.getType().toType()).getArgTypes();
42 for (unsigned j = 0; j < argTypes.size(); j++)
43 {
44 TypeNode atn = TypeNode::fromType(argTypes[j]);
45 std::stringstream ss;
46 ss << "a" << j;
47 Node k = NodeManager::currentNM()->mkBoundVar(ss.str(), atn);
48 d_arg_vars.push_back(k);
49 d_arg_var_num[k] = j;
50 d_arg_props.push_back(SynthConjectureProcessArg());
51 }
52 }
53
checkMatch(Node cn,Node n,std::unordered_map<unsigned,Node> & n_arg_map)54 bool SynthConjectureProcessFun::checkMatch(
55 Node cn, Node n, std::unordered_map<unsigned, Node>& n_arg_map)
56 {
57 std::vector<Node> vars;
58 std::vector<Node> subs;
59 for (std::unordered_map<unsigned, Node>::iterator it = n_arg_map.begin();
60 it != n_arg_map.end();
61 ++it)
62 {
63 Assert(it->first < d_arg_vars.size());
64 Assert(
65 it->second.getType().isComparableTo(d_arg_vars[it->first].getType()));
66 vars.push_back(d_arg_vars[it->first]);
67 subs.push_back(it->second);
68 }
69 Node cn_subs =
70 cn.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
71 cn_subs = Rewriter::rewrite(cn_subs);
72 Assert(Rewriter::rewrite(n) == n);
73 return cn_subs == n;
74 }
75
isArgVar(Node n,unsigned & arg_index)76 bool SynthConjectureProcessFun::isArgVar(Node n, unsigned& arg_index)
77 {
78 if (n.isVar())
79 {
80 std::unordered_map<Node, unsigned, NodeHashFunction>::iterator ita =
81 d_arg_var_num.find(n);
82 if (ita != d_arg_var_num.end())
83 {
84 arg_index = ita->second;
85 return true;
86 }
87 }
88 return false;
89 }
90
inferDefinition(Node n,std::unordered_map<Node,unsigned,NodeHashFunction> & term_to_arg_carry,std::unordered_map<Node,std::unordered_set<Node,NodeHashFunction>,NodeHashFunction> & free_vars)91 Node SynthConjectureProcessFun::inferDefinition(
92 Node n,
93 std::unordered_map<Node, unsigned, NodeHashFunction>& term_to_arg_carry,
94 std::unordered_map<Node,
95 std::unordered_set<Node, NodeHashFunction>,
96 NodeHashFunction>& free_vars)
97 {
98 std::unordered_map<TNode, Node, TNodeHashFunction> visited;
99 std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
100 std::stack<TNode> visit;
101 TNode cur;
102 visit.push(n);
103 do
104 {
105 cur = visit.top();
106 visit.pop();
107 it = visited.find(cur);
108 if (it == visited.end())
109 {
110 // if it is ground, we can use it
111 if (free_vars[cur].empty())
112 {
113 visited[cur] = cur;
114 }
115 else
116 {
117 // if it is term used by another argument, use it
118 std::unordered_map<Node, unsigned, NodeHashFunction>::iterator itt =
119 term_to_arg_carry.find(cur);
120 if (itt != term_to_arg_carry.end())
121 {
122 visited[cur] = d_arg_vars[itt->second];
123 }
124 else if (cur.getNumChildren() > 0)
125 {
126 // try constructing children
127 visited[cur] = Node::null();
128 visit.push(cur);
129 for (unsigned i = 0; i < cur.getNumChildren(); i++)
130 {
131 visit.push(cur[i]);
132 }
133 }
134 else
135 {
136 return Node::null();
137 }
138 }
139 }
140 else if (it->second.isNull())
141 {
142 Node ret = cur;
143 bool childChanged = false;
144 std::vector<Node> children;
145 if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
146 {
147 children.push_back(cur.getOperator());
148 }
149 for (unsigned i = 0; i < cur.getNumChildren(); i++)
150 {
151 it = visited.find(cur[i]);
152 Assert(it != visited.end());
153 Assert(!it->second.isNull());
154 childChanged = childChanged || cur[i] != it->second;
155 children.push_back(it->second);
156 }
157 if (childChanged)
158 {
159 ret = NodeManager::currentNM()->mkNode(cur.getKind(), children);
160 }
161 visited[cur] = ret;
162 }
163 } while (!visit.empty());
164 Assert(visited.find(n) != visited.end());
165 Assert(!visited.find(n)->second.isNull());
166 return visited[n];
167 }
168
assignRelevantDef(Node def,std::vector<unsigned> & args)169 unsigned SynthConjectureProcessFun::assignRelevantDef(
170 Node def, std::vector<unsigned>& args)
171 {
172 unsigned id = 0;
173 if (def.isNull())
174 {
175 // prefer one that already has a definition, if one exists
176 for (unsigned j = 0; j < args.size(); j++)
177 {
178 unsigned i = args[j];
179 if (!d_arg_props[i].d_template.isNull())
180 {
181 id = j;
182 break;
183 }
184 }
185 }
186 unsigned rid = args[id];
187 // for merging previously equivalent definitions
188 std::unordered_map<Node, unsigned, NodeHashFunction> prev_defs;
189 for (unsigned j = 0; j < args.size(); j++)
190 {
191 unsigned i = args[j];
192 Trace("sygus-process-arg-deps") << " ...processed arg #" << i;
193 if (!d_arg_props[i].d_template.isNull())
194 {
195 if (d_arg_props[i].d_template == def)
196 {
197 // definition was consistent
198 }
199 else
200 {
201 Node t = d_arg_props[i].d_template;
202 std::unordered_map<Node, unsigned, NodeHashFunction>::iterator itt =
203 prev_defs.find(t);
204 if (itt != prev_defs.end())
205 {
206 // merge previously equivalent definitions
207 d_arg_props[i].d_template = d_arg_vars[itt->second];
208 Trace("sygus-process-arg-deps")
209 << " (merged equivalent def from argument ";
210 Trace("sygus-process-arg-deps") << itt->second << ")." << std::endl;
211 }
212 else
213 {
214 // store this as previous
215 prev_defs[t] = i;
216 // now must be relevant
217 d_arg_props[i].d_relevant = true;
218 Trace("sygus-process-arg-deps")
219 << " (marked relevant, overwrite definition)." << std::endl;
220 }
221 }
222 }
223 else
224 {
225 if (def.isNull())
226 {
227 if (i != rid)
228 {
229 // marked as relevant, but template can be set equal to master
230 d_arg_props[i].d_template = d_arg_vars[rid];
231 Trace("sygus-process-arg-deps") << " (new definition, map to master "
232 << d_arg_vars[rid] << ")."
233 << std::endl;
234 }
235 else
236 {
237 d_arg_props[i].d_relevant = true;
238 Trace("sygus-process-arg-deps") << " (marked relevant)." << std::endl;
239 }
240 }
241 else
242 {
243 // has new definition
244 d_arg_props[i].d_template = def;
245 Trace("sygus-process-arg-deps") << " (new definition " << def << ")."
246 << std::endl;
247 }
248 }
249 }
250 return rid;
251 }
252
processTerms(std::vector<Node> & ns,std::vector<Node> & ks,Node nf,std::unordered_set<Node,NodeHashFunction> & synth_fv,std::unordered_map<Node,std::unordered_set<Node,NodeHashFunction>,NodeHashFunction> & free_vars)253 void SynthConjectureProcessFun::processTerms(
254 std::vector<Node>& ns,
255 std::vector<Node>& ks,
256 Node nf,
257 std::unordered_set<Node, NodeHashFunction>& synth_fv,
258 std::unordered_map<Node,
259 std::unordered_set<Node, NodeHashFunction>,
260 NodeHashFunction>& free_vars)
261 {
262 Assert(ns.size() == ks.size());
263 Trace("sygus-process-arg-deps") << "Process " << ns.size()
264 << " applications of " << d_synth_fun << "..."
265 << std::endl;
266
267 // get the relevant variables
268 // relevant variables are those that appear in the body of the conjunction
269 std::unordered_set<Node, NodeHashFunction> rlv_vars;
270 Assert(free_vars.find(nf) != free_vars.end());
271 rlv_vars = free_vars[nf];
272
273 // get the single occurrence variables
274 // single occurrence variables are those that appear in only one position,
275 // as an argument to the function-to-synthesize.
276 std::unordered_map<Node, bool, NodeHashFunction> single_occ_variables;
277 for (unsigned index = 0; index < ns.size(); index++)
278 {
279 Node n = ns[index];
280 for (unsigned i = 0; i < n.getNumChildren(); i++)
281 {
282 Node nn = n[i];
283 if (nn.isVar())
284 {
285 std::unordered_map<Node, bool, NodeHashFunction>::iterator its =
286 single_occ_variables.find(nn);
287 if (its == single_occ_variables.end())
288 {
289 // only irrelevant variables
290 single_occ_variables[nn] = rlv_vars.find(nn) == rlv_vars.end();
291 }
292 else
293 {
294 single_occ_variables[nn] = false;
295 }
296 }
297 else
298 {
299 std::unordered_map<Node,
300 std::unordered_set<Node, NodeHashFunction>,
301 NodeHashFunction>::iterator itf = free_vars.find(nn);
302 Assert(itf != free_vars.end());
303 for (std::unordered_set<Node, NodeHashFunction>::iterator itfv =
304 itf->second.begin();
305 itfv != itf->second.end();
306 ++itfv)
307 {
308 single_occ_variables[*itfv] = false;
309 }
310 }
311 }
312 }
313
314 // update constant argument information
315 for (unsigned index = 0; index < ns.size(); index++)
316 {
317 Node n = ns[index];
318 Trace("sygus-process-arg-deps")
319 << " Analyze argument information for application #" << index << ": "
320 << n << std::endl;
321
322 // in the following, we say an argument a "carries" a term t if
323 // the function to synthesize would use argument a to construct
324 // the term t in its definition.
325
326 // map that assumes all arguments carry their respective term
327 std::unordered_map<unsigned, Node> n_arg_map;
328 // terms to the argument that is carrying it.
329 // the arguments in the range of this map must be marked as relevant.
330 std::unordered_map<Node, unsigned, NodeHashFunction> term_to_arg_carry;
331 // map of terms to (unprocessed) arguments where it occurs
332 std::unordered_map<Node, std::vector<unsigned>, NodeHashFunction>
333 term_to_args;
334
335 // initialize
336 for (unsigned a = 0; a < n.getNumChildren(); a++)
337 {
338 n_arg_map[a] = n[a];
339 }
340
341 for (unsigned a = 0; a < n.getNumChildren(); a++)
342 {
343 bool processed = false;
344 if (d_arg_props[a].d_relevant)
345 {
346 // we can assume all relevant arguments carry their terms
347 processed = true;
348 Trace("sygus-process-arg-deps") << " ...processed arg #" << a
349 << " (already relevant)." << std::endl;
350 if (term_to_arg_carry.find(n[a]) == term_to_arg_carry.end())
351 {
352 Trace("sygus-process-arg-deps") << " carry " << n[a]
353 << " by argument #" << a << std::endl;
354 term_to_arg_carry[n[a]] = a;
355 }
356 }
357 else
358 {
359 // first, check if single occurrence variable
360 // check if an irrelevant variable
361 if (n[a].isVar() && synth_fv.find(n[a]) != synth_fv.end())
362 {
363 Assert(single_occ_variables.find(n[a]) != single_occ_variables.end());
364 // may be able to make this more precise?
365 // check if a single-occurrence variable
366 if (single_occ_variables[n[a]])
367 {
368 // if we do not already have a template definition, or the
369 // template is a single occurrence variable
370 if (d_arg_props[a].d_template.isNull()
371 || d_arg_props[a].d_var_single_occ)
372 {
373 processed = true;
374 Trace("sygus-process-arg-deps") << " ...processed arg #" << a;
375 Trace("sygus-process-arg-deps")
376 << " (single occurrence variable ";
377 Trace("sygus-process-arg-deps") << n[a] << ")." << std::endl;
378 d_arg_props[a].d_var_single_occ = true;
379 d_arg_props[a].d_template = n[a];
380 }
381 }
382 }
383 if (!processed && !d_arg_props[a].d_template.isNull()
384 && !d_arg_props[a].d_var_single_occ)
385 {
386 // argument already has a definition, see if it is maintained
387 if (checkMatch(d_arg_props[a].d_template, n[a], n_arg_map))
388 {
389 processed = true;
390 Trace("sygus-process-arg-deps") << " ...processed arg #" << a;
391 Trace("sygus-process-arg-deps") << " (consistent definition "
392 << n[a];
393 Trace("sygus-process-arg-deps")
394 << " with " << d_arg_props[a].d_template << ")." << std::endl;
395 }
396 }
397 }
398 if (!processed)
399 {
400 // otherwise, add it to the list of arguments for this term
401 term_to_args[n[a]].push_back(a);
402 }
403 }
404
405 Trace("sygus-process-arg-deps") << " Look at argument terms..."
406 << std::endl;
407
408 // list of all arguments
409 std::vector<Node> arg_list;
410 // now look at the terms for unprocessed arguments
411 for (std::unordered_map<Node, std::vector<unsigned>, NodeHashFunction>::
412 iterator it = term_to_args.begin();
413 it != term_to_args.end();
414 ++it)
415 {
416 Node nn = it->first;
417 arg_list.push_back(nn);
418 if (Trace.isOn("sygus-process-arg-deps"))
419 {
420 Trace("sygus-process-arg-deps") << " argument " << nn;
421 Trace("sygus-process-arg-deps") << " (" << it->second.size()
422 << " positions)";
423 // check the status of this term
424 if (nn.isVar() && synth_fv.find(nn) != synth_fv.end())
425 {
426 // is it relevant?
427 if (rlv_vars.find(nn) != rlv_vars.end())
428 {
429 Trace("sygus-process-arg-deps") << " is a relevant variable."
430 << std::endl;
431 }
432 else
433 {
434 Trace("sygus-process-arg-deps") << " is an irrelevant variable."
435 << std::endl;
436 }
437 }
438 else
439 {
440 // this can be more precise
441 Trace("sygus-process-arg-deps") << " is a relevant term."
442 << std::endl;
443 }
444 }
445 }
446
447 unsigned arg_list_counter = 0;
448 // sort arg_list by term size?
449
450 while (arg_list_counter < arg_list.size())
451 {
452 Node infer_def_t;
453 do
454 {
455 infer_def_t = Node::null();
456 // see if we can infer a definition
457 for (std::unordered_map<Node, std::vector<unsigned>, NodeHashFunction>::
458 iterator it = term_to_args.begin();
459 it != term_to_args.end();
460 ++it)
461 {
462 Node def = inferDefinition(it->first, term_to_arg_carry, free_vars);
463 if (!def.isNull())
464 {
465 Trace("sygus-process-arg-deps") << " *** Inferred definition "
466 << def << " for " << it->first
467 << std::endl;
468 // assign to each argument
469 assignRelevantDef(def, it->second);
470 // term_to_arg_carry[it->first] = rid;
471 infer_def_t = it->first;
472 break;
473 }
474 }
475 if (!infer_def_t.isNull())
476 {
477 term_to_args.erase(infer_def_t);
478 }
479 } while (!infer_def_t.isNull());
480
481 // decide to make an argument relevant
482 bool success = false;
483 while (arg_list_counter < arg_list.size() && !success)
484 {
485 Node curr = arg_list[arg_list_counter];
486 std::unordered_map<Node, std::vector<unsigned>, NodeHashFunction>::
487 iterator it = term_to_args.find(curr);
488 if (it != term_to_args.end())
489 {
490 Trace("sygus-process-arg-deps") << " *** Decide relevant " << curr
491 << std::endl;
492 // assign relevant to each
493 Node null_def;
494 unsigned rid = assignRelevantDef(null_def, it->second);
495 term_to_arg_carry[curr] = rid;
496 Trace("sygus-process-arg-deps")
497 << " carry " << curr << " by argument #" << rid << std::endl;
498 term_to_args.erase(curr);
499 success = true;
500 }
501 arg_list_counter++;
502 }
503 }
504 }
505 }
506
isArgRelevant(unsigned i)507 bool SynthConjectureProcessFun::isArgRelevant(unsigned i)
508 {
509 return d_arg_props[i].d_relevant;
510 }
511
getIrrelevantArgs(std::unordered_set<unsigned> & args)512 void SynthConjectureProcessFun::getIrrelevantArgs(
513 std::unordered_set<unsigned>& args)
514 {
515 for (unsigned i = 0; i < d_arg_vars.size(); i++)
516 {
517 if (!d_arg_props[i].d_relevant)
518 {
519 args.insert(i);
520 }
521 }
522 }
523
SynthConjectureProcess(QuantifiersEngine * qe)524 SynthConjectureProcess::SynthConjectureProcess(QuantifiersEngine* qe) {}
~SynthConjectureProcess()525 SynthConjectureProcess::~SynthConjectureProcess() {}
preSimplify(Node q)526 Node SynthConjectureProcess::preSimplify(Node q)
527 {
528 Trace("sygus-process") << "Pre-simplify conjecture : " << q << std::endl;
529 return q;
530 }
531
postSimplify(Node q)532 Node SynthConjectureProcess::postSimplify(Node q)
533 {
534 Trace("sygus-process") << "Post-simplify conjecture : " << q << std::endl;
535 Assert(q.getKind() == FORALL);
536
537 if (options::sygusArgRelevant())
538 {
539 // initialize the information about each function to synthesize
540 for (unsigned i = 0, size = q[0].getNumChildren(); i < size; i++)
541 {
542 Node f = q[0][i];
543 if (f.getType().isFunction())
544 {
545 d_sf_info[f].init(f);
546 }
547 }
548
549 // get the base on the conjecture
550 Node base = q[1];
551 std::unordered_set<Node, NodeHashFunction> synth_fv;
552 if (base.getKind() == NOT && base[0].getKind() == FORALL)
553 {
554 for (unsigned j = 0, size = base[0][0].getNumChildren(); j < size; j++)
555 {
556 synth_fv.insert(base[0][0][j]);
557 }
558 base = base[0][1];
559 }
560 std::vector<Node> conjuncts;
561 getComponentVector(AND, base, conjuncts);
562
563 // process the conjunctions
564 for (std::map<Node, SynthConjectureProcessFun>::iterator it =
565 d_sf_info.begin();
566 it != d_sf_info.end();
567 ++it)
568 {
569 Node f = it->first;
570 for (const Node& conj : conjuncts)
571 {
572 processConjunct(conj, f, synth_fv);
573 }
574 }
575 }
576
577 return q;
578 }
579
initialize(Node n,std::vector<Node> & candidates)580 void SynthConjectureProcess::initialize(Node n, std::vector<Node>& candidates)
581 {
582 if (Trace.isOn("sygus-process"))
583 {
584 Trace("sygus-process") << "Process conjecture : " << n
585 << " with candidates: " << std::endl;
586 for (unsigned i = 0; i < candidates.size(); i++)
587 {
588 Trace("sygus-process") << " " << candidates[i] << std::endl;
589 }
590 }
591 }
592
isArgRelevant(Node f,unsigned i)593 bool SynthConjectureProcess::isArgRelevant(Node f, unsigned i)
594 {
595 if (!options::sygusArgRelevant())
596 {
597 return true;
598 }
599 std::map<Node, SynthConjectureProcessFun>::iterator its = d_sf_info.find(f);
600 if (its != d_sf_info.end())
601 {
602 return its->second.isArgRelevant(i);
603 }
604 Assert(false);
605 return true;
606 }
607
getIrrelevantArgs(Node f,std::unordered_set<unsigned> & args)608 bool SynthConjectureProcess::getIrrelevantArgs(
609 Node f, std::unordered_set<unsigned>& args)
610 {
611 std::map<Node, SynthConjectureProcessFun>::iterator its = d_sf_info.find(f);
612 if (its != d_sf_info.end())
613 {
614 its->second.getIrrelevantArgs(args);
615 return true;
616 }
617 return false;
618 }
619
processConjunct(Node n,Node f,std::unordered_set<Node,NodeHashFunction> & synth_fv)620 void SynthConjectureProcess::processConjunct(
621 Node n, Node f, std::unordered_set<Node, NodeHashFunction>& synth_fv)
622 {
623 Trace("sygus-process-arg-deps") << "Process conjunct: " << std::endl;
624 Trace("sygus-process-arg-deps") << " " << n << " for synth fun " << f
625 << "..." << std::endl;
626
627 // first, flatten the conjunct
628 // make a copy of free variables since we may add new ones
629 std::unordered_set<Node, NodeHashFunction> synth_fv_n = synth_fv;
630 std::unordered_map<Node, Node, NodeHashFunction> defs;
631 Node nf = flatten(n, f, synth_fv_n, defs);
632
633 Trace("sygus-process-arg-deps") << "Flattened to: " << std::endl;
634 Trace("sygus-process-arg-deps") << " " << nf << std::endl;
635
636 // get free variables in nf
637 std::unordered_map<Node,
638 std::unordered_set<Node, NodeHashFunction>,
639 NodeHashFunction>
640 free_vars;
641 getFreeVariables(nf, synth_fv_n, free_vars);
642 // get free variables in each application
643 std::vector<Node> ns;
644 std::vector<Node> ks;
645 for (std::unordered_map<Node, Node, NodeHashFunction>::iterator it =
646 defs.begin();
647 it != defs.end();
648 ++it)
649 {
650 getFreeVariables(it->second, synth_fv_n, free_vars);
651 ns.push_back(it->second);
652 ks.push_back(it->first);
653 }
654
655 // process the applications of synthesis functions
656 if (!ns.empty())
657 {
658 std::map<Node, SynthConjectureProcessFun>::iterator its = d_sf_info.find(f);
659 if (its != d_sf_info.end())
660 {
661 its->second.processTerms(ns, ks, nf, synth_fv_n, free_vars);
662 }
663 }
664 }
665
flatten(Node n,Node f,std::unordered_set<Node,NodeHashFunction> & synth_fv,std::unordered_map<Node,Node,NodeHashFunction> & defs)666 Node SynthConjectureProcess::SynthConjectureProcess::flatten(
667 Node n,
668 Node f,
669 std::unordered_set<Node, NodeHashFunction>& synth_fv,
670 std::unordered_map<Node, Node, NodeHashFunction>& defs)
671 {
672 std::unordered_map<Node, Node, NodeHashFunction> visited;
673 std::unordered_map<Node, Node, NodeHashFunction>::iterator it;
674 std::stack<Node> visit;
675 Node cur;
676 visit.push(n);
677 do
678 {
679 cur = visit.top();
680 visit.pop();
681 it = visited.find(cur);
682
683 if (it == visited.end())
684 {
685 visited[cur] = Node::null();
686 visit.push(cur);
687 for (unsigned i = 0; i < cur.getNumChildren(); i++)
688 {
689 visit.push(cur[i]);
690 }
691 }
692 else if (it->second.isNull())
693 {
694 Node ret = cur;
695 bool childChanged = false;
696 std::vector<Node> children;
697 if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
698 {
699 children.push_back(cur.getOperator());
700 }
701 for (unsigned i = 0; i < cur.getNumChildren(); i++)
702 {
703 it = visited.find(cur[i]);
704 Assert(it != visited.end());
705 Assert(!it->second.isNull());
706 childChanged = childChanged || cur[i] != it->second;
707 children.push_back(it->second);
708 }
709 if (childChanged)
710 {
711 ret = NodeManager::currentNM()->mkNode(cur.getKind(), children);
712 }
713 // is it the function to synthesize?
714 if (cur.getKind() == APPLY_UF && cur.getOperator() == f)
715 {
716 // if so, flatten
717 Node k = NodeManager::currentNM()->mkBoundVar("vf", cur.getType());
718 defs[k] = ret;
719 ret = k;
720 synth_fv.insert(k);
721 }
722 // post-rewrite
723 visited[cur] = ret;
724 }
725 } while (!visit.empty());
726 Assert(visited.find(n) != visited.end());
727 Assert(!visited.find(n)->second.isNull());
728 return visited[n];
729 }
730
getFreeVariables(Node n,std::unordered_set<Node,NodeHashFunction> & synth_fv,std::unordered_map<Node,std::unordered_set<Node,NodeHashFunction>,NodeHashFunction> & free_vars)731 void SynthConjectureProcess::getFreeVariables(
732 Node n,
733 std::unordered_set<Node, NodeHashFunction>& synth_fv,
734 std::unordered_map<Node,
735 std::unordered_set<Node, NodeHashFunction>,
736 NodeHashFunction>& free_vars)
737 {
738 // first must compute free variables in each subterm of n,
739 // as well as contains_synth_fun
740 std::unordered_map<Node, bool, NodeHashFunction> visited;
741 std::unordered_map<Node, bool, NodeHashFunction>::iterator it;
742 std::stack<Node> visit;
743 Node cur;
744 visit.push(n);
745 do
746 {
747 cur = visit.top();
748 visit.pop();
749 it = visited.find(cur);
750
751 if (it == visited.end())
752 {
753 visited[cur] = false;
754 visit.push(cur);
755 for (unsigned i = 0; i < cur.getNumChildren(); i++)
756 {
757 visit.push(cur[i]);
758 }
759 }
760 else if (!it->second)
761 {
762 free_vars[cur].clear();
763 if (synth_fv.find(cur) != synth_fv.end())
764 {
765 // it is a free variable
766 free_vars[cur].insert(cur);
767 }
768 else
769 {
770 // otherwise, carry the free variables from the children
771 for (unsigned i = 0; i < cur.getNumChildren(); i++)
772 {
773 free_vars[cur].insert(free_vars[cur[i]].begin(),
774 free_vars[cur[i]].end());
775 }
776 }
777 visited[cur] = true;
778 }
779 } while (!visit.empty());
780 }
781
getSymmetryBreakingPredicate(Node x,Node e,TypeNode tn,unsigned tindex,unsigned depth)782 Node SynthConjectureProcess::getSymmetryBreakingPredicate(
783 Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth)
784 {
785 return Node::null();
786 }
787
debugPrint(const char * c)788 void SynthConjectureProcess::debugPrint(const char* c) {}
getComponentVector(Kind k,Node n,std::vector<Node> & args)789 void SynthConjectureProcess::getComponentVector(Kind k,
790 Node n,
791 std::vector<Node>& args)
792 {
793 if (n.getKind() == k)
794 {
795 for (unsigned i = 0; i < n.getNumChildren(); i++)
796 {
797 args.push_back(n[i]);
798 }
799 }
800 else
801 {
802 args.push_back(n);
803 }
804 }
805
806 } /* namespace CVC4::theory::quantifiers */
807 } /* namespace CVC4::theory */
808 } /* namespace CVC4 */
809