New model-based array procedure

5 files changed, 1012 insertions, 128 deletions

diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp
index bb9a9e417..32eaff355 100644
--- a/src/theory/arrays/array_info.cpp
+++ b/src/theory/arrays/array_info.cpp
@@ -167,6 +167,20 @@ void ArrayInfo::setRIntro1Applied(const TNode a) {
   
 }
 
+void ArrayInfo::setModelRep(const TNode a, const TNode b) {
+  Assert(a.getType().isArray());
+  Info* temp_info;
+  CNodeInfoMap::iterator it = info_map.find(a);
+  if(it == info_map.end()) {
+    temp_info = new Info(ct, bck);
+    temp_info->modelRep = b;
+    info_map[a] = temp_info;
+  } else {
+    (*it).second->modelRep = b;
+  }
+  
+}
+
 /**
  * Returns the information associated with TNode a
  */
@@ -200,6 +214,16 @@ const bool ArrayInfo::rIntro1Applied(const TNode a) const
   return false;
 }
 
+const TNode ArrayInfo::getModelRep(const TNode a) const
+{
+  CNodeInfoMap::const_iterator it = info_map.find(a);
+
+  if(it!= info_map.end()) {
+    return (*it).second->modelRep;
+  }
+  return TNode();
+}
+
 const CTNodeList* ArrayInfo::getIndices(const TNode a) const{
   CNodeInfoMap::const_iterator it = info_map.find(a);
   if(it!= info_map.end()) {
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index 13fae2ae5..10c15fd0e 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -63,11 +63,12 @@ class Info {
 public:
   context::CDO<bool> isNonLinear;
   context::CDO<bool> rIntro1Applied;
+  context::CDO<TNode> modelRep;
   CTNodeList* indices;
   CTNodeList* stores;
   CTNodeList* in_stores;
 
-  Info(context::Context* c, Backtracker<TNode>* bck) : isNonLinear(c, false), rIntro1Applied(c, false) {
+  Info(context::Context* c, Backtracker<TNode>* bck) : isNonLinear(c, false), rIntro1Applied(c, false), modelRep(c,TNode()) {
     indices = new(true)CTNodeList(c);
     stores = new(true)CTNodeList(c);
     in_stores = new(true)CTNodeList(c);
@@ -209,6 +210,7 @@ public:
 
   void setNonLinear(const TNode a);
   void setRIntro1Applied(const TNode a);
+  void setModelRep(const TNode a, const TNode rep);
 
   /**
    * Returns the information associated with TNode a
@@ -220,6 +222,8 @@ public:
 
   const bool rIntro1Applied(const TNode a) const;
 
+  const TNode getModelRep(const TNode a) const;
+
   const CTNodeList* getIndices(const TNode a) const;
 
   const CTNodeList* getStores(const TNode a) const;
diff --git a/src/theory/arrays/options b/src/theory/arrays/options
index 755cf239c..41c56f51d 100644
--- a/src/theory/arrays/options
+++ b/src/theory/arrays/options
@@ -11,4 +11,10 @@ option arraysOptimizeLinear --arrays-optimize-linear bool :default true :read-wr
 option arraysLazyRIntro1 --arrays-lazy-rintro1 bool :default true :read-write
  turn on optimization to only perform RIntro1 rule lazily (see Jovanovic/Barrett 2012: Being Careful with Theory Combination)
 
+option arraysModelBased --arrays-model-based bool :default false :read-write
+ turn on model-based arrray solver
+
+option arraysEagerIndexSplitting --arrays-eager-index bool :default false :read-write
+ turn on eager index splitting for generated array lemmas
+
 endmodule
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index dcf4813fc..5984296e3 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -48,7 +48,7 @@ const bool d_solveWrite2 = false;
   // These are now options
   //bool d_useNonLinearOpt = true;
   //bool d_lazyRIntro1 = true;
-const bool d_eagerIndexSplitting = true;
+  //bool d_eagerIndexSplitting = false;
 
 TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
   Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo, qe),
@@ -58,6 +58,10 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC
   d_numExplain("theory::arrays::number of explanations", 0),
   d_numNonLinear("theory::arrays::number of calls to setNonLinear", 0),
   d_numSharedArrayVarSplits("theory::arrays::number of shared array var splits", 0),
+  d_numGetModelValSplits("theory::arrays::number of getModelVal splits", 0),
+  d_numGetModelValConflicts("theory::arrays::number of getModelVal conflicts", 0),
+  d_numSetModelValSplits("theory::arrays::number of setModelVal splits", 0),
+  d_numSetModelValConflicts("theory::arrays::number of setModelVal conflicts", 0),
   d_checkTimer("theory::arrays::checkTime"),
   d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP"),
   d_ppFacts(u),
@@ -79,8 +83,11 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC
   d_sharedOther(c),
   d_sharedTerms(c, false),
   d_reads(c),
+  d_skolemIndex(c, 0),
   d_decisionRequests(c),
-  d_permRef(c)
+  d_permRef(c),
+  d_modelConstraints(c),
+  d_inCheckModel(false)
 {
   StatisticsRegistry::registerStat(&d_numRow);
   StatisticsRegistry::registerStat(&d_numExt);
@@ -88,6 +95,10 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC
   StatisticsRegistry::registerStat(&d_numExplain);
   StatisticsRegistry::registerStat(&d_numNonLinear);
   StatisticsRegistry::registerStat(&d_numSharedArrayVarSplits);
+  StatisticsRegistry::registerStat(&d_numGetModelValSplits);
+  StatisticsRegistry::registerStat(&d_numGetModelValConflicts);
+  StatisticsRegistry::registerStat(&d_numSetModelValSplits);
+  StatisticsRegistry::registerStat(&d_numSetModelValConflicts);
   StatisticsRegistry::registerStat(&d_checkTimer);
 
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
@@ -140,6 +151,128 @@ bool TheoryArrays::ppDisequal(TNode a, TNode b) {
           Rewriter::rewrite(a.eqNode(b)) == d_false);
 }
 
+
+Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck)
+{
+  if (!solve1) {
+    return term;
+  }
+  if (term[0].getKind() != kind::STORE &&
+      term[1].getKind() != kind::STORE) {
+    return term;
+  }
+  TNode left = term[0];
+  TNode right = term[1];
+  int leftWrites = 0, rightWrites = 0;
+
+  // Count nested writes
+  TNode e1 = left;
+  while (e1.getKind() == kind::STORE) {
+    ++leftWrites;
+    e1 = e1[0];
+  }
+
+  TNode e2 = right;
+  while (e2.getKind() == kind::STORE) {
+    ++rightWrites;
+    e2 = e2[0];
+  }
+
+  if (rightWrites > leftWrites) {
+    TNode tmp = left;
+    left = right;
+    right = tmp;
+    int tmpWrites = leftWrites;
+    leftWrites = rightWrites;
+    rightWrites = tmpWrites;
+  }
+
+  NodeManager* nm = NodeManager::currentNM();
+  if (rightWrites == 0) {
+    if (e1 != e2) {
+      return term;
+    }
+    // write(store, index_0, v_0, index_1, v_1, ..., index_n, v_n) = store IFF
+    //
+    // read(store, index_n) = v_n &
+    // index_{n-1} != index_n -> read(store, index_{n-1}) = v_{n-1} &
+    // (index_{n-2} != index_{n-1} & index_{n-2} != index_n) -> read(store, index_{n-2}) = v_{n-2} &
+    // ...
+    // (index_1 != index_2 & ... & index_1 != index_n) -> read(store, index_1) = v_1
+    // (index_0 != index_1 & index_0 != index_2 & ... & index_0 != index_n) -> read(store, index_0) = v_0
+    TNode write_i, write_j, index_i, index_j;
+    Node conc;
+    NodeBuilder<> result(kind::AND);
+    int i, j;
+    write_i = left;
+    for (i = leftWrites-1; i >= 0; --i) {
+      index_i = write_i[1];
+
+      // build: [index_i /= index_n && index_i /= index_(n-1) &&
+      //         ... && index_i /= index_(i+1)] -> read(store, index_i) = v_i
+      write_j = left;
+      {
+        NodeBuilder<> hyp(kind::AND);
+        for (j = leftWrites - 1; j > i; --j) {
+          index_j = write_j[1];
+          if (!ppCheck || !ppDisequal(index_i, index_j)) {
+            Node hyp2(index_i.getType() == nm->booleanType()?
+                      index_i.iffNode(index_j) : index_i.eqNode(index_j));
+            hyp << hyp2.notNode();
+          }
+          write_j = write_j[0];
+        }
+
+        Node r1 = nm->mkNode(kind::SELECT, e1, index_i);
+        conc = (r1.getType() == nm->booleanType())?
+          r1.iffNode(write_i[2]) : r1.eqNode(write_i[2]);
+        if (hyp.getNumChildren() != 0) {
+          if (hyp.getNumChildren() == 1) {
+            conc = hyp.getChild(0).impNode(conc);
+          }
+          else {
+            r1 = hyp;
+            conc = r1.impNode(conc);
+          }
+        }
+
+        // And into result
+        result << conc;
+
+        // Prepare for next iteration
+        write_i = write_i[0];
+      }
+    }
+    Assert(result.getNumChildren() > 0);
+    if (result.getNumChildren() == 1) {
+      return result.getChild(0);
+    }
+    return result;
+  }
+  else {
+    if (!solve2) {
+      return term;
+    }
+    // store(...) = store(a,i,v) ==>
+    // store(store(...),i,select(a,i)) = a && select(store(...),i)=v
+    Node l = left;
+    Node tmp;
+    NodeBuilder<> nb(kind::AND);
+    while (right.getKind() == kind::STORE) {
+      tmp = nm->mkNode(kind::SELECT, l, right[1]);
+      nb << tmp.eqNode(right[2]);
+      tmp = nm->mkNode(kind::SELECT, right[0], right[1]);
+      l = nm->mkNode(kind::STORE, l, right[1], tmp);
+      right = right[0];
+    }
+    nb << solveWrite(l.eqNode(right), solve1, solve2, ppCheck);
+    return nb;
+  }
+  Unreachable();
+  return term;
+}
+
+
 Node TheoryArrays::ppRewrite(TNode term) {
   if (!d_preprocess) return term;
   d_ppEqualityEngine.addTerm(term);
@@ -163,115 +296,7 @@ Node TheoryArrays::ppRewrite(TNode term) {
       break;
     }
     case kind::EQUAL: {
-      if (!d_solveWrite) break;
-      if (term[0].getKind() == kind::STORE ||
-          term[1].getKind() == kind::STORE) {
-        TNode left = term[0];
-        TNode right = term[1];
-        int leftWrites = 0, rightWrites = 0;
-
-        // Count nested writes
-        TNode e1 = left;
-        while (e1.getKind() == kind::STORE) {
-          ++leftWrites;
-          e1 = e1[0];
-        }
-
-        TNode e2 = right;
-        while (e2.getKind() == kind::STORE) {
-          ++rightWrites;
-          e2 = e2[0];
-        }
-
-        if (rightWrites > leftWrites) {
-          TNode tmp = left;
-          left = right;
-          right = tmp;
-          int tmpWrites = leftWrites;
-          leftWrites = rightWrites;
-          rightWrites = tmpWrites;
-        }
-
-        NodeManager* nm = NodeManager::currentNM();
-        if (rightWrites == 0) {
-          if (e1 == e2) {
-            // write(store, index_0, v_0, index_1, v_1, ..., index_n, v_n) = store IFF
-            //
-            // read(store, index_n) = v_n &
-            // index_{n-1} != index_n -> read(store, index_{n-1}) = v_{n-1} &
-            // (index_{n-2} != index_{n-1} & index_{n-2} != index_n) -> read(store, index_{n-2}) = v_{n-2} &
-            // ...
-            // (index_1 != index_2 & ... & index_1 != index_n) -> read(store, index_1) = v_1
-            // (index_0 != index_1 & index_0 != index_2 & ... & index_0 != index_n) -> read(store, index_0) = v_0
-            TNode write_i, write_j, index_i, index_j;
-            Node conc;
-            NodeBuilder<> result(kind::AND);
-            int i, j;
-            write_i = left;
-            for (i = leftWrites-1; i >= 0; --i) {
-              index_i = write_i[1];
-
-              // build: [index_i /= index_n && index_i /= index_(n-1) &&
-              //         ... && index_i /= index_(i+1)] -> read(store, index_i) = v_i
-              write_j = left;
-              {
-                NodeBuilder<> hyp(kind::AND);
-                for (j = leftWrites - 1; j > i; --j) {
-                  index_j = write_j[1];
-                  if (!ppDisequal(index_i, index_j)) {
-                    Node hyp2(index_i.getType() == nm->booleanType()?
-                              index_i.iffNode(index_j) : index_i.eqNode(index_j));
-                    hyp << hyp2.notNode();
-                  }
-                  write_j = write_j[0];
-                }
-
-                Node r1 = nm->mkNode(kind::SELECT, e1, index_i);
-                conc = (r1.getType() == nm->booleanType())?
-                  r1.iffNode(write_i[2]) : r1.eqNode(write_i[2]);
-                if (hyp.getNumChildren() != 0) {
-                  if (hyp.getNumChildren() == 1) {
-                    conc = hyp.getChild(0).impNode(conc);
-                  }
-                  else {
-                    r1 = hyp;
-                    conc = r1.impNode(conc);
-                  }
-                }
-
-                // And into result
-                result << conc;
-
-                // Prepare for next iteration
-                write_i = write_i[0];
-              }
-            }
-            Assert(result.getNumChildren() > 0);
-            if (result.getNumChildren() == 1) {
-              return result.getChild(0);
-            }
-            return result;
-          }
-          break;
-        }
-        else {
-          if (!d_solveWrite2) break;
-          // store(...) = store(a,i,v) ==>
-          // store(store(...),i,select(a,i)) = a && select(store(...),i)=v
-          Node l = left;
-          Node tmp;
-          NodeBuilder<> nb(kind::AND);
-          while (right.getKind() == kind::STORE) {
-            tmp = nm->mkNode(kind::SELECT, l, right[1]);
-            nb << tmp.eqNode(right[2]);
-            tmp = nm->mkNode(kind::SELECT, right[0], right[1]);
-            l = nm->mkNode(kind::STORE, l, right[1], tmp);
-            right = right[0];
-          }
-          nb << l.eqNode(right);
-          return nb;
-        }
-      }
+      return solveWrite(term, d_solveWrite, d_solveWrite2, true);
       break;
     }
     default:
@@ -330,6 +355,9 @@ bool TheoryArrays::propagate(TNode literal)
   }
 
   // Propagate away
+  if (d_inCheckModel && getSatContext()->getLevel() != d_topLevel) {
+    return true;
+  }
   bool ok = d_out->propagate(literal);
   if (!ok) {
     d_conflict = true;
@@ -453,6 +481,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
 
     d_infoMap.addStore(node, node);
     d_infoMap.addInStore(a, node);
+    d_infoMap.setModelRep(node, node);
 
     checkStore(node);
     break;
@@ -821,7 +850,40 @@ void TheoryArrays::presolve()
 /////////////////////////////////////////////////////////////////////////////
 
 
+Node TheoryArrays::getSkolem(TNode ref, const string& name, const TypeNode& type, const string& comment, bool makeEqual)
+{
+  Node skolem;
+  std::hash_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(ref);
+  if (it == d_skolemCache.end()) {
+    NodeManager* nm = NodeManager::currentNM();
+    skolem = nm->mkSkolem(name, type, comment);
+    d_skolemCache[ref] = skolem;
+  }
+  else {
+    skolem = (*it).second;
+    if (d_equalityEngine.hasTerm(ref) &&
+        d_equalityEngine.hasTerm(skolem) &&
+        d_equalityEngine.areEqual(ref, skolem)) {
+      makeEqual = false;
+    }
+  }
+  preRegisterTermInternal(skolem);
+  if (makeEqual) {
+    Node d = skolem.eqNode(ref);
+    Debug("arrays-model-based") << "Asserting skolem equality " << d << endl;
+    d_equalityEngine.assertEquality(d, true, d_true);
+    Assert(!d_conflict);
+    d_skolemAssertions.push_back(d);
+    d_skolemIndex = d_skolemIndex + 1;
+  }
+  return skolem;
+}
+
+
 void TheoryArrays::check(Effort e) {
+  if (done() && !fullEffort(e)) {
+    return;
+  }
   TimerStat::CodeTimer codeTimer(d_checkTimer);
 
   while (!done() && !d_conflict)
@@ -852,13 +914,18 @@ void TheoryArrays::check(Effort e) {
     switch (fact.getKind()) {
       case kind::EQUAL:
         d_equalityEngine.assertEquality(fact, true, fact);
+        if (!fact[0].getType().isArray()) {
+          d_modelConstraints.push_back(fact);
+        }
         break;
       case kind::SELECT:
         d_equalityEngine.assertPredicate(fact, true, fact);
+        d_modelConstraints.push_back(fact);
         break;
       case kind::NOT:
         if (fact[0].getKind() == kind::SELECT) {
           d_equalityEngine.assertPredicate(fact[0], false, fact);
+          d_modelConstraints.push_back(fact);
         } else if (!d_equalityEngine.areDisequal(fact[0][0], fact[0][1], false)) {
           // Assert the dis-equality
           d_equalityEngine.assertEquality(fact[0], false, fact);
@@ -867,16 +934,7 @@ void TheoryArrays::check(Effort e) {
           if(fact[0][0].getType().isArray() && !d_conflict) {
             NodeManager* nm = NodeManager::currentNM();
             TypeNode indexType = fact[0][0].getType()[0];
-            TNode k;
-            std::hash_map<TNode, Node, TNodeHashFunction>::iterator it = d_diseqCache.find(fact);
-            if (it == d_diseqCache.end()) {
-              Node newk = nm->mkSkolem("array_ext_index_$$", indexType, "an extensional lemma index variable from the theory of arrays");
-              d_diseqCache[fact] = newk;
-              k = newk;
-            }
-            else {
-              k = (*it).second;
-            }
+            TNode k = getSkolem(fact,"array_ext_index_$$", indexType, "an extensional lemma index variable from the theory of arrays", false);
 
             Node ak = nm->mkNode(kind::SELECT, fact[0][0], k);
             Node bk = nm->mkNode(kind::SELECT, fact[0][1], k);
@@ -887,6 +945,9 @@ void TheoryArrays::check(Effort e) {
             d_out->lemma(lemma);
             ++d_numExt;
           }
+          else {
+            d_modelConstraints.push_back(fact);
+          }
         }
         break;
       default:
@@ -894,8 +955,11 @@ void TheoryArrays::check(Effort e) {
     }
   }
 
-  // If in conflict, output the conflict
-  if(!d_eagerLemmas && fullEffort(e) && !d_conflict) {
+  if (options::arraysModelBased() && !d_conflict && (options::arraysEagerIndexSplitting() || fullEffort(e))) {
+    checkModel();
+  }
+
+  if(!d_eagerLemmas && fullEffort(e) && !d_conflict && !options::arraysModelBased()) {
     // generate the lemmas on the worklist
     Trace("arrays-lem")<<"Arrays::discharging lemmas: "<<d_RowQueue.size()<<"\n";
     dischargeLemmas();
@@ -905,6 +969,599 @@ void TheoryArrays::check(Effort e) {
 }
 
 
+void TheoryArrays::convertNodeToAssumptions(TNode node, vector<TNode>& assumptions, TNode nodeSkip)
+{
+  Assert(node.getKind() == kind::AND);
+  for(TNode::iterator child_it = node.begin(); child_it != node.end(); ++child_it) {
+    if ((*child_it).getKind() == kind::AND) {
+      convertNodeToAssumptions(*child_it, assumptions, nodeSkip);
+    }
+    else if (*child_it != nodeSkip) {
+      assumptions.push_back(*child_it);
+    }
+  }
+}
+
+
+void TheoryArrays::preRegisterStores(TNode s)
+{
+  if (d_equalityEngine.hasTerm(s)) {
+    return;
+  }
+  if (s.getKind() == kind::STORE) {
+    preRegisterStores(s[0]);
+    preRegisterTermInternal(s);
+  }
+}
+
+
+void TheoryArrays::checkModel()
+{
+  d_inCheckModel = true;
+  d_topLevel = getSatContext()->getLevel();
+  Assert(d_skolemIndex == 0);
+  Assert(d_skolemAssertions.empty());
+
+  // TODO: record and replay decisions
+  unsigned constraintIdx;
+  Node assertion, assertionToCheck;
+  vector<TNode> assumptions;
+  while (true) {
+    int level = getSatContext()->getLevel();
+    d_getModelValCache.clear();
+    for (constraintIdx = 0; constraintIdx < d_modelConstraints.size(); ++constraintIdx) {
+      assertion = d_modelConstraints[constraintIdx];
+      if (getModelValRec(assertion) != d_true) {
+        break;
+      }
+    }
+    getSatContext()->popto(level);
+    if (constraintIdx == d_modelConstraints.size()) {
+      break;
+    }
+    
+    if (assertion.getKind() == kind::EQUAL && assertion[0].getType().isArray()) {
+      assertionToCheck = solveWrite(expandStores(assertion[0], assumptions).eqNode(expandStores(assertion[1], assumptions)), true, true, false);
+      if (assertionToCheck.getKind() == kind::AND &&
+          assertionToCheck[assertionToCheck.getNumChildren()-1].getKind() == kind::EQUAL) {
+        TNode s = assertionToCheck[assertionToCheck.getNumChildren()-1][0];
+        preRegisterStores(s);
+      }
+    }
+    else {
+      assertionToCheck = assertion;
+    }
+    // TODO: try not collecting assumptions the first time
+    while (!setModelVal(assertionToCheck, d_true, false, true, assumptions)) {
+    restart:
+      if (assertion.getKind() == kind::EQUAL) {
+        d_equalityEngine.explainEquality(assertion[0], assertion[1], true, assumptions);
+      }
+      else {
+        assumptions.push_back(assertion);
+      }
+#ifdef CVC4_ASSERTIONS
+      std::set<TNode> validAssumptions;
+      context::CDList<Assertion>::const_iterator assert_it2 = facts_begin();
+      for (; assert_it2 != facts_end(); ++assert_it2) {
+        validAssumptions.insert(*assert_it2);
+      }
+      for (unsigned i = 0; i < d_decisions.size(); ++i) {
+        validAssumptions.insert(d_decisions[i]);
+      }
+#endif
+      std::set<TNode> all;
+      std::set<TNode> explained;
+      unsigned i = 0;
+      TNode t;
+      for (; i < assumptions.size(); ++i) {
+        t = assumptions[i];
+        if (t == d_true) {
+          continue;
+        }
+        if (t.getKind() == kind::AND) {
+          for(TNode::iterator child_it = t.begin(); child_it != t.end(); ++child_it) {
+            // Assert(validAssumptions.find(*child_it) != validAssumptions.end());
+            all.insert(*child_it);
+          }
+        }
+        // Expand explanation resulting from propagating a ROW lemma
+        else if (t.getKind() == kind::OR) {
+          if ((explained.find(t) == explained.end())) {
+            Assert(t[1].getKind() == kind::EQUAL);
+            d_equalityEngine.explainEquality(t[1][0], t[1][1], false, assumptions);
+            explained.insert(t);
+          }
+          continue;
+        }
+        else {
+          // Assert(validAssumptions.find(t) != validAssumptions.end());
+          all.insert(t);
+        }
+      }
+
+      bool eq = false;
+      Node decision, explanation;
+      while (!d_decisions.empty()) {
+        getSatContext()->pop();
+        decision = d_decisions.back();
+        d_decisions.pop_back();
+        if (all.find(decision) != all.end()) {
+          all.erase(decision);
+          eq = false;
+          if (decision.getKind() == kind::NOT) {
+            decision = decision[0];
+            eq = true;
+          }
+          while (!d_decisions.empty() && all.find(d_decisions.back()) == all.end()) {
+            getSatContext()->pop();
+            d_decisions.pop_back();
+          }
+          break;
+        }
+        else {
+          decision = Node();
+        }
+      }
+      if (all.size() == 0) {
+        explanation = d_true;
+      }
+      if (all.size() == 1) {
+        // All the same, or just one
+        explanation = *(all.begin());
+      }
+      else {
+        NodeBuilder<> conjunction(kind::AND);
+        std::set<TNode>::const_iterator it = all.begin();
+        std::set<TNode>::const_iterator it_end = all.end();
+        while (it != it_end) {
+          conjunction << *it;
+          ++it;
+        }
+        explanation = conjunction;
+        d_permRef.push_back(explanation);
+      }
+      if (decision.isNull()) {
+        d_conflictNode = explanation;
+        d_conflict = true;
+        break;
+      }
+      d_equalityEngine.assertEquality(decision, eq, explanation);
+      if (!eq) decision = decision.notNode();
+      Debug("arrays-model-based") << "Asserting learned literal " << decision << " with explanation " << explanation << endl;
+      if (d_conflict) {
+        assumptions.clear();
+        convertNodeToAssumptions(d_conflictNode, assumptions, TNode());
+        assertion = d_true;
+        goto restart;
+      }
+      assumptions.clear();
+
+      // Reassert skolems if necessary
+      Node d;
+      while (d_skolemIndex < d_skolemAssertions.size()) {
+        d = d_skolemAssertions[d_skolemIndex];
+        Assert(isLeaf(d[0]));
+        if (!d_equalityEngine.hasTerm(d[0])) {
+          preRegisterTermInternal(d[0]);
+        }
+        if (d[0].getType().isArray()) {
+          Assert(d[1].getKind() == kind::STORE);
+          if (d[1][0].getKind() == kind::STORE) {
+            preRegisterTermInternal(d[1][0][0]);
+            preRegisterTermInternal(d[1][0][2]);
+          }
+          preRegisterTermInternal(d[1][0]);
+          preRegisterTermInternal(d[1][2]);
+          preRegisterTermInternal(d[1]);
+        }
+        Debug("arrays-model-based") << "Re-asserting skolem equality " << d << endl;
+        d_equalityEngine.assertEquality(d, true, d_true);
+        Assert(!d_conflict);
+        if (!d[0].getType().isArray()) {
+          if (!setModelVal(d[1], d[0], false, true, assumptions)) {
+            assertion = d_true;
+            goto restart;
+          }
+          assumptions.clear();
+        }
+        d_skolemIndex = d_skolemIndex + 1;
+      }
+    }
+    if (d_conflict) {
+      break;
+    }
+    Assert(getModelVal(assertion) == d_true);
+    assumptions.clear();
+  }
+#ifdef CVC4_ASSERTIONS
+  if (!d_conflict) {
+    context::CDList<Assertion>::const_iterator assert_it = facts_begin(), assert_it_end = facts_end();
+    for (; assert_it != assert_it_end; ++assert_it) {
+      Assert(getModelVal(*assert_it) == d_true);
+    }
+  }
+#endif
+  while (!d_decisions.empty()) {
+    Assert(!d_conflict);
+    getSatContext()->pop();
+    d_decisions.pop_back();
+  }
+  d_skolemAssertions.clear();
+  d_skolemIndex = 0;
+  Assert(getSatContext()->getLevel() == d_topLevel);
+  if (d_conflict) {
+    Node tmp = d_conflictNode;
+    d_out->conflict(tmp);
+  }
+  d_inCheckModel = false;
+}
+
+
+Node TheoryArrays::getModelVal(TNode node)
+{
+  int level = getSatContext()->getLevel();
+  d_getModelValCache.clear();
+  Node ret = getModelValRec(node);
+  getSatContext()->popto(level);
+  return ret;
+}
+
+
+Node TheoryArrays::getModelValRec(TNode node)
+{
+  if (node.isConst()) {
+    return node;
+  }
+  NodeMap::iterator it = d_getModelValCache.find(node);
+  if (it != d_getModelValCache.end()) {
+    return (*it).second;
+  }
+  Node val;
+  switch (node.getKind()) {
+    case kind::NOT:
+      val = getModelValRec(node[0]) == d_true ? d_false : d_true;
+      break;
+    case kind::AND: {
+      val = d_true;
+      for(TNode::iterator child_it = node.begin(); child_it != node.end(); ++child_it) {
+        if (getModelValRec(*child_it) != d_true) {
+          val = d_false;
+          break;
+        }
+      }
+      break;
+    }
+    case kind::IMPLIES:
+      if (getModelValRec(node[0]) == d_false) {
+        val = d_true;
+      }
+      else {
+        val = getModelValRec(node[1]);
+      }
+    case kind::EQUAL:
+      val = getModelValRec(node[0]);
+      val = (val == getModelValRec(node[1])) ? d_true : d_false;
+      break;
+    case kind::SELECT: {
+      NodeManager* nm = NodeManager::currentNM();
+      Node indexVal = getModelValRec(node[1]);
+      val = Rewriter::rewrite(nm->mkNode(kind::SELECT, node[0], indexVal));
+      if (val.isConst()) {
+        break;
+      }
+      val = Rewriter::rewrite(nm->mkNode(kind::SELECT, getModelValRec(node[0]), indexVal));
+      Assert(val.isConst());
+      break;
+    }
+    case kind::STORE: {
+      NodeManager* nm = NodeManager::currentNM();
+      val = getModelValRec(node[0]);
+      val = Rewriter::rewrite(nm->mkNode(kind::STORE, val, getModelValRec(node[1]), getModelValRec(node[2])));
+      Assert(val.isConst());
+      break;
+    }
+    default: {
+      Assert(isLeaf(node));
+      TNode eRep = d_equalityEngine.getRepresentative(node);
+      if (eRep.isConst()) {
+        val = eRep;
+        break;
+      }
+      TNode rep = d_infoMap.getModelRep(eRep);
+      if (!rep.isNull()) {
+        // TODO: check for loop here
+        val = getModelValRec(rep);
+      }
+      else {
+        NodeMap::iterator it = d_lastVal.find(eRep);
+        if (it != d_lastVal.end()) {
+          val = (*it).second;
+          if (!d_equalityEngine.hasTerm(val) ||
+              !d_equalityEngine.areDisequal(eRep, val, true)) {
+            getSatContext()->push();
+            ++d_numGetModelValSplits;
+            d_equalityEngine.assertEquality(eRep.eqNode(val), true, d_true);
+            if (!d_conflict) {
+              break;
+            }
+            ++d_numGetModelValConflicts;
+            getSatContext()->pop();
+          }
+        }
+
+        TypeEnumerator te(eRep.getType());
+        val = *te;
+        while (true) {
+          if (!d_equalityEngine.hasTerm(val) ||
+              !d_equalityEngine.areDisequal(eRep, val, true)) {
+            getSatContext()->push();
+            ++d_numGetModelValSplits;
+            d_equalityEngine.assertEquality(eRep.eqNode(val), true, d_true);
+            if (!d_conflict) {
+              d_lastVal[eRep] = val;
+              break;
+            }
+            ++d_numGetModelValConflicts;
+            getSatContext()->pop();
+          } 
+          ++te;
+          if (te.isFinished()) {
+            Assert(false);
+            // TODO: conflict
+            break;
+          }
+          val = *te;
+        }
+      }
+      break;
+    }
+  }
+  d_getModelValCache[node] = val;
+  return val;
+}
+
+
+bool TheoryArrays::hasLoop(TNode node, TNode target)
+{
+  if (node == target) {
+    return true;
+  }
+
+  if (isLeaf(node)) {
+    TNode rep = d_infoMap.getModelRep(d_equalityEngine.getRepresentative(node));
+    if (!rep.isNull()) {
+      return hasLoop(rep, target);
+    }
+    return false;
+  }
+
+  for(TNode::iterator child_it = node.begin(); child_it != node.end(); ++child_it) {
+    if (hasLoop(*child_it, target)) {
+      return true;
+    }
+  }
+  
+  return false;
+}
+
+
+// Return true iff it we were able to modify model so that value of node has same value as val
+bool TheoryArrays::setModelVal(TNode node, TNode val, bool invert, bool explain, vector<TNode>& assumptions)
+{
+  Assert(!d_conflict);
+  if (node == val) {
+    return !invert;
+  }
+  if (node.isConst()) {
+    if (invert) {
+      return (val.isConst() && node != val);
+    }
+    return val == node;
+  }
+  switch(node.getKind()) {
+    case kind::NOT:
+      Assert(val == d_true || val == d_false);
+      return setModelVal(node[0], val, !invert, explain, assumptions);
+      break;
+    case kind::AND: {
+      Assert(val == d_true || val == d_false);
+      if (val == d_false) {
+        invert = !invert;
+      }
+      int i;
+      for(i = node.getNumChildren()-1; i >=0; --i) {
+        if (setModelVal(node[i], d_true, invert, explain, assumptions) == invert) {
+          return invert;
+        }
+      }
+      return !invert;
+    }
+    case kind::IMPLIES:
+      Assert(val == d_true || val == d_false);
+      if (val == d_false) {
+        invert = !invert;
+      }
+      if (setModelVal(node[0], d_false, invert, explain, assumptions) == !invert) {
+        return !invert;
+      }
+      if (setModelVal(node[1], d_true, invert, explain, assumptions) == !invert) {
+        return !invert;
+      }
+      return invert;
+    case kind::EQUAL:
+      Assert(val == d_true || val == d_false);
+      if (val == d_false) {
+        invert = !invert;
+      }
+      if (node[0].isConst()) {
+        return setModelVal(node[1], node[0], invert, explain, assumptions);
+      }
+      else {
+        return setModelVal(node[0], node[1], invert, explain, assumptions);
+      }
+    case kind::SELECT: {
+      TNode s = node[0];
+      Node index = node[1];
+
+      while (s.getKind() == kind::STORE) {
+        if (setModelVal(s[1].eqNode(index), d_true, false, explain, assumptions)) {
+          if (setModelVal(s[2].eqNode(val), d_true, invert, explain, assumptions)) {
+            return true;
+          }
+          // Now try to set the indices to be disequal
+          if (!setModelVal(s[1].eqNode(index), d_false, false, explain, assumptions)) {
+            return false;
+          }
+          Unreachable();
+        }
+        s = s[0];
+      }
+      TNode rep = d_infoMap.getModelRep(d_equalityEngine.getRepresentative(s));
+      NodeManager* nm = NodeManager::currentNM();
+      if (!rep.isNull()) {
+        // TODO: check for loop
+        if (explain) {
+          d_equalityEngine.explainEquality(s, rep, true, assumptions);
+        }
+        return setModelVal(nm->mkNode(kind::SELECT, rep, index), val, invert, explain, assumptions);
+      }
+      if (val.getKind() == kind::SELECT && val[0].getKind() == kind::STORE) {
+        return setModelVal(val, nm->mkNode(kind::SELECT, s, index), invert, explain, assumptions);
+      }
+
+      // Solve equation for s: select(s,index) op val --> s = store(s',i',v') /\ index = i' /\ v' op val
+      Node newVarArr = getSkolem(s, "array_model_arr_var_$$", s.getType(), "a new array variable from the theory of arrays", false);
+      Assert(d_infoMap.getModelRep(d_equalityEngine.getRepresentative(newVarArr)).isNull());
+      Node lookup;
+      bool checkIndex1 = false, checkIndex2 = false, checkIndex3 = false;
+      if (!isLeaf(index)) {
+        index = getSkolem(index, "array_model_index_$$", index.getType(), "a new index variable from the theory of arrays");
+        if (!index.getType().isArray()) {
+          checkIndex1 = true;
+        }
+      }
+      lookup = nm->mkNode(kind::SELECT, s, index);
+      Node newVarVal = getSkolem(lookup, "array_model_var_$$", val.getType(), "a new value variable from the theory of arrays", false);
+
+      Node newVarVal2;
+      Node index2;
+      TNode saveVal = val;
+      if (val.getKind() == kind::SELECT && val[0] == s) {
+        // Special case: select(s,index) = select(s,j): solution becomes s = store(store(s',j,v'),index,w') /\ v' = w'
+        index2 = val[1];
+        if (!isLeaf(index2)) {
+          index2 = getSkolem(val, "array_model_index_$$", index2.getType(), "a new index variable from the theory of arrays");
+          if (!index2.getType().isArray()) {
+            checkIndex2 = true;
+          }
+        }
+        if (invert) {
+          checkIndex3 = true;
+        }
+        lookup = nm->mkNode(kind::SELECT, s, index2);
+        newVarVal2 = getSkolem(lookup, "array_model_var_$$", val.getType(), "a new value variable from the theory of arrays", false);
+        newVarArr = nm->mkNode(kind::STORE, newVarArr, index2, newVarVal2);
+        preRegisterTermInternal(newVarArr);
+        val = newVarVal2;
+      }
+
+      Node d = nm->mkNode(kind::STORE, newVarArr, index, newVarVal);
+      preRegisterTermInternal(d);
+      d = s.eqNode(d);
+      Debug("arrays-model-based") << "Asserting array skolem equality " << d << endl;
+      d_equalityEngine.assertEquality(d, true, d_true);
+      d_skolemAssertions.push_back(d);
+      d_skolemIndex = d_skolemIndex + 1;
+      Assert(!d_conflict);
+      if (checkIndex1) {
+        if (!setModelVal(node[1], index, false, explain, assumptions)) {
+          return false;
+        }
+      }
+      if (checkIndex2) {
+        if (!setModelVal(saveVal[1], index2, false, explain, assumptions)) {
+          return false;
+        }
+      }
+      if (checkIndex3) {
+        if (!setModelVal(index2, index, true, explain, assumptions)) {
+          return false;
+        }
+      }
+      return setModelVal(newVarVal, val, invert, explain, assumptions);
+    }
+    case kind::STORE:
+      if (val.getKind() != kind::STORE) {
+        return setModelVal(val, node, invert, explain, assumptions);
+      }
+      Unreachable();
+      break;
+    default: {
+      Assert(isLeaf(node));
+      TNode rep = d_infoMap.getModelRep(d_equalityEngine.getRepresentative(node));
+      if (!rep.isNull()) {
+        // Assume this array equation has already been dealt with - otherwise, it shouldn't have a rep
+        return true;
+      }
+      if (val.getKind() == kind::SELECT) {
+        return setModelVal(val, node, invert, explain, assumptions);
+      }
+      if (d_equalityEngine.hasTerm(node) &&
+          d_equalityEngine.hasTerm(val)) {
+        if ((!invert && d_equalityEngine.areDisequal(node, val, true)) ||
+            (invert && d_equalityEngine.areEqual(node, val))) {
+          if (explain) {
+            d_equalityEngine.explainEquality(node, val, invert, assumptions);
+          }
+          return false;
+        }
+        if ((!invert && d_equalityEngine.areEqual(node, val)) ||
+            (invert && d_equalityEngine.areDisequal(node, val, true))) {
+          return true;
+        }
+      }
+      getSatContext()->push();
+      Node d = node.eqNode(val);
+      d_decisions.push_back(invert ? d.notNode() : d);
+      d_equalityEngine.assertEquality(d, !invert, d_decisions.back());
+      Debug("arrays-model-based") << "Asserting " << d_decisions.back() << " with explanation " << d_decisions.back() << endl;
+      ++d_numSetModelValSplits;
+      while (d_conflict) {
+        ++d_numSetModelValConflicts;
+        Debug("arrays-model-based") << "...which results in a conflict!" << endl;
+        d = d_decisions.back();
+        unsigned sz = assumptions.size();
+        convertNodeToAssumptions(d_conflictNode, assumptions, d);
+        NodeBuilder<> conjunction(kind::AND);
+        for (unsigned i = sz; i < assumptions.size(); ++i) {
+          conjunction << assumptions[i];
+        }
+        Node explanation = conjunction;
+        getSatContext()->pop();
+        d_decisions.pop_back();
+        d_permRef.push_back(explanation);
+        d = d.negate();
+        Debug("arrays-model-based") << "Asserting learned literal " << d << " with explanation " << explanation << endl;
+        bool eq = true;
+        if (d.getKind() == kind::NOT) {
+          d = d[0];
+          eq = false;
+        }
+        d_equalityEngine.assertEquality(d, eq, explanation);
+        if (d_conflict) {
+          Assert(false);
+        }
+        return false;
+      }
+      return true;
+    }
+  }
+  Unreachable();
+  return false;
+}
+
+
 Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions)
 {
   Assert(conjunctions.size() > 0);
@@ -916,6 +1573,15 @@ Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions)
   TNode t;
   for (; i < conjunctions.size(); ++i) {
     t = conjunctions[i];
+    if (t == d_true) {
+      continue;
+    }
+
+    if (t.getKind() == kind::AND) {
+      for(TNode::iterator child_it = t.begin(); child_it != t.end(); ++child_it) {
+        all.insert(*child_it);
+      }
+    }
 
     // Expand explanation resulting from propagating a ROW lemma
     if (t.getKind() == kind::OR) {
@@ -951,6 +1617,7 @@ Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions)
 
 void TheoryArrays::setNonLinear(TNode a)
 {
+  if (options::arraysModelBased()) return;
   if (d_infoMap.isNonLinear(a)) return;
 
   Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::setNonLinear (" << a << ")\n";
@@ -1063,6 +1730,86 @@ void TheoryArrays::checkRIntro1(TNode a, TNode b)
 }
 
 
+Node TheoryArrays::removeRepLoops(TNode a, TNode rep)
+{
+  if (rep.getKind() != kind::STORE) {
+    Assert(isLeaf(rep));
+    TNode tmp = d_infoMap.getModelRep(d_equalityEngine.getRepresentative(rep));
+    if (!tmp.isNull()) {
+      Node tmp2 = removeRepLoops(a, tmp);
+      if (tmp != tmp2) {
+        return tmp2;
+      }
+    }
+    return rep;
+  }
+
+  Node s = removeRepLoops(a, rep[0]);
+  bool changed = (s != rep[0]);
+
+  Node index = rep[1];
+  Node value = rep[2];
+  Node lookup;
+
+  // TODO: Change to hasLoop?
+  if (!isLeaf(index)) {
+    changed = true;
+    index = getSkolem(index, "array_model_index_$$", index.getType(), "a new index variable from the theory of arrays", false);
+    if (!d_equalityEngine.hasTerm(index) ||
+        !d_equalityEngine.hasTerm(rep[1]) ||
+        !d_equalityEngine.areEqual(rep[1], index)) {
+      Node d = index.eqNode(rep[1]);
+      Debug("arrays-model-based") << "Asserting skolem equality " << d << endl;
+      d_equalityEngine.assertEquality(d, true, d_true);
+      d_modelConstraints.push_back(d);
+    }
+  }
+  if (!isLeaf(value)) {
+    changed = true;
+    value = getSkolem(value, "array_model_var_$$", value.getType(), "a new value variable from the theory of arrays", false);
+    if (!d_equalityEngine.hasTerm(value) ||
+        !d_equalityEngine.hasTerm(rep[2]) ||
+        !d_equalityEngine.areEqual(rep[2], value)) {
+      Node d = value.eqNode(rep[2]);
+      Debug("arrays-model-based") << "Asserting skolem equality " << d << endl;
+      d_equalityEngine.assertEquality(d, true, d_true);
+      d_modelConstraints.push_back(d);
+    }
+  }
+  if (changed) {
+    NodeManager* nm = NodeManager::currentNM();
+    return nm->mkNode(kind::STORE, s, index, value);
+  }
+  return rep;
+}
+
+
+Node TheoryArrays::expandStores(TNode s, vector<TNode>& assumptions, bool checkLoop, TNode a, TNode loopRep)
+{
+  if (s.getKind() != kind::STORE) {
+    Assert(isLeaf(s));
+    TNode tmp = d_equalityEngine.getRepresentative(s);
+    if (checkLoop && tmp == a) {
+      // Loop detected
+      d_equalityEngine.explainEquality(s, loopRep, true, assumptions);
+      return loopRep;
+    }
+    tmp = d_infoMap.getModelRep(tmp);
+    if (!tmp.isNull()) {
+      d_equalityEngine.explainEquality(s, tmp, true, assumptions);
+      return expandStores(tmp, assumptions, checkLoop, a, loopRep);
+    }
+    return s;
+  }
+  Node tmp = expandStores(s[0], assumptions, checkLoop, a, loopRep);
+  if (tmp != s[0]) {
+    NodeManager* nm = NodeManager::currentNM();
+    return nm->mkNode(kind::STORE, tmp, s[1], s[2]);
+  }
+  return s;
+}
+
+
 void TheoryArrays::mergeArrays(TNode a, TNode b)
 {
   // Note: a is the new representative
@@ -1085,7 +1832,7 @@ void TheoryArrays::mergeArrays(TNode a, TNode b)
       checkRIntro1(b, a);
     }
 
-    if (options::arraysOptimizeLinear()) {
+    if (options::arraysOptimizeLinear() && !options::arraysModelBased()) {
       bool aNL = d_infoMap.isNonLinear(a);
       bool bNL = d_infoMap.isNonLinear(b);
       if (aNL) {
@@ -1120,6 +1867,74 @@ void TheoryArrays::mergeArrays(TNode a, TNode b)
     checkRowLemmas(a,b);
     checkRowLemmas(b,a);
 
+    if (options::arraysModelBased()) {
+      TNode repA = d_infoMap.getModelRep(a);
+      Assert(repA.isNull() || d_equalityEngine.areEqual(a, repA));
+      TNode repB = d_infoMap.getModelRep(b);
+      Assert(repB.isNull() || d_equalityEngine.areEqual(a, repB));
+      Node rep;
+      bool done = false;
+      if (repA.isNull()) {
+        if (repB.isNull()) {
+          done = true;
+        }
+        else {
+          rep = repB;
+        }
+      }
+      else {
+        if (repB.isNull()) {
+          rep = repA;
+        }
+        else {
+          vector<TNode> assumptions;
+          rep = expandStores(repA, assumptions, true, a, repB);
+          if (rep != repA) {
+            Debug("arrays-model-based") << "Merging (" << a << "," << b << "): new rep is " << rep << endl;
+            d_infoMap.setModelRep(a, rep);
+            Node reason = mkAnd(assumptions);
+            d_permRef.push_back(reason);
+            d_equalityEngine.assertEquality(repA.eqNode(rep), true, reason);
+          }
+          d_modelConstraints.push_back(rep.eqNode(repB));
+          done = true;
+        }
+      }
+      if (!done) {
+        // 1. Check for store loop
+        TNode s = rep;
+        while (true) {
+          Assert(s.getKind() == kind::STORE);
+          while (s.getKind() == kind::STORE) {
+            s = s[0];
+          }
+          Assert(isLeaf(s));
+          TNode tmp = d_equalityEngine.getRepresentative(s);
+          if (tmp == a) {
+            d_modelConstraints.push_back(s.eqNode(rep));
+            rep = TNode();
+            break;
+          }
+          tmp = d_infoMap.getModelRep(tmp);
+          if (tmp.isNull()) {
+            break;
+          }
+          s = tmp;
+        }
+        if (!rep.isNull()) {
+          Node repOrig = rep;
+          rep = removeRepLoops(a, rep);
+          if (repOrig != rep) {
+            d_equalityEngine.assertEquality(repOrig.eqNode(rep), true, d_true);
+          }
+        }
+        if (rep != repA) {
+          Debug("arrays-model-based") << "Merging (" << a << "," << b << "): new rep is " << rep << endl;
+          d_infoMap.setModelRep(a, rep);
+        }
+      }
+    }
+
     // merge info adds the list of the 2nd argument to the first
     d_infoMap.mergeInfo(a, b);
 
@@ -1139,6 +1954,7 @@ void TheoryArrays::mergeArrays(TNode a, TNode b)
 
 
 void TheoryArrays::checkStore(TNode a) {
+  if (options::arraysModelBased()) return;
   Trace("arrays-cri")<<"Arrays::checkStore "<<a<<"\n";
 
   if(Trace.isOn("arrays-cri")) {
@@ -1168,6 +1984,7 @@ void TheoryArrays::checkStore(TNode a) {
 
 void TheoryArrays::checkRowForIndex(TNode i, TNode a)
 {
+  if (options::arraysModelBased()) return;
   Trace("arrays-cri")<<"Arrays::checkRowForIndex "<<a<<"\n";
   Trace("arrays-cri")<<"                   index "<<i<<"\n";
 
@@ -1211,6 +2028,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a)
 // look for new ROW lemmas
 void TheoryArrays::checkRowLemmas(TNode a, TNode b)
 {
+  if (options::arraysModelBased()) return;
   Trace("arrays-crl")<<"Arrays::checkLemmas begin \n"<<a<<"\n";
   if(Trace.isOn("arrays-crl"))
     d_infoMap.getInfo(a)->print();
@@ -1323,7 +2141,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
   }
 
   // Prefer equality between indexes so as not to introduce new read terms
-  if (d_eagerIndexSplitting && !bothExist && !d_equalityEngine.areDisequal(i,j, false)) {
+  if (options::arraysEagerIndexSplitting() && !bothExist && !d_equalityEngine.areDisequal(i,j, false)) {
     Node i_eq_j = d_valuation.ensureLiteral(i.eqNode(j));
     getOutputChannel().requirePhase(i_eq_j, true);
     d_decisionRequests.push(i_eq_j);
@@ -1494,7 +2312,9 @@ void TheoryArrays::conflict(TNode a, TNode b) {
   } else {
     d_conflictNode = explain(a.eqNode(b));
   }
-  d_out->conflict(d_conflictNode);
+  if (!d_inCheckModel) {
+    d_out->conflict(d_conflictNode);
+  }
   d_conflict = true;
 }
 
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 172482e71..ef1f3b506 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -115,6 +115,14 @@ class TheoryArrays : public Theory {
   IntStat d_numNonLinear;
   /** splits on array variables */
   IntStat d_numSharedArrayVarSplits;
+  /** splits in getModelVal */
+  IntStat d_numGetModelValSplits;
+  /** conflicts in getModelVal */
+  IntStat d_numGetModelValConflicts;
+  /** splits in setModelVal */
+  IntStat d_numSetModelValSplits;
+  /** conflicts in setModelVal */
+  IntStat d_numSetModelValConflicts;
   /** time spent in check() */
   TimerStat d_checkTimer;
 
@@ -152,6 +160,7 @@ class TheoryArrays : public Theory {
   Node preprocessTerm(TNode term);
   Node recursivePreprocessTerm(TNode term);
   bool ppDisequal(TNode a, TNode b);
+  Node solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck);
 
   public:
 
@@ -339,17 +348,23 @@ class TheoryArrays : public Theory {
   CDNodeSet d_sharedOther;
   context::CDO<bool> d_sharedTerms;
   context::CDList<TNode> d_reads;
-  std::hash_map<TNode, Node, TNodeHashFunction> d_diseqCache;
+  std::hash_map<Node, Node, NodeHashFunction> d_skolemCache;
+  context::CDO<unsigned> d_skolemIndex;
+  std::vector<Node> d_skolemAssertions;
 
   // The decision requests we have for the core
   context::CDQueue<Node> d_decisionRequests;
 
   // List of nodes that need permanent references in this context
   context::CDList<Node> d_permRef;
+  context::CDList<Node> d_modelConstraints;
 
+  Node getSkolem(TNode ref, const std::string& name, const TypeNode& type, const std::string& comment, bool makeEqual = true);
   Node mkAnd(std::vector<TNode>& conjunctions);
   void setNonLinear(TNode a);
   void checkRIntro1(TNode a, TNode b);
+  Node removeRepLoops(TNode a, TNode rep);
+  Node expandStores(TNode s, std::vector<TNode>& assumptions, bool checkLoop = false, TNode a = TNode(), TNode b = TNode());
   void mergeArrays(TNode a, TNode b);
   void checkStore(TNode a);
   void checkRowForIndex(TNode i, TNode a);
@@ -357,6 +372,21 @@ class TheoryArrays : public Theory {
   void queueRowLemma(RowLemmaType lem);
   void dischargeLemmas();
 
+  std::vector<Node> d_decisions;
+  bool d_inCheckModel;
+  int d_topLevel;
+  void convertNodeToAssumptions(TNode node, std::vector<TNode>& assumptions, TNode nodeSkip);
+  void preRegisterStores(TNode s);
+  void checkModel();
+  bool hasLoop(TNode node, TNode target);
+  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+  NodeMap d_getModelValCache;
+  NodeMap d_lastVal;
+  Node getModelVal(TNode node);
+  Node getModelValRec(TNode node);
+  bool setModelVal(TNode node, TNode val, bool invert,
+                   bool explain, std::vector<TNode>& assumptions);
+
   public:
 
   eq::EqualityEngine* getEqualityEngine() {