blob: 58558d302c1430b7b40bf4f81f3d043b1ecbdc8a (
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
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
|
/********************* */
/*! \file term_enumeration.cpp
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 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/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::isClosedEnumerableType(TypeNode tn)
{
std::unordered_map<TypeNode, bool, TypeNodeHashFunction>::iterator it =
d_typ_closed_enum.find(tn);
if (it == d_typ_closed_enum.end())
{
d_typ_closed_enum[tn] = true;
bool ret = true;
if (tn.isArray() || tn.isSort() || tn.isCodatatype() || tn.isFunction())
{
ret = false;
}
else if (tn.isSet())
{
ret = isClosedEnumerableType(tn.getSetElementType());
}
else if (tn.isDatatype())
{
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
for (unsigned i = 0; i < dt.getNumConstructors(); i++)
{
for (unsigned j = 0; j < dt[i].getNumArgs(); j++)
{
TypeNode ctn = TypeNode::fromType(dt[i][j].getRangeType());
if (tn != ctn && !isClosedEnumerableType(ctn))
{
ret = false;
break;
}
}
if (!ret)
{
break;
}
}
}
// other parametric sorts go here
d_typ_closed_enum[tn] = ret;
return ret;
}
else
{
return it->second;
}
}
// checks whether a type is closed enumerable and is reasonably small enough (<1000)
// such that all of its domain elements can be enumerated
bool TermEnumeration::mayComplete(TypeNode tn)
{
std::unordered_map<TypeNode, bool, TypeNodeHashFunction>::iterator it =
d_may_complete.find(tn);
if (it == d_may_complete.end())
{
bool mc = false;
if (isClosedEnumerableType(tn) && tn.getCardinality().isFinite()
&& !tn.getCardinality().isLargeFinite())
{
Node card = NodeManager::currentNM()->mkConst(
Rational(tn.getCardinality().getFiniteCardinality()));
Node oth = NodeManager::currentNM()->mkConst(Rational(1000));
Node eq = NodeManager::currentNM()->mkNode(LEQ, card, oth);
eq = Rewriter::rewrite(eq);
mc = eq.isConst() && eq.getConst<bool>();
}
d_may_complete[tn] = mc;
return mc;
}
else
{
return it->second;
}
}
} /* CVC4::theory::quantifiers namespace */
} /* CVC4::theory namespace */
} /* CVC4 namespace */
|
