GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arrays/theory_arrays_rewriter.h Lines: 293 295 99.3 %
Date: 2021-03-22 Branches: 773 1433 53.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_arrays_rewriter.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Clark Barrett, Morgan Deters, Andres Noetzli
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 [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "cvc4_private.h"
19
20
#ifndef CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
21
#define CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
22
23
#include <unordered_map>
24
#include <unordered_set>
25
26
#include "theory/rewriter.h"
27
#include "theory/theory_rewriter.h"
28
#include "theory/type_enumerator.h"
29
30
namespace CVC4 {
31
namespace theory {
32
namespace arrays {
33
34
Node getMostFrequentValue(TNode store);
35
uint64_t getMostFrequentValueCount(TNode store);
36
void setMostFrequentValue(TNode store, TNode value);
37
void setMostFrequentValueCount(TNode store, uint64_t count);
38
39
22396
static inline Node mkEqNode(Node a, Node b) {
40
22396
  return a.eqNode(b);
41
}
42
43
17987
class TheoryArraysRewriter : public TheoryRewriter
44
{
45
8114
  static Node normalizeConstant(TNode node) {
46
8114
    return normalizeConstant(node, node[1].getType().getCardinality());
47
  }
48
49
 public:
50
  //this function is called by printers when using the option "--model-u-dt-enum"
51
8114
  static Node normalizeConstant(TNode node, Cardinality indexCard) {
52
16228
    TNode store = node[0];
53
16228
    TNode index = node[1];
54
16228
    TNode value = node[2];
55
56
16228
    std::vector<TNode> indices;
57
16228
    std::vector<TNode> elements;
58
59
    // Normal form for nested stores is just ordering by index - but also need
60
    // to check if we are writing to default value
61
62
    // Go through nested stores looking for where to insert index
63
    // Also check whether we are replacing an existing store
64
16228
    TNode replacedValue;
65
8114
    unsigned depth = 1;
66
8114
    unsigned valCount = 1;
67
9640
    while (store.getKind() == kind::STORE) {
68
2844
      if (index == store[1]) {
69
158
        replacedValue = store[2];
70
158
        store = store[0];
71
158
        break;
72
      }
73
2686
      else if (!(index < store[1])) {
74
1923
        break;
75
      }
76
763
      if (value == store[2]) {
77
140
        valCount += 1;
78
      }
79
763
      depth += 1;
80
763
      indices.push_back(store[1]);
81
763
      elements.push_back(store[2]);
82
763
      store = store[0];
83
    }
84
16228
    Node n = store;
85
86
    // Get the default value at the bottom of the nested stores
87
18938
    while (store.getKind() == kind::STORE) {
88
5412
      if (value == store[2]) {
89
654
        valCount += 1;
90
      }
91
5412
      depth += 1;
92
5412
      store = store[0];
93
    }
94
8114
    Assert(store.getKind() == kind::STORE_ALL);
95
16228
    ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
96
16228
    Node defaultValue = storeAll.getValue();
97
8114
    NodeManager* nm = NodeManager::currentNM();
98
99
    // Check if we are writing to default value - if so the store
100
    // to index can be ignored
101
8114
    if (value == defaultValue) {
102
345
      if (replacedValue.isNull()) {
103
        // Quick exit - if writing to default value and nothing was
104
        // replaced, we can just return node[0]
105
331
        return node[0];
106
      }
107
      // else rebuild the store without the replaced write and then exit
108
    }
109
    else {
110
7769
      n = nm->mkNode(kind::STORE, n, index, value);
111
    }
112
113
    // Build the rest of the store after inserting/deleting
114
9117
    while (!indices.empty()) {
115
667
      n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
116
667
      indices.pop_back();
117
667
      elements.pop_back();
118
    }
119
120
    // Ready to exit if write was to the default value (see previous comment)
121
7783
    if (value == defaultValue) {
122
14
      return n;
123
    }
124
125
7769
    if (indexCard.isInfinite()) {
126
6189
      return n;
127
    }
128
129
    // When index sort is finite, we have to check whether there is any value
130
    // that is written to more than the default value.  If so, it must become
131
    // the new default value
132
133
3160
    TNode mostFrequentValue;
134
1580
    unsigned mostFrequentValueCount = 0;
135
1580
    store = node[0];
136
1580
    if (store.getKind() == kind::STORE) {
137
845
      mostFrequentValue = getMostFrequentValue(store);
138
845
      mostFrequentValueCount = getMostFrequentValueCount(store);
139
    }
140
141
    // Compute the most frequently written value for n
142
2611
    if (valCount > mostFrequentValueCount ||
143
531
        (valCount == mostFrequentValueCount && value < mostFrequentValue)) {
144
1031
      mostFrequentValue = value;
145
1031
      mostFrequentValueCount = valCount;
146
    }
147
148
    // Need to make sure the default value count is larger, or the same and the default value is expression-order-less-than nextValue
149
1580
    Cardinality::CardinalityComparison compare = indexCard.compare(mostFrequentValueCount + depth);
150
1580
    Assert(compare != Cardinality::UNKNOWN);
151
3072
    if (compare == Cardinality::GREATER ||
152
414
        (compare == Cardinality::EQUAL && (defaultValue < mostFrequentValue))) {
153
1492
      return n;
154
    }
155
156
    // Bad case: have to recompute value counts and/or possibly switch out
157
    // default value
158
88
    store = n;
159
176
    std::unordered_set<TNode, TNodeHashFunction> indexSet;
160
176
    std::unordered_map<TNode, unsigned, TNodeHashFunction> elementsMap;
161
88
    std::unordered_map<TNode, unsigned, TNodeHashFunction>::iterator it;
162
    unsigned count;
163
88
    unsigned max = 0;
164
176
    TNode maxValue;
165
348
    while (store.getKind() == kind::STORE) {
166
130
      indices.push_back(store[1]);
167
130
      indexSet.insert(store[1]);
168
130
      elements.push_back(store[2]);
169
130
      it = elementsMap.find(store[2]);
170
130
      if (it != elementsMap.end()) {
171
30
        (*it).second = (*it).second + 1;
172
30
        count = (*it).second;
173
      }
174
      else {
175
100
        elementsMap[store[2]] = 1;
176
100
        count = 1;
177
      }
178
385
      if (count > max ||
179
142
          (count == max && store[2] < maxValue)) {
180
125
        max = count;
181
125
        maxValue = store[2];
182
      }
183
130
      store = store[0];
184
    }
185
186
88
    Assert(depth == indices.size());
187
88
    compare = indexCard.compare(max + depth);
188
88
    Assert(compare != Cardinality::UNKNOWN);
189
88
    if (compare == Cardinality::GREATER ||
190
71
        (compare == Cardinality::EQUAL && (defaultValue < maxValue))) {
191
      Assert(!replacedValue.isNull() && mostFrequentValue == replacedValue);
192
      return n;
193
    }
194
195
    // Out of luck: have to swap out default value
196
197
    // Enumerate values from index type into newIndices and sort
198
176
    std::vector<Node> newIndices;
199
176
    TypeEnumerator te(index.getType());
200
88
    bool needToSort = false;
201
88
    unsigned numTe = 0;
202
536
    while (!te.isFinished() && (!indexCard.isFinite() || numTe<indexCard.getFiniteCardinality().toUnsignedInt())) {
203
224
      if (indexSet.find(*te) == indexSet.end()) {
204
94
        if (!newIndices.empty() && (!(newIndices.back() < (*te)))) {
205
6
          needToSort = true;
206
        }
207
94
        newIndices.push_back(*te);
208
      }
209
224
      ++numTe;
210
224
      ++te;
211
    }
212
88
    Assert(indexCard.compare(newIndices.size() + depth) == Cardinality::EQUAL);
213
88
    if (needToSort) {
214
4
      std::sort(newIndices.begin(), newIndices.end());
215
    }
216
217
88
    n = nm->mkConst(ArrayStoreAll(node.getType(), maxValue));
218
88
    std::vector<Node>::iterator itNew = newIndices.begin(), it_end = newIndices.end();
219
536
    while (itNew != it_end || !indices.empty()) {
220
224
      if (itNew != it_end && (indices.empty() || (*itNew) < indices.back())) {
221
94
        n = nm->mkNode(kind::STORE, n, (*itNew), defaultValue);
222
94
        ++itNew;
223
      }
224
130
      else if (itNew == it_end || indices.back() < (*itNew)) {
225
130
        if (elements.back() != maxValue) {
226
12
          n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
227
        }
228
130
        indices.pop_back();
229
130
        elements.pop_back();
230
      }
231
    }
232
88
    return n;
233
  }
234
235
 public:
236
59856
  RewriteResponse postRewrite(TNode node) override
237
  {
238
59856
    Trace("arrays-postrewrite") << "Arrays::postRewrite start " << node << std::endl;
239
59856
    switch (node.getKind()) {
240
22392
      case kind::SELECT: {
241
22392
        TNode store = node[0];
242
22392
        TNode index = node[1];
243
22392
        Node n;
244
        bool val;
245
23640
        while (store.getKind() == kind::STORE) {
246
8765
          if (index == store[1]) {
247
39
            val = true;
248
          }
249
8726
          else if (index.isConst() && store[1].isConst()) {
250
294
            val = false;
251
          }
252
          else {
253
8432
            n = Rewriter::rewrite(mkEqNode(store[1], index));
254
8432
            if (n.getKind() != kind::CONST_BOOLEAN) {
255
8102
              break;
256
            }
257
330
            val = n.getConst<bool>();
258
          }
259
663
          if (val) {
260
            // select(store(a,i,v),j) = v if i = j
261
39
            Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << store[2] << std::endl;
262
39
            return RewriteResponse(REWRITE_DONE, store[2]);
263
          }
264
          // select(store(a,i,v),j) = select(a,j) if i /= j
265
624
          store = store[0];
266
        }
267
22353
        if (store.getKind() == kind::STORE_ALL) {
268
          // select(store_all(v),i) = v
269
522
          ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
270
261
          n = storeAll.getValue();
271
261
          Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n << std::endl;
272
261
          Assert(n.isConst());
273
261
          return RewriteResponse(REWRITE_DONE, n);
274
        }
275
22092
        else if (store != node[0]) {
276
64
          n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index);
277
64
          Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n << std::endl;
278
64
          return RewriteResponse(REWRITE_DONE, n);
279
        }
280
22028
        break;
281
      }
282
17312
      case kind::STORE: {
283
17312
        TNode store = node[0];
284
17312
        TNode value = node[2];
285
        // store(a,i,select(a,i)) = a
286
36104
        if (value.getKind() == kind::SELECT &&
287
53366
            value[0] == store &&
288
18002
            value[1] == node[1]) {
289
40
          Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << store << std::endl;
290
40
          return RewriteResponse(REWRITE_DONE, store);
291
        }
292
17272
        TNode index = node[1];
293
17272
        if (store.isConst() && index.isConst() && value.isConst()) {
294
          // normalize constant
295
16228
          Node n = normalizeConstant(node);
296
8114
          Assert(n.isConst());
297
8114
          Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n << std::endl;
298
8114
          return RewriteResponse(REWRITE_DONE, n);
299
        }
300
9158
        if (store.getKind() == kind::STORE) {
301
          // store(store(a,i,v),j,w)
302
          bool val;
303
6146
          if (index == store[1]) {
304
20
            val = true;
305
          }
306
6126
          else if (index.isConst() && store[1].isConst()) {
307
398
            val = false;
308
          }
309
          else {
310
9332
            Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index));
311
5728
            if (eqRewritten.getKind() != kind::CONST_BOOLEAN) {
312
2124
              Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << node << std::endl;
313
2124
              return RewriteResponse(REWRITE_DONE, node);
314
            }
315
3604
            val = eqRewritten.getConst<bool>();
316
          }
317
4022
          NodeManager* nm = NodeManager::currentNM();
318
4022
          if (val) {
319
            // store(store(a,i,v),i,w) = store(a,i,w)
320
40
            Node result = nm->mkNode(kind::STORE, store[0], index, value);
321
20
            Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << result << std::endl;
322
20
            return RewriteResponse(REWRITE_AGAIN, result);
323
          }
324
4002
          else if (index < store[1]) {
325
            // store(store(a,i,v),j,w) = store(store(a,j,w),i,v)
326
            //    IF i != j and j comes before i in the ordering
327
422
            std::vector<TNode> indices;
328
422
            std::vector<TNode> elements;
329
211
            indices.push_back(store[1]);
330
211
            elements.push_back(store[2]);
331
211
            store = store[0];
332
422
            Node n;
333
2103
            while (store.getKind() == kind::STORE) {
334
1064
              if (index == store[1]) {
335
4
                val = true;
336
              }
337
1060
              else if (index.isConst() && store[1].isConst()) {
338
15
                val = false;
339
              }
340
              else {
341
1045
                n = Rewriter::rewrite(mkEqNode(store[1], index));
342
1045
                if (n.getKind() != kind::CONST_BOOLEAN) {
343
28
                  break;
344
                }
345
1017
                val = n.getConst<bool>();
346
              }
347
1036
              if (val) {
348
4
                store = store[0];
349
4
                break;
350
              }
351
1032
              else if (!(index < store[1])) {
352
86
                break;
353
              }
354
946
              indices.push_back(store[1]);
355
946
              elements.push_back(store[2]);
356
946
              store = store[0];
357
            }
358
450
            if (value.getKind() == kind::SELECT &&
359
675
                value[0] == store &&
360
239
                value[1] == index) {
361
6
              n = store;
362
            }
363
            else {
364
205
              n = nm->mkNode(kind::STORE, store, index, value);
365
            }
366
2525
            while (!indices.empty()) {
367
1157
              n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
368
1157
              indices.pop_back();
369
1157
              elements.pop_back();
370
            }
371
211
            Assert(n != node);
372
211
            Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n << std::endl;
373
211
            return RewriteResponse(REWRITE_AGAIN, n);
374
          }
375
        }
376
6803
        break;
377
      }
378
18868
      case kind::EQUAL:{
379
18868
        if(node[0] == node[1]) {
380
732
          Trace("arrays-postrewrite") << "Arrays::postRewrite returning true" << std::endl;
381
732
          return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
382
        }
383
18136
        else if (node[0].isConst() && node[1].isConst()) {
384
168
          Trace("arrays-postrewrite") << "Arrays::postRewrite returning false" << std::endl;
385
168
          return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false));
386
        }
387
17968
        if (node[0] > node[1]) {
388
6804
          Node newNode = NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
389
3402
          Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << newNode << std::endl;
390
3402
          return RewriteResponse(REWRITE_DONE, newNode);
391
        }
392
14566
        break;
393
      }
394
1284
      default:
395
1284
        break;
396
    }
397
44681
    Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << node << std::endl;
398
44681
    return RewriteResponse(REWRITE_DONE, node);
399
  }
