2 files changed, 19 insertions, 0 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 8997138cb..55a539f44 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -18,6 +18,7 @@
 
 
 #include "theory/arrays/theory_arrays.h"
+#include "theory/theory_engine.h"
 #include "expr/kind.h"
 
 
@@ -58,3 +59,20 @@ void TheoryArrays::check(Effort e) {
   }
   Debug("arrays") << "TheoryArrays::check(): done" << endl;
 }
+
+Node TheoryArrays::getValue(TNode n, TheoryEngine* engine) {
+  NodeManager* nodeManager = NodeManager::currentNM();
+
+  switch(n.getKind()) {
+
+  case kind::VARIABLE:
+    Unhandled(kind::VARIABLE);
+
+  case kind::EQUAL: // 2 args
+    return nodeManager->
+      mkConst( engine->getValue(n[0]) == engine->getValue(n[1]) );
+
+  default:
+    Unhandled(n.getKind());
+  }
+}
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index cb738d085..89631d59f 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -53,6 +53,7 @@ public:
   void check(Effort e);
   void propagate(Effort e) { }
   void explain(TNode n, Effort e) { }
+  Node getValue(TNode n, TheoryEngine* engine);
   void shutdown() { }
   std::string identify() const { return std::string("TheoryArrays"); }
 };/* class TheoryArrays */