GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/sygus_enumerator.cpp Lines: 579 659 87.9 %
Date: 2021-03-23 Branches: 928 2300 40.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_enumerator.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner
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 sygus_enumerator
13
 **/
14
15
#include "theory/quantifiers/sygus/sygus_enumerator.h"
16
17
#include "expr/dtype_cons.h"
18
#include "expr/node_algorithm.h"
19
#include "options/datatypes_options.h"
20
#include "options/quantifiers_options.h"
21
#include "smt/logic_exception.h"
22
#include "theory/datatypes/theory_datatypes_utils.h"
23
#include "theory/quantifiers/sygus/synth_engine.h"
24
#include "theory/quantifiers/sygus/type_node_id_trie.h"
25
#include "theory/rewriter.h"
26
27
using namespace CVC4::kind;
28
29
namespace CVC4 {
30
namespace theory {
31
namespace quantifiers {
32
33
193
SygusEnumerator::SygusEnumerator(TermDbSygus* tds,
34
                                 SynthConjecture* p,
35
                                 SygusStatistics& s,
36
193
                                 bool enumShapes)
37
    : d_tds(tds),
38
      d_parent(p),
39
      d_stats(s),
40
      d_enumShapes(enumShapes),
41
      d_tlEnum(nullptr),
42
193
      d_abortSize(-1)
43
{
44
193
}
45
46
193
void SygusEnumerator::initialize(Node e)
47
{
48
193
  Trace("sygus-enum") << "SygusEnumerator::initialize " << e << std::endl;
49
193
  d_enum = e;
50
193
  d_etype = d_enum.getType();
51
193
  Assert(d_etype.isDatatype());
52
193
  Assert(d_etype.getDType().isSygus());
53
193
  d_tlEnum = getMasterEnumForType(d_etype);
54
193
  d_abortSize = options::sygusAbortSize();
55
56
  // Get the statically registered symmetry breaking clauses for e, see if they
57
  // can be used for speeding up the enumeration.
58
193
  NodeManager* nm = NodeManager::currentNM();
59
386
  std::vector<Node> sbl;
60
193
  d_tds->getSymBreakLemmas(e, sbl);
61
386
  Node ag = d_tds->getActiveGuardForEnumerator(e);
62
386
  Node truen = nm->mkConst(true);
63
  // use TNode for substitute below
64
386
  TNode agt = ag;
65
386
  TNode truent = truen;
66
193
  Assert(d_tcache.find(d_etype) != d_tcache.end());
67
193
  const DType& dt = d_etype.getDType();
68
303
  for (const Node& lem : sbl)
69
  {
70
110
    if (!d_tds->isSymBreakLemmaTemplate(lem))
71
    {
72
      // substitute its active guard by true and rewrite
73
126
      Node slem = lem.substitute(agt, truent);
74
63
      slem = Rewriter::rewrite(slem);
75
      // break into conjuncts
76
126
      std::vector<Node> sblc;
77
63
      if (slem.getKind() == AND)
78
      {
79
18
        for (const Node& slemc : slem)
80
        {
81
12
          sblc.push_back(slemc);
82
        }
83
      }
84
      else
85
      {
86
57
        sblc.push_back(slem);
87
      }
88
132
      for (const Node& sblemma : sblc)
89
      {
90
138
        Trace("sygus-enum")
91
69
            << "  symmetry breaking lemma : " << sblemma << std::endl;
92
        // if its a negation of a unit top-level tester, then this specifies
93
        // that we should not enumerate terms whose top symbol is that
94
        // constructor
95
69
        if (sblemma.getKind() == NOT)
96
        {
97
130
          Node a;
98
65
          int tst = datatypes::utils::isTester(sblemma[0], a);
99
65
          if (tst >= 0)
100
          {
101
65
            if (a == e)
102
            {
103
130
              Node cons = dt[tst].getConstructor();
104
130
              Trace("sygus-enum") << "  ...unit exclude constructor #" << tst
105
65
                                  << ", constructor " << cons << std::endl;
106
65
              d_sbExcTlCons.insert(cons);
107
            }
108
          }
109
        }
110
        // other symmetry breaking lemmas such as disjunctions are not used
111
      }
112
    }
113
  }
114
193
}
115
116
193
void SygusEnumerator::addValue(Node v)
117
{
118
  // do nothing
119
193
}
120
121
48772
bool SygusEnumerator::increment() { return d_tlEnum->increment(); }
122
48959
Node SygusEnumerator::getCurrent()
123
{
124
48959
  if (d_abortSize >= 0)
125
  {
126
6875
    int cs = static_cast<int>(d_tlEnum->getCurrentSize());
127
6875
    if (cs > d_abortSize)
128
    {
129
24
      std::stringstream ss;
130
12
      ss << "Maximum term size (" << options::sygusAbortSize()
131
12
         << ") for enumerative SyGuS exceeded.";
132
12
      throw LogicException(ss.str());
133
    }
134
  }
135
48947
  Node ret = d_tlEnum->getCurrent();
136
48947
  if (!ret.isNull() && !d_sbExcTlCons.empty())
137
  {
138
708
    Assert(ret.hasOperator());
139
    // might be excluded by an externally provided symmetry breaking clause
140
708
    if (d_sbExcTlCons.find(ret.getOperator()) != d_sbExcTlCons.end())
141
    {
142
76
      Trace("sygus-enum-exc")
143
38
          << "Exclude (external) : " << d_tds->sygusToBuiltin(ret) << std::endl;
144
38
      ret = Node::null();
145
    }
146
  }
147
48947
  if (Trace.isOn("sygus-enum"))
148
  {
149
    Trace("sygus-enum") << "Enumerate : ";
150
    TermDbSygus::toStreamSygus("sygus-enum", ret);
151
    Trace("sygus-enum") << std::endl;
152
  }
153
48947
  return ret;
154
}
155
156
375
bool SygusEnumerator::isEnumShapes() const { return d_enumShapes; }
157
158
394
SygusEnumerator::TermCache::TermCache()
159
    : d_tds(nullptr),
160
      d_eec(nullptr),
161
      d_isSygusType(false),
162
      d_numConClasses(0),
163
      d_sizeEnum(0),
164
      d_isComplete(false),
165
394
      d_sampleRrVInit(false)
166
{
167
394
}
168
169
394
void SygusEnumerator::TermCache::initialize(SygusStatistics* s,
170
                                            Node e,
171
                                            TypeNode tn,
172
                                            TermDbSygus* tds,
173
                                            ExampleEvalCache* eec)
174
{
175
394
  Trace("sygus-enum-debug") << "Init term cache " << tn << "..." << std::endl;
176
394
  d_stats = s;
177
394
  d_enum = e;
178
394
  d_tn = tn;
179
394
  d_tds = tds;
180
394
  d_eec = eec;
181
394
  d_sizeStartIndex[0] = 0;
182
394
  d_isSygusType = false;
183
184
  // compute static information about tn
185
394
  if (!d_tn.isDatatype())
186
  {
187
    // not a datatype, finish
188
38
    return;
189
  }
190
375
  const DType& dt = tn.getDType();
191
375
  if (!dt.isSygus())
192
  {
193
    // not a sygus datatype, finish
194
    return;
195
  }
196
197
375
  d_isSygusType = true;
198
199
  // get argument types for all constructors
200
750
  std::map<unsigned, std::vector<TypeNode>> argTypes;
201
  // map weights to constructors
202
750
  std::map<unsigned, std::vector<unsigned>> weightsToIndices;
203
204
  // constructor class 0 is reserved for nullary operators with 0 weight
205
  // this is an optimization so that we always skip them for sizes >= 1
206
375
  ConstructorClass& ccZero = d_cclass[0];
207
375
  ccZero.d_weight = 0;
208
375
  d_numConClasses = 1;
209
  // we must indicate that we should process zero weight constructor classes
210
375
  weightsToIndices[0].clear();
211
2271
  for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
212
  {
213
    // record weight information
214
1896
    unsigned w = dt[i].getWeight();
215
3792
    Trace("sygus-enum-debug") << "Weight " << dt[i].getSygusOp() << ": " << w
216
1896
                              << std::endl;
217
1896
    weightsToIndices[w].push_back(i);
218
    // record type information
219
3905
    for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
220
    {
221
4018
      TypeNode type = dt[i].getArgType(j);
222
2009
      argTypes[i].push_back(type);
223
    }
224
  }
225
375
  NodeManager* nm = NodeManager::currentNM();
226
1047
  for (std::pair<const unsigned, std::vector<unsigned>>& wp : weightsToIndices)
227
  {
228
672
    unsigned w = wp.first;
229
230
    // assign constructors to constructor classes
231
1344
    TypeNodeIdTrie tnit;
232
1344
    std::map<Node, unsigned> nToC;
233
2568
    for (unsigned i : wp.second)
234
    {
235
1896
      if (argTypes[i].empty() && w == 0)
236
      {
237
760
        ccZero.d_cons.push_back(i);
238
      }
239
      else
240
      {
241
        // we merge those whose argument types are the same
242
        // We could, but choose not to, order these types, which would lead to
243
        // more aggressive merging of constructor classes. On the negative side,
244
        // this adds another level of indirection to remember which argument
245
        // positions the argument types occur in, for each constructor.
246
2272
        Node n = nm->mkConst(Rational(i));
247
1136
        nToC[n] = i;
248
1136
        tnit.add(n, argTypes[i]);
249
      }
250
    }
251
1344
    std::map<Node, unsigned> assign;
252
672
    tnit.assignIds(assign, d_numConClasses);
253
1808
    for (std::pair<const Node, unsigned>& cp : assign)
254
    {
255
      // determine which constructor class this goes into using tnit
256
1136
      unsigned cclassi = cp.second;
257
1136
      unsigned i = nToC[cp.first];
258
2272
      Trace("sygus-enum-debug") << "Constructor class for "
259
2272
                                << dt[i].getSygusOp() << " is " << cclassi
260
1136
                                << std::endl;
261
      // initialize the constructor class
262
1136
      if (d_cclass.find(cclassi) == d_cclass.end())
263
      {
264
637
        d_cclass[cclassi].d_weight = w;
265
2548
        d_cclass[cclassi].d_types.insert(d_cclass[cclassi].d_types.end(),
266
637
                                         argTypes[i].begin(),
267
2548
                                         argTypes[i].end());
268
      }
269
      // add to constructor class
270
1136
      d_cclass[cclassi].d_cons.push_back(i);
271
    }
272
1344
    Trace("sygus-enum-debug") << "#cons classes for weight <= " << w << " : "
273
672
                              << d_numConClasses << std::endl;
274
672
    d_weightToCcIndex[w] = d_numConClasses;
275
  }
276
375
  Trace("sygus-enum-debug") << "...finish" << std::endl;
277
}
278
279
64599
unsigned SygusEnumerator::TermCache::getLastConstructorClassIndexForWeight(
280
    unsigned w) const
281
{
282
64599
  std::map<unsigned, unsigned>::const_iterator it = d_weightToCcIndex.find(w);
283
64599
  if (it == d_weightToCcIndex.end())
284
  {
285
53566
    return d_numConClasses;
286
  }
287
11033
  return it->second;
288
}
289
116
unsigned SygusEnumerator::TermCache::getNumConstructorClasses() const
290
{
291
116
  return d_numConClasses;
292
}
293
1247
void SygusEnumerator::TermCache::getConstructorClass(
294
    unsigned i, std::vector<unsigned>& cclass) const
295
{
296
1247
  std::map<unsigned, ConstructorClass>::const_iterator it = d_cclass.find(i);
297
1247
  Assert(it != d_cclass.end());
298
1247
  cclass.insert(
299
2494
      cclass.end(), it->second.d_cons.begin(), it->second.d_cons.end());
300
1247
}
301
1194
void SygusEnumerator::TermCache::getTypesForConstructorClass(
302
    unsigned i, std::vector<TypeNode>& types) const
303
{
304
1194
  std::map<unsigned, ConstructorClass>::const_iterator it = d_cclass.find(i);
305
1194
  Assert(it != d_cclass.end());
306
1194
  types.insert(
307
2388
      types.end(), it->second.d_types.begin(), it->second.d_types.end());
308
1194
}
309
310
1194
unsigned SygusEnumerator::TermCache::getWeightForConstructorClass(
311
    unsigned i) const
312
{
313
1194
  std::map<unsigned, ConstructorClass>::const_iterator it = d_cclass.find(i);
314
1194
  Assert(it != d_cclass.end());
315
1194
  return it->second.d_weight;
316
}
317
318
63300
bool SygusEnumerator::TermCache::addTerm(Node n)
319
{
320
63300
  if (!d_isSygusType)
321
  {
322
    // non-sygus terms generated by TermEnumMasterInterp/TermEnumMasterFv
323
    // enumeration are unique by construction
324
146
    Trace("sygus-enum-terms") << "tc(" << d_tn << "): term (builtin): " << n
325
73
                              << std::endl;
326
73
    d_terms.push_back(n);
327
73
    return true;
328
  }
329
63227
  Assert(!n.isNull());
330
63227
  if (options::sygusSymBreakDynamic())
331
  {
332
87379
    Node bn = d_tds->sygusToBuiltin(n);
333
87379
    Node bnr = d_tds->getExtRewriter()->extendedRewrite(bn);
334
63227
    ++(d_stats->d_enumTermsRewrite);
335
63227
    if (options::sygusRewVerify())
336
    {
337
1626
      if (bn != bnr)
338
      {
339
1064
        if (!d_sampleRrVInit)
340
        {
341
8
          d_sampleRrVInit = true;
342
16
          d_samplerRrV.initializeSygus(
343
8
              d_tds, d_enum, options::sygusSamples(), false);
344
        }
345
1064
        d_samplerRrV.checkEquivalent(bn, bnr);
346
      }
347
    }
348
    // must be unique up to rewriting
349
63227
    if (d_bterms.find(bnr) != d_bterms.end())
350
    {
351
24773
      Trace("sygus-enum-exc") << "Exclude: " << bn << std::endl;
352
24773
      return false;
353
    }
354
    // insert to builtin term cache, regardless of whether it is redundant
355
    // based on examples.
356
38454
    d_bterms.insert(bnr);
357
    // if we are doing PBE symmetry breaking
358
38454
    if (d_eec != nullptr)
359
    {
360
24009
      ++(d_stats->d_enumTermsExampleEval);
361
      // Is it equivalent under examples?
362
33716
      Node bne = d_eec->addSearchVal(d_tn, bnr);
363
24009
      if (!bne.isNull())
364
      {
365
24009
        if (bnr != bne)
366
        {
367
28604
          Trace("sygus-enum-exc")
368
14302
              << "Exclude (by examples): " << bn << ", since we already have "
369
14302
              << bne << std::endl;
370
14302
          return false;
371
        }
372
      }
373
    }
374
24152
    Trace("sygus-enum-terms") << "tc(" << d_tn << "): term " << bn << std::endl;
375
  }
376
24152
  ++(d_stats->d_enumTerms);
377
24152
  d_terms.push_back(n);
378
24152
  return true;
379
}
380
598
void SygusEnumerator::TermCache::pushEnumSizeIndex()
381
{
382
598
  d_sizeEnum++;
383
598
  d_sizeStartIndex[d_sizeEnum] = d_terms.size();
384
1196
  Trace("sygus-enum-debug") << "tc(" << d_tn << "): size " << d_sizeEnum
385
1196
                            << " terms start at index " << d_terms.size()
386
598
                            << std::endl;
387
598
}
388
42820
unsigned SygusEnumerator::TermCache::getEnumSize() const { return d_sizeEnum; }
389
34683
unsigned SygusEnumerator::TermCache::getIndexForSize(unsigned s) const
390
{
391
34683
  Assert(s <= d_sizeEnum);
392
34683
  std::map<unsigned, unsigned>::const_iterator it = d_sizeStartIndex.find(s);
393
34683
  Assert(it != d_sizeStartIndex.end());
394
34683
  return it->second;
395
}
396
238760
Node SygusEnumerator::TermCache::getTerm(unsigned index) const
397
{
398
238760
  Assert(index < d_terms.size());
399
238760
  return d_terms[index];
400
}
401
402
65957
unsigned SygusEnumerator::TermCache::getNumTerms() const
403
{
404
65957
  return d_terms.size();
405
}
406
407
64843
bool SygusEnumerator::TermCache::isComplete() const { return d_isComplete; }
408
57
void SygusEnumerator::TermCache::setComplete() { d_isComplete = true; }
409
237894
unsigned SygusEnumerator::TermEnum::getCurrentSize() { return d_currSize; }
410
4240
SygusEnumerator::TermEnum::TermEnum() : d_se(nullptr), d_currSize(0) {}
411
3846
SygusEnumerator::TermEnumSlave::TermEnumSlave()
412
    : TermEnum(),
413
      d_sizeLim(0),
414
      d_index(0),
415
      d_indexNextEnd(0),
416
      d_hasIndexNextEnd(false),
417
3846
      d_master(nullptr)
418
{
419
3846
}
420
421
3846
bool SygusEnumerator::TermEnumSlave::initialize(SygusEnumerator* se,
422
                                                TypeNode tn,
423
                                                unsigned sizeMin,
424
                                                unsigned sizeMax)
425
{
426
3846
  d_se = se;
427
3846
  d_tn = tn;
428
3846
  d_sizeLim = sizeMax;
429
7692
  Trace("sygus-enum-debug2") << "slave(" << d_tn
430
3846
                             << "): init, min/max=" << sizeMin << "/" << sizeMax
431
3846
                             << "...\n";
432
433
  // must have pointer to the master
434
3846
  d_master = d_se->getMasterEnumForType(d_tn);
435
436
3846
  SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn];
437
  // if the size is exact, we start at the limit
438
3846
  d_currSize = sizeMin;
439
  // initialize the index
440
3854
  while (d_currSize > tc.getEnumSize())
441
  {
442
146
    Trace("sygus-enum-debug2") << "slave(" << d_tn
443
73
                               << "): init force increment master...\n";
444
    // increment the master until we have enough terms
445
73
    if (!d_master->increment())
446
    {
447
138
      Trace("sygus-enum-debug2") << "slave(" << d_tn
448
69
                                 << "): ...fail init force master\n";
449
69
      return false;
450
    }
451
8
    Trace("sygus-enum-debug2") << "slave(" << d_tn
452
4
                               << "): ...success init force master\n";
453
  }
454
3777
  d_index = tc.getIndexForSize(d_currSize);
455
3777
  Trace("sygus-enum-debug2") << "slave(" << d_tn << "): validate indices...\n";
456
  // initialize the next end index (marks where size increments)
457
3777
  validateIndexNextEnd();
458
7554
  Trace("sygus-enum-debug2")
459
3777
      << "slave(" << d_tn << "): validate init end: " << d_hasIndexNextEnd
460
3777
      << " " << d_indexNextEnd << " " << d_index << " " << d_currSize << "\n";
461
  // ensure that indexNextEnd is valid (it must be greater than d_index)
462
3777
  bool ret = validateIndex();
463
7554
  Trace("sygus-enum-debug2")
464
7554
      << "slave(" << d_tn << "): ..." << (ret ? "success" : "fail")
465
3777
      << " init, now: " << d_hasIndexNextEnd << " " << d_indexNextEnd << " "
466
3777
      << d_index << " " << d_currSize << "\n";
467
3777
  return ret;
468
}
469
470
119380
Node SygusEnumerator::TermEnumSlave::getCurrent()
471
{
472
119380
  SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn];
473
238760
  Node curr = tc.getTerm(d_index);
474
238760
  Trace("sygus-enum-debug2")
475
119380
      << "slave(" << d_tn
476
238760
      << "): current : " << d_se->d_tds->sygusToBuiltin(curr)
477
238760
      << ", sizes = " << d_se->d_tds->getSygusTermSize(curr) << " "
478
119380
      << getCurrentSize() << std::endl;
479
238760
  Trace("sygus-enum-debug2") << "slave(" << d_tn
480
119380
                             << "): indices : " << d_hasIndexNextEnd << " "
481
119380
                             << d_indexNextEnd << " " << d_index << std::endl;
482
  // lookup in the cache
483
238760
  return tc.getTerm(d_index);
484
}
485
486
31848
bool SygusEnumerator::TermEnumSlave::increment()
487
{
488
  // increment index
489
31848
  d_index++;
490
  // ensure that index is valid
491
31848
  return validateIndex();
492
}
493
494
35625
bool SygusEnumerator::TermEnumSlave::validateIndex()
495
{
496
35625
  Trace("sygus-enum-debug2") << "slave(" << d_tn << ") : validate index...\n";
497
35625
  SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn];
498
  // ensure that index is in the range
499
65069
  while (d_index >= tc.getNumTerms())
500
  {
501
15553
    Assert(d_index == tc.getNumTerms());
502
15553
    Trace("sygus-enum-debug2") << "slave(" << d_tn << ") : force master...\n";
503
    // if the size of the master is larger than the size limit, then
504
    // there is no use continuing, since there are no more terms that this
505
    // slave enumerator can return.
506
15553
    if (d_master->getCurrentSize() > d_sizeLim)
507
    {
508
655
      return false;
509
    }
510
    // must push the master index
511
14898
    if (!d_master->increment())
512
    {
513
352
      Trace("sygus-enum-debug2") << "slave(" << d_tn
514
176
                                 << ") : ...fail force master\n";
515
176
      return false;
516
    }
517
29444
    Trace("sygus-enum-debug2") << "slave(" << d_tn
518
14722
                               << ") : ...success force master\n";
519
  }
520
  // always validate the next index end here
521
34794
  validateIndexNextEnd();
522
69588
  Trace("sygus-enum-debug2") << "slave(" << d_tn
523
34794
                             << ") : validate index end...\n";
524
  // if we are at the beginning of the next size, increment current size
525
35540
  while (d_hasIndexNextEnd && d_index == d_indexNextEnd)
526
  {
527
2888
    d_currSize++;
528
5776
    Trace("sygus-enum-debug2") << "slave(" << d_tn << ") : size++ ("
529
2888
                               << d_currSize << "/" << d_sizeLim << ")\n";
530
    // if we've hit the size limit, return false
531
2888
    if (d_currSize > d_sizeLim)
532
    {
533
2515
      Trace("sygus-enum-debug2") << "slave(" << d_tn << ") : fail size\n";
534
2515
      return false;
535
    }
536
373
    validateIndexNextEnd();
537
  }
538
32279
  Trace("sygus-enum-debug2") << "slave(" << d_tn << ") : finished\n";
539
32279
  return true;
540
}
541
542
38944
void SygusEnumerator::TermEnumSlave::validateIndexNextEnd()
543
{
544
38944
  SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn];
