GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/enum_stream_substitution.cpp Lines: 230 345 66.7 %
Date: 2021-03-23 Branches: 326 1118 29.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file enum_stream_substitution.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Haniel Barbosa, Andrew Reynolds, Gereon Kremer
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 class for streaming concrete values (through substitutions) from
13
 ** enumerated abstract ones
14
 **/
15
16
#include "theory/quantifiers/sygus/enum_stream_substitution.h"
17
18
#include "expr/dtype_cons.h"
19
#include "options/base_options.h"
20
#include "options/datatypes_options.h"
21
#include "options/quantifiers_options.h"
22
#include "printer/printer.h"
23
#include "theory/quantifiers/sygus/term_database_sygus.h"
24
25
#include <numeric>  // for std::iota
26
27
using namespace CVC4::kind;
28
29
namespace CVC4 {
30
namespace theory {
31
namespace quantifiers {
32
33
2
EnumStreamPermutation::EnumStreamPermutation(quantifiers::TermDbSygus* tds)
34
2
    : d_tds(tds), d_first(true), d_curr_ind(0)
35
{
36
2
}
37
38
2
void EnumStreamPermutation::reset(Node value)
39
{
40
  // clean state
41
2
  d_var_classes.clear();
42
2
  d_var_tn_cons.clear();
43
2
  d_first = true;
44
2
  d_perm_state_class.clear();
45
2
  d_perm_values.clear();
46
2
  d_value = value;
47
  // get variables in value's type
48
4
  TypeNode tn = value.getType();
49
4
  Node var_list = tn.getDType().getSygusVarList();
50
2
  NodeManager* nm = NodeManager::currentNM();
51
  // get subtypes in value's type
52
2
  SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
53
4
  std::vector<TypeNode> sf_types;
54
2
  ti.getSubfieldTypes(sf_types);
55
  // associate variables with constructors in all subfield types
56
4
  std::map<Node, Node> cons_var;
57
6
  for (const Node& v : var_list)
58
  {
59
    // collect constructors for variable in all subtypes
60
8
    for (const TypeNode& stn : sf_types)
61
    {
62
4
      const DType& dt = stn.getDType();
63
16
      for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i)
64
      {
65
12
        if (dt[i].getNumArgs() == 0 && dt[i].getSygusOp() == v)
66
        {
67
8
          Node cons = nm->mkNode(APPLY_CONSTRUCTOR, dt[i].getConstructor());
68
4
          d_var_tn_cons[v][stn] = cons;
69
4
          cons_var[cons] = v;
70
        }
71
      }
72
    }
73
  }
74
  // collect variables occurring in value
75
4
  std::vector<Node> vars;
76
4
  std::unordered_set<Node, NodeHashFunction> visited;
77
2
  collectVars(value, vars, visited);
78
  // partition permutation variables
79
2
  d_curr_ind = 0;
80
2
  Trace("synth-stream-concrete") << " ..permutting vars :";
81
4
  std::unordered_set<Node, NodeHashFunction> seen_vars;
82
4
  for (const Node& v_cons : vars)
83
  {
84
2
    Assert(cons_var.find(v_cons) != cons_var.end());
85
4
    Node var = cons_var[v_cons];
86
2
    if (seen_vars.insert(var).second)
87
    {
88
      // do not add repeated vars
89
2
      d_var_classes[ti.getSubclassForVar(var)].push_back(var);
90
    }
91
  }
92
4
  for (const std::pair<const unsigned, std::vector<Node>>& p : d_var_classes)
93
  {
94
2
    d_perm_state_class.push_back(PermutationState(p.second));
95
2
    if (Trace.isOn("synth-stream-concrete"))
96
    {
97
      Trace("synth-stream-concrete") << " " << p.first << " -> [";
98
      for (const Node& var : p.second)
99
      {
100
        std::stringstream ss;
101
        TermDbSygus::toStreamSygus(ss, var);
102
        Trace("synth-stream-concrete") << " " << ss.str();
103
      }
104
      Trace("synth-stream-concrete") << " ]";
105
    }
106
  }
107
2
  Trace("synth-stream-concrete") << "\n";
108
2
}
109
110
4
Node EnumStreamPermutation::getNext()
111
{
112
4
  if (Trace.isOn("synth-stream-concrete"))
113
  {
114
    std::stringstream ss;
115
    TermDbSygus::toStreamSygus(ss, d_value);
116
    Trace("synth-stream-concrete")
117
        << " ....streaming next permutation for value : " << ss.str()
118
        << " with " << d_perm_state_class.size() << " permutation classes\n";
119
  }
120
  // initial value
121
4
  if (d_first)
122
  {
123
2
    d_first = false;
124
4
    Node bultin_value = d_tds->sygusToBuiltin(d_value, d_value.getType());
125
2
    d_perm_values.insert(
126
4
        d_tds->getExtRewriter()->extendedRewrite(bultin_value));
127
2
    return d_value;
128
  }
129
2
  unsigned n_classes = d_perm_state_class.size();
130
4
  Node perm_value, bultin_perm_value;
131
  do
132
  {
133
2
    bool new_perm = false;
134
6
    while (!new_perm && d_curr_ind < n_classes)
135
    {
136
2
      if (d_perm_state_class[d_curr_ind].getNextPermutation())
137
      {
138
        new_perm = true;
139
        Trace("synth-stream-concrete-debug2")
140
            << " ....class " << d_curr_ind << " has new perm\n";
141
        d_curr_ind = 0;
142
      }
143
      else
144
      {
145
4
        Trace("synth-stream-concrete-debug2")
146
2
            << " ....class " << d_curr_ind << " reset\n";
147
2
        d_perm_state_class[d_curr_ind].reset();
148
2
        d_curr_ind++;
149
      }
150
    }
151
    // no new permutation
152
2
    if (!new_perm)
153
    {
154
2
      Trace("synth-stream-concrete") << " ....no new perm, return null\n";
155
2
      return Node::null();
156
    }
157
    // building substitution
158
    std::vector<Node> domain_sub, range_sub;
159
    for (unsigned i = 0, size = d_perm_state_class.size(); i < size; ++i)
160
    {
161
      Trace("synth-stream-concrete") << " ..perm for class " << i << " is";
162
      std::vector<Node> raw_sub;
163
      d_perm_state_class[i].getLastPerm(raw_sub);
164
      // retrieve variables for substitution domain
165
      const std::vector<Node>& domain_sub_class =
166
          d_perm_state_class[i].getVars();
167
      Assert(domain_sub_class.size() == raw_sub.size());
168
      // build proper substitution based on variables types and constructors
169
      for (unsigned j = 0, size_j = raw_sub.size(); j < size_j; ++j)
170
      {
171
        for (std::pair<const TypeNode, Node>& p :
172
             d_var_tn_cons[domain_sub_class[j]])
173
        {
174
          // get constructor of type p.first from variable being permuted
175
          domain_sub.push_back(p.second);
176
          // get constructor of type p.first from variable to be permuted for
177
          range_sub.push_back(d_var_tn_cons[raw_sub[j]][p.first]);
178
          Trace("synth-stream-concrete-debug2")
179
              << "\n ....{ adding " << domain_sub.back() << " ["
180
              << domain_sub.back().getType() << "] -> " << range_sub.back()
181
              << " [" << range_sub.back().getType() << "] }";
182
        }
183
      }
184
      Trace("synth-stream-concrete") << "\n";
185
    }
186
    perm_value = d_value.substitute(domain_sub.begin(),
187
                                    domain_sub.end(),
188
                                    range_sub.begin(),
189
                                    range_sub.end());
190
    bultin_perm_value = d_tds->sygusToBuiltin(perm_value, perm_value.getType());
191
    Trace("synth-stream-concrete-debug")
192
        << " ......perm builtin is " << bultin_perm_value;
193
    if (options::sygusSymBreakDynamic())
194
    {
195
      bultin_perm_value =
196
          d_tds->getExtRewriter()->extendedRewrite(bultin_perm_value);
197
      Trace("synth-stream-concrete-debug")
198
          << " and rewrites to " << bultin_perm_value;
199
    }
200
    Trace("synth-stream-concrete-debug") << "\n";
201
    // if permuted value is equivalent modulo rewriting to a previous one, look
202
    // for another
203
  } while (!d_perm_values.insert(bultin_perm_value).second);
204
  if (Trace.isOn("synth-stream-concrete"))
205
  {
206
    std::stringstream ss;
207
    TermDbSygus::toStreamSygus(ss, perm_value);
208
    Trace("synth-stream-concrete")
209
        << " ....return new perm " << ss.str() << "\n";
210
  }
211
  return perm_value;
212
}
213
214
4
const std::vector<Node>& EnumStreamPermutation::getVarsClass(unsigned id) const
215
{
216
  std::map<unsigned, std::vector<Node>>::const_iterator it =
217
4
      d_var_classes.find(id);
218
4
  Assert(it != d_var_classes.end());
219
4
  return it->second;
220
}
221
222
2
unsigned EnumStreamPermutation::getVarClassSize(unsigned id) const
223
{
224
  std::map<unsigned, std::vector<Node>>::const_iterator it =
225
2
      d_var_classes.find(id);
226
2
  if (it == d_var_classes.end())
227
  {
228
    return 0;
229
  }
230
2
  return it->second.size();
231
}
232
233
2
void EnumStreamPermutation::collectVars(
234
    Node n,
235
    std::vector<Node>& vars,
236
    std::unordered_set<Node, NodeHashFunction>& visited)
237
{
238
2
  if (visited.find(n) != visited.end())
239
  {
240
    return;
241
  }
242
2
  visited.insert(n);
243
2
  if (n.getNumChildren() > 0)
244
  {
245
    for (const Node& ni : n)
246
    {
247
      collectVars(ni, vars, visited);
248
    }
249
    return;
250
  }
251
2
  if (d_tds->sygusToBuiltin(n, n.getType()).getKind() == kind::BOUND_VARIABLE)
252
  {
253
2
    if (std::find(vars.begin(), vars.end(), n) == vars.end())
254
    {
255
2
      vars.push_back(n);
256
    }
257
2
    return;
258
  }
259
}
260
261
2
EnumStreamPermutation::PermutationState::PermutationState(
262
2
    const std::vector<Node>& vars)
263
{
264
2
  d_vars = vars;
265
2
  d_curr_ind = 0;
266
2
  d_seq.resize(vars.size());
267
2
  std::fill(d_seq.begin(), d_seq.end(), 0);
268
  // initialize variable indices
269
2
  d_last_perm.resize(vars.size());
270
2
  std::iota(d_last_perm.begin(), d_last_perm.end(), 0);
271
2
}
272
273
2
void EnumStreamPermutation::PermutationState::reset()
274
{
275
2
  d_curr_ind = 0;
276
2
  std::fill(d_seq.begin(), d_seq.end(), 0);
277
2
  std::iota(d_last_perm.begin(), d_last_perm.end(), 0);
278
2
}
279
280
const std::vector<Node>& EnumStreamPermutation::PermutationState::getVars()
281
    const
282
{
283
  return d_vars;
284
}
285
286
void EnumStreamPermutation::PermutationState::getLastPerm(
287
    std::vector<Node>& vars)
288
{
289
  for (unsigned i = 0, size = d_last_perm.size(); i < size; ++i)
290
  {
291
    if (Trace.isOn("synth-stream-concrete"))
292
    {
293
      std::stringstream ss;
294
      TermDbSygus::toStreamSygus(ss, d_vars[d_last_perm[i]]);
295
      Trace("synth-stream-concrete") << " " << ss.str();
296
    }
297
    vars.push_back(d_vars[d_last_perm[i]]);
298
  }
299
}
300
301
4
bool EnumStreamPermutation::PermutationState::getNextPermutation()
302
{
303
  // exhausted permutations
304
4
  if (d_curr_ind == d_vars.size())
305
  {
306
2
    Trace("synth-stream-concrete-debug2") << "exhausted perms, ";
307
2
    return false;
308
  }
309
2
  if (d_seq[d_curr_ind] >= d_curr_ind)
310
  {
311
2
    d_seq[d_curr_ind] = 0;
312
2
    d_curr_ind++;
313
2
    return getNextPermutation();
314
  }
315
  if (d_curr_ind % 2 == 0)
316
  {
317
    // swap with first element
318
    std::swap(d_last_perm[0], d_last_perm[d_curr_ind]);
319
  }
320
  else
321
  {
322
    // swap with element in index in sequence of current index
323
    std::swap(d_last_perm[d_seq[d_curr_ind]], d_last_perm[d_curr_ind]);
324
  }
325
  d_seq[d_curr_ind] += 1;
326
  d_curr_ind = 0;
327
  return true;
328
}
329
330
2
EnumStreamSubstitution::EnumStreamSubstitution(quantifiers::TermDbSygus* tds)
331
2
    : d_tds(tds), d_stream_permutations(tds), d_curr_ind(0)
332
{
333
2
}
334
335
2
void EnumStreamSubstitution::initialize(TypeNode tn)
336
{
337
2
  d_tn = tn;
338
  // get variables in value's type
339
4
  Node var_list = tn.getDType().getSygusVarList();
340
  // get subtypes in value's type
341
2
  NodeManager* nm = NodeManager::currentNM();
342
2
  SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
343
4
  std::vector<TypeNode> sf_types;
344
2
  ti.getSubfieldTypes(sf_types);
345
  // associate variables with constructors in all subfield types
346
6
  for (const Node& v : var_list)
347
  {
348
    // collect constructors for variable in all subtypes
349
8
    for (const TypeNode& stn : sf_types)
350
    {
351
4
      const DType& dt = stn.getDType();
352
16
      for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i)
353
      {
354
12
        if (dt[i].getNumArgs() == 0 && dt[i].getSygusOp() == v)
355
        {
356
4
          d_var_tn_cons[v][stn] =
357
8
              nm->mkNode(APPLY_CONSTRUCTOR, dt[i].getConstructor());
358
        }
359
      }
360
    }
361
  }
362
  // split initial variables into classes
363
6
  for (const Node& v : var_list)
364
  {
365
4
    Assert(ti.getSubclassForVar(v) > 0);
366
4
    d_var_classes[ti.getSubclassForVar(v)].push_back(v);
367
  }
368
2
}
369
370
2
void EnumStreamSubstitution::resetValue(Node value)
371
{
372
2
  if (Trace.isOn("synth-stream-concrete"))
373
  {
374
    std::stringstream ss;
375
    TermDbSygus::toStreamSygus(ss, value);
376
    Trace("synth-stream-concrete")
377
        << " * Streaming concrete: registering value " << ss.str() << "\n";
378
  }
379
2
  d_last = Node::null();
380
2
  d_value = value;
381
  // reset permutation util
382
2
  d_stream_permutations.reset(value);
383
  // reset combination utils
384
2
  d_curr_ind = 0;
385
2
  d_comb_state_class.clear();
386
2
  Trace("synth-stream-concrete") << " ..combining vars  :";
387
4
  for (const std::pair<const unsigned, std::vector<Node>>& p : d_var_classes)
388
  {
389
    // ignore classes without variables being permuted
390
2
    unsigned perm_var_class_sz = d_stream_permutations.getVarClassSize(p.first);
391
2
    if (perm_var_class_sz == 0)
392
    {
393
      continue;
394
    }
395
6
    d_comb_state_class.push_back(CombinationState(
396
4
        p.second.size(), perm_var_class_sz, p.first, p.second));
397
2
    if (Trace.isOn("synth-stream-concrete"))
398
    {
399
      Trace("synth-stream-concrete")
400
          << " " << p.first << " -> " << perm_var_class_sz << " from [ ";
401
      for (const Node& var : p.second)
402
      {
403
        std::stringstream ss;
404
        TermDbSygus::toStreamSygus(ss, var);
405
        Trace("synth-stream-concrete") << " " << ss.str();
406
      }
407
      Trace("synth-stream-concrete") << " ]";
408
    }
409
  }
410
2
  Trace("synth-stream-concrete") << "\n";
411
2
}
412
413
6
Node EnumStreamSubstitution::getNext()
414
{
415
6
  if (Trace.isOn("synth-stream-concrete"))
416
  {
417
    std::stringstream ss;
418
    TermDbSygus::toStreamSygus(ss, d_value);
419
    Trace("synth-stream-concrete")
420
        << " ..streaming next combination of " << ss.str() << "\n";
421
  }
422
6
  unsigned n_classes = d_comb_state_class.size();
423
  // intial case
424
6
  if (d_last.isNull())
425
  {
426
2
    d_last = d_stream_permutations.getNext();
427
  }
428
  else
429
  {
430
4
    bool new_comb = false;
431
12
    while (!new_comb && d_curr_ind < n_classes)
432
    {
433
4
      if (d_comb_state_class[d_curr_ind].getNextCombination())
434
      {
435
2
        new_comb = true;
436
4
        Trace("synth-stream-concrete-debug2")
437
2
            << " ....class " << d_curr_ind << " has new comb\n";
438
2
        d_curr_ind = 0;
439
      }
440
      else
441
      {
442
4
        Trace("synth-stream-concrete-debug2")
443
2
            << " ....class " << d_curr_ind << " reset\n";
444
2
        d_comb_state_class[d_curr_ind].reset();
445
2
        d_curr_ind++;
446
      }
447
    }
448
    // no new combination
449
4
    if (!new_comb)
450
    {
451
4
      Trace("synth-stream-concrete")
452
          << " ..no new comb, get next permutation\n ....total combs until "
453
2
             "here : "
454
2
          << d_comb_values.size() << "\n";
455
2
      d_last = d_stream_permutations.getNext();
456
      // exhausted permutations
457
2
      if (d_last.isNull())
458
      {
459
2
        Trace("synth-stream-concrete") << " ..no new comb, return null\n";
460
2
        return Node::null();
461
      }
462
      // reset combination classes for next permutation
463
      d_curr_ind = 0;
464
      for (unsigned i = 0, size = d_comb_state_class.size(); i < size; ++i)
465
      {
466
        d_comb_state_class[i].reset();
467
      }
468
    }
469
  }
470
4
  if (Trace.isOn("synth-stream-concrete-debug"))
471
  {
472
    std::stringstream ss;
473
    TermDbSygus::toStreamSygus(ss, d_last);
474
    Trace("synth-stream-concrete-debug")
475
        << " ..using base perm " << ss.str() << "\n";
476
  }
477
  // building substitution
478
8
  std::vector<Node> domain_sub, range_sub;
479
8
  for (unsigned i = 0, size = d_comb_state_class.size(); i < size; ++i)
480
  {
481
8
    Trace("synth-stream-concrete")
482
8
        << " ..comb for class " << d_comb_state_class[i].getSubclassId()
483
4
        << " is";
484
8
    std::vector<Node> raw_sub;
485
4
    d_comb_state_class[i].getLastComb(raw_sub);
486
    // retrieve variables for substitution domain
487
    const std::vector<Node>& domain_sub_class =
488
        d_stream_permutations.getVarsClass(
489
4
            d_comb_state_class[i].getSubclassId());
490
4
    Assert(domain_sub_class.size() == raw_sub.size());
491
    // build proper substitution based on variables types and constructors
492
8
    for (unsigned j = 0, size_j = raw_sub.size(); j < size_j; ++j)
493
    {
494
4
      for (std::pair<const TypeNode, Node>& p :
495
4
           d_var_tn_cons[domain_sub_class[j]])
496
      {
497
        // get constructor of type p.first from variable being permuted
498
4
        domain_sub.push_back(p.second);
499
        // get constructor of type p.first from variable to be permuted for
500
4
        range_sub.push_back(d_var_tn_cons[raw_sub[j]][p.first]);
501
8
        Trace("synth-stream-concrete-debug2")
502
4
            << "\n ....{ adding " << domain_sub.back() << " ["
503
8
            << domain_sub.back().getType() << "] -> " << range_sub.back()
504
4
            << " [" << range_sub.back().getType() << "] }";
505
      }
506
    }
507
4
    Trace("synth-stream-concrete") << "\n";
508
  }
509
  Node comb_value = d_last.substitute(
510
8
      domain_sub.begin(), domain_sub.end(), range_sub.begin(), range_sub.end());
511
  // the new combination value should be fresh, modulo rewriting, by
512
  // construction (unless it's equiv to a constant, e.g. true / false)
513
  Node builtin_comb_value =
514
8
      d_tds->sygusToBuiltin(comb_value, comb_value.getType());
515
4
  if (options::sygusSymBreakDynamic())
516
  {
517
4
    builtin_comb_value =
518
8
        d_tds->getExtRewriter()->extendedRewrite(builtin_comb_value);
519
  }
520
4
  if (Trace.isOn("synth-stream-concrete"))
521
  {
522
    std::stringstream ss;
523
    TermDbSygus::toStreamSygus(ss, comb_value);
524
    Trace("synth-stream-concrete")
525
        << " ....register new comb value " << ss.str()
526
        << " with rewritten form " << builtin_comb_value
527
        << (builtin_comb_value.isConst() ? " (isConst)" : "") << "\n";
528
  }
529
8
  if (!builtin_comb_value.isConst()
530
4
      && !d_comb_values.insert(builtin_comb_value).second)
531
  {
532
    if (Trace.isOn("synth-stream-concrete"))
533
    {
534
      std::stringstream ss, ss1;
535
      TermDbSygus::toStreamSygus(ss, comb_value);
536
      Trace("synth-stream-concrete")
537
          << " ..term " << ss.str() << " is REDUNDANT with " << builtin_comb_value
538
          << "\n ..excluding all other concretizations (had "
539
          << d_comb_values.size() << " already)\n\n";
540
    }
541
    return Node::null();
542
  }
543
4
  if (Trace.isOn("synth-stream-concrete"))
544
  {
545
    std::stringstream ss;
546
    TermDbSygus::toStreamSygus(ss, comb_value);
547
    Trace("synth-stream-concrete")
548
        << " ..return new comb " << ss.str() << "\n\n";
549
  }
550
4
  return comb_value;
551
}
552
553
2
EnumStreamSubstitution::CombinationState::CombinationState(
554
2
    unsigned n, unsigned k, unsigned subclass_id, const std::vector<Node>& vars)
555
2
    : d_n(n), d_k(k)
556
{
557
2
  Assert(!vars.empty());
558
2
  Assert(k <= n);
559
2
  d_last_comb.resize(k);
560
2
  std::iota(d_last_comb.begin(), d_last_comb.end(), 0);
561
2
  d_vars = vars;
562
2
  d_subclass_id = subclass_id;
563
2
}
564
565
8
const unsigned EnumStreamSubstitution::CombinationState::getSubclassId() const
566
{
567
8
  return d_subclass_id;
568
}
569
570
2
void EnumStreamSubstitution::CombinationState::reset()
571
{
572
2
  std::iota(d_last_comb.begin(), d_last_comb.end(), 0);
573
2
}
574
575
4
void EnumStreamSubstitution::CombinationState::getLastComb(
576
    std::vector<Node>& vars)
577
{
578
8
  for (unsigned i = 0, size = d_last_comb.size(); i < size; ++i)
579
  {
580
4
    if (Trace.isOn("synth-stream-concrete"))
581
    {
582
      std::stringstream ss;
583
      TermDbSygus::toStreamSygus(ss, d_vars[d_last_comb[i]]);
584
      Trace("synth-stream-concrete") << " " << ss.str();
585
    }
586
4
    vars.push_back(d_vars[d_last_comb[i]]);
587
  }
588
4
}
589
590
4
bool EnumStreamSubstitution::CombinationState::getNextCombination()
591
{
592
  // find what to increment
593
4
  bool new_comb = false;
594
6
  for (int i = d_k - 1; i >= 0; --i)
595
  {
596
4
    if (d_last_comb[i] < d_n - d_k + i)
597
    {
598
2
      unsigned j = d_last_comb[i] + 1;
599
6
      while (static_cast<unsigned>(i) <= d_k - 1)
600
      {
601
2
        d_last_comb[i++] = j++;
602
      }
603
2
      new_comb = true;
604
2
      break;
605
    }
606
  }
607
4
  return new_comb;
608
}
609
610
2
void EnumStreamConcrete::initialize(Node e) { d_ess.initialize(e.getType()); }
611
2
void EnumStreamConcrete::addValue(Node v)
612
{
613
2
  d_ess.resetValue(v);
614
2
  d_currTerm = d_ess.getNext();
615
2
}
616
4
bool EnumStreamConcrete::increment()
617
{
618
4
  d_currTerm = d_ess.getNext();
619
4
  return !d_currTerm.isNull();
620
}
621
4
Node EnumStreamConcrete::getCurrent() { return d_currTerm; }
622
}  // namespace quantifiers
623
}  // namespace theory
624
26685
}  // namespace CVC4