From f12e84734aa26c602b1cebba21e8024fa32b7f00 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Sat, 30 Mar 2013 20:27:37 -0400
Subject: [PATCH] Disabling eager array index splitting for QF_AUFLIA Minor
 changes to model-based array solver

---
 src/smt/smt_engine.cpp              | 10 ++++++++++
 src/theory/arrays/theory_arrays.cpp | 22 ++++++++++++++++++++--
 2 files changed, 30 insertions(+), 2 deletions(-)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 147cea85b..21a37a43d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -864,6 +864,16 @@ void SmtEngine::setLogicInternal() throw() {
     Trace("smt") << "setting ite simplification to " << iteSimp << endl;
     options::doITESimp.set(iteSimp);
   }
+  // Turn off array eager index splitting for QF_AUFLIA
+  if(! options::arraysEagerIndexSplitting.wasSetByUser()) {
+    if (not d_logic.isQuantified() &&
+        d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+        d_logic.isTheoryEnabled(THEORY_UF) &&
+        d_logic.isTheoryEnabled(THEORY_ARITH)) {
+      Trace("smt") << "setting array eager index splitting to false" << endl;
+      options::arraysEagerIndexSplitting.set(false);
+    }
+  }
   // Turn on multiple-pass non-clausal simplification for QF_AUFBV
   if(! options::repeatSimp.wasSetByUser()) {
     bool repeatSimp = !d_logic.isQuantified() &&
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 783929f97..02f4152e9 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1060,7 +1060,9 @@ void TheoryArrays::checkModel(Effort e)
   unsigned constraintIdx;
   Node assertion, assertionToCheck;
   vector<TNode> assumptions;
+  //  int numrestarts = 0;
   while (true) {
+    //    ++numrestarts;
     int level = getSatContext()->getLevel();
     d_getModelValCache.clear();
     for (constraintIdx = 0; constraintIdx < d_modelConstraints.size(); ++constraintIdx) {
@@ -1133,7 +1135,6 @@ void TheoryArrays::checkModel(Effort e)
           all.insert(t);
         }
       }
-      //      d_lemmas.push_back(mkAnd(assumptions, true));
 
       bool eq = false;
       Node decision, explanation;
@@ -1198,6 +1199,23 @@ void TheoryArrays::checkModel(Effort e)
         d_conflict = true;
         break;
       }
+      {
+        // generate lemma
+        // if (all.size() == 0) {
+        //   d_lemmas.push_back(decision.negate());
+        // }
+        // else {
+        //   NodeBuilder<> disjunction(kind::OR);
+        //   std::set<TNode>::const_iterator it = all.begin();
+        //   std::set<TNode>::const_iterator it_end = all.end();
+        //   while (it != it_end) {
+        //     disjunction << (*it).negate();
+        //     ++it;
+        //   }
+        //   disjunction << decision.negate();
+        //   d_lemmas.push_back(disjunction);
+        // }
+      }
       d_equalityEngine.assertEquality(decision, eq, explanation);
       if (!eq) decision = decision.notNode();
       Debug("arrays-model-based") << "Asserting learned literal " << decision << " with explanation " << explanation << endl;
@@ -1257,7 +1275,7 @@ void TheoryArrays::checkModel(Effort e)
     assumptions.clear();
   }
 #ifdef CVC4_ASSERTIONS
-  if (!d_conflict) {
+  if (!d_conflict && fullEffort(e)) {
     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);
-- 
2.30.2