545
  // update the next end index
546
38944
  d_hasIndexNextEnd = d_currSize < tc.getEnumSize();
547
38944
  if (d_hasIndexNextEnd)
548
  {
549
30906
    d_indexNextEnd = tc.getIndexForSize(d_currSize + 1);
550
  }
551
38944
}
552
553
394
void SygusEnumerator::initializeTermCache(TypeNode tn)
554
{
555
  // initialize the term cache
556
  // see if we use an example evaluation cache for symmetry breaking
557
394
  ExampleEvalCache* eec = nullptr;
558
394
  if (d_parent != nullptr && options::sygusSymBreakPbe())
559
  {
560
394
    eec = d_parent->getExampleEvalCache(d_enum);
561
  }
562
394
  d_tcache[tn].initialize(&d_stats, d_enum, tn, d_tds, eec);
563
394
}
564
565
4039
SygusEnumerator::TermEnum* SygusEnumerator::getMasterEnumForType(TypeNode tn)
566
{
567
4039
  if (tn.isDatatype() && tn.getDType().isSygus())
568
  {
569
4010
    std::map<TypeNode, TermEnumMaster>::iterator it = d_masterEnum.find(tn);
570
4010
    if (it != d_masterEnum.end())
571
    {
572
3635
      return &it->second;
573
    }
574
375
    initializeTermCache(tn);
575
    // initialize the master enumerator
576
375
    bool ret = d_masterEnum[tn].initialize(this, tn);
577
375
    AlwaysAssert(ret);
578
375
    return &d_masterEnum[tn];
579
  }
580
29
  if (options::sygusRepairConst())
581
  {
582
8
    std::map<TypeNode, TermEnumMasterFv>::iterator it = d_masterEnumFv.find(tn);
583
8
    if (it != d_masterEnumFv.end())
584
    {
585
      return &it->second;
586
    }
587
8
    initializeTermCache(tn);
588
    // initialize the master enumerator
589
8
    bool ret = d_masterEnumFv[tn].initialize(this, tn);
590
8
    AlwaysAssert(ret);
591
8
    return &d_masterEnumFv[tn];
592
  }
593
  std::map<TypeNode, std::unique_ptr<TermEnumMasterInterp>>::iterator it =
594
21
      d_masterEnumInt.find(tn);
595
21
  if (it != d_masterEnumInt.end())
596
  {
597
10
    return it->second.get();
598
  }
599
11
  initializeTermCache(tn);
600
  // create the master enumerator
601
11
  d_masterEnumInt[tn].reset(new TermEnumMasterInterp(tn));
602
  // initialize the master enumerator
603
11
  TermEnumMasterInterp* temi = d_masterEnumInt[tn].get();
604
11
  bool ret = temi->initialize(this, tn);
605
11
  AlwaysAssert(ret);
606
11
  return temi;
607
}
608
609
375
SygusEnumerator::TermEnumMaster::TermEnumMaster()
610
    : TermEnum(),
