GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/term_tuple_enumerator.cpp Lines: 142 192 74.0 %
Date: 2021-03-23 Branches: 224 572 39.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file  term_tuple_enumerator.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mikolas Janota
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 an enumeration of tuples of terms for the purpose
13
 *of quantifier instantiation.
14
 **/
15
#include "theory/quantifiers/term_tuple_enumerator.h"
16
17
#include <algorithm>
18
#include <functional>
19
#include <iterator>
20
#include <map>
21
#include <vector>
22
23
#include "base/map_util.h"
24
#include "base/output.h"
25
#include "options/quantifiers_options.h"
26
#include "smt/smt_statistics_registry.h"
27
#include "theory/quantifiers/index_trie.h"
28
#include "theory/quantifiers/quant_module.h"
29
#include "theory/quantifiers/relevant_domain.h"
30
#include "theory/quantifiers/term_registry.h"
31
#include "theory/quantifiers/term_util.h"
32
#include "theory/quantifiers_engine.h"
33
#include "util/statistics_registry.h"
34
35
namespace CVC4 {
36
37
template <typename T>
38
9636
static CVC4ostream& operator<<(CVC4ostream& out, const std::vector<T>& v)
39
{
40
9636
  out << "[ ";
41
9636
  std::copy(v.begin(), v.end(), std::ostream_iterator<T>(out, " "));
42
9636
  return out << "]";
43
}
44
45
/** Tracing purposes, printing a masked vector of indices. */
46
static void traceMaskedVector(const char* trace,
47
                              const char* name,
48
                              const std::vector<bool>& mask,
49
                              const std::vector<size_t>& values)
50
{
51
  Assert(mask.size() == values.size());
52
  Trace(trace) << name << " [ ";
53
  for (size_t variableIx = 0; variableIx < mask.size(); variableIx++)
54
  {
55
    if (mask[variableIx])
56
    {
57
      Trace(trace) << values[variableIx] << " ";
58
    }
59
    else
60
    {
61
      Trace(trace) << "_ ";
62
    }
63
  }
64
  Trace(trace) << "]" << std::endl;
65
}
66
67
namespace theory {
68
namespace quantifiers {
69
/**
70
 * Base class for enumerators of tuples of terms for the purpose of
71
 * quantification instantiation. The tuples are represented as tuples of
72
 * indices of  terms, where the tuple has as many elements as there are
73
 * quantified variables in the considered quantifier.
74
 *
75
 * Like so, we see a tuple as a number, where the digits may have different
76
 * ranges. The most significant digits are stored first.
77
 *
78
 * Tuples are enumerated  in a lexicographic order in stages. There are 2
79
 * possible strategies, either  all tuples in a given stage have the same sum of
80
 * digits, or, the maximum  over these digits is the same.
81
 * */
82
class TermTupleEnumeratorBase : public TermTupleEnumeratorInterface
83
{
84
 public:
85
  /** Initialize the class with the quantifier to be instantiated. */
86
1965
  TermTupleEnumeratorBase(Node quantifier,
87
                          const TermTupleEnumeratorContext* context)
88
1965
      : d_quantifier(quantifier),
89
3930
        d_variableCount(d_quantifier[0].getNumChildren()),
90
        d_context(context),
91
        d_stepCounter(0),
92
        d_disabledCombinations(
93
5895
            true)  // do not record combinations with no blanks
94
95
  {
96
1965
    d_changePrefix = d_variableCount;
97
1965
  }
98
99
1965
  virtual ~TermTupleEnumeratorBase() = default;
100
101
  // implementation of the TermTupleEnumeratorInterface
102
  virtual void init() override;
103
  virtual bool hasNext() override;
104
  virtual void next(/*out*/ std::vector<Node>& terms) override;
105
  virtual void failureReason(const std::vector<bool>& mask) override;
106
  // end of implementation of the TermTupleEnumeratorInterface
107
108
 protected:
109
  /** the quantifier whose variables are being instantiated */
110
  const Node d_quantifier;
111
  /** number of variables in the quantifier */
112
  const size_t d_variableCount;
113
  /** context of structures with a longer lifespan */
114
  const TermTupleEnumeratorContext* const d_context;
115
  /** type for each variable */
116
  std::vector<TypeNode> d_typeCache;
117
  /** number of candidate terms for each variable */
118
  std::vector<size_t> d_termsSizes;
119
  /** tuple of indices of the current terms */
120
  std::vector<size_t> d_termIndex;
121
  /** total number of steps of the enumerator */
122
  uint32_t d_stepCounter;
123
124
  /** a data structure storing disabled combinations of terms */
125
  IndexTrie d_disabledCombinations;
126
127
  /** current sum/max  of digits, depending on the strategy */
128
  size_t d_currentStage;
129
  /**total number of stages*/
130
  size_t d_stageCount;
131
  /**becomes false once the enumerator runs out of options*/
132
  bool d_hasNext;
133
  /** the length of the prefix that has to be changed in the next
134
  combination, i.e.  the number of the most significant digits that need to be
135
  changed in order to escape a  useless instantiation */
136
  size_t d_changePrefix;
137
  /** Move onto the next stage */
138
  bool increaseStage();
139
  /** Move onto the next stage, sum strategy. */
140
  bool increaseStageSum();
141
  /** Move onto the next stage, max strategy. */
142
  bool increaseStageMax();
143
  /** Move on in the current stage */
144
  bool nextCombination();
145
  /** Move onto the next combination. */
146
  bool nextCombinationInternal();
147
  /** Find the next lexicographically smallest combination of terms that change
148
   * on the change prefix, each digit is within the current state,  and there is
149
   * at least one digit not in the previous stage. */
150
  bool nextCombinationSum();
151
  /** Find the next lexicographically smallest combination of terms that change
152
   * on the change prefix and their sum is equal to d_currentStage. */
153
  bool nextCombinationMax();
154
  /** Set up terms for given variable.  */
155
  virtual size_t prepareTerms(size_t variableIx) = 0;
156
  /** Get a given term for a given variable.  */
157
  virtual Node getTerm(size_t variableIx,
158
                       size_t term_index) CVC4_WARN_UNUSED_RESULT = 0;
159
};
160
161
/**
162
 * Enumerate ground terms as they come from the term database.
163
 */
164
class TermTupleEnumeratorBasic : public TermTupleEnumeratorBase
165
{
166
 public:
167
414
  TermTupleEnumeratorBasic(Node quantifier,
168
                           const TermTupleEnumeratorContext* context)
169
414
      : TermTupleEnumeratorBase(quantifier, context)
170
  {
171
414
  }
172
173
828
  virtual ~TermTupleEnumeratorBasic() = default;
174
175
 protected:
176
  /**  a list of terms for each type */
177
  std::map<TypeNode, std::vector<Node> > d_termDbList;
178
  virtual size_t prepareTerms(size_t variableIx) override;
179
  virtual Node getTerm(size_t variableIx, size_t term_index) override;
180
};
181
182
/**
183
 * Enumerate ground terms according to the relevant domain class.
184
 */
185
class TermTupleEnumeratorRD : public TermTupleEnumeratorBase
186
{
187
 public:
188
1551
  TermTupleEnumeratorRD(Node quantifier,
189
                        const TermTupleEnumeratorContext* context)
190
1551
      : TermTupleEnumeratorBase(quantifier, context)
191
  {
192
1551
  }
193
3102
  virtual ~TermTupleEnumeratorRD() = default;
194
195
 protected:
196
10146
  virtual size_t prepareTerms(size_t variableIx) override
197
  {
198
20292
    return d_context->d_rd->getRDomain(d_quantifier, variableIx)
199
20292
        ->d_terms.size();
200
  }
201
22066
  virtual Node getTerm(size_t variableIx, size_t term_index) override
202
  {
203
44132
    return d_context->d_rd->getRDomain(d_quantifier, variableIx)
204
44132
        ->d_terms[term_index];
205
  }
206
};
207
208
1965
TermTupleEnumeratorInterface* mkTermTupleEnumerator(
209
    Node quantifier, const TermTupleEnumeratorContext* context)
210
{
211
5895
  return context->d_isRd ? static_cast<TermTupleEnumeratorInterface*>(
212
1551
             new TermTupleEnumeratorRD(quantifier, context))
213
                         : static_cast<TermTupleEnumeratorInterface*>(
214
4344
                             new TermTupleEnumeratorBasic(quantifier, context));
215
}
216
217
1965
void TermTupleEnumeratorBase::init()
218
{
219
3930
  Trace("inst-alg-rd") << "Initializing enumeration " << d_quantifier
220
1965
                       << std::endl;
221
1965
  d_currentStage = 0;
222
1965
  d_hasNext = true;
223
1965
  d_stageCount = 1;  // in the case of full effort we do at least one stage
224
225
1965
  if (d_variableCount == 0)
226
  {
227
    d_hasNext = false;
228
    return;
229
  }
230
231
  // prepare a sequence of terms for each quantified variable
232
  // additionally initialize the cache for variable types
233
12774
  for (size_t variableIx = 0; variableIx < d_variableCount; variableIx++)
234
  {
235
10809
    d_typeCache.push_back(d_quantifier[0][variableIx].getType());
236
10809
    const size_t termsSize = prepareTerms(variableIx);
237
21618
    Trace("inst-alg-rd") << "Variable " << variableIx << " has " << termsSize
238
10809
                         << " in relevant domain." << std::endl;
239
10809
    if (termsSize == 0 && !d_context->d_fullEffort)
240
    {
241
      d_hasNext = false;
242
      return;  // give up on an empty dommain
243
    }
244
10809
    d_termsSizes.push_back(termsSize);
245
10809
    d_stageCount = std::max(d_stageCount, termsSize);
246
  }
247
248
3930
  Trace("inst-alg-rd") << "Will do " << d_stageCount
249
1965
                       << " stages of instantiation." << std::endl;
250
1965
  d_termIndex.resize(d_variableCount, 0);
251
}
252
253
9775
bool TermTupleEnumeratorBase::hasNext()
254
{
255
9775
  if (!d_hasNext)
256
  {
257
    return false;
258
  }
259
260
9775
  if (d_stepCounter++ == 0)
261
  {  // TODO:any (nice)  way of avoiding this special if?
262
1965
    Assert(d_currentStage == 0);
263
3930
    Trace("inst-alg-rd") << "Try stage " << d_currentStage << "..."
264
1965
                         << std::endl;
265
1965
    return true;
266
  }
267
268
  // try to find the next combination
269
7810
  return d_hasNext = nextCombination();
270
}
271
272
7810
void TermTupleEnumeratorBase::failureReason(const std::vector<bool>& mask)
273
{
274
7810
  if (Trace.isOn("inst-alg"))
275
  {
276
    traceMaskedVector("inst-alg", "failureReason", mask, d_termIndex);
277
  }
278
7810
  d_disabledCombinations.add(mask, d_termIndex);  // record failure
279
  // update change prefix accordingly
280
10256
  for (d_changePrefix = mask.size();
281
10256
       d_changePrefix && !mask[d_changePrefix - 1];
282
2446
       d_changePrefix--)
283
    ;
284
7810
}
285
286
8973
void TermTupleEnumeratorBase::next(/*out*/ std::vector<Node>& terms)
287
{
288
8973
  Trace("inst-alg-rd") << "Try instantiation: " << d_termIndex << std::endl;
289
8973
  terms.resize(d_variableCount);
290
37984
  for (size_t variableIx = 0; variableIx < d_variableCount; variableIx++)
291
  {
292
29011
    const Node t = d_termsSizes[variableIx] == 0
293
                       ? Node::null()
294
58022
                       : getTerm(variableIx, d_termIndex[variableIx]);
295
29011
    terms[variableIx] = t;
296
29011
    Trace("inst-alg-rd") << t << "  ";
297
29011
    Assert(terms[variableIx].isNull()
298
           || terms[variableIx].getType().isComparableTo(
299
               d_quantifier[0][variableIx].getType()));
300
  }
301
8973
  Trace("inst-alg-rd") << std::endl;
302
8973
}
303
304
bool TermTupleEnumeratorBase::increaseStageSum()
305
{
306
  const size_t lowerBound = d_currentStage + 1;
307
  Trace("inst-alg-rd") << "Try sum " << lowerBound << "..." << std::endl;
308
  d_currentStage = 0;
309
  for (size_t digit = d_termIndex.size();
310
       d_currentStage < lowerBound && digit--;)
311
  {
312
    const size_t missing = lowerBound - d_currentStage;
313
    const size_t maxValue = d_termsSizes[digit] ? d_termsSizes[digit] - 1 : 0;
314
    d_termIndex[digit] = std::min(missing, maxValue);
315
    d_currentStage += d_termIndex[digit];
316
  }
317
  return d_currentStage >= lowerBound;
318
}
319
320
5208
bool TermTupleEnumeratorBase::increaseStage()
321
{
322
5208
  d_changePrefix = d_variableCount;  // simply reset upon increase stage
323
5208
  return d_context->d_increaseSum ? increaseStageSum() : increaseStageMax();
324
}
325
326
5208
bool TermTupleEnumeratorBase::increaseStageMax()
327
{
328
5208
  d_currentStage++;
329
5208
  if (d_currentStage >= d_stageCount)
330
  {
331
802
    return false;
332
  }
333
4406
  Trace("inst-alg-rd") << "Try stage " << d_currentStage << "..." << std::endl;
334
  // skipping some elements that have already been definitely seen
335
  // find the least significant digit that can be set to the current stage
336
  // TODO: should we skip all?
337
4406
  std::fill(d_termIndex.begin(), d_termIndex.end(), 0);
338
4406
  bool found = false;
339
9367
  for (size_t digit = d_termIndex.size(); !found && digit--;)
340
  {
341
4961
    if (d_termsSizes[digit] > d_currentStage)
342
    {
343
4406
      found = true;
344
4406
      d_termIndex[digit] = d_currentStage;
345
    }
346
  }
347
4406
  Assert(found);
348
4406
  return found;
349
}
350
351
8553
bool TermTupleEnumeratorBase::nextCombination()
352
{
353
  while (true)
354
  {
355
9296
    Trace("inst-alg-rd") << "changePrefix " << d_changePrefix << std::endl;
356
8553
    if (!nextCombinationInternal() && !increaseStage())
357
    {
358
802
      return false;  // ran out of combinations
359
    }
360
7751
    if (!d_disabledCombinations.find(d_termIndex, d_changePrefix))
361
    {
362
7008
      return true;  // current combination vetted by disabled combinations
363
    }
364
  }
365
}
366
367
/** Move onto the next combination, depending on the strategy. */
368
8553
bool TermTupleEnumeratorBase::nextCombinationInternal()
369
{
370
8553
  return d_context->d_increaseSum ? nextCombinationSum() : nextCombinationMax();
371
}
372
373
/** Find the next lexicographically smallest combination of terms that change
374
 * on the change prefix and their sum is equal to d_currentStage. */
375
8553
bool TermTupleEnumeratorBase::nextCombinationMax()
376
{
377
  // look for the least significant digit, within change prefix,
378
  // that can be increased
379
8553
  bool found = false;
380
8553
  size_t increaseDigit = d_changePrefix;
381
39327
  while (!found && increaseDigit--)
382
  {
383
15387
    const size_t new_value = d_termIndex[increaseDigit] + 1;
384
15387
    if (new_value < d_termsSizes[increaseDigit] && new_value <= d_currentStage)
385
    {
386
3345
      d_termIndex[increaseDigit] = new_value;
387
      // send everything after the increased digit to 0
388
3345
      std::fill(d_termIndex.begin() + increaseDigit + 1, d_termIndex.end(), 0);
389
3345
      found = true;
390
    }
391
  }
392
8553
  if (!found)
393
  {
394
5208
    return false;  // nothing to increase
395
  }
396
  // check if the combination has at least one digit in the current stage,
397
  // since at least one digit was increased, no need for this in stage 1
398
3345
  bool inStage = d_currentStage <= 1;
399
5869
  for (size_t i = increaseDigit + 1; !inStage && i--;)
400
  {
401
2524
    inStage = d_termIndex[i] >= d_currentStage;
402
  }
403
3345
  if (!inStage)  // look for a digit that can increase to current stage
404
  {
405
1292
    for (increaseDigit = d_variableCount, found = false;
406
1292
         !found && increaseDigit--;)
407
    {
408
646
      found = d_termsSizes[increaseDigit] > d_currentStage;
409
    }
410
646
    if (!found)
411
    {
412
      return false;  // nothing to increase to the current stage
413
    }
414
646
    Assert(d_termsSizes[increaseDigit] > d_currentStage
415
           && d_termIndex[increaseDigit] < d_currentStage);
416
646
    d_termIndex[increaseDigit] = d_currentStage;
417
    // send everything after the increased digit to 0
418
646
    std::fill(d_termIndex.begin() + increaseDigit + 1, d_termIndex.end(), 0);
419
  }
420
3345
  return true;
421
}
422
423
/** Find the next lexicographically smallest combination of terms that change
424
 * on the change prefix, each digit is within the current state,  and there is
425
 * at least one digit not in the previous stage. */
426
bool TermTupleEnumeratorBase::nextCombinationSum()
427
{
428
  size_t suffixSum = 0;
429
  bool found = false;
430
  size_t increaseDigit = d_termIndex.size();
431
  while (increaseDigit--)
432
  {
433
    const size_t newValue = d_termIndex[increaseDigit] + 1;
434
    found = suffixSum > 0 && newValue < d_termsSizes[increaseDigit]
435
            && increaseDigit < d_changePrefix;
436
    if (found)
437
    {
438
      // digit can be increased and suffix can be decreased
439
      d_termIndex[increaseDigit] = newValue;
440
      break;
441
    }
442
    suffixSum += d_termIndex[increaseDigit];
443
    d_termIndex[increaseDigit] = 0;
444
  }
445
  if (!found)
446
  {
447
    return false;
448
  }
449
  Assert(suffixSum > 0);
450
  // increaseDigit went up by one, hence, distribute (suffixSum - 1) in the
451
  // least significant digits
452
  suffixSum--;
453
  for (size_t digit = d_termIndex.size(); suffixSum > 0 && digit--;)
454
  {
455
    const size_t maxValue = d_termsSizes[digit] ? d_termsSizes[digit] - 1 : 0;
456
    d_termIndex[digit] = std::min(suffixSum, maxValue);
457
    suffixSum -= d_termIndex[digit];
458
  }
459
  Assert(suffixSum == 0);  // everything should have been distributed
460
  return true;
461
}
462
463
663
size_t TermTupleEnumeratorBasic::prepareTerms(size_t variableIx)
464
{
465
663
  TermDb* const tdb = d_context->d_quantEngine->getTermDatabase();
466
663
  QuantifiersState& qs = d_context->d_quantEngine->getState();
467
1326
  const TypeNode type_node = d_typeCache[variableIx];
468
469
663
  if (!ContainsKey(d_termDbList, type_node))
470
  {
471
510
    const size_t ground_terms_count = tdb->getNumTypeGroundTerms(type_node);
472
1020
    std::map<Node, Node> repsFound;
473
44145
    for (size_t j = 0; j < ground_terms_count; j++)
474
    {
475
87270
      Node gt = tdb->getTypeGroundTerm(type_node, j);
476
43635
      if (!options::cegqi() || !quantifiers::TermUtil::hasInstConstAttr(gt))
477
      {
478
87270
        Node rep = qs.getRepresentative(gt);
479
43635
        if (repsFound.find(rep) == repsFound.end())
480
        {
481
4539
          repsFound[rep] = gt;
482
4539
          d_termDbList[type_node].push_back(gt);
483
        }
484
      }
485
    }
486
  }
487
488
1326
  Trace("inst-alg-rd") << "Instantiation Terms for child " << variableIx << ": "
489
663
                       << d_termDbList[type_node] << std::endl;
490
1326
  return d_termDbList[type_node].size();
491
}
492
493
4697
Node TermTupleEnumeratorBasic::getTerm(size_t variableIx, size_t term_index)
494
{
495
9394
  const TypeNode type_node = d_typeCache[variableIx];
496
4697
  Assert(term_index < d_termDbList[type_node].size());
497
9394
  return d_termDbList[type_node][term_index];
498
}
499
500
}  // namespace quantifiers
501
}  // namespace theory
502
26685
}  // namespace CVC4