GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arrays/theory_arrays.cpp Lines: 907 1245 72.9 %
Date: 2021-03-22 Branches: 2426 6641 36.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_arrays.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Clark Barrett, Andrew Reynolds, Morgan Deters
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 Implementation of the theory of arrays.
13
 **
14
 ** Implementation of the theory of arrays.
15
 **/
16
17
#include "theory/arrays/theory_arrays.h"
18
19
#include <map>
20
#include <memory>
21
22
#include "expr/kind.h"
23
#include "expr/node_algorithm.h"
24
#include "expr/proof_checker.h"
25
#include "options/arrays_options.h"
26
#include "options/smt_options.h"
27
#include "smt/logic_exception.h"
28
#include "smt/smt_statistics_registry.h"
29
#include "theory/arrays/skolem_cache.h"
30
#include "theory/arrays/theory_arrays_rewriter.h"
31
#include "theory/decision_manager.h"
32
#include "theory/rewriter.h"
33
#include "theory/theory_model.h"
34
#include "theory/trust_substitutions.h"
35
#include "theory/valuation.h"
36
37
using namespace std;
38
39
namespace CVC4 {
40
namespace theory {
41
namespace arrays {
42
43
// These are the options that produce the best empirical results on QF_AX benchmarks.
44
// eagerLemmas = true
45
// eagerIndexSplitting = false
46
47
// Use static configuration of options for now
48
const bool d_ccStore = false;
49
  //const bool d_eagerLemmas = false;
50
const bool d_preprocess = true;
51
const bool d_solveWrite = true;
52
const bool d_solveWrite2 = false;
53
  // These are now options
54
  //const bool d_propagateLemmas = true;
55
  //bool d_useNonLinearOpt = true;
56
  //bool d_eagerIndexSplitting = false;
57
58
8995
TheoryArrays::TheoryArrays(context::Context* c,
59
                           context::UserContext* u,
60
                           OutputChannel& out,
61
                           Valuation valuation,
62
                           const LogicInfo& logicInfo,
63
                           ProofNodeManager* pnm,
64
8995
                           std::string name)
65
    : Theory(THEORY_ARRAYS, c, u, out, valuation, logicInfo, pnm, name),
66
17990
      d_numRow(name + "theory::arrays::number of Row lemmas", 0),
67
17990
      d_numExt(name + "theory::arrays::number of Ext lemmas", 0),
68
17990
      d_numProp(name + "theory::arrays::number of propagations", 0),
69
17990
      d_numExplain(name + "theory::arrays::number of explanations", 0),
70
17990
      d_numNonLinear(name + "theory::arrays::number of calls to setNonLinear",
71
                     0),
72
      d_numSharedArrayVarSplits(
73
17990
          name + "theory::arrays::number of shared array var splits", 0),
74
      d_numGetModelValSplits(
75
17990
          name + "theory::arrays::number of getModelVal splits", 0),
76
      d_numGetModelValConflicts(
77
17990
          name + "theory::arrays::number of getModelVal conflicts", 0),
78
      d_numSetModelValSplits(
79
17990
          name + "theory::arrays::number of setModelVal splits", 0),
80
      d_numSetModelValConflicts(
81
17990
          name + "theory::arrays::number of setModelVal conflicts", 0),
82
17990
      d_ppEqualityEngine(u, name + "theory::arrays::pp", true),
83
      d_ppFacts(u),
84
      d_state(c, u, valuation),
85
      d_im(*this, d_state, pnm),
86
      d_literalsToPropagate(c),
87
      d_literalsToPropagateIndex(c, 0),
88
      d_isPreRegistered(c),
89
17990
      d_mayEqualEqualityEngine(c, name + "theory::arrays::mayEqual", true),
90
      d_notify(*this),
91
      d_backtracker(c),
92
      d_infoMap(c, &d_backtracker, name),
93
      d_mergeQueue(c),
94
      d_mergeInProgress(false),
95
      d_RowQueue(c),
96
      d_RowAlreadyAdded(u),
97
      d_sharedArrays(c),
98
      d_sharedOther(c),
99
      d_sharedTerms(c, false),
100
      d_reads(c),
101
      d_constReadsList(c),
102
8995
      d_constReadsContext(new context::Context()),
103
      d_contextPopper(c, d_constReadsContext),
104
      d_skolemIndex(c, 0),
105
      d_decisionRequests(c),
106
      d_permRef(c),
107
      d_modelConstraints(c),
108
      d_lemmasSaved(c),
109
      d_defValues(c),
110
8995
      d_readTableContext(new context::Context()),
111
      d_arrayMerges(c),
112
      d_inCheckModel(false),
113
8995
      d_dstrat(new TheoryArraysDecisionStrategy(this)),
114
251860
      d_dstratInit(false)
115
{
116
8995
  smtStatisticsRegistry()->registerStat(&d_numRow);
117
8995
  smtStatisticsRegistry()->registerStat(&d_numExt);
118
8995
  smtStatisticsRegistry()->registerStat(&d_numProp);
119
8995
  smtStatisticsRegistry()->registerStat(&d_numExplain);
120
8995
  smtStatisticsRegistry()->registerStat(&d_numNonLinear);
121
8995
  smtStatisticsRegistry()->registerStat(&d_numSharedArrayVarSplits);
122
8995
  smtStatisticsRegistry()->registerStat(&d_numGetModelValSplits);
123
8995
  smtStatisticsRegistry()->registerStat(&d_numGetModelValConflicts);
124
8995
  smtStatisticsRegistry()->registerStat(&d_numSetModelValSplits);
125
8995
  smtStatisticsRegistry()->registerStat(&d_numSetModelValConflicts);
126
127
8995
  d_true = NodeManager::currentNM()->mkConst<bool>(true);
128
8995
  d_false = NodeManager::currentNM()->mkConst<bool>(false);
129
130
  // The preprocessing congruence kinds
131
8995
  d_ppEqualityEngine.addFunctionKind(kind::SELECT);
132
8995
  d_ppEqualityEngine.addFunctionKind(kind::STORE);
133
134
8995
  ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
135
8995
  if (pc != nullptr)
136
  {
137
962
    d_pchecker.registerTo(pc);
138
  }
139
  // indicate we are using the default theory state object, and the arrays
140
  // inference manager
141
8995
  d_theoryState = &d_state;
142
8995
  d_inferManager = &d_im;
143
8995
}
144
145
26976
TheoryArrays::~TheoryArrays() {
146
8992
  vector<CTNodeList*>::iterator it = d_readBucketAllocations.begin(), iend = d_readBucketAllocations.end();
147
8992
  for (; it != iend; ++it) {
148
    (*it)->deleteSelf();
149
  }
150
8992
  delete d_readTableContext;
151
8992
  CNodeNListMap::iterator it2 = d_constReads.begin();
152
10270
  for( ; it2 != d_constReads.end(); ++it2 ) {
153
639
    it2->second->deleteSelf();
154
  }
155
8992
  delete d_constReadsContext;
156
8992
  smtStatisticsRegistry()->unregisterStat(&d_numRow);
157
8992
  smtStatisticsRegistry()->unregisterStat(&d_numExt);
158
8992
  smtStatisticsRegistry()->unregisterStat(&d_numProp);
159
8992
  smtStatisticsRegistry()->unregisterStat(&d_numExplain);
160
8992
  smtStatisticsRegistry()->unregisterStat(&d_numNonLinear);
161
8992
  smtStatisticsRegistry()->unregisterStat(&d_numSharedArrayVarSplits);
162
8992
  smtStatisticsRegistry()->unregisterStat(&d_numGetModelValSplits);
163
8992
  smtStatisticsRegistry()->unregisterStat(&d_numGetModelValConflicts);
164
8992
  smtStatisticsRegistry()->unregisterStat(&d_numSetModelValSplits);
165
8992
  smtStatisticsRegistry()->unregisterStat(&d_numSetModelValConflicts);
166
17984
}
167
168
8995
TheoryRewriter* TheoryArrays::getTheoryRewriter() { return &d_rewriter; }
169
170
8995
bool TheoryArrays::needsEqualityEngine(EeSetupInfo& esi)
171
{
172
8995
  esi.d_notify = &d_notify;
173
8995
  esi.d_name = d_instanceName + "theory::arrays::ee";
174
8995
  return true;
175
}
176
177
8995
void TheoryArrays::finishInit()
178
{
179
8995
  Assert(d_equalityEngine != nullptr);
180
181
  // The kinds we are treating as function application in congruence
182
8995
  d_equalityEngine->addFunctionKind(kind::SELECT);
183
  if (d_ccStore)
184
  {
185
    d_equalityEngine->addFunctionKind(kind::STORE);
186
  }
187
8995
}
188
189
/////////////////////////////////////////////////////////////////////////////
190
// PREPROCESSING
191
/////////////////////////////////////////////////////////////////////////////
192
193
194
3658
bool TheoryArrays::ppDisequal(TNode a, TNode b) {
195
3658
  bool termsExist = d_ppEqualityEngine.hasTerm(a) && d_ppEqualityEngine.hasTerm(b);
196
3658
  Assert(!termsExist || !a.isConst() || !b.isConst() || a == b
197
         || d_ppEqualityEngine.areDisequal(a, b, false));
198
14574
  return ((termsExist && d_ppEqualityEngine.areDisequal(a, b, false)) ||
199
14574
          Rewriter::rewrite(a.eqNode(b)) == d_false);
200
}
201
202
203
1518
Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck)
204
{
205
1518
  if (!solve1) {
206
    return term;
207
  }
208
5786
  if (term[0].getKind() != kind::STORE &&
209
4268
      term[1].getKind() != kind::STORE) {
210
1226
    return term;
211
  }
212
584
  TNode left = term[0];
213
584
  TNode right = term[1];
214
292
  int leftWrites = 0, rightWrites = 0;
215
216
  // Count nested writes
217
584
  TNode e1 = left;
218
1558
  while (e1.getKind() == kind::STORE) {
219
633
    ++leftWrites;
220
633
    e1 = e1[0];
221
  }
222
223
584
  TNode e2 = right;
224
1966
  while (e2.getKind() == kind::STORE) {
225
837
    ++rightWrites;
226
837
    e2 = e2[0];
227
  }
228
229
292
  if (rightWrites > leftWrites) {
230
358
    TNode tmp = left;
231
179
    left = right;
232
179
    right = tmp;
233
179
    int tmpWrites = leftWrites;
234
179
    leftWrites = rightWrites;
235
179
    rightWrites = tmpWrites;
236
  }
237
238
292
  NodeManager* nm = NodeManager::currentNM();
239
292
  if (rightWrites == 0) {
240
197
    if (e1 != e2) {
241
155
      return term;
242
    }
243
    // write(store, index_0, v_0, index_1, v_1, ..., index_n, v_n) = store IFF
244
    //
245
    // read(store, index_n) = v_n &
246
    // index_{n-1} != index_n -> read(store, index_{n-1}) = v_{n-1} &
247
    // (index_{n-2} != index_{n-1} & index_{n-2} != index_n) -> read(store, index_{n-2}) = v_{n-2} &
248
    // ...
249
    // (index_1 != index_2 & ... & index_1 != index_n) -> read(store, index_1) = v_1
250
    // (index_0 != index_1 & index_0 != index_2 & ... & index_0 != index_n) -> read(store, index_0) = v_0
251
84
    TNode write_i, write_j, index_i, index_j;
252
84
    Node conc;
253
84
    NodeBuilder<> result(kind::AND);
254
    int i, j;
255
42
    write_i = left;
256
121
    for (i = leftWrites-1; i >= 0; --i) {
257
79
      index_i = write_i[1];
258
259
      // build: [index_i /= index_n && index_i /= index_(n-1) &&
260
      //         ... && index_i /= index_(i+1)] -> read(store, index_i) = v_i
261
79
      write_j = left;
262
      {
263
158
        NodeBuilder<> hyp(kind::AND);
264
130
        for (j = leftWrites - 1; j > i; --j) {
265
51
          index_j = write_j[1];
266
51
          if (!ppCheck || !ppDisequal(index_i, index_j)) {
267
44
            Node hyp2(index_i.eqNode(index_j));
268
22
            hyp << hyp2.notNode();
269
          }
270
51
          write_j = write_j[0];
271
        }
272
273
158
        Node r1 = nm->mkNode(kind::SELECT, e1, index_i);
274
79
        conc = r1.eqNode(write_i[2]);
275
79
        if (hyp.getNumChildren() != 0) {
276
22
          if (hyp.getNumChildren() == 1) {
277
22
            conc = hyp.getChild(0).impNode(conc);
278
          }
279
          else {
280
            r1 = hyp;
281
            conc = r1.impNode(conc);
282
          }
283
        }
284
285
        // And into result
286
79
        result << conc;
287
288
        // Prepare for next iteration
289
79
        write_i = write_i[0];
290
      }
291
    }
292
42
    Assert(result.getNumChildren() > 0);
293
42
    if (result.getNumChildren() == 1) {
294
15
      return result.getChild(0);
295
    }
296
27
    return result;
297
  }
298
  else {
299
95
    if (!solve2) {
300
95
      return term;
301
    }
302
    // store(...) = store(a,i,v) ==>
303
    // store(store(...),i,select(a,i)) = a && select(store(...),i)=v
304
    Node l = left;
305
    Node tmp;
306
    NodeBuilder<> nb(kind::AND);
307
    while (right.getKind() == kind::STORE) {
308
      tmp = nm->mkNode(kind::SELECT, l, right[1]);
309
      nb << tmp.eqNode(right[2]);
310
      tmp = nm->mkNode(kind::SELECT, right[0], right[1]);
311
      l = nm->mkNode(kind::STORE, l, right[1], tmp);
312
      right = right[0];
313
    }
314
    nb << solveWrite(l.eqNode(right), solve1, solve2, ppCheck);
315
    return nb;
316
  }
317
  Unreachable();
318
  return term;
319
}
320
321
24113
TrustNode TheoryArrays::ppRewrite(TNode term, std::vector<SkolemLemma>& lems)
322
{
323
  // first, see if we need to expand definitions
324
48226
  TrustNode texp = expandDefinition(term);
325
24113
  if (!texp.isNull())
326
  {
327
20
    return texp;
328
  }
329
  if (!d_preprocess)
330
  {
331
    return TrustNode::null();
332
  }
333
24093
  d_ppEqualityEngine.addTerm(term);
334
48186
  Node ret;
335
24093
  switch (term.getKind()) {
336
6693
    case kind::SELECT: {
337
      // select(store(a,i,v),j) = select(a,j)
338
      //    IF i != j
339
6693
      if (term[0].getKind() == kind::STORE && ppDisequal(term[0][1], term[1])) {
340
        ret = NodeBuilder<2>(kind::SELECT) << term[0][0] << term[1];
341
      }
342
6693
      break;
343
    }
344
1774
    case kind::STORE: {
345
      // store(store(a,i,v),j,w) = store(store(a,j,w),i,v)
346
      //    IF i != j and j comes before i in the ordering
347
1774
      if (term[0].getKind() == kind::STORE && (term[1] < term[0][1]) && ppDisequal(term[1],term[0][1])) {
348
        Node inner = NodeBuilder<3>(kind::STORE) << term[0][0] << term[1] << term[2];
349
        Node outer = NodeBuilder<3>(kind::STORE) << inner << term[0][1] << term[0][2];
350
        ret = outer;
351
      }
352
1774
      break;
353
    }
354
1518
    case kind::EQUAL: {
355
1518
      ret = solveWrite(term, d_solveWrite, d_solveWrite2, true);
356
1518
      break;
357
    }
358
14108
    default:
359
14108
      break;
360
  }
361
24093
  if (!ret.isNull() && ret != term)
362
  {
363
42
    return TrustNode::mkTrustRewrite(term, ret, nullptr);
364
  }
365
24051
  return TrustNode::null();
366
}
367
368
274
Theory::PPAssertStatus TheoryArrays::ppAssert(
369
    TrustNode tin, TrustSubstitutionMap& outSubstitutions)
370
{
371
548
  TNode in = tin.getNode();
372
274
  switch(in.getKind()) {
373
166
    case kind::EQUAL:
374
    {
375
166
      d_ppFacts.push_back(in);
376
166
      d_ppEqualityEngine.assertEquality(in, true, in);
377
166
      if (in[0].isVar() && isLegalElimination(in[0], in[1]))
378
      {
379
111
        outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
380
111
        return PP_ASSERT_STATUS_SOLVED;
381
      }
382
55
      if (in[1].isVar() && isLegalElimination(in[1], in[0]))
383
      {
384
4
        outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
385
4
        return PP_ASSERT_STATUS_SOLVED;
386
      }
387
51
      break;
388
    }
389
92
    case kind::NOT:
390
    {
391
92
      d_ppFacts.push_back(in);
392
92
      if (in[0].getKind() == kind::EQUAL ) {
393
184
        Node a = in[0][0];
394
184
        Node b = in[0][1];
395
92
        d_ppEqualityEngine.assertEquality(in[0], false, in);
396
      }
397
92
      break;
398
    }
399
16
    default:
400
16
      break;
401
  }
402
159
  return PP_ASSERT_STATUS_UNSOLVED;
403
}
404
405
406
/////////////////////////////////////////////////////////////////////////////
407
// T-PROPAGATION / REGISTRATION
408
/////////////////////////////////////////////////////////////////////////////
409
410
154529
bool TheoryArrays::propagateLit(TNode literal)
411
{
412
309058
  Debug("arrays") << spaces(getSatContext()->getLevel())
413
154529
                  << "TheoryArrays::propagateLit(" << literal << ")"
414
154529
                  << std::endl;
415
416
  // If already in conflict, no more propagation
417
154529
  if (d_state.isInConflict())
418
  {
419
    Debug("arrays") << spaces(getSatContext()->getLevel())
420
                    << "TheoryArrays::propagateLit(" << literal
421
                    << "): already in conflict" << std::endl;
422
    return false;
423
  }
424
425
  // Propagate away
426
154529
  if (d_inCheckModel && getSatContext()->getLevel() != d_topLevel) {
427
    return true;
428
  }
429
154529
  bool ok = d_out->propagate(literal);
430
154529
  if (!ok) {
431
1961
    d_state.notifyInConflict();
432
  }
433
154529
  return ok;
434
}/* TheoryArrays::propagate(TNode) */
435
436
437
TNode TheoryArrays::weakEquivGetRep(TNode node) {
438
  TNode pointer;
439
  while (true) {
440
    pointer = d_infoMap.getWeakEquivPointer(node);
441
    if (pointer.isNull()) {
442
      return node;
443
    }
444
    node = pointer;
445
  }
446
}
447
448
TNode TheoryArrays::weakEquivGetRepIndex(TNode node, TNode index) {
449
  Assert(!index.isNull());
450
  TNode pointer, index2;
451
  while (true) {
452
    pointer = d_infoMap.getWeakEquivPointer(node);
453
    if (pointer.isNull()) {
454
      return node;
455
    }
456
    index2 = d_infoMap.getWeakEquivIndex(node);
457
    if (index2.isNull() || !d_equalityEngine->areEqual(index, index2))
458
    {
459
      node = pointer;
460
    }
461
    else {
462
      TNode secondary = d_infoMap.getWeakEquivSecondary(node);
463
      if (secondary.isNull()) {
464
        return node;
465
      }
466
      node = secondary;
467
    }
468
  }
469
}
470
471
void TheoryArrays::visitAllLeaves(TNode reason, vector<TNode>& conjunctions) {
472
  switch (reason.getKind()) {
473
    case kind::AND:
474
      Assert(reason.getNumChildren() == 2);
475
      visitAllLeaves(reason[0], conjunctions);
476
      visitAllLeaves(reason[1], conjunctions);
477
      break;
478
    case kind::NOT:
479
      conjunctions.push_back(reason);
480
      break;
481
    case kind::EQUAL:
482
      d_equalityEngine->explainEquality(
483
          reason[0], reason[1], true, conjunctions);
484
      break;
485
    default:
486
      Unreachable();
487
  }
488
}
489
490
void TheoryArrays::weakEquivBuildCond(TNode node, TNode index, vector<TNode>& conjunctions) {
491
  Assert(!index.isNull());
492
  TNode pointer, index2;
493
  while (true) {
494
    pointer = d_infoMap.getWeakEquivPointer(node);
495
    if (pointer.isNull()) {
496
      return;
497
    }
498
    index2 = d_infoMap.getWeakEquivIndex(node);
499
    if (index2.isNull()) {
500
      // Null index means these two nodes became equal: explain the equality.
501
      d_equalityEngine->explainEquality(node, pointer, true, conjunctions);
502
      node = pointer;
503
    }
504
    else if (!d_equalityEngine->areEqual(index, index2))
505
    {
506
      // If indices are not equal in current context, need to add that to the lemma.
507
      Node reason = index.eqNode(index2).notNode();
508
      d_permRef.push_back(reason);
509
      conjunctions.push_back(reason);
510
      node = pointer;
511
    }
512
    else {
513
      TNode secondary = d_infoMap.getWeakEquivSecondary(node);
514
      if (secondary.isNull()) {
515
        return;
516
      }
517
      TNode reason = d_infoMap.getWeakEquivSecondaryReason(node);
518
      Assert(!reason.isNull());
519
      visitAllLeaves(reason, conjunctions);
520
      node = secondary;
521
    }
522
  }
523
}
524
525
void TheoryArrays::weakEquivMakeRep(TNode node) {
526
  TNode pointer = d_infoMap.getWeakEquivPointer(node);
527
  if (pointer.isNull()) {
528
    return;
529
  }
530
  weakEquivMakeRep(pointer);
531
  d_infoMap.setWeakEquivPointer(pointer, node);
532
  d_infoMap.setWeakEquivIndex(pointer, d_infoMap.getWeakEquivIndex(node));
533
  d_infoMap.setWeakEquivPointer(node, TNode());
534
  weakEquivMakeRepIndex(node);
535
}
536
537
void TheoryArrays::weakEquivMakeRepIndex(TNode node) {
538
  TNode secondary = d_infoMap.getWeakEquivSecondary(node);
539
  if (secondary.isNull()) {
540
    return;
541
  }
542
  TNode index = d_infoMap.getWeakEquivIndex(node);
543
  Assert(!index.isNull());
544
  TNode index2 = d_infoMap.getWeakEquivIndex(secondary);
545
  Node reason;
546
  TNode next;
547
  while (index2.isNull() || !d_equalityEngine->areEqual(index, index2))
548
  {
549
    next = d_infoMap.getWeakEquivPointer(secondary);
550
    d_infoMap.setWeakEquivSecondary(node, next);
551
    reason = d_infoMap.getWeakEquivSecondaryReason(node);
552
    if (index2.isNull()) {
553
      reason = reason.andNode(secondary.eqNode(next));
554
    }
555
    else {
556
      reason = reason.andNode(index.eqNode(index2).notNode());
557
    }
558
    d_permRef.push_back(reason);
559
    d_infoMap.setWeakEquivSecondaryReason(node, reason);
560
    if (next.isNull()) {
561
      return;
562
    }
563
    secondary = next;
564
    index2 = d_infoMap.getWeakEquivIndex(secondary);
565
  }
566
  weakEquivMakeRepIndex(secondary);
567
  d_infoMap.setWeakEquivSecondary(secondary, node);
568
  d_infoMap.setWeakEquivSecondaryReason(secondary, d_infoMap.getWeakEquivSecondaryReason(node));
569
  d_infoMap.setWeakEquivSecondary(node, TNode());
570
  d_infoMap.setWeakEquivSecondaryReason(node, TNode());
571
}
572
573
void TheoryArrays::weakEquivAddSecondary(TNode index, TNode arrayFrom, TNode arrayTo, TNode reason) {
574
  std::unordered_set<TNode, TNodeHashFunction> marked;
575
  vector<TNode> index_trail;
576
  vector<TNode>::iterator it, iend;
577
  Node equivalence_trail = reason;
578
  Node current_reason;
579
  TNode pointer, indexRep;
580
  if (!index.isNull()) {
581
    index_trail.push_back(index);
582
    marked.insert(d_equalityEngine->getRepresentative(index));
583
  }
584
  while (arrayFrom != arrayTo) {
585
    index = d_infoMap.getWeakEquivIndex(arrayFrom);
586
    pointer = d_infoMap.getWeakEquivPointer(arrayFrom);
587
    if (!index.isNull()) {
588
      indexRep = d_equalityEngine->getRepresentative(index);
589
      if (marked.find(indexRep) == marked.end() && weakEquivGetRepIndex(arrayFrom, index) != arrayTo) {
590
        weakEquivMakeRepIndex(arrayFrom);
591
        d_infoMap.setWeakEquivSecondary(arrayFrom, arrayTo);
592
        current_reason = equivalence_trail;
593
        for (it = index_trail.begin(), iend = index_trail.end(); it != iend; ++it) {
594
          current_reason = current_reason.andNode(index.eqNode(*it).notNode());
595
        }
596
        d_permRef.push_back(current_reason);
597
        d_infoMap.setWeakEquivSecondaryReason(arrayFrom, current_reason);
598
      }
599
      marked.insert(indexRep);
600
    }
601
    else {
602
      equivalence_trail = equivalence_trail.andNode(arrayFrom.eqNode(pointer));
603
    }
604
    arrayFrom = pointer;
605
  }
606
}
607
608
void TheoryArrays::checkWeakEquiv(bool arraysMerged) {
609
  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_mayEqualEqualityEngine);
610
  for (; !eqcs_i.isFinished(); ++eqcs_i) {
611
    Node eqc = (*eqcs_i);
612
    if (!eqc.getType().isArray()) {
613
      continue;
614
    }
615
    eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &d_mayEqualEqualityEngine);
616
    TNode rep = d_mayEqualEqualityEngine.getRepresentative(*eqc_i);
617
    TNode weakEquivRep = weakEquivGetRep(rep);
618
    for (; !eqc_i.isFinished(); ++eqc_i) {
619
      TNode n = *eqc_i;
620
      Assert(!arraysMerged || weakEquivGetRep(n) == weakEquivRep);
621
      TNode pointer = d_infoMap.getWeakEquivPointer(n);
622
      TNode index = d_infoMap.getWeakEquivIndex(n);
623
      TNode secondary = d_infoMap.getWeakEquivSecondary(n);
624
      Assert(pointer.isNull() == (weakEquivGetRep(n) == n));
625
      Assert(!pointer.isNull() || secondary.isNull());
626
      Assert(!index.isNull() || secondary.isNull());
627
      Assert(d_infoMap.getWeakEquivSecondaryReason(n).isNull()
628
             || !secondary.isNull());
629
      if (!pointer.isNull()) {
630
        if (index.isNull()) {
631
          Assert(d_equalityEngine->areEqual(n, pointer));
632
        }
633
        else {
634
          Assert(
635
              (n.getKind() == kind::STORE && n[0] == pointer && n[1] == index)
636
              || (pointer.getKind() == kind::STORE && pointer[0] == n
637
                  && pointer[1] == index));
638
        }
639
      }
640
    }
641
  }
642
}
643
644
/**
645
 * Stores in d_infoMap the following information for each term a of type array:
646
 *
647
 *    - all i, such that there exists a term a[i] or a = store(b i v)
648
 *      (i.e. all indices it is being read atl; store(b i v) is implicitly read at
649
 *      position i due to the implicit axiom store(b i v)[i] = v )
650
 *
651
 *    - all the stores a is congruent to (this information is context dependent)
652
 *
653
 *    - all store terms of the form store (a i v) (i.e. in which a appears
654
 *      directly; this is invariant because no new store terms are created)
655
 *
656
 * Note: completeness depends on having pre-register called on all the input
657
 *       terms before starting to instantiate lemmas.
658
 */
