From cb7363eef352200615e1a0d3729cea8b2c74d265 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 25 Apr 2011 06:56:14 +0000
Subject: Weekend work.  The main points:

* Type::getCardinality() returns the cardinality for for all types.
  Theories give a cardinality in the their kinds file.  For
  cardinalities that depend on a type argument, a "cardinality
  computer" function is named in the kinds file, which takes a
  TypeNode and returns its cardinality.

* There's a bitmap for the set of "active theories" in the
  TheoryEngine.  Theories become "active" when a term that is owned by
  them, or whose type is owned by them, is pre-registered (run CVC4
  with --verbose to see theory activation).  Non-active theories don't
  get any calls for check() or propagate() or anything, and if we're
  running in single-theory mode, the shared term manager doesn't have
  to get involved.  This is really important for get() performance
  (which can only skimp on walking the entire sub-DAG only if the
  theory doesn't require it AND the shared term manager doesn't
  require it).

* TheoryEngine now does not call presolve(), registerTerm(),
  notifyRestart(), etc., on a Theory if that theory doesn't declare
  that property in its kinds file.  To avoid coding errors,
  mktheorytraits greps the theory header and gives warnings if:
  + the theory appears to declare one of the functions (check,
    propagate, etc.) that isn't listed among its kinds file properties
    (but probably should be)
  + the theory appears NOT to declare one of the functions listed in
    its kinds file properties

* some bounded token stream work
---
 src/theory/bv/kinds                  |  8 ++++++--
 src/theory/bv/theory_bv.h            |  4 ++--
 src/theory/bv/theory_bv_type_rules.h | 14 ++++++++++++++
 3 files changed, 22 insertions(+), 4 deletions(-)

(limited to 'src/theory/bv')

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 */
-- 
cgit v1.2.3