squash-merge from proof branch

6 files changed, 142 insertions, 41 deletions

diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp
index 55f013f8c..16412c05b 100644
--- a/src/theory/arrays/array_info.cpp
+++ b/src/theory/arrays/array_info.cpp
@@ -44,16 +44,16 @@ Info::~Info() {
   in_stores->deleteSelf();
 }
 
-ArrayInfo::ArrayInfo(context::Context* c, Backtracker<TNode>* b)
+ArrayInfo::ArrayInfo(context::Context* c, Backtracker<TNode>* b, std::string statisticsPrefix)
     : ct(c), bck(b), info_map(),
-      d_mergeInfoTimer("theory::arrays::mergeInfoTimer"),
-      d_avgIndexListLength("theory::arrays::avgIndexListLength"),
-      d_avgStoresListLength("theory::arrays::avgStoresListLength"),
-      d_avgInStoresListLength("theory::arrays::avgInStoresListLength"),
-      d_listsCount("theory::arrays::listsCount",0),
-      d_callsMergeInfo("theory::arrays::callsMergeInfo",0),
-      d_maxList("theory::arrays::maxList",0),
-      d_tableSize("theory::arrays::infoTableSize", info_map) {
+      d_mergeInfoTimer(statisticsPrefix + "theory::arrays::mergeInfoTimer"),
+      d_avgIndexListLength(statisticsPrefix + "theory::arrays::avgIndexListLength"),
+      d_avgStoresListLength(statisticsPrefix + "theory::arrays::avgStoresListLength"),
+      d_avgInStoresListLength(statisticsPrefix + "theory::arrays::avgInStoresListLength"),
+      d_listsCount(statisticsPrefix + "theory::arrays::listsCount",0),
+      d_callsMergeInfo(statisticsPrefix + "theory::arrays::callsMergeInfo",0),
+      d_maxList(statisticsPrefix + "theory::arrays::maxList",0),
+      d_tableSize(statisticsPrefix + "theory::arrays::infoTableSize", info_map) {
   emptyList = new(true) CTNodeList(ct);
   emptyInfo = new Info(ct, bck);
   smtStatisticsRegistry()->registerStat(&d_mergeInfoTimer);
@@ -208,7 +208,7 @@ void ArrayInfo::setNonLinear(const TNode a) {
   } else {
     (*it).second->isNonLinear = true;
   }
-  
+
 }
 
 void ArrayInfo::setRIntro1Applied(const TNode a) {
@@ -222,7 +222,7 @@ void ArrayInfo::setRIntro1Applied(const TNode a) {
   } else {
     (*it).second->rIntro1Applied = true;
   }
-  
+
 }
 
 void ArrayInfo::setModelRep(const TNode a, const TNode b) {
@@ -236,7 +236,7 @@ void ArrayInfo::setModelRep(const TNode a, const TNode b) {
   } else {
     (*it).second->modelRep = b;
   }
-  
+
 }
 
 void ArrayInfo::setConstArr(const TNode a, const TNode constArr) {
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index 319864c34..04b9cffb1 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -155,7 +155,8 @@ public:
   currentStatisticsRegistry()->registerStat(&d_maxList);
   currentStatisticsRegistry()->registerStat(&d_tableSize);
   }*/
-  ArrayInfo(context::Context* c, Backtracker<TNode>* b);
+
+  ArrayInfo(context::Context* c, Backtracker<TNode>* b, std::string statisticsPrefix = "");
 
   ~ArrayInfo();
 
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index d5f313ca1..be16d684d 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -54,6 +54,11 @@ typerule STORE_ALL ::CVC4::theory::arrays::ArrayStoreTypeRule
 typerule ARR_TABLE_FUN ::CVC4::theory::arrays::ArrayTableFunTypeRule
 typerule ARRAY_LAMBDA ::CVC4::theory::arrays::ArrayLambdaTypeRule
 
+operator PARTIAL_SELECT_0 0:2 "partial array select, for internal use only"
+operator PARTIAL_SELECT_1 0:2 "partial array select, for internal use only"
+typerule PARTIAL_SELECT_0 ::CVC4::theory::arrays::ArrayPartialSelectTypeRule
+typerule PARTIAL_SELECT_1 ::CVC4::theory::arrays::ArrayPartialSelectTypeRule
+
 # store operations that are ordered (by index) over a store-all are constant
 construle STORE ::CVC4::theory::arrays::ArrayStoreTypeRule
 
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 631785437..fcde18b66 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -21,13 +21,14 @@
 #include "expr/kind.h"
 #include "options/arrays_options.h"
 #include "options/smt_options.h"
+#include "proof/array_proof.h"
+#include "proof/proof_manager.h"
+#include "proof/theory_proof.h"
 #include "smt/command.h"
 #include "smt/logic_exception.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
-#include "proof/theory_proof.h"
-#include "proof/proof_manager.h"
 #include "theory/valuation.h"
 
 using namespace std;
@@ -78,7 +79,7 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u,
       d_equalityEngine(d_notify, c, name + "theory::arrays::TheoryArrays", true),
       d_conflict(c, false),
       d_backtracker(c),
-      d_infoMap(c, &d_backtracker),
+      d_infoMap(c, &d_backtracker, name),
       d_mergeQueue(c),
       d_mergeInProgress(false),
       d_RowQueue(c),
@@ -383,21 +384,27 @@ bool TheoryArrays::propagate(TNode literal)
 }/* TheoryArrays::propagate(TNode) */
 
 