659
51655
void TheoryArrays::preRegisterTermInternal(TNode node)
660
{
661
51655
  if (d_state.isInConflict())
662
  {
663
21394
    return;
664
  }
665
51585
  Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::preRegisterTerm(" << node << ")" << std::endl;
666
51585
  Kind nk = node.getKind();
667
51585
  if (nk == kind::EQUAL)
668
  {
669
    // Add the trigger for equality
670
    // NOTE: note that if the equality is true or false already, it might not be added
671
14485
    d_equalityEngine->addTriggerPredicate(node);
672
14485
    return;
673
  }
674
37100
  else if (d_equalityEngine->hasTerm(node))
675
  {
676
    // Invariant: array terms should be preregistered before being added to the equality engine
677
6769
    Assert(nk != kind::SELECT
678
           || d_isPreRegistered.find(node) != d_isPreRegistered.end());
679
6769
    return;
680
  }
681
  // add to equality engine and the may equality engine
682
60662
  TypeNode nodeType = node.getType();
683
30331
  if (nodeType.isArray())
684
  {
685
    // index type should not be an array, otherwise we throw a logic exception
686
3586
    if (nodeType.getArrayIndexType().isArray())
687
    {
688
      std::stringstream ss;
689
      ss << "Arrays cannot be indexed by array types, offending array type is "
690
         << nodeType;
691
      throw LogicException(ss.str());
692
    }
693
3586
    d_mayEqualEqualityEngine.addTerm(node);
694
  }
695
30331
  d_equalityEngine->addTerm(node);
696
697
30331
  switch (node.getKind())
698
  {
699
21184
    case kind::SELECT:
700
    {
701
      // Reads
702
42368
      TNode store = d_equalityEngine->getRepresentative(node[0]);
703
704
      // The may equal needs the store
705
21184
      d_mayEqualEqualityEngine.addTerm(store);
706
707
21184
      Assert((d_isPreRegistered.insert(node), true));
708
709
21184
      Assert(d_equalityEngine->getRepresentative(store) == store);
710
21184
      d_infoMap.addIndex(store, node[1]);
711
712
      // Synchronize d_constReadsContext with SAT context
713
21184
      Assert(d_constReadsContext->getLevel() <= getSatContext()->getLevel());
714
44718
      while (d_constReadsContext->getLevel() < getSatContext()->getLevel())
715
      {
716
11767
        d_constReadsContext->push();
717
      }
718
719
      // Record read in sharing data structure
720
42368
      TNode index = d_equalityEngine->getRepresentative(node[1]);
721
131525
      if (!options::arraysWeakEquivalence() && index.isConst())
722
      {
723
        CTNodeList* temp;
724
4047
        CNodeNListMap::iterator it = d_constReads.find(index);
725
4047
        if (it == d_constReads.end())
726
        {
727
474
          temp = new (true) CTNodeList(d_constReadsContext);
728
474
          d_constReads[index] = temp;
729
        }
730
        else
731
        {
732
3573
          temp = (*it).second;
733
        }
734
4047
        temp->push_back(node);
735
4047
        d_constReadsList.push_back(node);
736
      }
737
      else
738
      {
739
17137
        d_reads.push_back(node);
740
      }
741
742
21184
      checkRowForIndex(node[1], store);
743
21184
      break;
744
    }
745
1583
    case kind::STORE:
746
    {
747
3166
      TNode a = d_equalityEngine->getRepresentative(node[0]);
748
749
1583
      if (node.isConst())
750
      {
751
        // Can't use d_mayEqualEqualityEngine to merge node with a because they
752
        // are both constants, so just set the default value manually for node.
753
61
        Assert(a == node[0]);
754
61
        d_mayEqualEqualityEngine.addTerm(node);
755
61
        Assert(d_mayEqualEqualityEngine.getRepresentative(node) == node);
756
61
        Assert(d_mayEqualEqualityEngine.getRepresentative(a) == a);
757
61
        DefValMap::iterator it = d_defValues.find(a);
758
61
        Assert(it != d_defValues.end());
759
61
        d_defValues[node] = (*it).second;
760
      }
761
      else
762
      {
763
1522
        d_mayEqualEqualityEngine.assertEquality(node.eqNode(a), true, d_true);
764
1522
        Assert(d_mayEqualEqualityEngine.consistent());
765
      }
766
767
3166
      TNode i = node[1];
768
3166
      TNode v = node[2];
769
1583
      NodeManager* nm = NodeManager::currentNM();
770
3166
      Node ni = nm->mkNode(kind::SELECT, node, i);
771
1583
      if (!d_equalityEngine->hasTerm(ni))
772
      {
773
1583
        preRegisterTermInternal(ni);
774
      }
775
      // Apply RIntro1 Rule
776
1583
      d_im.assertInference(ni.eqNode(v),
777
                           true,
778
                           InferenceId::ARRAYS_READ_OVER_WRITE_1,
779
                           d_true,
780
                           PfRule::ARRAYS_READ_OVER_WRITE_1);
781
782
1583
      d_infoMap.addStore(node, node);
783
1583
      d_infoMap.addInStore(a, node);
784
1583
      d_infoMap.setModelRep(node, node);
785
786
      // Add-Store for Weak Equivalence
787
1583
      if (options::arraysWeakEquivalence())
788
      {
789
        Assert(weakEquivGetRep(node[0]) == weakEquivGetRep(a));
790
        Assert(weakEquivGetRep(node) == node);
791
        d_infoMap.setWeakEquivPointer(node, node[0]);
792
        d_infoMap.setWeakEquivIndex(node, node[1]);
793
#ifdef CVC4_ASSERTIONS
794
      checkWeakEquiv(false);
795
#endif
796
    }
797
798
1583
    checkStore(node);
799
1583
    break;
800
  }
801
42
  case kind::STORE_ALL: {
802
84
    ArrayStoreAll storeAll = node.getConst<ArrayStoreAll>();
803
84
    Node defaultValue = storeAll.getValue();
804
42
    if (!defaultValue.isConst()) {
805
      throw LogicException("Array theory solver does not yet support non-constant default values for arrays");
806
    }
807
42
    d_infoMap.setConstArr(node, node);
808
42
    Assert(d_mayEqualEqualityEngine.getRepresentative(node) == node);
809
42
    d_defValues[node] = defaultValue;
810
42
    break;
811
  }
812
7522
  default:
813
    // Variables etc, already processed above
814
7522
    break;
815
  }
816
  // Invariant: preregistered terms are exactly the terms in the equality engine
817
  // Disabled, see comment above for kind::EQUAL
818
  // Assert(d_equalityEngine->hasTerm(node) ||
819
  // !d_equalityEngine->consistent());
820
}
821
822
40055
void TheoryArrays::preRegisterTerm(TNode node)
823
{
824
40055
  preRegisterTermInternal(node);
825
  // If we have a select from an array of Bools, mark it as a term that can be propagated.
826
  // Note: do this here instead of in preRegisterTermInternal to prevent internal select
827
  // terms from being propagated out (as this results in an assertion failure).
828
40055
  if (node.getKind() == kind::SELECT && node.getType().isBoolean()) {
829
81
    d_equalityEngine->addTriggerPredicate(node);
830
  }
831
40055
}
832
833
void TheoryArrays::explain(TNode literal, Node& explanation)
834
{
835
  ++d_numExplain;
836
  Debug("arrays") << spaces(getSatContext()->getLevel())
837
                  << "TheoryArrays::explain(" << literal << ")" << std::endl;
838
  std::vector<TNode> assumptions;
839
  // Do the work
840
  bool polarity = literal.getKind() != kind::NOT;
841
  TNode atom = polarity ? literal : literal[0];
842
  if (atom.getKind() == kind::EQUAL)
843
  {
844
    d_equalityEngine->explainEquality(
845
        atom[0], atom[1], polarity, assumptions, nullptr);
846
  }
847
  else
848
  {
849
    d_equalityEngine->explainPredicate(atom, polarity, assumptions, nullptr);
850
  }
851
  explanation = mkAnd(assumptions);
852
}
853
854
26054
TrustNode TheoryArrays::explain(TNode literal)
855
{
856
26054
  return d_im.explainLit(literal);
857
}
858
859
/////////////////////////////////////////////////////////////////////////////
860
// SHARING
861
/////////////////////////////////////////////////////////////////////////////
862
863
45751
void TheoryArrays::notifySharedTerm(TNode t)
864
{
865
91502
  Debug("arrays::sharing") << spaces(getSatContext()->getLevel())
866
45751
                           << "TheoryArrays::notifySharedTerm(" << t << ")"
867
45751
                           << std::endl;
868
45751
  if (t.getType().isArray()) {
869
2158
    d_sharedArrays.insert(t);
870
  }
871
  else {
872
#ifdef CVC4_ASSERTIONS
873
43593
    d_sharedOther.insert(t);
874
#endif
875
43593
    d_sharedTerms = true;
876
  }
877
45751
}
878
879
419366
void TheoryArrays::checkPair(TNode r1, TNode r2)
880
{
881
419366
  Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): checking reads " << r1 << " and " << r2 << std::endl;
