src/theory/arrays/theory_arrays.cpp

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