5 files changed, 162 insertions, 5 deletions
diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am
index c429fc0c6..e4c814660 100644
--- a/src/theory/arrays/Makefile.am
+++ b/src/theory/arrays/Makefile.am
@@ -18,6 +18,8 @@ libarrays_la_SOURCES = \
 	static_fact_manager.h \
 	static_fact_manager.cpp \
 	theory_arrays_instantiator.h \
-	theory_arrays_instantiator.cpp
+	theory_arrays_instantiator.cpp \
+	theory_arrays_model.h \
+	theory_arrays_model.cpp
 
 EXTRA_DIST = kinds
diff --git a/src/theory/arrays/theory_arrays_instantiator.cpp b/src/theory/arrays/theory_arrays_instantiator.cpp
index ca9001fe5..67c42d124 100644
--- a/src/theory/arrays/theory_arrays_instantiator.cpp
+++ b/src/theory/arrays/theory_arrays_instantiator.cpp
@@ -17,7 +17,7 @@
 #include "theory/theory_engine.h"
 #include "theory/arrays/theory_arrays_instantiator.h"
 #include "theory/arrays/theory_arrays.h"
-#include "theory/uf/theory_uf_candidate_generator.h"
+#include "theory/rr_candidate_generator.h"
 
 using namespace std;
 using namespace CVC4;