882
883
424214
  TNode x = r1[1];
884
424214
  TNode y = r2[1];
885
419366
  Assert(d_equalityEngine->isTriggerTerm(x, THEORY_ARRAYS));
886
887
1677464
  if (d_equalityEngine->hasTerm(x) && d_equalityEngine->hasTerm(y)
888
2454021
      && (d_equalityEngine->areEqual(x, y)
889
502150
          || d_equalityEngine->areDisequal(x, y, false)))
890
  {
891
357191
    Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): equality known, skipping" << std::endl;
892
357191
    return;
893
  }
894
895
  // If the terms are already known to be equal, we are also in good shape
896
62175
  if (d_equalityEngine->areEqual(r1, r2))
897
  {
898
1895
    Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): equal, skipping" << std::endl;
899
1895
    return;
900
  }
901
902
60280
  if (r1[0] != r2[0]) {
903
    // If arrays are known to be disequal, or cannot become equal, we can continue
904
53835
    Assert(d_mayEqualEqualityEngine.hasTerm(r1[0])
905
           && d_mayEqualEqualityEngine.hasTerm(r2[0]));
906
215340
    if (r1[0].getType() != r2[0].getType()
907
215340
        || d_equalityEngine->areDisequal(r1[0], r2[0], false))
908
    {
909
4158
      Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): arrays can't be equal, skipping" << std::endl;
910
4158
      return;
911
    }
