blob: 2945750c12651190c5020e0df15822c40aced279 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
|
/********************* */
/*! \file term_enumeration.cpp
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
** in the top-level source directory and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief Implementation of term enumeration utility
**/
#include "theory/quantifiers/term_enumeration.h"
#include "theory/quantifiers/quant_bound_inference.h"
using namespace CVC5::kind;
namespace CVC5 {
namespace theory {
namespace quantifiers {
TermEnumeration::TermEnumeration(QuantifiersBoundInference* qbi) : d_qbi(qbi) {}
Node TermEnumeration::getEnumerateTerm(TypeNode tn, unsigned index)
{
Trace("term-db-enum") << "Get enumerate term " << tn << " " << index
<< std::endl;
std::unordered_map<TypeNode, size_t, TypeNodeHashFunction>::iterator it =
d_typ_enum_map.find(tn);
size_t teIndex;
if (it == d_typ_enum_map.end())
{
teIndex = d_typ_enum.size();
d_typ_enum_map[tn] = teIndex;
d_typ_enum.push_back(TypeEnumerator(tn));
}
else
{
teIndex = it->second;
}
while (index >= d_enum_terms[tn].size())
{
if (d_typ_enum[teIndex].isFinished())
{
return Node::null();
}
d_enum_terms[tn].push_back(*d_typ_enum[teIndex]);
++d_typ_enum[teIndex];
}
return d_enum_terms[tn][index];
}
bool TermEnumeration::getDomain(TypeNode tn, std::vector<Node>& dom)
{
if (!d_qbi || !d_qbi->mayComplete(tn))
{
return false;
}
Node curre;
unsigned counter = 0;
do
{
curre = getEnumerateTerm(tn, counter);
counter++;
if (!curre.isNull())
{
dom.push_back(curre);
}
} while (!curre.isNull());
return true;
}
} // namespace quantifiers
} // namespace theory
} // namespace CVC5
|
