src/theory/arrays/theory_arrays.cpp

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