912
49677
    else if (!d_mayEqualEqualityEngine.areEqual(r1[0], r2[0])) {
913
682
      return;
914
    }
915
  }
916
917
55440
  if (!d_equalityEngine->isTriggerTerm(y, THEORY_ARRAYS))
918
  {
919
10
    Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): not connected to shared terms, skipping" << std::endl;
920
10
    return;
921
  }
922
923
  // Get representative trigger terms
924
  TNode x_shared =
925
60278
      d_equalityEngine->getTriggerTermRepresentative(x, THEORY_ARRAYS);
926
  TNode y_shared =
927
60278
      d_equalityEngine->getTriggerTermRepresentative(y, THEORY_ARRAYS);
928
55430
  EqualityStatus eqStatusDomain = d_valuation.getEqualityStatus(x_shared, y_shared);
929
55430
  switch (eqStatusDomain) {
930
    case EQUALITY_TRUE_AND_PROPAGATED:
931
      // Should have been propagated to us
932
      Assert(false);
933
      break;
934
2717
    case EQUALITY_TRUE:
935
      // Missed propagation - need to add the pair so that theory engine can force propagation
936
2717
      Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): missed propagation" << std::endl;
937
2717
      break;
938
    case EQUALITY_FALSE_AND_PROPAGATED:
939
      Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): checkPair "
940
                                  "called when false in model"
941
                               << std::endl;
942
      // Should have been propagated to us
943
      Assert(false);
944
      break;
945
50582
    case EQUALITY_FALSE: CVC4_FALLTHROUGH;
946
    case EQUALITY_FALSE_IN_MODEL:
947
      // This is unlikely, but I think it could happen
948
50582
      Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): checkPair called when false in model" << std::endl;
949
50582
      return;
950
2131
    default:
951
      // Covers EQUALITY_TRUE_IN_MODEL (common case) and EQUALITY_UNKNOWN
952
2131
      break;
953
  }
954
955
  // Add this pair
956
4848
  Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): adding to care-graph" << std::endl;
957
4848
  addCarePair(x_shared, y_shared);
958
}
959
960
961
6786
void TheoryArrays::computeCareGraph()
962
{
963
6786
  if (d_sharedArrays.size() > 0) {
964
432
    CDNodeSet::key_iterator it1 = d_sharedArrays.key_begin(), it2, iend = d_sharedArrays.key_end();
965
4166
    for (; it1 != iend; ++it1) {
966
14594
      for (it2 = it1, ++it2; it2 != iend; ++it2) {
967
12727
        if ((*it1).getType() != (*it2).getType()) {
968
4798
          continue;
969
        }
970
7929
        EqualityStatus eqStatusArr = getEqualityStatus((*it1), (*it2));
971
7929
        if (eqStatusArr != EQUALITY_UNKNOWN) {
972
7800
          continue;
973
        }
974
129
        Assert(d_valuation.getEqualityStatus((*it1), (*it2))
975
               == EQUALITY_UNKNOWN);
976
129
        addCarePair((*it1), (*it2));
977
129
        ++d_numSharedArrayVarSplits;
978
258
        return;
979
      }
980
    }
981
  }
982
6657
  if (d_sharedTerms) {
983
    // Synchronize d_constReadsContext with SAT context
984
583
    Assert(d_constReadsContext->getLevel() <= getSatContext()->getLevel());
985
9175
    while (d_constReadsContext->getLevel() < getSatContext()->getLevel()) {
986
4296
      d_constReadsContext->push();
987
    }
988
989
    // Go through the read terms and see if there are any to split on
990
991
    // Give constReadsContext a push so that all the work it does here is erased - models can change if context changes at all
992
    // The context is popped at the end.  If this loop is interrupted for some reason, we have to make sure the context still
993
    // gets popped or the solver will be in an inconsistent state
994
583
    d_constReadsContext->push();
995
583
    unsigned size = d_reads.size();
996
10751
    for (unsigned i = 0; i < size; ++ i) {
997
20110
      TNode r1 = d_reads[i];
998
999
10168
      Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): checking read " << r1 << std::endl;
1000
10168
      Assert(d_equalityEngine->hasTerm(r1));
1001
20110
      TNode x = r1[1];
1002
1003
10394
      if (!d_equalityEngine->isTriggerTerm(x, THEORY_ARRAYS))
1004
      {
1005
226
        Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): not connected to shared terms, skipping" << std::endl;
1006
226
        continue;
1007
      }
1008
      Node x_shared =
1009
19884
          d_equalityEngine->getTriggerTermRepresentative(x, THEORY_ARRAYS);
1010
1011
      // Get the model value of index and find all reads that read from that same model value: these are the pairs we have to check
1012
      // Also, insert this read in the list at the proper index
1013
1014
9942
      if (!x_shared.isConst()) {
1015
5516
        x_shared = d_valuation.getModelValue(x_shared);
1016
      }
1017
9942
      if (!x_shared.isNull()) {
1018
        CTNodeList* temp;
1019
8224
        CNodeNListMap::iterator it = d_constReads.find(x_shared);
1020
8224
        if (it == d_constReads.end()) {
1021
          // This is the only x_shared with this model value - no need to create any splits
1022
165
          temp = new(true) CTNodeList(d_constReadsContext);
1023
165
          d_constReads[x_shared] = temp;
1024
        }
1025
        else {
1026
8059
          temp = (*it).second;
1027
326370
          for (size_t j = 0; j < temp->size(); ++j) {
1028
318311
            checkPair(r1, (*temp)[j]);
1029
          }
1030
        }
1031
8224
        temp->push_back(r1);
1032
      }
1033
      else {
1034
        // We don't know the model value for x.  Just do brute force examination of all pairs of reads
1035
90559
        for (unsigned j = 0; j < size; ++j) {
1036
177682
          TNode r2 = d_reads[j];
1037
88841
          Assert(d_equalityEngine->hasTerm(r2));
1038
88841
          checkPair(r1,r2);
1039
        }
1040
13932
        for (unsigned j = 0; j < d_constReadsList.size(); ++j) {
1041
24428
          TNode r2 = d_constReadsList[j];
1042
12214
          Assert(d_equalityEngine->hasTerm(r2));
1043
12214
          checkPair(r1,r2);
1044
        }
1045
      }
1046
    }
1047
583
    d_constReadsContext->pop();
1048
  }
1049
}
1050
1051
1052
/////////////////////////////////////////////////////////////////////////////
1053
// MODEL GENERATION
1054
/////////////////////////////////////////////////////////////////////////////
1055
1056
4901
bool TheoryArrays::collectModelValues(TheoryModel* m,
1057
                                      const std::set<Node>& termSet)
1058
{
1059
  // termSet contains terms appearing in assertions and shared terms, and also
1060
  // includes additional reads due to the RIntro1 and RIntro2 rules.
1061
4901
  NodeManager* nm = NodeManager::currentNM();
1062
  // Compute arrays that we need to produce representatives for
1063
9802
  std::vector<Node> arrays;
1064
1065
4901
  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
1066
29963
  for (; !eqcs_i.isFinished(); ++eqcs_i) {
1067
13511
    Node eqc = (*eqcs_i);
1068
12531
    if (!eqc.getType().isArray())
1069
    {
1070
      // not an array, skip
1071
11551
      continue;
1072
    }
1073
980
    eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, d_equalityEngine);
1074
1778
    for (; !eqc_i.isFinished(); ++eqc_i) {
1075
1442
      Node n = *eqc_i;
1076
      // If this EC is an array type and it contains something other than STORE nodes, we have to compute a representative explicitly
1077
1043
      if (termSet.find(n) != termSet.end())
1078
      {
1079
1017
        if (n.getKind() != kind::STORE)
1080
        {
1081
644
          arrays.push_back(n);
1082
644
          break;
1083
        }
1084
      }
1085
    }
1086
  }
1087
1088
  // Build a list of all the relevant reads, indexed by the store representative
1089
9802
  std::map<Node, std::vector<Node> > selects;
1090
4901
  set<Node>::iterator set_it = termSet.begin(), set_it_end = termSet.end();
1091
21647
  for (; set_it != set_it_end; ++set_it) {
1092
16746
    Node n = *set_it;
1093
    // If this term is a select, record that the EC rep of its store parameter is being read from using this term
1094
8373
    if (n.getKind() == kind::SELECT) {
1095
4482
      selects[d_equalityEngine->getRepresentative(n[0])].push_back(n);
1096
    }
1097
  }
1098
1099
9802
  Node rep;
1100
4901
  DefValMap::iterator it;
1101
9802
  TypeSet defaultValuesSet;
1102
1103
  // Compute all default values already in use
1104
  //if (fullModel) {
1105
5545
    for (size_t i=0; i<arrays.size(); ++i) {
1106
1288
      TNode nrep = d_equalityEngine->getRepresentative(arrays[i]);
1107
644
      d_mayEqualEqualityEngine.addTerm(nrep); // add the term in case it isn't there already
1108
1288
      TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(nrep);
1109
644
      it = d_defValues.find(mayRep);
1110
644
      if (it != d_defValues.end()) {
1111
171
        defaultValuesSet.add(nrep.getType().getArrayConstituentType(), (*it).second);
1112
      }
1113
    }
1114
  //}
1115
1116
  // Loop through all array equivalence classes that need a representative computed
1117
5545
    for (size_t i = 0; i < arrays.size(); ++i)
1118
    {
1119
1288
      TNode n = arrays[i];
1120
1288
      TNode nrep = d_equalityEngine->getRepresentative(n);
1121
1122
      // if (fullModel) {
1123
      // Compute default value for this array - there is one default value for
1124
      // every mayEqual equivalence class
1125
1288
      TNode mayRep = d_mayEqualEqualityEngine.getRepresentative(nrep);
1126
644
      it = d_defValues.find(mayRep);
1127
      // If this mayEqual EC doesn't have a default value associated, get the next available default value for the associated array element type
1128
644
      if (it == d_defValues.end()) {
1129
818
        TypeNode valueType = nrep.getType().getArrayConstituentType();
1130
409
        rep = defaultValuesSet.nextTypeEnum(valueType);
1131
409
        if (rep.isNull()) {
1132
          Assert(defaultValuesSet.getSet(valueType)->begin()
1133
                 != defaultValuesSet.getSet(valueType)->end());
1134
          rep = *(defaultValuesSet.getSet(valueType)->begin());
1135
        }
1136
409
        Trace("arrays-models") << "New default value = " << rep << endl;
1137
409
        d_defValues[mayRep] = rep;
1138
      }
1139
      else {
1140
235
        rep = (*it).second;
1141
      }
1142
1143
      // Build the STORE_ALL term with the default value
1144
644
      rep = nm->mkConst(ArrayStoreAll(nrep.getType(), rep));
1145
      /*
1146
    }
1147
    else {
1148
      std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(n);
1149
      if (it == d_skolemCache.end()) {
1150
        rep = nm->mkSkolem("array_collect_model_var", n.getType(), "base model variable for array collectModelInfo");
1151
        d_skolemCache[n] = rep;
1152
      }
1153
      else {
1154
        rep = (*it).second;
1155
      }
1156
    }
1157
*/
1158
1159
    // For each read, require that the rep stores the right value
1160
644
    vector<Node>& reads = selects[nrep];
1161
3454
    for (unsigned j = 0; j < reads.size(); ++j) {
1162
2810
      rep = nm->mkNode(kind::STORE, rep, reads[j][1], reads[j]);
1163
    }
1164
644
    if (!m->assertEquality(n, rep, true))
1165
    {
1166
      return false;
1167
    }
1168
644
    if (!n.isConst()) {
1169
545
      m->assertSkeleton(rep);
1170
    }
1171
  }
