3 files changed, 22 insertions, 4 deletions
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index 381e90d47..d10e32ee0 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -6,7 +6,8 @@
 
 theory THEORY_BV ::CVC4::theory::bv::TheoryBV "theory/bv/theory_bv.h"
 
-properties finite check propagate
+properties finite
+properties check propagate
 
 rewriter ::CVC4::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h"
 
@@ -15,6 +16,9 @@ constant BITVECTOR_TYPE \
 	"::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorSize >" \
 	"util/bitvector.h" \
 	"bit-vector type"
+cardinality BITVECTOR_TYPE \
+	"::CVC4::theory::bv::CardinalityComputer::computeCardinality(%TYPE%)" \
+	"theory/bv/theory_bv_type_rules.h"
 
 constant CONST_BITVECTOR \
     ::CVC4::BitVector \
@@ -95,4 +99,4 @@ parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign-
 parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left"
 parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right"
 
-endtheory
-\ No newline at end of file
+endtheory
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index d65f0388b..748352321 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -113,11 +113,11 @@ public:
 
   void preRegisterTerm(TNode n);
 
-  void registerTerm(TNode n) { }
+  //void registerTerm(TNode n) { }
 
   void check(Effort e);
 
-  void presolve() { }
+  //void presolve() { }
 
   void propagate(Effort e) { }
 
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index a27fd351c..613df47f3 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -189,6 +189,20 @@ public:
   }
 };
 
+class CardinalityComputer {
+public:
+  inline static Cardinality computeCardinality(TypeNode type) {
+    Assert(type.getKind() == kind::BITVECTOR_TYPE);
+
+    unsigned size = type.getConst<BitVectorSize>();
+    if(size == 0) {
+      return 0;
+    }
+    Integer i = Integer(2).pow(size);
+    return i;
+  }
+};/* class CardinalityComputer */
+
 }/* CVC4::theory::bv namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */