4 files changed, 51 insertions, 26 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 460289439..5add52d1f 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -24,6 +24,7 @@
 #include "theory/rewriter.h"
 #include "expr/command.h"
 #include "theory/arrays/theory_arrays_instantiator.h"
+#include "theory/model.h"
 
 using namespace std;
 
@@ -57,7 +58,7 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC
   d_checkTimer("theory::arrays::checkTime"),
   d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP"),
   d_ppFacts(u),
-  //  d_ppCache(u),  
+  //  d_ppCache(u),
   d_literalsToPropagate(c),
   d_literalsToPropagateIndex(c, 0),
   d_isPreRegistered(c),
@@ -211,7 +212,7 @@ Node TheoryArrays::ppRewrite(TNode term) {
                 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()? 
+                    Node hyp2(index_i.getType() == nm->booleanType()?
                               index_i.iffNode(index_j) : index_i.eqNode(index_j));
                     hyp << hyp2.notNode();
                   }
@@ -623,27 +624,10 @@ void TheoryArrays::computeCareGraph()
 // MODEL GENERATION
 /////////////////////////////////////////////////////////////////////////////
 
-
-Node TheoryArrays::getValue(TNode n)
-{
-  // TODO: Implement this
-  NodeManager* nodeManager = NodeManager::currentNM();
-
-  switch(n.getKind()) {
-
-  case kind::VARIABLE:
-    Unhandled(kind::VARIABLE);
-
-  case kind::EQUAL: // 2 args
-    return nodeManager->
-      mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) );
-
-  default:
-    Unhandled(n.getKind());
-  }
+void TheoryArrays::collectModelInfo( TheoryModel* m ){
+  m->assertEqualityEngine( &d_equalityEngine );
 }
 
-
 /////////////////////////////////////////////////////////////////////////////
 // NOTIFICATIONS
 /////////////////////////////////////////////////////////////////////////////
@@ -663,7 +647,7 @@ void TheoryArrays::presolve()
 void TheoryArrays::check(Effort e) {
   TimerStat::CodeTimer codeTimer(d_checkTimer);
 
-  while (!done() && !d_conflict) 
+  while (!done() && !d_conflict)
   {
     // Get all the assertions
     Assertion assertion = get();
@@ -1306,7 +1290,7 @@ void TheoryArrays::dischargeLemmas()
       d_equalityEngine.assertEquality(eq2, true, d_true);
       continue;
     }
-    
+
     Node lem = nm->mkNode(kind::OR, eq2_r, eq1_r);
 
     Trace("arrays-lem")<<"Arrays::addRowLemma adding "<<lem<<"\n";
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 25797dda3..6787f8ad8 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -219,7 +219,7 @@ class TheoryArrays : public Theory {
   private:
   public:
 
-  Node getValue(TNode n);
+  void collectModelInfo( TheoryModel* m );
 
   /////////////////////////////////////////////////////////////////////////////
   // NOTIFICATIONS
@@ -346,6 +346,12 @@ class TheoryArrays : public Theory {
   void queueRowLemma(RowLemmaType lem);
   void dischargeLemmas();
 
+  public:
+
+  eq::EqualityEngine* getEqualityEngine() {
+    return &d_equalityEngine;
+  }
+
 };/* class TheoryArrays */
 
 }/* CVC4::theory::arrays namespace */
diff --git a/src/theory/arrays/theory_arrays_instantiator.cpp b/src/theory/arrays/theory_arrays_instantiator.cpp
index 334d70eea..2e446c57f 100644
--- a/src/theory/arrays/theory_arrays_instantiator.cpp
+++ b/src/theory/arrays/theory_arrays_instantiator.cpp
@@ -51,6 +51,35 @@ void InstantiatorTheoryArrays::processResetInstantiationRound( Theory::Effort ef
 
 }
 
-int InstantiatorTheoryArrays::process( Node f, Theory::Effort effort, int e, int limitInst ){
+int InstantiatorTheoryArrays::process( Node f, Theory::Effort effort, int e ){
   return InstStrategy::STATUS_SAT;
 }
+
+bool InstantiatorTheoryArrays::hasTerm( Node a ){
+  return ((TheoryArrays*)d_th)->getEqualityEngine()->hasTerm( a );
+}
+
+bool InstantiatorTheoryArrays::areEqual( Node a, Node b ){
+  if( hasTerm( a ) && hasTerm( b ) ){
+    return ((TheoryArrays*)d_th)->getEqualityEngine()->areEqual( a, b );
+  }else{
+    return a==b;
+  }
+}
+
+bool InstantiatorTheoryArrays::areDisequal( Node a, Node b ){
+  if( hasTerm( a ) && hasTerm( b ) ){
+    return ((TheoryArrays*)d_th)->getEqualityEngine()->areDisequal( a, b, false );
+  }else{
+    return false;
+  }
+}
+
+Node InstantiatorTheoryArrays::getRepresentative( Node a ){
+  if( hasTerm( a ) ){
+    return ((TheoryArrays*)d_th)->getEqualityEngine()->getRepresentative( a );
+  }else{
+    return a;
+  }
+}
+
diff --git a/src/theory/arrays/theory_arrays_instantiator.h b/src/theory/arrays/theory_arrays_instantiator.h
index 6a7c9c3ed..ade43fdb0 100644
--- a/src/theory/arrays/theory_arrays_instantiator.h
+++ b/src/theory/arrays/theory_arrays_instantiator.h
@@ -32,7 +32,7 @@ protected:
   /** reset instantiation round */
   void processResetInstantiationRound( Theory::Effort effort );
   /** process quantifier */
-  int process( Node f, Theory::Effort effort, int e, int limitInst = 0 );
+  int process( Node f, Theory::Effort effort, int e );
 public:
   InstantiatorTheoryArrays(context::Context* c, QuantifiersEngine* ie, Theory* th);
   ~InstantiatorTheoryArrays() {}
@@ -42,6 +42,12 @@ public:
   void assertNode( Node assertion );
   /** identify */
   std::string identify() const { return std::string("InstantiatorTheoryArrays"); }
+public:
+  /** general queries about equality */
+  bool hasTerm( Node a );
+  bool areEqual( Node a, Node b );
+  bool areDisequal( Node a, Node b );
+  Node getRepresentative( Node a );
 };/* class Instantiatior */
 
 }