1172
4901
  return true;
1173
}
1174
1175
/////////////////////////////////////////////////////////////////////////////
1176
// NOTIFICATIONS
1177
/////////////////////////////////////////////////////////////////////////////
1178
1179
1180
12416
void TheoryArrays::presolve()
1181
{
1182
12416
  Trace("arrays")<<"Presolving \n";
1183
12416
  if (!d_dstratInit)
1184
  {
1185
8592
    d_dstratInit = true;
1186
    // add the decision strategy, which is user-context-independent
1187
17184
    getDecisionManager()->registerStrategy(
1188
        DecisionManager::STRAT_ARRAYS,
1189
8592
        d_dstrat.get(),
1190
        DecisionManager::STRAT_SCOPE_CTX_INDEPENDENT);
1191
  }
1192
12416
}
1193
1194
1195
/////////////////////////////////////////////////////////////////////////////
1196
// MAIN SOLVER
1197
/////////////////////////////////////////////////////////////////////////////
1198
1199
3691
Node TheoryArrays::getSkolem(TNode ref)
1200
{
1201
  // the call to SkolemCache::getExtIndexSkolem should be deterministic, but use
1202
  // cache anyways for now
1203
3691
  Node skolem;
1204
3691
  std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(ref);
1205
3691
  if (it == d_skolemCache.end()) {
1206
579
    Assert(ref.getKind() == kind::NOT && ref[0].getKind() == kind::EQUAL);
1207
    // make the skolem using the skolem cache utility
1208
579
    skolem = SkolemCache::getExtIndexSkolem(ref);
1209
579
    d_skolemCache[ref] = skolem;
1210
  }
1211
  else {
1212
3112
    skolem = (*it).second;
1213
  }
1214
1215
3691
  Debug("pf::array") << "Pregistering a Skolem" << std::endl;
1216
3691
  preRegisterTermInternal(skolem);
1217
3691
  Debug("pf::array") << "Pregistering a Skolem DONE" << std::endl;
1218
1219
3691
  Debug("pf::array") << "getSkolem DONE" << std::endl;
1220
3691
  return skolem;
1221
}
1222
1223
66577
void TheoryArrays::postCheck(Effort level)
1224
{
1225
349216
  if ((options::arraysEagerLemmas() || fullEffort(level))
1226
88827
      && !d_state.isInConflict() && options::arraysWeakEquivalence())
1227
  {
1228
    // Replay all array merges to update weak equivalence data structures
1229
    context::CDList<Node>::iterator it = d_arrayMerges.begin(), iend = d_arrayMerges.end();
1230
    TNode a, b, eq;
1231
    for (; it != iend; ++it) {
1232
      eq = *it;
1233
      a = eq[0];
1234
      b = eq[1];
1235
      weakEquivMakeRep(b);
1236
      if (weakEquivGetRep(a) == b) {
1237
        weakEquivAddSecondary(TNode(), a, b, eq);
1238
      }
1239
      else {
1240
        d_infoMap.setWeakEquivPointer(b, a);
1241
        d_infoMap.setWeakEquivIndex(b, TNode());
1242
      }
1243
#ifdef CVC4_ASSERTIONS
1244
    checkWeakEquiv(false);
1245
#endif
1246
    }
1247
#ifdef CVC4_ASSERTIONS
1248
    checkWeakEquiv(true);
1249
#endif
1250
1251
    d_readTableContext->push();
1252
    TNode mayRep, iRep;
1253
    CTNodeList* bucketList = NULL;
1254
    CTNodeList::const_iterator i = d_reads.begin(), readsEnd = d_reads.end();
1255
    for (; i != readsEnd; ++i) {
1256
      const TNode& r = *i;
1257
1258
      Debug("arrays::weak") << "TheoryArrays::check(): checking read " << r << std::endl;
1259
1260
      // Find the bucket for this read.
1261
      mayRep = d_mayEqualEqualityEngine.getRepresentative(r[0]);
1262
      iRep = d_equalityEngine->getRepresentative(r[1]);
1263
      std::pair<TNode, TNode> key(mayRep, iRep);
1264
      ReadBucketMap::iterator rbm_it = d_readBucketTable.find(key);
1265
      if (rbm_it == d_readBucketTable.end())
1266
      {
1267
        bucketList = new(true) CTNodeList(d_readTableContext);
1268
        d_readBucketAllocations.push_back(bucketList);
1269
        d_readBucketTable[key] = bucketList;
1270
      }
1271
      else {
1272
        bucketList = rbm_it->second;
1273
      }
1274
      CTNodeList::const_iterator ctnl_it = bucketList->begin(),
1275
                                 ctnl_iend = bucketList->end();
1276
      for (; ctnl_it != ctnl_iend; ++ctnl_it)
1277
      {
1278
        const TNode& r2 = *ctnl_it;
1279
        Assert(r2.getKind() == kind::SELECT);
1280
        Assert(mayRep == d_mayEqualEqualityEngine.getRepresentative(r2[0]));
1281
        Assert(iRep == d_equalityEngine->getRepresentative(r2[1]));
1282
        if (d_equalityEngine->areEqual(r, r2))
1283
        {
1284
          continue;
1285
        }
1286
        if (weakEquivGetRepIndex(r[0], r[1]) == weakEquivGetRepIndex(r2[0], r[1])) {
1287
          // add lemma: r[1] = r2[1] /\ cond(r[0],r2[0]) => r = r2
1288
          vector<TNode> conjunctions;
1289
          Assert(d_equalityEngine->areEqual(r, Rewriter::rewrite(r)));
1290
          Assert(d_equalityEngine->areEqual(r2, Rewriter::rewrite(r2)));
1291
          Node lemma = Rewriter::rewrite(r).eqNode(Rewriter::rewrite(r2)).negate();
1292
          d_permRef.push_back(lemma);
1293
          conjunctions.push_back(lemma);
1294
          if (r[1] != r2[1]) {
1295
            d_equalityEngine->explainEquality(r[1], r2[1], true, conjunctions);
1296
          }
1297
          // TODO: get smaller lemmas by eliminating shared parts of path
1298
          weakEquivBuildCond(r[0], r[1], conjunctions);
1299
          weakEquivBuildCond(r2[0], r[1], conjunctions);
1300
          lemma = mkAnd(conjunctions, true);
1301
          // LSH FIXME: which kind of arrays lemma is this
1302
          Trace("arrays-lem")
1303
              << "Arrays::addExtLemma (weak-eq) " << lemma << "\n";
1304
          d_out->lemma(lemma, LemmaProperty::SEND_ATOMS);
1305
          d_readTableContext->pop();
1306
          Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl;
1307
          return;
1308
        }
1309
      }
1310
      bucketList->push_back(r);
1311
    }
1312
    d_readTableContext->pop();
1313
  }
1314
1315
199731
  if (!options::arraysEagerLemmas() && fullEffort(level)
1316
88827
      && !d_state.isInConflict() && !options::arraysWeakEquivalence())
1317
  {
1318
    // generate the lemmas on the worklist
1319
22250
    Trace("arrays-lem")<< "Arrays::discharging lemmas. Number of queued lemmas: " << d_RowQueue.size() << "\n";
1320
22912
    while (d_RowQueue.size() > 0 && !d_state.isInConflict())
1321
    {
1322
1493
      if (dischargeLemmas()) {
1323
1162
        break;
1324
      }
1325
    }
1326
  }
1327
1328
66577
  Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl;
1329
}
1330
1331
157755
bool TheoryArrays::preNotifyFact(
1332
    TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
1333
{
1334
157755
  if (!isInternal && !isPrereg)
1335
  {
1336
109156
    if (atom.getKind() == kind::EQUAL)
1337
    {
1338
109096
      if (!d_equalityEngine->hasTerm(atom[0]))
1339
      {
1340
658
        Assert(atom[0].isConst());
1341
658
        d_equalityEngine->addTerm(atom[0]);
1342
      }
1343
109096
      if (!d_equalityEngine->hasTerm(atom[1]))
1344
      {
1345
152
        Assert(atom[1].isConst());
1346
152
        d_equalityEngine->addTerm(atom[1]);
1347
      }
1348
    }
1349
  }
1350
157755
  return false;
1351
}
1352
1353
157752
void TheoryArrays::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
1354
{
1355
  // if a disequality
1356
157752
  if (atom.getKind() == kind::EQUAL && !pol && !isInternal)
1357
  {
1358
    // Notice that this should be an external assertion, since we do not
1359
    // internally infer disequalities.
1360
    // Apply ArrDiseq Rule if diseq is between arrays
1361
43989
    if (fact[0][0].getType().isArray() && !d_state.isInConflict())
1362
    {
1363
3691
      NodeManager* nm = NodeManager::currentNM();
1364
1365
7382
      TNode k;
1366
      // k is the skolem for this disequality.
1367
7382
      Debug("pf::array") << "Check: kind::NOT: array theory making a skolem"
1368
3691
                          << std::endl;
1369
1370
      // If not in replay mode, generate a fresh skolem variable
1371
3691
      k = getSkolem(fact);
1372
1373
7382
      Node ak = nm->mkNode(kind::SELECT, fact[0][0], k);
1374
7382
      Node bk = nm->mkNode(kind::SELECT, fact[0][1], k);
1375
7382
      Node eq = ak.eqNode(bk);
1376
7382
      Node lemma = fact[0].orNode(eq.notNode());
1377
1378
71071
      if (options::arraysPropagate() > 0 && d_equalityEngine->hasTerm(ak)
1379
10298
          && d_equalityEngine->hasTerm(bk))
1380
      {
1381
        // Propagate witness disequality - might produce a conflict
1382
5832
        Debug("pf::array") << "Asserting to the equality engine:" << std::endl
1383
2916
                           << "\teq = " << eq << std::endl
1384
2916
                           << "\treason = " << fact << std::endl;
1385
2916
        d_im.assertInference(eq, false, InferenceId::ARRAYS_EXT, fact, PfRule::ARRAYS_EXT);
1386
2916
        ++d_numProp;
1387
      }
1388
1389
      // If this is the solution pass, generate the lemma. Otherwise, don't
1390
      // generate it - as this is the lemma that we're reproving...
1391
3691
      Trace("arrays-lem") << "Arrays::addExtLemma " << lemma << "\n";
1392
3691
      d_im.arrayLemma(eq.notNode(), InferenceId::ARRAYS_EXT, fact, PfRule::ARRAYS_EXT);
1393
3691
      ++d_numExt;
1394
    }
1395
    else
1396
    {
1397
80596
      Debug("pf::array") << "Check: kind::NOT: array theory NOT making a skolem"
1398
40298
                         << std::endl;
1399
40298
      d_modelConstraints.push_back(fact);
1400
    }
1401
  }
1402
157752
}
1403
1404
Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions, bool invert, unsigned startIndex)
1405
{
1406
  if (conjunctions.empty())
1407
  {
1408
    return invert ? d_false : d_true;
1409
  }
1410
1411
  std::set<TNode> all;
1412
1413
  unsigned i = startIndex;
1414
  TNode t;
1415
  for (; i < conjunctions.size(); ++i) {
1416
    t = conjunctions[i];
1417
    if (t == d_true) {
1418
      continue;
1419
    }
1420
    else if (t.getKind() == kind::AND) {
1421
      for(TNode::iterator child_it = t.begin(); child_it != t.end(); ++child_it) {
1422
        if (*child_it == d_true) {
1423
          continue;
1424
        }
1425
        all.insert(*child_it);
1426
      }
1427
    }
1428
    else {
1429
      all.insert(t);
1430
    }
1431
  }
1432
1433
  if (all.size() == 0) {
1434
    return invert ? d_false : d_true;
1435
  }
1436
  if (all.size() == 1) {
1437
    // All the same, or just one
1438
    if (invert) {
1439
      return (*(all.begin())).negate();
1440
    }
1441
    else {
1442
      return *(all.begin());
1443
    }
1444
  }
1445
1446
  NodeBuilder<> conjunction(invert ? kind::OR : kind::AND);
1447
  std::set<TNode>::const_iterator it = all.begin();
1448
  std::set<TNode>::const_iterator it_end = all.end();
1449
  while (it != it_end) {
1450
    if (invert) {
1451
      conjunction << (*it).negate();
1452
    }
1453
    else {
1454
      conjunction << *it;
1455
    }
1456
    ++ it;
1457
  }
1458
1459
  return conjunction;
1460
}
1461
1462
1463
802
void TheoryArrays::setNonLinear(TNode a)
1464
{
1465
884
  if (options::arraysWeakEquivalence()) return;
1466
802
  if (d_infoMap.isNonLinear(a)) return;
1467
1468
720
  Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::setNonLinear (" << a << ")\n";
1469
720
  d_infoMap.setNonLinear(a);
1470
720
  ++d_numNonLinear;
1471
1472
720
  const CTNodeList* i_a = d_infoMap.getIndices(a);
1473
720
  const CTNodeList* st_a = d_infoMap.getStores(a);
1474
720
  const CTNodeList* inst_a = d_infoMap.getInStores(a);
1475
1476
720
  size_t it = 0;
1477
1478
  // Propagate non-linearity down chain of stores
1479
1408
  for( ; it < st_a->size(); ++it) {
1480
688
    TNode store = (*st_a)[it];
1481
344
    Assert(store.getKind() == kind::STORE);
1482
344
    setNonLinear(store[0]);
1483
  }
1484
1485
  // Instantiate ROW lemmas that were ignored before
1486
720
  size_t it2 = 0;
1487
1440
  RowLemmaType lem;
1488
9202
  for(; it2 < i_a->size(); ++it2) {
1489
8482
    TNode i = (*i_a)[it2];
1490
4241
    it = 0;
1491
12503
    for ( ; it < inst_a->size(); ++it) {
1492
8262
      TNode store = (*inst_a)[it];
1493
4131
      Assert(store.getKind() == kind::STORE);
1494
8262
      TNode j = store[1];
1495
8262
      TNode c = store[0];
1496
4131
      lem = std::make_tuple(store, c, j, i);
1497
4131
      Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::setNonLinear ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n";
1498
4131
      queueRowLemma(lem);
1499
    }
1500
  }
1501
1502
}
1503
1504
5229
void TheoryArrays::mergeArrays(TNode a, TNode b)
1505
{
1506
  // Note: a is the new representative
1507
5229
  Assert(a.getType().isArray() && b.getType().isArray());
1508
1509
5229
  if (d_mergeInProgress) {
1510
    // Nested call to mergeArrays, just push on the queue and return
1511
    d_mergeQueue.push(a.eqNode(b));
1512
    return;
1513
  }
1514
1515
5229
  d_mergeInProgress = true;
1516
1517
10458
  Node n;
1518
  while (true) {
1519
    // Normally, a is its own representative, but it's possible for a to have
1520
    // been merged with another array after it got queued up by the equality engine,
1521
    // so we take its representative to be safe.
1522
5229
    a = d_equalityEngine->getRepresentative(a);
1523
5229
    Assert(d_equalityEngine->getRepresentative(b) == a);
1524
5229
    Trace("arrays-merge") << spaces(getSatContext()->getLevel()) << "Arrays::merge: (" << a << ", " << b << ")\n";
1525
1526
5229
    if (options::arraysOptimizeLinear() && !options::arraysWeakEquivalence()) {
1527
3827
      bool aNL = d_infoMap.isNonLinear(a);
1528
3827
      bool bNL = d_infoMap.isNonLinear(b);
1529
3827
      if (aNL) {
1530
214
        if (bNL) {
1531
          // already both marked as non-linear - no need to do anything
1532
        }
1533
        else {
1534
          // Set b to be non-linear
1535
192
          setNonLinear(b);
1536
        }
1537
      }
1538
      else {
1539
3613
        if (bNL) {
1540
          // Set a to be non-linear
1541
20
          setNonLinear(a);
1542
        }
1543
        else {
1544
          // Check for new non-linear arrays
1545
3593
          const CTNodeList* astores = d_infoMap.getStores(a);
1546
3593
          const CTNodeList* bstores = d_infoMap.getStores(b);
1547
3593
          Assert(astores->size() <= 1 && bstores->size() <= 1);
1548
3593
          if (astores->size() > 0 && bstores->size() > 0) {
1549
123
            setNonLinear(a);
1550
123
            setNonLinear(b);
1551
          }
1552
        }
1553
      }
1554
    }
1555
1556
5232
    TNode constArrA = d_infoMap.getConstArr(a);
1557
5232
    TNode constArrB = d_infoMap.getConstArr(b);
1558
5229
    if (constArrA.isNull()) {
1559
5118
      if (!constArrB.isNull()) {
1560
        d_infoMap.setConstArr(a,constArrB);
1561
      }
1562
    }
1563
111
    else if (!constArrB.isNull()) {
1564
      if (constArrA != constArrB) {
1565
        conflict(constArrA,constArrB);
1566
      }
1567
    }
1568
1569
5232
    TNode mayRepA = d_mayEqualEqualityEngine.getRepresentative(a);
1570
5232
    TNode mayRepB = d_mayEqualEqualityEngine.getRepresentative(b);
1571
1572
    // If a and b have different default values associated with their mayequal equivalence classes,
1573
    // things get complicated.  Similarly, if two mayequal equivalence classes have different
1574
    // constant representatives, it's not clear what to do. - disallow these cases for now.  -Clark
1575
5229
    DefValMap::iterator it = d_defValues.find(mayRepA);
1576
5229
    DefValMap::iterator it2 = d_defValues.find(mayRepB);
1577
5232
    TNode defValue;
1578
1579
5229
    if (it != d_defValues.end()) {
1580
302
      defValue = (*it).second;
1581
605
      if ((it2 != d_defValues.end() && (defValue != (*it2).second)) ||
1582
600
          (mayRepA.isConst() && mayRepB.isConst() && mayRepA != mayRepB)) {
1583
3
        throw LogicException("Array theory solver does not yet support write-chains connecting two different constant arrays");
1584
      }
1585
    }
1586
4927
    else if (it2 != d_defValues.end()) {
1587
      defValue = (*it2).second;
1588
    }
1589
5226
    d_mayEqualEqualityEngine.assertEquality(a.eqNode(b), true, d_true);
1590
5226
    Assert(d_mayEqualEqualityEngine.consistent());
1591
5226
    if (!defValue.isNull()) {
1592
299
      mayRepA = d_mayEqualEqualityEngine.getRepresentative(a);
1593
299
      d_defValues[mayRepA] = defValue;
1594
    }
1595
1596
5226
    checkRowLemmas(a,b);
1597
5226
    checkRowLemmas(b,a);
1598
1599
    // merge info adds the list of the 2nd argument to the first
1600
5226
    d_infoMap.mergeInfo(a, b);
1601
1602
5226
    if (options::arraysWeakEquivalence()) {
1603
      d_arrayMerges.push_back(a.eqNode(b));
1604
    }
1605
1606
    // If no more to do, break
1607
5226
    if (d_state.isInConflict() || d_mergeQueue.empty())
1608
    {
1609
5226
      break;
1610
    }
1611
1612
    // Otherwise, prepare for next iteration
1613
    n = d_mergeQueue.front();
1614
    a = n[0];
1615
    b = n[1];
1616
    d_mergeQueue.pop();
1617
  }
1618
5226
  d_mergeInProgress = false;
1619
}
1620
1621
1622
1583
void TheoryArrays::checkStore(TNode a) {
1623
1583
  if (options::arraysWeakEquivalence()) return;
1624
1583
  Trace("arrays-cri")<<"Arrays::checkStore "<<a<<"\n";
1625
1626
1583
  if(Trace.isOn("arrays-cri")) {
1627
    d_infoMap.getInfo(a)->print();
1628
  }
1629
1583
  Assert(a.getType().isArray());
1630
1583
  Assert(a.getKind() == kind::STORE);
1631
3166
  TNode b = a[0];
1632
3166
  TNode i = a[1];
1633
1634
3166
  TNode brep = d_equalityEngine->getRepresentative(b);
1635
1636
1583
  if (!options::arraysOptimizeLinear() || d_infoMap.isNonLinear(brep)) {
1637
281
    const CTNodeList* js = d_infoMap.getIndices(brep);
1638
281
    size_t it = 0;
1639
562
    RowLemmaType lem;
1640
895
    for(; it < js->size(); ++it) {
1641
591
      TNode j = (*js)[it];
1642
307
      if (i == j) continue;
1643
284
      lem = std::make_tuple(a, b, i, j);
1644
284
      Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkStore ("<<a<<", "<<b<<", "<<i<<", "<<j<<")\n";
1645
284
      queueRowLemma(lem);
1646
    }
1647
  }
1648
}
1649
1650
1651
21184
void TheoryArrays::checkRowForIndex(TNode i, TNode a)
1652
{
1653
21184
  if (options::arraysWeakEquivalence()) return;
1654
21184
  Trace("arrays-cri")<<"Arrays::checkRowForIndex "<<a<<"\n";
1655
21184
  Trace("arrays-cri")<<"                   index "<<i<<"\n";
1656
1657
21184
  if(Trace.isOn("arrays-cri")) {
1658
    d_infoMap.getInfo(a)->print();
1659
  }
1660
21184
  Assert(a.getType().isArray());
1661
21184
  Assert(d_equalityEngine->getRepresentative(a) == a);
1662
1663
42368
  TNode constArr = d_infoMap.getConstArr(a);
1664
21184
  if (!constArr.isNull()) {
1665
692
    ArrayStoreAll storeAll = constArr.getConst<ArrayStoreAll>();
1666
692
    Node defValue = storeAll.getValue();
1667
692
    Node selConst = NodeManager::currentNM()->mkNode(kind::SELECT, constArr, i);
1668
346
    if (!d_equalityEngine->hasTerm(selConst))
1669
    {
1670
2
      preRegisterTermInternal(selConst);
1671
    }
1672
346
    d_im.assertInference(selConst.eqNode(defValue),
1673
                         true,
1674
                         InferenceId::UNKNOWN,
1675
                         d_true,
1676
                         PfRule::ARRAYS_TRUST);
1677
  }
1678
1679
21184
  const CTNodeList* stores = d_infoMap.getStores(a);
1680
21184
  const CTNodeList* instores = d_infoMap.getInStores(a);
1681
21184
  size_t it = 0;
1682
42368
  RowLemmaType lem;
1683
1684
47900
  for(; it < stores->size(); ++it) {
1685
26604
    TNode store = (*stores)[it];
1686
13358
    Assert(store.getKind() == kind::STORE);
1687
26604
    TNode j = store[1];
1688
13358
    if (i == j) continue;
1689
13246
    lem = std::make_tuple(store, store[0], j, i);
1690
13246
    Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n";
1691
13246
    queueRowLemma(lem);
1692
  }
1693
1694
21184
  if (!options::arraysOptimizeLinear() || d_infoMap.isNonLinear(a)) {
1695
8036
    it = 0;
1696
22352
    for(; it < instores->size(); ++it) {
1697
14140
      TNode instore = (*instores)[it];
1698
7158
      Assert(instore.getKind() == kind::STORE);
1699
14140
      TNode j = instore[1];
1700
7158
      if (i == j) continue;
1701
6982
      lem = std::make_tuple(instore, instore[0], j, i);
1702
6982
      Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n";
1703
6982
      queueRowLemma(lem);
1704
    }
1705
  }
1706
}
1707
1708
1709
// a just became equal to b
1710
// look for new ROW lemmas
1711
10452
void TheoryArrays::checkRowLemmas(TNode a, TNode b)
1712
{
1713
10452
  if (options::arraysWeakEquivalence()) return;
1714
10452
  Trace("arrays-crl")<<"Arrays::checkLemmas begin \n"<<a<<"\n";
1715
10452
  if(Trace.isOn("arrays-crl"))
1716
    d_infoMap.getInfo(a)->print();
1717
10452
  Trace("arrays-crl")<<"  ------------  and "<<b<<"\n";
1718
10452
  if(Trace.isOn("arrays-crl"))
1719
    d_infoMap.getInfo(b)->print();
1720
1721
10452
  const CTNodeList* i_a = d_infoMap.getIndices(a);
1722
10452
  size_t it = 0;
1723
20904
  TNode constArr = d_infoMap.getConstArr(b);
1724
10452
  if (!constArr.isNull()) {
1725
775
    for( ; it < i_a->size(); ++it) {
1726
664
      TNode i = (*i_a)[it];
1727
664
      Node selConst = NodeManager::currentNM()->mkNode(kind::SELECT, constArr, i);
1728
332
      if (!d_equalityEngine->hasTerm(selConst))
1729
      {
1730
332
        preRegisterTermInternal(selConst);
1731
      }
1732
    }
1733
  }
1734
1735
10452
  const CTNodeList* st_b = d_infoMap.getStores(b);
1736
10452
  const CTNodeList* inst_b = d_infoMap.getInStores(b);
1737
  size_t its;
1738
1739
20904
  RowLemmaType lem;
1740
1741
68634
  for(it = 0 ; it < i_a->size(); ++it) {
1742
116364
    TNode i = (*i_a)[it];
1743
58182
    its = 0;
1744
95512
    for ( ; its < st_b->size(); ++its) {
1745
37330
      TNode store = (*st_b)[its];
1746
18665
      Assert(store.getKind() == kind::STORE);
1747
37330
      TNode j = store[1];
1748
37330
      TNode c = store[0];
1749
18665
      lem = std::make_tuple(store, c, j, i);
1750
18665
      Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowLemmas ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n";
1751
18665
      queueRowLemma(lem);
1752
    }
1753
  }
1754
1755
10452
  if (!options::arraysOptimizeLinear() || d_infoMap.isNonLinear(b)) {
1756
35906
    for(it = 0 ; it < i_a->size(); ++it ) {
1757
64788
      TNode i = (*i_a)[it];
1758
32394
      its = 0;
1759
65422
      for ( ; its < inst_b->size(); ++its) {
1760
33028
        TNode store = (*inst_b)[its];
1761
16514
        Assert(store.getKind() == kind::STORE);
1762
33028
        TNode j = store[1];
1763
33028
        TNode c = store[0];
1764
16514
        lem = std::make_tuple(store, c, j, i);
1765
16514
        Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::checkRowLemmas ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n";
1766
16514
        queueRowLemma(lem);
1767
      }
1768
    }
1769
  }
1770
10452
  Trace("arrays-crl")<<"Arrays::checkLemmas done.\n";
1771
}
1772
1773
18769
void TheoryArrays::propagateRowLemma(RowLemmaType lem)
1774
{
1775
37538
  Debug("pf::array") << "TheoryArrays: RowLemma Propagate called. options::arraysPropagate() = "
1776
18769
                     << options::arraysPropagate() << std::endl;
1777
1778
30453
  TNode a, b, i, j;
1779
18769
  std::tie(a, b, i, j) = lem;
1780
1781
18769
  Assert(a.getType().isArray() && b.getType().isArray());
1782
18769
  if (d_equalityEngine->areEqual(a, b) || d_equalityEngine->areEqual(i, j))
1783
  {
1784
    return;
1785
  }
1786
1787
18769
  NodeManager* nm = NodeManager::currentNM();
1788
30453
  Node aj = nm->mkNode(kind::SELECT, a, j);
1789
30453
  Node bj = nm->mkNode(kind::SELECT, b, j);
1790
1791
  // Try to avoid introducing new read terms: track whether these already exist
1792
18769
  bool ajExists = d_equalityEngine->hasTerm(aj);
1793
18769
  bool bjExists = d_equalityEngine->hasTerm(bj);
1794
18769
  bool bothExist = ajExists && bjExists;
1795
1796
  // If propagating, check propagations
1797
18769
  int prop = options::arraysPropagate();
1798
18769
  if (prop > 0) {
1799
18769
    if (d_equalityEngine->areDisequal(i, j, true) && (bothExist || prop > 1))
1800
    {
1801
7081
      Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::queueRowLemma: propagating aj = bj ("<<aj<<", "<<bj<<")\n";
1802
14162
      Node aj_eq_bj = aj.eqNode(bj);
1803
      Node reason =
1804
14162
          (i.isConst() && j.isConst()) ? d_true : i.eqNode(j).notNode();
1805
7081
      d_permRef.push_back(reason);
1806
7081
      if (!ajExists) {
1807
1831
        preRegisterTermInternal(aj);
1808
      }
1809
7081
      if (!bjExists) {
1810
4065
        preRegisterTermInternal(bj);
1811
      }
1812
7081
      d_im.assertInference(
1813
          aj_eq_bj, true, InferenceId::ARRAYS_READ_OVER_WRITE, reason, PfRule::ARRAYS_READ_OVER_WRITE);
1814
7081
      ++d_numProp;
1815
7081
      return;
1816
    }
1817
11688
    if (bothExist && d_equalityEngine->areDisequal(aj, bj, true))
1818
    {
1819
4
      Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::queueRowLemma: propagating i = j ("<<i<<", "<<j<<")\n";
1820
      Node reason =
1821
8
          (aj.isConst() && bj.isConst()) ? d_true : aj.eqNode(bj).notNode();
1822
8
      Node j_eq_i = j.eqNode(i);
1823
4
      d_im.assertInference(
1824
          j_eq_i, true, InferenceId::ARRAYS_READ_OVER_WRITE_CONTRA, reason, PfRule::ARRAYS_READ_OVER_WRITE_CONTRA);
1825
4
      ++d_numProp;
1826
4
      return;
1827
    }
1828
  }
1829
}
1830
1831
59822
void TheoryArrays::queueRowLemma(RowLemmaType lem)
1832
{
1833
59822
  Debug("pf::array") << "Array solver: queue row lemma called" << std::endl;
1834
1835
59822
  if (d_state.isInConflict() || d_RowAlreadyAdded.contains(lem))
1836
  {
1837
75384
    return;
1838
  }
1839
44260
  TNode a, b, i, j;
1840
28585
  std::tie(a, b, i, j) = lem;
1841
1842
28585
  Assert(a.getType().isArray() && b.getType().isArray());
1843
28585
  if (d_equalityEngine->areEqual(a, b) || d_equalityEngine->areEqual(i, j))
1844
  {
1845
12254
    return;
1846
  }
1847
1848
16331
  NodeManager* nm = NodeManager::currentNM();
1849
32006
  Node aj = nm->mkNode(kind::SELECT, a, j);
1850
32006
  Node bj = nm->mkNode(kind::SELECT, b, j);
1851
1852
  // Try to avoid introducing new read terms: track whether these already exist
1853
16331
  bool ajExists = d_equalityEngine->hasTerm(aj);
1854
16331
  bool bjExists = d_equalityEngine->hasTerm(bj);
1855
16331
  bool bothExist = ajExists && bjExists;
1856
1857
  // If propagating, check propagations
1858
16331
  int prop = options::arraysPropagate();
1859
16331
  if (prop > 0) {
1860
16331
    propagateRowLemma(lem);
1861
  }
1862
1863
  // Prefer equality between indexes so as not to introduce new read terms
1864
41726
  if (options::arraysEagerIndexSplitting() && !bothExist
1865
40038
      && !d_equalityEngine->areDisequal(i, j, false))
1866
  {
1867
9186
    Node i_eq_j;
1868
4593
    i_eq_j = d_valuation.ensureLiteral(i.eqNode(j));  // TODO: think about this
1869
#if 0
1870
    i_eq_j = i.eqNode(j);
1871
#endif
1872
4593
    getOutputChannel().requirePhase(i_eq_j, true);
1873
4593
    d_decisionRequests.push(i_eq_j);
1874
  }
1875
1876
  // TODO: maybe add triggers here
1877
1878
16331
  if (options::arraysEagerLemmas() || bothExist)
1879
  {
1880
    // Make sure that any terms introduced by rewriting are appropriately stored in the equality database
1881
3278
    Node aj2 = Rewriter::rewrite(aj);
1882
1967
    if (aj != aj2) {
1883
656
      if (!ajExists) {
1884
        preRegisterTermInternal(aj);
1885
      }
1886
656
      if (!d_equalityEngine->hasTerm(aj2))
1887
      {
1888
        preRegisterTermInternal(aj2);
1889
      }
1890
1968
      d_im.assertInference(
1891
1312
          aj.eqNode(aj2), true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO);
1892
    }
1893
3278
    Node bj2 = Rewriter::rewrite(bj);
1894
1967
    if (bj != bj2) {
1895
497
      if (!bjExists) {
1896
        preRegisterTermInternal(bj);
1897
      }
1898
497
      if (!d_equalityEngine->hasTerm(bj2))
1899
      {
1900
        preRegisterTermInternal(bj2);
1901
      }
1902
1491
      d_im.assertInference(
1903
994
          bj.eqNode(bj2), true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO);
1904
    }
1905
1967
    if (aj2 == bj2) {
1906
656
      return;
1907
    }
1908
1909
    // construct lemma
1910
2622
    Node eq1 = aj2.eqNode(bj2);
1911
2622
    Node eq1_r = Rewriter::rewrite(eq1);
1912
1311
    if (eq1_r == d_true) {
1913
      if (!d_equalityEngine->hasTerm(aj2))
1914
      {
1915
        preRegisterTermInternal(aj2);
1916
      }
1917
      if (!d_equalityEngine->hasTerm(bj2))
1918
      {
1919
        preRegisterTermInternal(bj2);
1920
      }
1921
      d_im.assertInference(eq1, true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO);
1922
      return;
1923
    }
1924
1925
2622
    Node eq2 = i.eqNode(j);
1926
2622
    Node eq2_r = Rewriter::rewrite(eq2);
1927
1311
    if (eq2_r == d_true) {
1928
      d_im.assertInference(eq2, true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO);
1929
      return;
1930
    }
1931
1932
2622
    Node lemma = nm->mkNode(kind::OR, eq2_r, eq1_r);
1933
1934
1311
    Trace("arrays-lem") << "Arrays::addRowLemma (1) adding " << lemma << "\n";
1935
1311
    d_RowAlreadyAdded.insert(lem);
1936
    // use non-rewritten nodes
1937
2622
    d_im.arrayLemma(
1938
2622
        aj.eqNode(bj), InferenceId::ARRAYS_READ_OVER_WRITE, eq2.notNode(), PfRule::ARRAYS_READ_OVER_WRITE);
1939
1311
    ++d_numRow;
1940
  }
1941
  else {
1942
14364
    d_RowQueue.push(lem);
1943
  }
1944
}
1945
1946
2523676
Node TheoryArrays::getNextDecisionRequest()
1947
{
1948
2523676
  if(! d_decisionRequests.empty()) {
1949
25558
    Node n = d_decisionRequests.front();
1950
12779
    d_decisionRequests.pop();
1951
12779
    return n;
1952
  }
1953
2510897
  return Node::null();
1954
}
1955
1956
1957
1493
bool TheoryArrays::dischargeLemmas()
1958
{
1959
1493
  bool lemmasAdded = false;
1960
1493
  size_t sz = d_RowQueue.size();
1961
19306
  for (unsigned count = 0; count < sz; ++count) {
1962
20180
    RowLemmaType l = d_RowQueue.front();
1963
18248
    d_RowQueue.pop();
1964
18248
    if (d_RowAlreadyAdded.contains(l)) {
1965
10434
      continue;
1966
    }
1967
1968
9746
    TNode a, b, i, j;
1969
7814
    std::tie(a, b, i, j) = l;
1970
7814
    Assert(a.getType().isArray() && b.getType().isArray());
1971
1972
7814
    NodeManager* nm = NodeManager::currentNM();
1973
9746
    Node aj = nm->mkNode(kind::SELECT, a, j);
1974
9746
    Node bj = nm->mkNode(kind::SELECT, b, j);
1975
7814
    bool ajExists = d_equalityEngine->hasTerm(aj);
1976
7814
    bool bjExists = d_equalityEngine->hasTerm(bj);
1977
1978
    // Check for redundant lemma
1979
    // TODO: more checks possible (i.e. check d_RowAlreadyAdded in context)
1980
31256
    if (!d_equalityEngine->hasTerm(i) || !d_equalityEngine->hasTerm(j)
1981
15628
        || d_equalityEngine->areEqual(i, j) || !d_equalityEngine->hasTerm(a)
1982
12892
        || !d_equalityEngine->hasTerm(b) || d_equalityEngine->areEqual(a, b)
1983
28092
        || (ajExists && bjExists && d_equalityEngine->areEqual(aj, bj)))
1984
    {
1985
5376
      continue;
1986
    }
1987
1988
2438
    int prop = options::arraysPropagate();
1989
2438
    if (prop > 0) {
1990
2438
      propagateRowLemma(l);
1991
2438
      if (d_state.isInConflict())
1992
      {
1993
435
        return true;
1994
      }
1995
    }
1996
1997
    // Make sure that any terms introduced by rewriting are appropriately stored in the equality database
1998
3935
    Node aj2 = Rewriter::rewrite(aj);
1999
2003
    if (aj != aj2) {
2000
71
      if (!ajExists) {
2001
71
        preRegisterTermInternal(aj);
2002
      }
2003
71
      if (!d_equalityEngine->hasTerm(aj2))
2004
      {
2005
        preRegisterTermInternal(aj2);
2006
      }
2007
213
      d_im.assertInference(
2008
142
          aj.eqNode(aj2), true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO);
2009
    }
2010
3935
    Node bj2 = Rewriter::rewrite(bj);
2011
2003
    if (bj != bj2) {
2012
98
      if (!bjExists) {
2013
25
        preRegisterTermInternal(bj);
2014
      }
2015
98
      if (!d_equalityEngine->hasTerm(bj2))
2016
      {
2017
        preRegisterTermInternal(bj2);
2018
      }
2019
294
      d_im.assertInference(
2020
196
          bj.eqNode(bj2), true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO);
2021
    }
2022
2003
    if (aj2 == bj2) {
2023
71
      continue;
2024
    }
2025
2026
    // construct lemma
2027
3864
    Node eq1 = aj2.eqNode(bj2);
2028
3864
    Node eq1_r = Rewriter::rewrite(eq1);
2029
1932
    if (eq1_r == d_true) {
2030
      if (!d_equalityEngine->hasTerm(aj2))
2031
      {
2032
        preRegisterTermInternal(aj2);
2033
      }
2034
      if (!d_equalityEngine->hasTerm(bj2))
2035
      {
2036
        preRegisterTermInternal(bj2);
2037
      }
2038
      d_im.assertInference(eq1, true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO);
2039
      continue;
2040
    }
2041
2042
3864
    Node eq2 = i.eqNode(j);
2043
3864
    Node eq2_r = Rewriter::rewrite(eq2);
2044
1932
    if (eq2_r == d_true) {
2045
      d_im.assertInference(eq2, true, InferenceId::UNKNOWN, d_true, PfRule::MACRO_SR_PRED_INTRO);
2046
      continue;
2047
    }
2048
2049
3864
    Node lem = nm->mkNode(kind::OR, eq2_r, eq1_r);
2050
2051
1932
    Trace("arrays-lem") << "Arrays::addRowLemma (2) adding " << lem << "\n";
2052
1932
    d_RowAlreadyAdded.insert(l);
2053
    // use non-rewritten nodes, theory preprocessing will rewrite
2054
3864
    d_im.arrayLemma(
2055
3864
        aj.eqNode(bj), InferenceId::ARRAYS_READ_OVER_WRITE, eq2.notNode(), PfRule::ARRAYS_READ_OVER_WRITE);
2056
1932
    ++d_numRow;
2057
1932
    lemmasAdded = true;
2058
3864
    if (options::arraysReduceSharing()) {
2059
      return true;
2060
    }
2061
  }
2062
1058
  return lemmasAdded;
2063
}
2064
2065
52
void TheoryArrays::conflict(TNode a, TNode b) {
2066
52
  Debug("pf::array") << "TheoryArrays::Conflict called" << std::endl;
2067
52
  if (d_inCheckModel)
2068
  {
2069
    // if in check model, don't send the conflict
2070
    d_state.notifyInConflict();
2071
    return;
2072
  }
2073
52
  d_im.conflictEqConstantMerge(a, b);
2074
}
2075
2076
8995
TheoryArrays::TheoryArraysDecisionStrategy::TheoryArraysDecisionStrategy(
2077
8995
    TheoryArrays* ta)
