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
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
/*
* This file is part of the source code of the software program
* Vampire. It is protected by applicable
* copyright laws.
*
* This source code is distributed under the licence found here
* https://vprover.github.io/license.html
* and in the source directory
*/
/**
* @file Sorts.cpp
* Implements class Sorts for handling collections of sorts.
*/
#include "OperatorType.hpp"
#include "Term.hpp"
#include "TermIterators.hpp"
using namespace std;
using namespace Kernel;
/**
* Pre-initialise an OperatorKey.
*
* If @c sorts is is NULL, all arguments will be initialized by the default sort,
* otherwise, by sorts from the array @c sorts
* @author Andrei Voronkov
*/
OperatorType::OperatorKey* OperatorType::setupKey(unsigned arity, const TermList* sorts)
{
OperatorKey* key = OperatorKey::allocate(arity+1);
if (!sorts) {
// initialise all argument types to the default type
for (unsigned i=0; i < arity; i++) {
(*key)[i] = AtomicSort::defaultSort();
}
} else {
// initialise all the argument types to those taken from sorts
for (unsigned i = 0; i < arity; i++) {
ASS(sorts[i].isVar() || sorts[i].term()->isSort());
(*key)[i] = sorts[i];
}
}
return key;
}
/**
* Pre-initialise an OperatorKey from an initializer list of sorts.
*/
OperatorType::OperatorKey* OperatorType::setupKey(std::initializer_list<TermList> sorts)
{
OperatorKey* key = OperatorKey::allocate(sorts.size()+1);
// initialise all the argument types to those taken from sorts
unsigned i = 0;
for (auto sort : sorts) {
ASS(sort.isVar() || sort.term()->isSort());
(*key)[i++] = sort;
}
return key;
}
/**
* Pre-initialise an OperatorKey from using a uniform range.
*/
OperatorType::OperatorKey* OperatorType::setupKeyUniformRange(unsigned arity, TermList argsSort)
{
ASS(argsSort.isVar() || argsSort.term()->isSort());
OperatorKey* key = OperatorKey::allocate(arity+1);
for (unsigned i=0; i < arity; i++) {
(*key)[i] = argsSort;
}
return key;
}
OperatorType::OperatorTypes& OperatorType::operatorTypes() {
struct DeletingOperatorTypes : public OperatorType::OperatorTypes {
~DeletingOperatorTypes() {
deleteAll();
}
};
static DeletingOperatorTypes _operatorTypes;
return _operatorTypes;
}
/**
* Check if OperatorType corresponding to the given key
* already exists. If so return it, if not create new,
* store it for future retrieval and return it.
*
* Release key if not needed.
*/
OperatorType* OperatorType::getTypeFromKey(OperatorKey* key, unsigned taArity)
{
/*
cout << "getTypeFromKey(" << key->length() << "): ";
for (unsigned i = 0; i < key->length(); i++) {
cout << (((*key)[i] == PREDICATE_FLAG) ? "FFFF" : env.sorts->sortName((*key)[i])) << ",";
}
*/
OperatorType* resultType = new OperatorType(key, taArity);
if (operatorTypes().find(resultType, resultType)) {
key->deallocate();
//cout << " Found " + resultType->toString() << endl;
return resultType;
}
/**
* This check is to make sure that @b taArity is properly set, leaving no variables in
* @b key unbound, as that would make those variables fixed which is very inconvenient,
* for example, if we want to rename variables anywhere.
*/
#if VDEBUG
for (unsigned i = 0; i < key->length(); i++) {
if ((*key)[i].isNonEmpty()) {
ASS_REP(iterTraits(VariableIterator((*key)[i])).all([&](TermList var) {
return var.var() < taArity;
}), "Unbound variable in type " + resultType->toString());
}
}
#endif
operatorTypes().insert(resultType);
//cout << " Created new " + resultType->toString() << endl;
return resultType;
}
/**
* Return the string representation of arguments of a non-atomic
* functional or a predicate sort in the form (t1 * ... * tn)
* @since 04/05/2013 bug fix (comma was used instead of *)
* @author Andrei Voronkov
*/
std::string OperatorType::argsToString() const
{
unsigned ar = arity();
ASS(ar);
std::string res = ar > 1 ? "(" : "";
for (unsigned i = _typeArgsArity; i < ar; i++) {
res += arg(i).toString();
if (i != ar-1) {
res += " * ";
}
}
res += ar > 1 ? ")" : "";
return res;
} // OperatorType::argsToString()
/**
* Return the TPTP string representation of the OpertorType.
*/
std::string OperatorType::toString() const
{
std::string res;
bool bracket = false;
if(_typeArgsArity){
res = "!>[";
for(unsigned i = 0; i < _typeArgsArity; i++){
if(i != 0){ res += ", "; }
res+= quantifiedVar(i).toString() + ": $tType";
}
res += "]:";
bracket = true;
}
return res + (bracket ? "(" : "") + (arity() - numTypeArguments() ? argsToString() + " > " : "") +
(isPredicateType() ? "$o" : result().toString()) + (bracket ? ")" : "");
}
/**
* True if all arguments of this type have sort @c str
* and so is the result sort if we are talking about a function type.
* @author Andrei Voronkov
*/
bool OperatorType::isSingleSortType(TermList srt) const
{
unsigned len = arity();
for (unsigned i = 0; i <len; i++) {
if (arg(i) != srt) { //term comparison with != should be OK on the basis that both are shared terms
return false;
}
}
if (isFunctionType() && result() != srt) {
return false;
}
return true;
} // isSingleSortType