611
      d_enumShapes(false),
612
      d_enumShapesInit(false),
613
      d_isIncrementing(false),
614
      d_currTermSet(false),
615
      d_consClassNum(0),
616
      d_ccWeight(0),
617
      d_consNum(0),
618
      d_currChildSize(0),
619
375
      d_childrenValid(0)
620
{
621
375
}
622
623
375
bool SygusEnumerator::TermEnumMaster::initialize(SygusEnumerator* se,
624
                                                 TypeNode tn)
625
{
626
375
  Trace("sygus-enum-debug") << "master(" << tn << "): init...\n";
627
375
  d_tds = se->d_tds;
628
375
  d_se = se;
629
375
  d_tn = tn;
630
631
375
  d_currSize = 0;
632
  // we will start with constructor class zero
633
375
  d_consClassNum = 0;
634
375
  d_currChildSize = 0;
635
375
  d_ccCons.clear();
636
375
  d_enumShapes = se->isEnumShapes();
637
375
  d_enumShapesInit = false;
638
375
  d_isIncrementing = false;
639
375
  d_currTermSet = false;
640
375
  bool ret = increment();
641
750
  Trace("sygus-enum-debug") << "master(" << tn
642
375
                            << "): finish init, ret = " << ret << "\n";
643
375
  return ret;
644
}
645
646
112174
Node SygusEnumerator::TermEnumMaster::getCurrent()
647
{
648
112174
  if (d_currTermSet)
649
  {
650
48947
    return d_currTerm;
651
  }
652
63227
  d_currTermSet = true;
653
  // construct based on the children
654
126454
  std::vector<Node> children;
655
63227
  const DType& dt = d_tn.getDType();
656
63227
  Assert(d_consNum > 0 && d_consNum <= d_ccCons.size());
657
  // get the current constructor number
658
63227
  unsigned cnum = d_ccCons[d_consNum - 1];
659
63227
  children.push_back(dt[cnum].getConstructor());
660
  // add the current of each child to children
661
182607
  for (unsigned i = 0, nargs = dt[cnum].getNumArgs(); i < nargs; i++)
662
  {
663
119380
    Assert(d_children.find(i) != d_children.end());
664
238760
    Node cc = d_children[i].getCurrent();
665
119380
    if (cc.isNull())
666
    {
667
      d_currTerm = cc;
668
      return cc;
669
    }
670
119380
    children.push_back(cc);
671
  }
672
63227
  if (d_enumShapes)
673
  {
674
    // ensure all variables are unique
675
    childrenToShape(children);
676
  }
677
63227
  d_currTerm = NodeManager::currentNM()->mkNode(APPLY_CONSTRUCTOR, children);
678
63227
  return d_currTerm;
679
}
680
681
64051
bool SygusEnumerator::TermEnumMaster::increment()
682
{
683
  // Am I already incrementing? If so, fail.
684
  // This is to break infinite loops for slave enumerators who request an
685
  // increment() from the master enumerator of their type that is also their
686
  // parent. This ensures we do not loop on a grammar like:
687
  //   A -> -( A ) | B+B
688
  //   B -> x | y
689
  // where we require the first term enumerated to be over B+B.
690
  // Set that we are incrementing
691
64051
  if (d_isIncrementing)
692
  {
693
    return false;
694
  }
695
128102
  Trace("sygus-enum-summary") << "SygusEnumerator::TermEnumMaster: increment "
696
64051
                              << d_tn << "..." << std::endl;
697
64051
  d_isIncrementing = true;
698
64051
  bool ret = incrementInternal();
699
64051
  d_isIncrementing = false;
700
128102
  Trace("sygus-enum-summary")
701
64051
      << "SygusEnumerator::TermEnumMaster: finished increment " << d_tn
702
64051
      << std::endl;
703
64051
  return ret;
704
}
705
706
64789
bool SygusEnumerator::TermEnumMaster::incrementInternal()
707
{
708
64789
  SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn];