400
401
33236
  RewriteResponse preRewrite(TNode node) override
402
  {
403
33236
    Trace("arrays-prerewrite") << "Arrays::preRewrite start " << node << std::endl;
404
33236
    switch (node.getKind()) {
405
13058
      case kind::SELECT: {
406
13058
        TNode store = node[0];
407
13058
        TNode index = node[1];
408
13058
        Node n;
409
        bool val;
410
17922
        while (store.getKind() == kind::STORE) {
411
7342
          if (index == store[1]) {
412
881
            val = true;
413
          }
414
6461
          else if (index.isConst() && store[1].isConst()) {
415
1732
            val = false;
416
          }
417
          else {
418
4729
            n = Rewriter::rewrite(mkEqNode(store[1], index));
419
4729
            if (n.getKind() != kind::CONST_BOOLEAN) {
420
3997
              break;
421
            }
422
732
            val = n.getConst<bool>();
423
          }
424
3345
          if (val) {
425
            // select(store(a,i,v),j) = v if i = j
426
913
            Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << store[2] << std::endl;
427
913
            return RewriteResponse(REWRITE_AGAIN, store[2]);
428
          }
429
          // select(store(a,i,v),j) = select(a,j) if i /= j
430
2432
          store = store[0];
431
        }
432
12145
        if (store.getKind() == kind::STORE_ALL) {
433
          // select(store_all(v),i) = v
434
792
          ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
435
396
          n = storeAll.getValue();
436
396
          Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << n << std::endl;
437
396
          Assert(n.isConst());
438
396
          return RewriteResponse(REWRITE_DONE, n);
439
        }
440
11749
        else if (store != node[0]) {
441
272
          n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index);
442
272
          Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << n << std::endl;
443
272
          return RewriteResponse(REWRITE_DONE, n);
444
        }
445
11477
        break;
446
      }
447
8754
      case kind::STORE: {
448
8754
        TNode store = node[0];
449
8754
        TNode value = node[2];
450
        // store(a,i,select(a,i)) = a
451
18228
        if (value.getKind() == kind::SELECT &&
452
26976
            value[0] == store &&
453
9108
            value[1] == node[1]) {
454
15
          Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << store << std::endl;
455
15
          return RewriteResponse(REWRITE_AGAIN, store);
456
        }
457
8739
        if (store.getKind() == kind::STORE) {
458
          // store(store(a,i,v),j,w)
459
6873
          TNode index = node[1];
460
          bool val;
461
4001
          if (index == store[1]) {
462
189
            val = true;
463
          }
464
3812
          else if (index.isConst() && store[1].isConst()) {
465
1350
            val = false;
466
          }
467
          else {
468
3998
            Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index));
469
2462
            if (eqRewritten.getKind() != kind::CONST_BOOLEAN) {
470
926
              break;
471
            }
472
1536
            val = eqRewritten.getConst<bool>();
473
          }
474
3075
          NodeManager* nm = NodeManager::currentNM();
475
3075
          if (val) {
476
            // store(store(a,i,v),i,w) = store(a,i,w)
477
406
            Node newNode = nm->mkNode(kind::STORE, store[0], index, value);
478
203
            Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << newNode << std::endl;
479
203
            return RewriteResponse(REWRITE_DONE, newNode);
480
          }
481
        }
482
7610
        break;
483
      }
484
10860
      case kind::EQUAL:{
485
10860
        if(node[0] == node[1]) {
486
825
          Trace("arrays-prerewrite") << "Arrays::preRewrite returning true" << std::endl;
487
825
          return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
488
        }
489
10035
        break;
490
      }
491
564
      default:
492
564
        break;
493
    }
494
495
30612
    Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << node << std::endl;
496
30612
    return RewriteResponse(REWRITE_DONE, node);
497
  }
498
499
  static inline void init() {}
500
  static inline void shutdown() {}
501
502
}; /* class TheoryArraysRewriter */
503
504
}/* CVC4::theory::arrays namespace */
505
}/* CVC4::theory namespace */
506
}/* CVC4 namespace */
507
508
#endif /* CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H */