src/theory/arrays/theory_arrays.cpp

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