709
64789
  if (tc.isComplete())
710
  {
711
190
    return false;
712
  }
713
129198
  Trace("sygus-enum-debug2") << "master(" << d_tn
714
64599
                             << "): get last constructor class..." << std::endl;
715
  // the maximum index of a constructor class to consider
716
64599
  unsigned ncc = tc.getLastConstructorClassIndexForWeight(d_currSize);
717
129198
  Trace("sygus-enum-debug2") << "Last constructor class " << d_currSize << ": "
718
64599
                             << ncc << std::endl;
719
  // If we are enumerating shapes, the first enumerated term is a free variable.
720
64599
  if (d_enumShapes && !d_enumShapesInit)
721
  {
722
    Node fv = d_tds->getFreeVar(d_tn, 0);
723
    d_enumShapesInit = true;
724
    d_currTermSet = true;
725
    d_currTerm = fv;
726
    // must add to term cache
727
    tc.addTerm(fv);
728
    return true;
729
  }
730
731
  // have we initialized the current constructor class?
732
67093
  while (d_ccCons.empty() && d_consClassNum < ncc)
733
  {
734
1247
    Assert(d_ccTypes.empty());
735
2494
    Trace("sygus-enum-debug2") << "master(" << d_tn
736
1247
                               << "): try constructor class " << d_consClassNum
737
1247
                               << std::endl;
738
    // get the list of constructors in the constructor class
739
1247
    tc.getConstructorClass(d_consClassNum, d_ccCons);
740
    // if there are any...
741
1247
    if (!d_ccCons.empty())
742
    {
743
      // successfully initialized the constructor class
744
1150
      d_consNum = 0;
745
      // we will populate the children
746
1150
      Assert(d_children.empty());
747
1150
      Assert(d_ccTypes.empty());
748
1150
      tc.getTypesForConstructorClass(d_consClassNum, d_ccTypes);
749
1150
      d_ccWeight = tc.getWeightForConstructorClass(d_consClassNum);
750
1150
      d_childrenValid = 0;
751
      // initialize the children into their initial state
752
1150
      if (!initializeChildren())
753
      {
754
        // didn't work (due to size), we will try the next class
755
183
        d_ccCons.clear();
756
183
        d_ccTypes.clear();
757
366
        Trace("sygus-enum-debug2") << "master(" << d_tn
758
183
                                   << "): failed due to init size\n";
759
      }
760
    }
761
    else
762
    {
763
      // No constructors in constructor class. This can happen for class 0 if a
764
      // type has no nullary constructors with weight 0.
765
194
      Trace("sygus-enum-debug2") << "master(" << d_tn
766
97
                                 << "): failed due to no cons\n";
767
    }
768
    // increment the next constructor class we will try
769
1247
    d_consClassNum++;
770
  }
