GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/sygus_process_conj.cpp Lines: 353 389 90.7 %
Date: 2021-03-22 Branches: 622 1414 44.0 %

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