@@ -61,15 +61,19 @@ bool InstantiatorTheoryArrays::hasTerm( Node a ){
 }
 
 bool InstantiatorTheoryArrays::areEqual( Node a, Node b ){
-  if( hasTerm( a ) && hasTerm( b ) ){
+  if( a==b ){
+    return true;
+  }else if( hasTerm( a ) && hasTerm( b ) ){
     return ((TheoryArrays*)d_th)->getEqualityEngine()->areEqual( a, b );
   }else{
-    return a==b;
+    return false;
   }
 }
 
 bool InstantiatorTheoryArrays::areDisequal( Node a, Node b ){
-  if( hasTerm( a ) && hasTerm( b ) ){
+  if( a==b ){
+    return false;
+  }else if( hasTerm( a ) && hasTerm( b ) ){
     return ((TheoryArrays*)d_th)->getEqualityEngine()->areDisequal( a, b, false );
   }else{
     return false;
@@ -84,6 +88,23 @@ Node InstantiatorTheoryArrays::getRepresentative( Node a ){
   }
 }
 
+eq::EqualityEngine* InstantiatorTheoryArrays::getEqualityEngine(){
+  return ((TheoryArrays*)d_th)->getEqualityEngine();
+}
+
+void InstantiatorTheoryArrays::getEquivalenceClass( Node a, std::vector< Node >& eqc ){
+  if( hasTerm( a ) ){
+    a = getEqualityEngine()->getRepresentative( a );
+    eq::EqClassIterator eqc_iter( a, getEqualityEngine() );
+    while( !eqc_iter.isFinished() ){
+      if( std::find( eqc.begin(), eqc.end(), *eqc_iter )==eqc.end() ){
+        eqc.push_back( *eqc_iter );
+      }
+      eqc_iter++;
+    }
+  }
+}
+
 rrinst::CandidateGenerator* InstantiatorTheoryArrays::getRRCanGenClasses(){
   arrays::TheoryArrays* ar = static_cast<arrays::TheoryArrays *>(getTheory());
   eq::EqualityEngine* ee =
diff --git a/src/theory/arrays/theory_arrays_instantiator.h b/src/theory/arrays/theory_arrays_instantiator.h
index f711229b2..23899afc1 100644
--- a/src/theory/arrays/theory_arrays_instantiator.h
+++ b/src/theory/arrays/theory_arrays_instantiator.h
@@ -49,6 +49,8 @@ public:
   bool areEqual( Node a, Node b );
   bool areDisequal( Node a, Node b );
   Node getRepresentative( Node a );
+  eq::EqualityEngine* getEqualityEngine();
+  void getEquivalenceClass( Node a, std::vector< Node >& eqc );
   /** general creators of candidate generators */
   rrinst::CandidateGenerator* getRRCanGenClasses();
   rrinst::CandidateGenerator* getRRCanGenClass();
diff --git a/src/theory/arrays/theory_arrays_model.cpp b/src/theory/arrays/theory_arrays_model.cpp
new file mode 100644
index 000000000..49da2f851
--- /dev/null
+++ b/src/theory/arrays/theory_arrays_model.cpp
@@ -0,0 +1,70 @@
+/*********************                                                        */
+/*! \file theory_arrays_model.cpp
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of theory_arrays_model class
+ **/
+
+#include "theory/theory_engine.h"
+#include "theory/arrays/theory_arrays_model.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/term_database.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::arrays;
+
+ArrayModel::ArrayModel( Node arr, quantifiers::FirstOrderModel* m ) : d_model( m ), d_arr( arr ){
+  Assert( arr.getKind()!=STORE );
+  //look at ground assertions
+  Node sel = NodeManager::currentNM()->mkNode( SELECT, arr, NodeManager::currentNM()->mkVar( arr.getType().getArrayIndexType() ) );
+  Node sel_op = sel.getOperator();  //FIXME: easier way to do this?
+  for( size_t i=0; i<d_model->getTermDatabase()->d_op_map[ sel_op ].size(); i++ ){
+    Node n = d_model->getTermDatabase()->d_op_map[ sel_op ][i];
+    Assert( n.getKind()==SELECT );
+    if( m->areEqual( n[0], arr ) ){
+      //d_model->getTermDatabase()->computeModelBasisArgAttribute( n );
+      //if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){
+        Node r = d_model->getRepresentative( n );
+        Node i = d_model->getRepresentative( n[1] );
+        d_values[i] = r;
+      //}
+    }
+  }
+}
+
+Node ArrayModel::getValue( Node n ){
+  Assert( n.getKind()==SELECT );
+  Assert( n[0]==d_arr );
+  std::map< Node, Node >::iterator it = d_values.find( n[0] );
+  if( it!=d_values.end() ){
+    return it->second;
+  }else{
+    return n;
+    //return d_default_value;   TODO: guarentee I can return this here
+  }
+}
+
+void ArrayModel::setDefaultValue( Node v ){
+  d_default_value = v;
+}
+
+Node ArrayModel::getArrayValue(){
+  Node curr = d_arr;    //TODO: make constant default
+  for( std::map< Node, Node >::iterator it = d_values.begin(); it != d_values.end(); ++it ){
+    curr = NodeManager::currentNM()->mkNode( STORE, curr, it->first, it->second );
+  }
+  return curr;
+}
diff --git a/src/theory/arrays/theory_arrays_model.h b/src/theory/arrays/theory_arrays_model.h
new file mode 100644
index 000000000..3895388e3
--- /dev/null
+++ b/src/theory/arrays/theory_arrays_model.h
@@ -0,0 +1,62 @@
+/*********************                                                        */
+/*! \file theory_arrays_model.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief MODEL for theory of arrays
+ **/
+
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY_ARRAYS_MODEL_H
+#define __CVC4__THEORY_ARRAYS_MODEL_H
+
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+
+namespace quantifiers{
+  class FirstOrderModel;
+}
+
+namespace arrays {
+
+class ArrayModel{
+protected:
+  /** reference to model */
+  quantifiers::FirstOrderModel* d_model;
+  /** the array this model is for */
+  Node d_arr;
+public:
+  ArrayModel(){}
+  ArrayModel( Node arr, quantifiers::FirstOrderModel* m );
+  ~ArrayModel() {}
+public:
+  /** pre-defined values */
+  std::map< Node, Node > d_values;
+  /** default value */
+  Node d_default_value;
+  /** get value, return arguments that the value depends on */
+  Node getValue( Node n );
+  /** set default */
+  void setDefaultValue( Node v );
+public:
+  /** get array value */
+  Node getArrayValue();
+};/* class ArrayModel */
+
+}
+}
+}
+
+#endif
+\ No newline at end of file