771
772
  // have we run out of constructor classes for this size?
773
64599
  if (d_ccCons.empty())
774
  {
775
    // check whether we should terminate
776
634
    if (d_tn.isInterpretedFinite())
777
    {
778
116
      if (ncc == tc.getNumConstructorClasses())
779
      {
780
85
        bool doTerminate = true;
781
101
        for (unsigned i = 1; i < ncc; i++)
782
        {
783
          // The maximum size of terms from a constructor class can be
784
          // determined if all of its argument types are finished enumerating.
785
          // If this maximum size is less than or equal to d_currSize for
786
          // each constructor class, we are done.
787
44
          unsigned sum = tc.getWeightForConstructorClass(i);
788
60
          std::vector<TypeNode> cctns;
789
44
          tc.getTypesForConstructorClass(i, cctns);
790
70
          for (unsigned j = 0, ntypes = cctns.size(); j < ntypes; j++)
791
          {
792
80
            TypeNode tnc = cctns[j];
793
54
            SygusEnumerator::TermCache& tcc = d_se->d_tcache[tnc];
794
54
            if (!tcc.isComplete())
795
            {
796
              // maximum size of this constructor class cannot be determined
797
28
              doTerminate = false;
798
28
              break;
799
            }
800
            else
801
            {
802
26
              sum += tcc.getEnumSize();
803
26
              if (sum > d_currSize)
804
              {
805
                // maximum size of this constructor class is greater than size
806
                doTerminate = false;
807
                break;
808
              }
809
            }
810
          }
811
44
          if (!doTerminate)
812
          {
813
28
            break;
814
          }
815
        }
816
85
        if (doTerminate)
817
        {
818
114
          Trace("sygus-engine") << "master(" << d_tn << "): complete at size "
819
57
                                << d_currSize << std::endl;
820
57
          tc.setComplete();
821
57
          return false;
822
        }
823
      }
824
    }
825
826
    // increment the size bound
827
577
    d_currSize++;
828
1154
    Trace("sygus-enum-debug2") << "master(" << d_tn
829
577
                               << "): size++ : " << d_currSize << "\n";
830
577
    if (Trace.isOn("sygus-engine"))
831
    {
832
      // am i the master enumerator? if so, print
833
      if (d_se->d_tlEnum == this)
834
      {
835
        Trace("sygus-engine") << "SygusEnumerator::size = " << d_currSize
836
                              << std::endl;
837
      }
838
    }
839
840
    // push the bound
841
577
    tc.pushEnumSizeIndex();
842
843
    // restart with constructor class one (skip nullary constructors)
844
577
    d_consClassNum = 1;
845
846
    // We break for a round: return the null term when we cross a size
847
    // boundary. This ensures that the necessary breaks are taken, e.g.
848
    // in slave enumerators who may instead want to abandon this call to
849
    // increment master when the size of the master makes their increment
850
    // infeasible.
851
577
    d_currTermSet = true;
852
577
    d_currTerm = Node::null();
853
577
    return true;
854
  }
