From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Sat, 26 Feb 2011 07:13:01 +0000 (+0000)
Subject: adding the variables count to the statistics in the expr manager
X-Git-Tag: cvc5-1.0.0~8689
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=956689a007e6ae107a47a3b5ea4ea683d3bce673;p=cvc5.git

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 3769d47d2..65429c87f 100644
--- 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 1bb9fd9fd..b5e4a62f0 100644
--- 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 9f6c42aa6..2df4c361c 100644
--- 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"