-void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions) {
+void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof *proof) {
   // Do the work
   bool polarity = literal.getKind() != kind::NOT;
   TNode atom = polarity ? literal : literal[0];
   //eq::EqProof * eqp = new eq::EqProof;
-  eq::EqProof * eqp = NULL;
+  // eq::EqProof * eqp = NULL;
   if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
-    d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, eqp);
+    d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, proof);
   } else {
-    d_equalityEngine.explainPredicate(atom, polarity, assumptions);
+    d_equalityEngine.explainPredicate(atom, polarity, assumptions, proof);
   }
-  if( eqp ){
-    Debug("array-pf") << " Proof is : " << std::endl;
-    eqp->debug_print("array-pf");
+  if(proof){
+    Debug("pf::array") << " Proof is : " << std::endl;
+    proof->debug_print("pf::array");
   }
+
+  Debug("pf::array") << "Array: explain( " << literal << " ):" << std::endl << "\t";
+  for (unsigned i = 0; i < assumptions.size(); ++i) {
+    Debug("pf::array") << assumptions[i] << " ";
+  }
+  Debug("pf::array") << std::endl;
 }
 
 TNode TheoryArrays::weakEquivGetRep(TNode node) {
@@ -597,7 +604,7 @@ void TheoryArrays::checkWeakEquiv(bool arraysMerged) {
         }
       }
     }