2078
8995
    : d_ta(ta)
2079
{
2080
8995
}
2081
8592
void TheoryArrays::TheoryArraysDecisionStrategy::initialize() {}
2082
2523676
Node TheoryArrays::TheoryArraysDecisionStrategy::getNextDecisionRequest()
2083
{
2084
2523676
  return d_ta->getNextDecisionRequest();
2085
}
2086
2532268
std::string TheoryArrays::TheoryArraysDecisionStrategy::identify() const
2087
{
2088
2532268
  return std::string("th_arrays_dec");
2089
}
2090
2091
24127
TrustNode TheoryArrays::expandDefinition(Node node)
2092
{
2093
24127
  NodeManager* nm = NodeManager::currentNM();
2094
24127
  Kind kind = node.getKind();
2095
2096
  /* Expand
2097
   *
2098
   *   (eqrange a b i j)
2099
   *
2100
   * to
2101
   *
2102
   *  forall k . i <= k <= j => a[k] = b[k]
2103
   *
2104
   */
2105
24127
  if (kind == kind::EQ_RANGE)
2106
  {
2107
40
    TNode a = node[0];
2108
40
    TNode b = node[1];
2109
40
    TNode i = node[2];
2110
40
    TNode j = node[3];
2111
40
    Node k = nm->mkBoundVar(i.getType());
2112
40
    Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, k);
2113
40
    TypeNode type = k.getType();
2114
2115
    Kind kle;
2116
40
    Node range;
2117
20
    if (type.isBitVector())
2118
    {
2119
16
      kle = kind::BITVECTOR_ULE;
2120
    }
2121
4
    else if (type.isFloatingPoint())
2122
    {
2123
      kle = kind::FLOATINGPOINT_LEQ;
2124
    }
2125
4
    else if (type.isInteger() || type.isReal())
2126
    {
2127
4
      kle = kind::LEQ;
2128
    }
2129
    else
2130
    {
2131
      Unimplemented() << "Type " << type << " is not supported for predicate "
2132
                      << kind;
2133
    }
2134
2135
20
    range = nm->mkNode(kind::AND, nm->mkNode(kle, i, k), nm->mkNode(kle, k, j));
2136
2137
    Node eq = nm->mkNode(kind::EQUAL,
2138
40
                         nm->mkNode(kind::SELECT, a, k),
2139
80
                         nm->mkNode(kind::SELECT, b, k));
2140
40
    Node implies = nm->mkNode(kind::IMPLIES, range, eq);
2141
40
    Node ret = nm->mkNode(kind::FORALL, bvl, implies);
2142
20
    return TrustNode::mkTrustRewrite(node, ret, nullptr);
2143
  }