855
856
63965
  bool incSuccess = false;
857
29409
  do
858
  {
859
185272
    Trace("sygus-enum-debug2") << "master(" << d_tn << "): check return "
860
185272
                               << d_childrenValid << "/" << d_ccTypes.size()
861
92636
                               << std::endl;
862
    // the children should be initialized by here
863
92636
    Assert(d_childrenValid == d_ccTypes.size());
864
865
    // do we have more constructors for the given children?
866
92636
    if (d_consNum < d_ccCons.size())
867
    {
868
126454
      Trace("sygus-enum-debug2") << "master(" << d_tn << "): try constructor "
869
63227
                                 << d_consNum << std::endl;
870
      // increment constructor index
871
      // we will build for the current constructor and the given children
872
63227
      d_consNum++;
873
63227
      d_currTermSet = false;
874
63227
      d_currTerm = Node::null();
875
126454
      Node c = getCurrent();
876
63227
      if (!c.isNull())
877
      {
878
63227
        if (!tc.addTerm(c))
879
        {
880
          // the term was not unique based on rewriting
881
78150
          Trace("sygus-enum-debug2") << "master(" << d_tn
882
39075
                                     << "): failed addTerm\n";
883
          // we will return null (d_currTermSet is true at this point)
884
39075
          Assert(d_currTermSet);
885
39075
          d_currTerm = Node::null();
886
        }
887
      }
888
63227
      return true;
889
    }
890
891
    // finished constructors for this set of children, must increment children
892
893
    // reset the constructor number
894
29409
    d_consNum = 0;
895
896
    // try incrementing the last child until we find one that works
897
29409
    incSuccess = false;
898
93105
    while (!incSuccess && d_childrenValid > 0)
899
    {
900
63696
      Trace("sygus-enum-debug2") << "master(" << d_tn << "): try incrementing "
901
31848
                                 << d_childrenValid << std::endl;
902
31848
      unsigned i = d_childrenValid - 1;
903
31848
      Assert(d_children[i].getCurrentSize() <= d_currChildSize);
904
      // track the size
905
31848
      d_currChildSize -= d_children[i].getCurrentSize();
906
31848
      if (d_children[i].increment())
907
      {
908
57360
        Trace("sygus-enum-debug2") << "master(" << d_tn
909
28680
                                   << "): increment success...\n";
910
28680
        d_currChildSize += d_children[i].getCurrentSize();
911
        // must see if we can initialize the remaining children here
912
        // if not, there is no use continuing.
913
28680
        if (initializeChildren())
914
        {
915
57342
          Trace("sygus-enum-debug2")
916
28671
              << "master(" << d_tn << "): success init children\n";
917
28671
          Assert(d_currChildSize + d_ccWeight <= d_currSize);
918
28671
          incSuccess = true;
919
        }
920
        else
921
        {
922
          // failed to initialize the remaining children (likely due to a
923
          // child having a non-zero minimum size bound).
924
18
          Trace("sygus-enum-debug2")
925
9
              << "master(" << d_tn << "): fail init children\n";
926
9
          d_currChildSize -= d_children[i].getCurrentSize();
927
        }
928
      }
929
31848
      if (!incSuccess)
930
      {
931
6354
        Trace("sygus-enum-debug2") << "master(" << d_tn
932
3177
                                   << "): fail, backtrack...\n";
933
        // current child is out of values
934
3177
        d_children.erase(i);
935
3177
        d_childrenValid--;
936
      }
937
    }
938
  } while (incSuccess);
