GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arrays/theory_arrays_type_rules.h Lines: 87 130 66.9 %
Date: 2021-03-22 Branches: 171 652 26.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_arrays_type_rules.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Clark Barrett, Mathias Preiner
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 Typing and cardinality rules for the theory of arrays
13
 **
14
 ** Typing and cardinality rules for the theory of arrays.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H
20
#define CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H
21
22
#include "theory/arrays/theory_arrays_rewriter.h" // for array-constant attributes
23
#include "theory/type_enumerator.h"
24
25
namespace CVC4 {
26
namespace theory {
27
namespace arrays {
28
29
struct ArraySelectTypeRule {
30
17948
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
31
  {
32
17948
    Assert(n.getKind() == kind::SELECT);
33
35896
    TypeNode arrayType = n[0].getType(check);
34
17948
    if( check ) {
35
17948
      if(!arrayType.isArray()) {
36
        throw TypeCheckingExceptionPrivate(n, "array select operating on non-array");
37
      }
38
35896
      TypeNode indexType = n[1].getType(check);
39
17948
      if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){
40
        throw TypeCheckingExceptionPrivate(n, "array select not indexed with correct type for array");
41
      }
42
    }
43
35896
    return arrayType.getArrayConstituentType();
44
  }
45
};/* struct ArraySelectTypeRule */
46
47
struct ArrayStoreTypeRule {
48
12643
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
49
  {
50
12643
    if (n.getKind() == kind::STORE) {
51
23994
      TypeNode arrayType = n[0].getType(check);
52
11997
      if( check ) {
53
11997
        if(!arrayType.isArray()) {
54
          throw TypeCheckingExceptionPrivate(n, "array store operating on non-array");
55
        }
56
23994
        TypeNode indexType = n[1].getType(check);
57
23994
        TypeNode valueType = n[2].getType(check);
58
11997
        if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){
59
          throw TypeCheckingExceptionPrivate(n, "array store not indexed with correct type for array");
60
        }
61
11997
        if(!valueType.isSubtypeOf(arrayType.getArrayConstituentType())){
62
          Debug("array-types") << "array type: "<< arrayType.getArrayConstituentType() << std::endl;
63
          Debug("array-types") << "value types: " << valueType << std::endl;
64
          throw TypeCheckingExceptionPrivate(n, "array store not assigned with correct type for array");
65
        }
66
      }
67
11997
      return arrayType;
68
    }
69
    else {
70
646
      Assert(n.getKind() == kind::STORE_ALL);
71
1292
      ArrayStoreAll storeAll = n.getConst<ArrayStoreAll>();
72
646
      return storeAll.getType();
73
    }
74
  }
75
76
8873
  inline static bool computeIsConst(NodeManager* nodeManager, TNode n)
77
  {
78
8873
    Assert(n.getKind() == kind::STORE);
79
17746
    NodeManagerScope nms(nodeManager);
80
81
17746
    TNode store = n[0];
82
17746
    TNode index = n[1];
83
17746
    TNode value = n[2];
84
85
    // A constant must have only constant children and be in normal form
86
    // If any child is non-const, this is not a constant
87
8873
    if (!store.isConst() || !index.isConst() || !value.isConst()) {
88
5352
      return false;
89
    }
90
91
    // Normal form for nested stores is just ordering by index but also need to check that we are not writing
92
    // to default value
93
3521
    if (store.getKind() == kind::STORE && (!(store[1] < index))) {
94
18
      return false;
95
    }
96
97
3503
    unsigned depth = 1;
98
3503
    unsigned valCount = 1;
99
7265
    while (store.getKind() == kind::STORE) {
100
1881
      depth += 1;
101
1881
      if (store[2] == value) {
102
250
        valCount += 1;
103
      }
104
1881
      store = store[0];
105
    }
106
3503
    Assert(store.getKind() == kind::STORE_ALL);
107
7006
    ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
108
7006
    Node defaultValue = storeAll.getValue();
109
3503
    if (value == defaultValue) {
110
20
      return false;
111
    }
112
113
    // Get the cardinality of the index type
114
6966
    Cardinality indexCard = index.getType().getCardinality();
115
116
3483
    if (indexCard.isInfinite()) {
117
2882
      return true;
118
    }
119
120
    // When index sort is finite, we have to check whether there is any value
121
    // that is written to more than the default value.  If so, it is not in
122
    // normal form.
123
124
    // Get the most frequently written value for n[0]
125
1202
    TNode mostFrequentValue;
126
601
    unsigned mostFrequentValueCount = 0;
127
601
    store = n[0];
128
601
    if (store.getKind() == kind::STORE) {
129
269
      mostFrequentValue = getMostFrequentValue(store);
130
269
      mostFrequentValueCount = getMostFrequentValueCount(store);
131
    }
132
133
    // Compute the most frequently written value for n
134
1044
    if (valCount > mostFrequentValueCount ||
135
163
        (valCount == mostFrequentValueCount && value < mostFrequentValue)) {
136
443
      mostFrequentValue = value;
137
443
      mostFrequentValueCount = valCount;
138
    }
139
140
    // Need to make sure the default value count is larger, or the same and the default value is expression-order-less-than nextValue
141
601
    Cardinality::CardinalityComparison compare = indexCard.compare(mostFrequentValueCount + depth);
142
601
    Assert(compare != Cardinality::UNKNOWN);
143
605
    if (compare == Cardinality::LESS ||
144
184
        (compare == Cardinality::EQUAL && (!(defaultValue < mostFrequentValue)))) {
145
4
      return false;
146
    }
147
597
    setMostFrequentValue(n, mostFrequentValue);
148
597
    setMostFrequentValueCount(n, mostFrequentValueCount);
149
597
    return true;
150
  }
151
152
};/* struct ArrayStoreTypeRule */
153
154
struct ArrayTableFunTypeRule {
155
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
156
  {
157
    Assert(n.getKind() == kind::ARR_TABLE_FUN);
158
    TypeNode arrayType = n[0].getType(check);
159
    if( check ) {
160
      if(!arrayType.isArray()) {
161
        throw TypeCheckingExceptionPrivate(n, "array table fun arg 0 is non-array");
162
      }
163
      TypeNode arrType2 = n[1].getType(check);
164
      if(!arrayType.isArray()) {
165
        throw TypeCheckingExceptionPrivate(n, "array table fun arg 1 is non-array");
166
      }
167
      TypeNode indexType = n[2].getType(check);
168
      if(!indexType.isComparableTo(arrayType.getArrayIndexType())){
169
        throw TypeCheckingExceptionPrivate(n, "array table fun arg 2 does not match type of array");
170
      }
171
      indexType = n[3].getType(check);
172
      if(!indexType.isComparableTo(arrayType.getArrayIndexType())){
173
        throw TypeCheckingExceptionPrivate(n, "array table fun arg 3 does not match type of array");
174
      }
175
    }
176
    return arrayType.getArrayIndexType();
177
  }
178
};/* struct ArrayTableFunTypeRule */
179
180
struct ArrayLambdaTypeRule {
181
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
182
  {
183
    Assert(n.getKind() == kind::ARRAY_LAMBDA);
184
    TypeNode lamType = n[0].getType(check);
185
    if( check ) {
186
      if(n[0].getKind() != kind::LAMBDA) {
187
        throw TypeCheckingExceptionPrivate(n, "array lambda arg is non-lambda");
188
      }
189
    }
190
    if(lamType.getNumChildren() != 2) {
191
      throw TypeCheckingExceptionPrivate(n, "array lambda arg is not unary lambda");
192
    }
193
    return nodeManager->mkArrayType(lamType[0], lamType[1]);
194
  }
195
};/* struct ArrayLambdaTypeRule */
196
197
struct ArraysProperties {
198
292
  inline static Cardinality computeCardinality(TypeNode type) {
199
292
    Assert(type.getKind() == kind::ARRAY_TYPE);
200
201
584
    Cardinality indexCard = type[0].getCardinality();
202
584
    Cardinality valueCard = type[1].getCardinality();
203
204
584
    return valueCard ^ indexCard;
205
  }
206
207
  inline static bool isWellFounded(TypeNode type) {
208
    return type[0].isWellFounded() && type[1].isWellFounded();
209
  }
210
211
19
  inline static Node mkGroundTerm(TypeNode type) {
212
19
    return *TypeEnumerator(type);
213
  }
214
};/* struct ArraysProperties */
215
216
217
struct ArrayPartialSelectTypeRule {
218
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
219
  {
220
    Assert(n.getKind() == kind::PARTIAL_SELECT_0
221
           || n.getKind() == kind::PARTIAL_SELECT_1);
222
    return nodeManager->integerType();
223
  }
224
};/* struct ArrayPartialSelectTypeRule */
225
226
struct ArrayEqRangeTypeRule
227
{
228
33
  inline static TypeNode computeType(NodeManager* nodeManager,
229
                                     TNode n,
230
                                     bool check)
231
  {
232
33
    Assert(n.getKind() == kind::EQ_RANGE);
233
33
    if (check)
234
    {
235
66
      TypeNode n0_type = n[0].getType(check);
236
66
      TypeNode n1_type = n[1].getType(check);
237
33
      if (!n0_type.isArray())
238
      {
239
        throw TypeCheckingExceptionPrivate(
240
            n, "first operand of eqrange is not an array");
241
      }
242
33
      if (!n1_type.isArray())
243
      {
244
        throw TypeCheckingExceptionPrivate(
245
            n, "second operand of eqrange is not an array");
246
      }
247
33
      if (n0_type != n1_type)
248
      {
249
        throw TypeCheckingExceptionPrivate(n, "array types do not match");
250
      }
251
66
      TypeNode indexType = n0_type.getArrayIndexType();
252
66
      TypeNode indexRangeType1 = n[2].getType(check);
253
66
      TypeNode indexRangeType2 = n[3].getType(check);
254
33
      if (!indexRangeType1.isSubtypeOf(indexType))
255
      {
256
        throw TypeCheckingExceptionPrivate(
257
            n, "eqrange lower index type does not match array index type");
258
      }
259
33
      if (!indexRangeType2.isSubtypeOf(indexType))
260
      {
261
        throw TypeCheckingExceptionPrivate(
262
            n, "eqrange upper index type does not match array index type");
263
      }
264
74
      if (!indexType.isBitVector() && !indexType.isFloatingPoint()
265
41
          && !indexType.isInteger() && !indexType.isReal())
266
      {
267
        throw TypeCheckingExceptionPrivate(
268
            n,
269
            "eqrange only supports bit-vectors, floating-points, integers, and "
270
            "reals as index type");
271
      }
272
    }
273
33
    return nodeManager->booleanType();
274
  }
275
}; /* struct ArrayEqRangeTypeRule */
276
277
}/* CVC4::theory::arrays namespace */
278
}/* CVC4::theory namespace */
279
}/* CVC4 namespace */
280
281
#endif /* CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H */