adding the variables count to the statistics in the expr manager

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 3769d47d2a700ec01c1f51fd14b954987c9e7140..65429c87fec54139a1423ea5d18d6e6d4c9e4ef3 100644 (file)
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -35,14 +35,31 @@ ${includes}
   { \
     if (d_exprStatistics[kind] == NULL) { \
       stringstream statName; \
-      statName << "CVC4::expr::count" << kind; \
+      statName << "expr::ExprManager::" << kind; \
       d_exprStatistics[kind] = new IntStat(statName.str(), 0); \
       StatisticsRegistry::registerStat(d_exprStatistics[kind]); \
     } \
     ++ *(d_exprStatistics[kind]); \
-  } 
+  }
+  #define INC_STAT_VAR(type) \
+  { \
+    TypeNode* typeNode = Type::getTypeNode(type); \
+    TypeConstant type = typeNode->getKind() == kind::TYPE_CONSTANT ? typeNode->getConst<TypeConstant>() : LAST_TYPE; \
+    if (d_exprStatisticsVars[type] == NULL) { \
+      stringstream statName; \
+      if (type == LAST_TYPE) { \
+        statName << "expr::ExprManager::VARIABLE:Parametrized type"; \
+      } else { \
+        statName << "expr::ExprManager::VARIABLE:" << type; \
+      } \
+      d_exprStatisticsVars[type] = new IntStat(statName.str(), 0); \
+      StatisticsRegistry::registerStat(d_exprStatisticsVars[type]); \
+    } \
+    ++ *(d_exprStatisticsVars[type]); \
+  }
 #else 
   #define INC_STAT(kind)
+  #define INC_STAT_VAR(type)
 #endif
 
 using namespace std;
@@ -58,13 +75,19 @@ ExprManager::ExprManager() :
   for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
     d_exprStatistics[i] = NULL;
   }
+  for (unsigned i = 0; i < LAST_TYPE; ++ i) {
+    d_exprStatisticsVars[i] = NULL;
+  }
 #endif
 }
 
 ExprManager::ExprManager(const Options& options) :
   d_ctxt(new Context),
   d_nodeManager(new NodeManager(d_ctxt, options)) {
-#ifdef CVC4_STATISTICS_ON   
+#ifdef CVC4_STATISTICS_ON  
+  for (unsigned i = 0; i < LAST_TYPE; ++ i) {
+    d_exprStatisticsVars[i] = NULL;
+  }
   for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
     d_exprStatistics[i] = NULL;
   }
@@ -81,6 +104,12 @@ ExprManager::~ExprManager() {
       delete d_exprStatistics[i];
     }
   }
+  for (unsigned i = 0; i < LAST_TYPE; ++ i) {
+    if (d_exprStatisticsVars[i] != NULL) {
+      StatisticsRegistry::unregisterStat(d_exprStatisticsVars[i]);
+      delete d_exprStatisticsVars[i];
+    }
+  }
 #endif
 }
 
@@ -363,11 +392,13 @@ Expr ExprManager::mkVar(const std::string& name, const Type& type) {
   NodeManagerScope nms(d_nodeManager);
   Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode);
   Debug("nm") << "set " << name << " on " << *n << std::endl;
+  INC_STAT_VAR(type);
   return Expr(this, n);
 }
 
 Expr ExprManager::mkVar(const Type& type) {
   NodeManagerScope nms(d_nodeManager);
+  INC_STAT_VAR(type);
   return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode));
 }
 

diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 1bb9fd9fd935225ab6a1a5a5c5d21121f05693d1..b5e4a62f0366701da012c2265eae676bb7edf8e8 100644 (file)
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -55,7 +55,8 @@ private:
   /** The internal node manager */
   NodeManager* d_nodeManager;
 
-  /** Counts of expressions created of a given kind */
+  /** Counts of expressions and variables created of a given kind */
+  IntStat* d_exprStatisticsVars[LAST_TYPE + 1];
   IntStat* d_exprStatistics[kind::LAST_KIND];
 
   /**

diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index 9f6c42aa6aa116b3c2ccbf8d20ac96f884027c4f..2df4c361cc9e744c33d5022233a4f62e349aaa40 100644 (file)
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -26,7 +26,7 @@ operator BITVECTOR_CONCAT 2: "bit-vector concatenation"
 operator BITVECTOR_AND 2 "bitwise and"
 operator BITVECTOR_OR 2 "bitwise or"
 operator BITVECTOR_XOR 2 "bitwise xor"
-operator BITVECTOR_NOT 2 "bitwise not"
+operator BITVECTOR_NOT 1 "bitwise not"
 operator BITVECTOR_NAND 2 "bitwise nand"
 operator BITVECTOR_NOR 2 "bitwise nor"
 operator BITVECTOR_XNOR 2 "bitwise xnor"