939
1476
  Trace("sygus-enum-debug2") << "master(" << d_tn
940
738
                             << "): failed increment children\n";
941
  // restart with the next constructor class
942
738
  d_ccCons.clear();
943
738
  d_ccTypes.clear();
944
738
  return incrementInternal();
945
}
946
947
29830
bool SygusEnumerator::TermEnumMaster::initializeChildren()
948
{
949
59660
  Trace("sygus-enum-debug2")
950
29830
      << "master(" << d_tn << "): init children, start = " << d_childrenValid
951
59660
      << ", #types=" << d_ccTypes.size() << ", sizes=" << d_currChildSize << "/"
952
29830
      << d_currSize << std::endl;
953
29830
  unsigned currChildren = d_childrenValid;
954
29830
  unsigned sizeMin = 0;
955
  // while we need to initialize the current child
956
37232
  while (d_childrenValid < d_ccTypes.size())
957
  {
958
3893
    if (!initializeChild(d_childrenValid, sizeMin))
959
    {
960
294
      if (d_childrenValid == currChildren)
961
      {
962
        // we are back to the child we started with, we terminate now.
963
384
        Trace("sygus-enum-debug2") << "master(" << d_tn
964
192
                                   << "): init children : failed, finished"
965
192
                                   << std::endl;
966
192
        return false;
967
      }
968
204
      Trace("sygus-enum-debug2") << "master(" << d_tn
969
102
                                 << "): init children : failed" << std::endl;
970
      // we failed in this size configuration
971
      // reinitialize with the next size up
972
102
      unsigned currSize = d_children[d_childrenValid - 1].getCurrentSize();
973
102
      d_currChildSize -= currSize;
974
102
      sizeMin = currSize + 1;
975
102
      d_children.erase(d_childrenValid - 1);
976
102
      d_childrenValid--;
977
    }
978
    else
979
    {
980
3599
      sizeMin = 0;
981
3599
      d_childrenValid++;
982
    }
983
  }
984
59276
  Trace("sygus-enum-debug2") << "master(" << d_tn
985
29638
                             << "): init children : success" << std::endl;
986
  // initialized all children
987
29638
  return true;
988
}
989
990
3893
bool SygusEnumerator::TermEnumMaster::initializeChild(unsigned i,
991
                                                      unsigned sizeMin)
992
{
993
3893
  Assert(d_ccWeight <= d_currSize);
994
3893
  Assert(d_currChildSize + d_ccWeight <= d_currSize);
995
3893
  unsigned sizeMax = (d_currSize - d_ccWeight) - d_currChildSize;
996
7786
  Trace("sygus-enum-debug2") << "master(" << d_tn << "): initializeChild " << i
997
3893
                             << " (" << d_currSize << ", " << d_ccWeight << ", "
998
3893
                             << d_currChildSize << ")\n";
999
3893
  if (sizeMin > sizeMax)
1000
  {
1001
94
    Trace("sygus-enum-debug2") << "master(" << d_tn << "): failed due to size "
1002
47
                               << sizeMin << "/" << sizeMax << "\n";
1003
47
    return false;
1004
  }
1005
  // initialize the child to enumerate exactly the terms that sum to size
1006
3846
  sizeMin = (i + 1 == d_ccTypes.size()) ? sizeMax : sizeMin;
1007
3846
  TermEnumSlave& te = d_children[i];
1008
3846
  bool init = te.initialize(d_se, d_ccTypes[i], sizeMin, sizeMax);
1009
3846
  if (!init)
1010
  {
1011
    // failed to initialize
1012
247
    d_children.erase(i);
1013
494
    Trace("sygus-enum-debug2") << "master(" << d_tn
1014
247
                               << "): failed due to child init\n";
1015
247
    return false;
1016
  }
1017
3599
  unsigned teSize = te.getCurrentSize();
1018
  // fail if the initial children size does not fit d_currSize-d_ccWeight
1019
3599
  if (teSize + d_currChildSize + d_ccWeight > d_currSize)
1020
  {
1021
    d_children.erase(i);
1022
    Trace("sygus-enum-debug2") << "master(" << d_tn
1023
                               << "): failed due to child size\n";
1024
    return false;
1025
  }
1026
3599
  d_currChildSize += teSize;
1027
7198
  Trace("sygus-enum-debug2") << "master(" << d_tn
1028
3599
                             << "): success initializeChild " << i << "\n";
1029
3599
  return true;
1030
}
1031
1032
void SygusEnumerator::TermEnumMaster::childrenToShape(
1033
    std::vector<Node>& children)
