3 files changed, 22 insertions, 7 deletions
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 7738f50ca..533145dc2 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -6,11 +6,15 @@
 
 theory THEORY_ARRAY ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_arrays.h"
 
-properties polite stable-infinite 
+properties polite stable-infinite
+properties check
 
 rewriter ::CVC4::theory::arrays::TheoryArraysRewriter "theory/arrays/theory_arrays_rewriter.h"
 
 operator ARRAY_TYPE 2 "array type"
+cardinality ARRAY_TYPE \
+    "::CVC4::theory::arrays::CardinalityComputer::computeCardinality(%TYPE%)" \
+    "theory/arrays/theory_arrays_type_rules.h"
 
 # select a i  is  a[i]
 operator SELECT 2 "array select"
@@ -18,4 +22,4 @@ operator SELECT 2 "array select"
 # store a i e  is  a[i] <= e
 operator STORE 3 "array store"
 
-endtheory
-\ No newline at end of file
+endtheory
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 64fdd8303..fbbda9e44 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -34,14 +34,14 @@ public:
   TheoryArrays(context::Context* c, OutputChannel& out, Valuation valuation);
   ~TheoryArrays();
   void preRegisterTerm(TNode n) { }
-  void registerTerm(TNode n) { }
+  //void registerTerm(TNode n) { }
 
-  void presolve() { }
+  //void presolve() { }
 
   void addSharedTerm(TNode t);
   void notifyEq(TNode lhs, TNode rhs);
   void check(Effort e);
-  void propagate(Effort e) { }
+  //void propagate(Effort e) { }
   void explain(TNode n) { }
   Node getValue(TNode n);
   void shutdown() { }
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index 11e8a8443..bd3c8ad67 100644
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -11,9 +11,9 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Theory of arrays.
+ ** \brief Typing and cardinality rules for the theory of arrays
  **
- ** Theory of arrays.
+ ** Typing and cardinality rules for the theory of arrays.
  **/
 
 #include "cvc4_private.h"
@@ -65,6 +65,17 @@ struct ArrayStoreTypeRule {
   }
 };/* struct ArrayStoreTypeRule */
 
+struct CardinalityComputer {
+  inline static Cardinality computeCardinality(TypeNode type) {
+    Assert(type.getKind() == kind::ARRAY_TYPE);
+
+    Cardinality indexCard = type[0].getCardinality();
+    Cardinality valueCard = type[1].getCardinality();
+
+    return valueCard ^ indexCard;
+  }
+};/* struct CardinalityComputer */
+
 }/* CVC4::theory::arrays namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */