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