1034
{
1035
  if (children.size() <= 2)
1036
  {
1037
    // don't need to convert constants and unary applications
1038
    return;
1039
  }
1040
  std::map<TypeNode, int> vcounter;
1041
  // Buffered child, so that we only compute vcounter if there are more than
1042
  // one children with free variables, since otherwise there is no change.
1043
  // For example, if we are given { C, (+ x1 x2), 1 }, we buffer child (+ x1 x2)
1044
  // noting that it has free variables. We proceed with processing the remaining
1045
  // children, and note that no other child contains free variables, and hence
1046
  // no change is necessary (since by construction, all children have the
1047
  // property of having unique variable subterms). On the other hand if the
1048
  // last child above was x1, then this would trigger us to convert (+ x1 x2)
1049
  // while computing vcounter, and subsequently update x1 to x3 to obtain
1050
  // { C, (+ x1 x2), x3 }.
1051
  // Have we set the buffer child index
1052
  bool bufferChildSet = false;
1053
  // Have we processed the buffer child index
1054
  bool bufferChildProcessed = false;
1055
  // The buffer child index
1056
  size_t bufferChild = 0;
1057
  for (size_t i = 1, nchildren = children.size(); i < nchildren; i++)
1058
  {
1059
    if (!expr::hasBoundVar(children[i]))
1060
    {
1061
      // don't need to care about expressions with no bound variables
1062
      continue;
1063
    }
1064
    else if (!bufferChildSet)
1065
    {
1066
      bufferChild = i;
1067
      bufferChildSet = true;
1068
      continue;
1069
    }
1070
    else if (!bufferChildProcessed)
1071
    {
1072
      // process the buffer child
1073
      children[bufferChild] = convertShape(children[bufferChild], vcounter);
1074
      bufferChildProcessed = true;
1075
    }
1076
    children[i] = convertShape(children[i], vcounter);
1077
  }
1078
}
1079
1080
Node SygusEnumerator::TermEnumMaster::convertShape(
1081
    Node n, std::map<TypeNode, int>& vcounter)
1082
{
1083
  NodeManager* nm = NodeManager::currentNM();
1084
  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
1085
  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
1086
  std::vector<TNode> visit;
1087
  TNode cur;
1088
  visit.push_back(n);
1089
  do
1090
  {
1091
    cur = visit.back();
1092
    visit.pop_back();
1093
    it = visited.find(cur);
1094
1095
    if (it == visited.end())
1096
    {
1097
      if (cur.isVar())
1098
      {
1099
        // do the conversion
1100
        visited[cur] = d_tds->getFreeVarInc(cur.getType(), vcounter);
1101
      }
1102
      else if (!expr::hasBoundVar(cur))
1103
      {
1104
        // no bound variables, no change
1105
        visited[cur] = cur;
1106
      }
1107
      else
1108
      {
1109
        visited[cur] = Node::null();
1110
        visit.push_back(cur);
1111
        visit.insert(visit.end(), cur.begin(), cur.end());
1112
      }
1113
    }
1114
    else if (it->second.isNull())
1115
    {
1116
      Node ret = cur;
1117
      bool childChanged = false;
1118
      std::vector<Node> children;
1119
      if (cur.getMetaKind() == metakind::PARAMETERIZED)
1120
      {
1121
        children.push_back(cur.getOperator());
1122
      }
1123
      for (const Node& cn : cur)
1124
      {
1125
        it = visited.find(cn);
1126
        Assert(it != visited.end());
1127
        Assert(!it->second.isNull());
1128
        childChanged = childChanged || cn != it->second;
1129
        children.push_back(it->second);
1130
      }
1131
      if (childChanged)
1132
      {
1133
        ret = nm->mkNode(cur.getKind(), children);
1134
      }
1135
      visited[cur] = ret;
1136
    }
1137
  } while (!visit.empty());
1138
  Assert(visited.find(n) != visited.end());
1139
  Assert(!visited.find(n)->second.isNull());
1140
  return visited[n];
1141
}
1142
1143
11
SygusEnumerator::TermEnumMasterInterp::TermEnumMasterInterp(TypeNode tn)
1144
11
    : TermEnum(), d_te(tn), d_currNumConsts(0), d_nextIndexEnd(0)
1145
{
1146
11
}
1147
1148
11
bool SygusEnumerator::TermEnumMasterInterp::initialize(SygusEnumerator* se,
1149
                                                       TypeNode tn)
1150
{
1151
11
  d_se = se;
1152
11
  d_tn = tn;
1153
11
  d_currSize = 0;
1154
11
  d_currNumConsts = 1;
1155
11
  d_nextIndexEnd = 1;
1156
11
  return true;
1157
}
1158
1159
57
Node SygusEnumerator::TermEnumMasterInterp::getCurrent() { return *d_te; }
1160
59
bool SygusEnumerator::TermEnumMasterInterp::increment()
1161
{
1162
59
  if (d_te.isFinished())
1163
  {
1164
2
    return false;
1165
  }
1166
57
  SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn];
1167
114
  Node curr = getCurrent();
1168
57
  tc.addTerm(curr);
1169
57
  if (tc.getNumTerms() == d_nextIndexEnd)
1170
  {
1171
13
    tc.pushEnumSizeIndex();
1172
13
    d_currSize++;
1173
26
    d_currNumConsts = d_currNumConsts * options::sygusActiveGenEnumConsts();
1174
13
    d_nextIndexEnd = d_nextIndexEnd + d_currNumConsts;
1175
  }
1176
57
  ++d_te;
1177
57
  return !d_te.isFinished();
1178
}
1179
8
SygusEnumerator::TermEnumMasterFv::TermEnumMasterFv() : TermEnum() {}
1180
8
bool SygusEnumerator::TermEnumMasterFv::initialize(SygusEnumerator* se,
1181
                                                   TypeNode tn)
1182
{
1183
8
  d_se = se;
1184
8
  d_tn = tn;
1185
8
  d_currSize = 0;
1186
16
  Node ret = getCurrent();
1187
8
  AlwaysAssert(!ret.isNull());
1188
8
  SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn];
1189
8
  tc.addTerm(ret);
1190
16
  return true;
1191
}
1192
1193
16
Node SygusEnumerator::TermEnumMasterFv::getCurrent()
1194
{
1195
16
  Node ret = d_se->d_tds->getFreeVar(d_tn, d_currSize);
1196
32
  Trace("sygus-enum-debug2") << "master_fv(" << d_tn << "): mk " << ret
1197
16
                             << std::endl;
1198
16
  return ret;
1199
}
1200
1201
8
bool SygusEnumerator::TermEnumMasterFv::increment()
1202
{
1203
8
  SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn];
1204
  // size increments at a constant rate
1205
8
  d_currSize++;
1206
8
  tc.pushEnumSizeIndex();
1207
16
  Node curr = getCurrent();
1208
16
  Trace("sygus-enum-debug2") << "master_fv(" << d_tn << "): increment, add "
1209
8
                             << curr << std::endl;
1210
8
  bool ret = tc.addTerm(curr);
1211
8
  AlwaysAssert(ret);
1212
16
  return true;
1213
}
1214
1215
}  // namespace quantifiers
1216
}  // namespace theory
1217
26685
}  // namespace CVC4