GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/term_enumeration.cpp Lines: 16 29 55.2 %
Date: 2021-03-22 Branches: 27 86 31.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file term_enumeration.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 term enumeration utility
13
 **/
14
15
#include "theory/quantifiers/term_enumeration.h"
16
17
#include "theory/quantifiers/quant_bound_inference.h"
18
19
using namespace CVC4::kind;
20
21
namespace CVC4 {
22
namespace theory {
23
namespace quantifiers {
24
25
15972
TermEnumeration::TermEnumeration(QuantifiersBoundInference* qbi) : d_qbi(qbi) {}
26
27
3248
Node TermEnumeration::getEnumerateTerm(TypeNode tn, unsigned index)
28
{
29
6496
  Trace("term-db-enum") << "Get enumerate term " << tn << " " << index
30
3248
                        << std::endl;
31
  std::unordered_map<TypeNode, size_t, TypeNodeHashFunction>::iterator it =
32
3248
      d_typ_enum_map.find(tn);
33
  size_t teIndex;
34
3248
  if (it == d_typ_enum_map.end())
35
  {
36
439
    teIndex = d_typ_enum.size();
37
439
    d_typ_enum_map[tn] = teIndex;
38
439
    d_typ_enum.push_back(TypeEnumerator(tn));
39
  }
40
  else
41
  {
42
2809
    teIndex = it->second;
43
  }
44
8038
  while (index >= d_enum_terms[tn].size())
45
  {
46
2395
    if (d_typ_enum[teIndex].isFinished())
47
    {
48
      return Node::null();
49
    }
50
2395
    d_enum_terms[tn].push_back(*d_typ_enum[teIndex]);
51
2395
    ++d_typ_enum[teIndex];
52
  }
53
3248
  return d_enum_terms[tn][index];
54
}
55
56
bool TermEnumeration::getDomain(TypeNode tn, std::vector<Node>& dom)
57
{
58
  if (!d_qbi || !d_qbi->mayComplete(tn))
59
  {
60
    return false;
61
  }
62
  Node curre;
63
  unsigned counter = 0;
64
  do
65
  {
66
    curre = getEnumerateTerm(tn, counter);
67
    counter++;
68
    if (!curre.isNull())
69
    {
70
      dom.push_back(curre);
71
    }
72
  } while (!curre.isNull());
73
  return true;
74
}
75
76
} /* CVC4::theory::quantifiers namespace */
77
} /* CVC4::theory namespace */
78
26676
} /* CVC4 namespace */