-  }  
+  }
 }
 
 /**
@@ -787,6 +794,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
     else {
       d_equalityEngine.addTerm(node);
     }
+
     break;
   }
   // Invariant: preregistered terms are exactly the terms in the equality engine
@@ -807,12 +815,16 @@ void TheoryArrays::propagate(Effort e)
 }
 
 
-Node TheoryArrays::explain(TNode literal)
+Node TheoryArrays::explain(TNode literal) {
+  return explain(literal, NULL);
+}
+
+Node TheoryArrays::explain(TNode literal, eq::EqProof *proof)
 {
   ++d_numExplain;
   Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::explain(" << literal << ")" << std::endl;
   std::vector<TNode> assumptions;
-  explain(literal, assumptions);
+  explain(literal, assumptions, proof);
   return mkAnd(assumptions);
 }
 
@@ -1230,7 +1242,11 @@ Node TheoryArrays::getSkolem(TNode ref, const string& name, const TypeNode& type
       makeEqual = false;
     }
   }
+
+  Debug("pf::array") << "Pregistering a Skolem" << std::endl;
   preRegisterTermInternal(skolem);
+  Debug("pf::array") << "Pregistering a Skolem DONE" << std::endl;
+
   if (makeEqual) {
     Node d = skolem.eqNode(ref);
     Debug("arrays-model-based") << "Asserting skolem equality " << d << endl;
@@ -1239,6 +1255,8 @@ Node TheoryArrays::getSkolem(TNode ref, const string& name, const TypeNode& type
     d_skolemAssertions.push_back(d);
     d_skolemIndex = d_skolemIndex + 1;
   }
+
+  Debug("pf::array") << "getSkolem DONE" << std::endl;
   return skolem;
 }
 
@@ -1293,28 +1311,76 @@ void TheoryArrays::check(Effort e) {
 
           // Apply ArrDiseq Rule if diseq is between arrays
           if(fact[0][0].getType().isArray() && !d_conflict) {
+            if (d_conflict) { Debug("pf::array") << "Entering the skolemization branch" << std::endl; }
+
             NodeManager* nm = NodeManager::currentNM();
             TypeNode indexType = fact[0][0].getType()[0];
-            TNode k = getSkolem(fact,"array_ext_index", indexType, "an extensional lemma index variable from the theory of arrays", false);
+
+            TNode k;
+            // k is the skolem for this disequality.
+            if (!d_proofsEnabled) {
+              Debug("pf::array") << "Check: kind::NOT: array theory making a skolem" << std::endl;
+
+              // If not in replay mode, generate a fresh skolem variable
+              k = getSkolem(fact,
+                            "array_ext_index",
+                            indexType,
+                            "an extensional lemma index variable from the theory of arrays",
+                            false);
+
+              // Register this skolem for the proof replay phase
+              PROOF(ProofManager::getSkolemizationManager()->registerSkolem(fact, k));
+            } else {
+              if (!ProofManager::getSkolemizationManager()->hasSkolem(fact)) {
+                // In the solution pass we didn't need this skolem. Therefore, we don't need it
+                // in this reply pass, either.
+                break;
+              }
+
+              // Reuse the same skolem as in the solution pass
+              k = ProofManager::getSkolemizationManager()->getSkolem(fact);
+              Debug("pf::array") << "Skolem = " << k << std::endl;
+            }
 
             Node ak = nm->mkNode(kind::SELECT, fact[0][0], k);
             Node bk = nm->mkNode(kind::SELECT, fact[0][1], k);
             Node eq = ak.eqNode(bk);
             Node lemma = fact[0].orNode(eq.notNode());
+
+            // In solve mode we don't care if ak and bk are registered. If they aren't, they'll be registered
+            // when we output the lemma. However, in replay need the lemma to be propagated, and so we
+            // preregister manually.
+            if (d_proofsEnabled) {
+              if (!d_equalityEngine.hasTerm(ak)) { preRegisterTermInternal(ak); }
+              if (!d_equalityEngine.hasTerm(bk)) { preRegisterTermInternal(bk); }
+            }
+
             if (options::arraysPropagate() > 0 && d_equalityEngine.hasTerm(ak) && d_equalityEngine.hasTerm(bk)) {
               // Propagate witness disequality - might produce a conflict
               d_permRef.push_back(lemma);
-              d_equalityEngine.assertEquality(eq, false, lemma, eq::MERGED_ARRAYS_EXT);
+              Debug("pf::array") << "Asserting to the equality engine:" << std::endl
+                                 << "\teq = " << eq << std::endl
+                                 << "\treason = " << fact << std::endl;
+
+              d_equalityEngine.assertEquality(eq, false, fact, eq::MERGED_ARRAYS_EXT);
               ++d_numProp;
             }
-            Trace("arrays-lem")<<"Arrays::addExtLemma " << lemma <<"\n";
-            d_out->lemma(lemma);
-            ++d_numExt;
+
+            if (!d_proofsEnabled) {
+              // If this is the solution pass, generate the lemma. Otherwise, don't generate it -
+              // as this is the lemma that we're reproving...
+              Trace("arrays-lem")<<"Arrays::addExtLemma " << lemma <<"\n";
+              d_out->lemma(lemma);
+              ++d_numExt;
+            }
+          } else {
+            Debug("pf::array") << "Check: kind::NOT: array theory NOT making a skolem" << std::endl;
+            d_modelConstraints.push_back(fact);
           }
         }
         break;
-      default:
-        Unreachable();
+    default:
+      Unreachable();
     }
   }
 
@@ -1389,8 +1455,10 @@ void TheoryArrays::check(Effort e) {
           weakEquivBuildCond(r2[0], r[1], conjunctions);
           lemma = mkAnd(conjunctions, true);
           // LSH FIXME: which kind of arrays lemma is this
+          Trace("arrays-lem") << "Arrays::addExtLemma " << lemma <<"\n";
           d_out->lemma(lemma, RULE_INVALID, false, false, true);
           d_readTableContext->pop();
+          Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl;
           return;
         }
       }
@@ -1401,7 +1469,7 @@ void TheoryArrays::check(Effort e) {
 
   if(!options::arraysEagerLemmas() && fullEffort(e) && !d_conflict && !options::arraysWeakEquivalence()) {
     // generate the lemmas on the worklist
-    Trace("arrays-lem")<<"Arrays::discharging lemmas: "<<d_RowQueue.size()<<"\n";
+    Trace("arrays-lem")<< "Arrays::discharging lemmas. Number of queued lemmas: " << d_RowQueue.size() << "\n";
     while (d_RowQueue.size() > 0 && !d_conflict) {
       if (dischargeLemmas()) {
         break;
@@ -1865,6 +1933,9 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b)
 
 void TheoryArrays::propagate(RowLemmaType lem)
 {
+  Debug("pf::array") << "TheoryArrays: RowLemma Propagate called. options::arraysPropagate() = "
+                     << options::arraysPropagate() << std::endl;
+
   TNode a = lem.first;
   TNode b = lem.second;
   TNode i = lem.third;
@@ -1919,6 +1990,8 @@ void TheoryArrays::propagate(RowLemmaType lem)
 
 void TheoryArrays::queueRowLemma(RowLemmaType lem)
 {
+  Debug("pf::array") << "Array solver: queue row lemma called" << std::endl;
+
   if (d_conflict || d_RowAlreadyAdded.contains(lem)) {
     return;
   }
@@ -1958,14 +2031,20 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
 
   // Prefer equality between indexes so as not to introduce new read terms
   if (options::arraysEagerIndexSplitting() && !bothExist && !d_equalityEngine.areDisequal(i,j, false)) {
-    Node i_eq_j = d_valuation.ensureLiteral(i.eqNode(j));
+    Node i_eq_j;
+    if (!d_proofsEnabled) {
+      i_eq_j = d_valuation.ensureLiteral(i.eqNode(j)); // TODO: think about this
+    } else {
+      i_eq_j = i.eqNode(j);
+    }
+
     getOutputChannel().requirePhase(i_eq_j, true);
     d_decisionRequests.push(i_eq_j);
   }
 
   // TODO: maybe add triggers here
 
-  if (options::arraysEagerLemmas() || bothExist) {
+  if ((options::arraysEagerLemmas() || bothExist) && !d_proofsEnabled) {
 
     // Make sure that any terms introduced by rewriting are appropriately stored in the equality database
     Node aj2 = Rewriter::rewrite(aj);
@@ -2137,14 +2216,20 @@ bool TheoryArrays::dischargeLemmas()
 }
 
 void TheoryArrays::conflict(TNode a, TNode b) {
+  Debug("pf::array") << "TheoryArrays::Conflict called" << std::endl;
+  eq::EqProof* proof = d_proofsEnabled ? new eq::EqProof() : NULL;
   if (a.getKind() == kind::CONST_BOOLEAN) {
-    d_conflictNode = explain(a.iffNode(b));
+    d_conflictNode = explain(a.iffNode(b), proof);
   } else {
-    d_conflictNode = explain(a.eqNode(b));
+    d_conflictNode = explain(a.eqNode(b), proof);
   }
+
   if (!d_inCheckModel) {
-    d_out->conflict(d_conflictNode);
+    if (proof) { proof->debug_print("pf::array"); }
+    ProofArray* proof_array = d_proofsEnabled ? new ProofArray( proof ) : NULL;
+    d_out->conflict(d_conflictNode, proof_array);
   }
+
   d_conflict = true;
 }
 
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index eba6c000e..2f69c52f9 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -128,7 +128,7 @@ class TheoryArrays : public Theory {
 
   TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out,
                Valuation valuation, const LogicInfo& logicInfo,
-               std::string instanceName = "");
+               std::string name = "");
   ~TheoryArrays();
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);
@@ -183,7 +183,7 @@ class TheoryArrays : public Theory {
   bool propagate(TNode literal);
 
   /** Explain why this literal is true by adding assumptions */
-  void explain(TNode literal, std::vector<TNode>& assumptions);
+  void explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof *proof);
 
   /** For debugging only- checks invariants about when things are preregistered*/
   context::CDHashSet<Node, NodeHashFunction > d_isPreRegistered;
@@ -195,6 +195,7 @@ class TheoryArrays : public Theory {
 
   void preRegisterTerm(TNode n);
   void propagate(Effort e);
+  Node explain(TNode n, eq::EqProof *proof);
   Node explain(TNode n);
 
   /////////////////////////////////////////////////////////////////////////////
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index 70e1c1a5b..a5d0eac69 100644
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -214,6 +214,15 @@ struct ArraysProperties {
   }
 };/* struct ArraysProperties */
 
+
+struct ArrayPartialSelectTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    Assert(n.getKind() == kind::PARTIAL_SELECT_0 || n.getKind() == kind::PARTIAL_SELECT_1);
+    return nodeManager->integerType();
+  }
+};/* struct ArrayPartialSelectTypeRule */
+
 }/* CVC4::theory::arrays namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */