From 99d7c85f7fd0523166b1cba283df97d6b16a4c0c Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 27 Jan 2020 15:47:20 -0800
Subject: Stats per skolem id

---
 src/theory/strings/skolem_cache.cpp | 58 ++++++++++++++++++++++++++++++-------
 src/theory/strings/skolem_cache.h   |  8 +++--
 2 files changed, 53 insertions(+), 13 deletions(-)

(limited to 'src')

diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index dc48da56f..424639a27 100644
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -46,13 +46,14 @@ Node SkolemCache::mkSkolemCached(Node a, SkolemId id, const char* c)
 Node SkolemCache::mkTypedSkolemCached(
     TypeNode tn, Node a, Node b, SkolemId id, const char* c)
 {
+  SkolemId reqId = id;
   a = a.isNull() ? a : Rewriter::rewrite(a);
   b = b.isNull() ? b : Rewriter::rewrite(b);
 
   if (d_skolemCachePreOnly[a][b].find(id) == d_skolemCachePreOnly[a][b].end())
   {
     d_skolemCachePreOnly[a][b][id] = Node::null();
-    d_statistics.d_numCachedSkolemsPre += 1;
+    d_statistics.d_numCachedSkolemsPre[reqId] += 1;
   }
 
   if (options::skolemSharing() && tn == d_strType)
@@ -65,7 +66,7 @@ Node SkolemCache::mkTypedSkolemCached(
   {
     Node sk = mkTypedSkolem(tn, c);
     d_skolemCache[a][b][id] = sk;
-    d_statistics.d_numCachedSkolemsPost += 1;
+    d_statistics.d_numCachedSkolemsPost[reqId] += 1;
     return sk;
   }
   else
@@ -219,20 +220,57 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
   return std::make_tuple(id, a, b);
 }
 
+SkolemCache::SkolemId& operator++(SkolemCache::SkolemId& c)
+{
+  using IntType = typename std::underlying_type<SkolemCache::SkolemId>::type;
+  if (c == SkolemCache::SkolemId::SK_LAST)
+  {
+    c = static_cast<SkolemCache::SkolemId>(0);
+  }
+  else
+  {
+    c = static_cast<SkolemCache::SkolemId>(static_cast<IntType>(c) + 1);
+  }
+  return c;
+}
+
 SkolemCache::Statistics::Statistics()
-    : d_numSkolems("theory::strings::NumSkolems", 0),
-      d_numCachedSkolemsPre("theory::strings::NumCachedSkolemsPre", 0),
-      d_numCachedSkolemsPost("theory::strings::NumCachedSkolemsPost", 0)
+    : d_numSkolems("theory::strings::NumSkolems", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_numSkolems);
-  smtStatisticsRegistry()->registerStat(&d_numCachedSkolemsPre);
-  smtStatisticsRegistry()->registerStat(&d_numCachedSkolemsPost);
+  for (SkolemId id = SK_PURIFY; id < SK_LAST; ++id)
+  {
+    std::stringstream sspre;
+    sspre << "theory::strings::NumCachedSkolemsPre[";
+    sspre << id;
+    sspre << "]";
+    d_numCachedSkolemsPre.emplace_back(sspre.str(), 0);
+    std::stringstream sspost;
+    sspost << "theory::strings::NumCachedSkolemsPost[";
+    sspost << id;
+    sspost << "]";
+    d_numCachedSkolemsPost.emplace_back(sspost.str(), 0);
+  }
+
+  for (SkolemId id = SK_PURIFY; id < SK_LAST; ++id)
+  {
+    smtStatisticsRegistry()->registerStat(
+        &d_numCachedSkolemsPre[static_cast<size_t>(id)]);
+    smtStatisticsRegistry()->registerStat(
+        &d_numCachedSkolemsPost[static_cast<size_t>(id)]);
+  }
 }
 
-SkolemCache::Statistics::~Statistics() {
+SkolemCache::Statistics::~Statistics()
+{
   smtStatisticsRegistry()->unregisterStat(&d_numSkolems);
-  smtStatisticsRegistry()->unregisterStat(&d_numCachedSkolemsPre);
-  smtStatisticsRegistry()->unregisterStat(&d_numCachedSkolemsPost);
+  for (SkolemId id = SK_PURIFY; id < SK_LAST; ++id)
+  {
+    smtStatisticsRegistry()->unregisterStat(
+        &d_numCachedSkolemsPre[static_cast<size_t>(id)]);
+    smtStatisticsRegistry()->unregisterStat(
+        &d_numCachedSkolemsPost[static_cast<size_t>(id)]);
+  }
 }
 
 }  // namespace strings
diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h
index a6d2390c2..6d15e3428 100644
--- a/src/theory/strings/skolem_cache.h
+++ b/src/theory/strings/skolem_cache.h
@@ -51,7 +51,7 @@ class SkolemCache
   enum SkolemId
   {
     // exists k. k = a
-    SK_PURIFY,
+    SK_PURIFY = 0,
     // a != "" ^ b = "ccccd" ^ a ++ "d" ++ a' = b ++ b' =>
     //    exists k. a = "cccc" + k
     SK_ID_C_SPT,
@@ -120,6 +120,8 @@ class SkolemCache
     //       k(x) is the end index of the x^th occurrence of b in a
     //   where n is the number of occurrences of b in a, and k(0)=0.
     SK_OCCUR_INDEX,
+
+    SK_LAST
   };
   /**
    * Returns a skolem of type string that is cached for (a,b,id) and has
@@ -177,8 +179,8 @@ class SkolemCache
   struct Statistics
   {
     IntStat d_numSkolems;
-    IntStat d_numCachedSkolemsPre;
-    IntStat d_numCachedSkolemsPost;
+    std::vector<IntStat> d_numCachedSkolemsPre;
+    std::vector<IntStat> d_numCachedSkolemsPost;
 
     Statistics();
     ~Statistics();
-- 
cgit v1.2.3