2144
24107
  return TrustNode::null();
2145
}
2146
2147
4901
void TheoryArrays::computeRelevantTerms(std::set<Node>& termSet)
2148
{
2149
4901
  NodeManager* nm = NodeManager::currentNM();
2150
  // make sure RIntro1 reads are included in the relevant set of reads
2151
4901
  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
2152
29963
  for (; !eqcs_i.isFinished(); ++eqcs_i)
2153
  {
2154
13511
    Node eqc = (*eqcs_i);
2155
12531
    if (!eqc.getType().isArray())
2156
    {
2157
      // not an array, skip
2158
11551
      continue;
2159
    }
2160
980
    eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, d_equalityEngine);
2161
4628
    for (; !eqc_i.isFinished(); ++eqc_i)
2162
    {
2163
3648
      Node n = *eqc_i;
2164
1824
      if (termSet.find(n) != termSet.end())
2165
      {
2166
1798
        if (n.getKind() == kind::STORE)
2167
        {
2168
          // Make sure RIntro1 reads are included
2169
1010
          Node r = nm->mkNode(kind::SELECT, n, n[1]);
2170
1010
          Trace("arrays::collectModelInfo")
2171
505
              << "TheoryArrays::collectModelInfo, adding RIntro1 read: " << r
2172
505
              << endl;
2173
505
          termSet.insert(r);
2174
        }
2175
      }
2176
    }
2177
  }
