blob: 1a066a886a5e097be544e7e2afec4fa5dbb8fe7f (
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
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
|
/********************* */
/*! \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 "options/quantifiers_options.h"
#include "theory/quantifiers/term_util.h"
#include "theory/rewriter.h"
using namespace CVC4::kind;
namespace CVC4 {
namespace theory {
namespace quantifiers {
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::mayComplete(TypeNode tn)
{
std::unordered_map<TypeNode, bool, TypeNodeHashFunction>::iterator it =
d_may_complete.find(tn);
if (it == d_may_complete.end())
{
// cache
bool mc = mayComplete(tn, options::fmfTypeCompletionThresh());
d_may_complete[tn] = mc;
return mc;
}
return it->second;
}
bool TermEnumeration::mayComplete(TypeNode tn, unsigned maxCard)
{
bool mc = false;
if (tn.isClosedEnumerable() && tn.isInterpretedFinite())
{
Cardinality c = tn.getCardinality();
if (!c.isLargeFinite())
{
NodeManager* nm = NodeManager::currentNM();
Node card = nm->mkConst(Rational(c.getFiniteCardinality()));
// check if less than fixed upper bound
Node oth = nm->mkConst(Rational(maxCard));
Node eq = nm->mkNode(LEQ, card, oth);
eq = Rewriter::rewrite(eq);
mc = eq.isConst() && eq.getConst<bool>();
}
}
return mc;
}
bool TermEnumeration::getDomain(TypeNode tn, std::vector<Node>& dom)
{
if (!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;
}
} /* CVC4::theory::quantifiers namespace */
} /* CVC4::theory namespace */
} /* CVC4 namespace */
|