2178
2179
  // Now do a fixed-point iteration to get all reads that need to be included
2180
  // because of RIntro2 rule
2181
  bool changed;
2182
5005
  do
2183
  {
2184
5005
    changed = false;
2185
5005
    eqcs_i = eq::EqClassesIterator(d_equalityEngine);
2186
33235
    for (; !eqcs_i.isFinished(); ++eqcs_i)
2187
    {
2188
28230
      Node eqc = (*eqcs_i);
2189
14115
      eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, d_equalityEngine);
2190
74955
      for (; !eqc_i.isFinished(); ++eqc_i)
2191
      {
2192
60840
        Node n = *eqc_i;
2193
30420
        if (n.getKind() == kind::SELECT && termSet.find(n) != termSet.end())
2194
        {
2195
          // Find all terms equivalent to n[0] and get corresponding read terms
2196
17120
          Node array_eqc = d_equalityEngine->getRepresentative(n[0]);
2197
          eq::EqClassIterator array_eqc_i =
2198
8560
              eq::EqClassIterator(array_eqc, d_equalityEngine);
2199
72508
          for (; !array_eqc_i.isFinished(); ++array_eqc_i)
2200
          {
2201
63948
            Node arr = *array_eqc_i;
2202
63948
            if (arr.getKind() == kind::STORE
2203
42151
                && termSet.find(arr) != termSet.end()
2204
74125
                && !d_equalityEngine->areEqual(arr[1], n[1]))
2205
            {
2206
12968
              Node r = nm->mkNode(kind::SELECT, arr, n[1]);
2207
12968
              if (termSet.find(r) == termSet.end()
2208
12968
                  && d_equalityEngine->hasTerm(r))
2209
              {
2210
66
                Trace("arrays::collectModelInfo")
2211
                    << "TheoryArrays::collectModelInfo, adding RIntro2(a) "
2212
33
                       "read: "
2213
33
                    << r << endl;
2214
33
                termSet.insert(r);
2215
33
                changed = true;
2216
              }
2217
6484
              r = nm->mkNode(kind::SELECT, arr[0], n[1]);
2218
12968
              if (termSet.find(r) == termSet.end()
2219
12968
                  && d_equalityEngine->hasTerm(r))
2220
              {
2221
134
                Trace("arrays::collectModelInfo")
2222
                    << "TheoryArrays::collectModelInfo, adding RIntro2(b) "
2223
67
                       "read: "
2224
67
                    << r << endl;
2225
67
                termSet.insert(r);
2226
67
                changed = true;
2227
              }
2228
            }
2229
          }
2230
2231
          // Find all stores in which n[0] appears and get corresponding read
2232
          // terms
2233
8560
          const CTNodeList* instores = d_infoMap.getInStores(array_eqc);
2234
8560
          size_t it = 0;
2235
30172
          for (; it < instores->size(); ++it)
2236
          {
2237
21612
            TNode instore = (*instores)[it];
2238
10806
            Assert(instore.getKind() == kind::STORE);
2239
21612
            if (termSet.find(instore) != termSet.end()
2240
21612
                && !d_equalityEngine->areEqual(instore[1], n[1]))
2241
            {
2242
14638
              Node r = nm->mkNode(kind::SELECT, instore, n[1]);
2243
14638
              if (termSet.find(r) == termSet.end()
2244
14638
                  && d_equalityEngine->hasTerm(r))
2245
              {
2246
486
                Trace("arrays::collectModelInfo")
2247
                    << "TheoryArrays::collectModelInfo, adding RIntro2(c) "
2248
243
                       "read: "
2249
243
                    << r << endl;
2250
243
                termSet.insert(r);
2251
243
                changed = true;
2252
              }
2253
7319
              r = nm->mkNode(kind::SELECT, instore[0], n[1]);
2254
14638
              if (termSet.find(r) == termSet.end()
2255
14638
                  && d_equalityEngine->hasTerm(r))
2256
              {
2257
152
                Trace("arrays::collectModelInfo")
2258
                    << "TheoryArrays::collectModelInfo, adding RIntro2(d) "
2259
76
                       "read: "
2260
76
                    << r << endl;
2261
76
                termSet.insert(r);
2262
76
                changed = true;
2263
              }
2264
            }
2265
          }
2266
        }
2267
      }
2268
    }
2269
  } while (changed);
2270
4901
}
2271
2272
}/* CVC4::theory::arrays namespace */
2273
}/* CVC4::theory namespace */
2274
26676
}/* CVC4 namespace */