Adds stats and option

6 files changed, 74 insertions, 6 deletions

diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index 3916c68f3..809f48b6d 100644
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -233,6 +233,15 @@ header = "options/strings_options.h"
   help       = "do flat form inferences"
 
 [[option]]
+  name       = "skolemSharing"
+  category   = "expert"
+  long       = "skolem-sharing"
+  type       = "bool"
+  default    = "true"
+  read_only  = true
+  help       = "use skolem sharing"
+
+[[option]]
   name       = "stringRegExpInterMode"
   category   = "expert"
   long       = "re-inter-mode=MODE"
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index b4e1c74ea..cd30d178a 100644
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -14,6 +14,8 @@
 
 #include "theory/strings/skolem_cache.h"
 
+#include "options/strings_options.h"
+#include "smt/smt_statistics_registry.h"
 #include "theory/rewriter.h"
 #include "theory/strings/theory_strings_rewriter.h"
 #include "util/rational.h"
@@ -47,7 +49,7 @@ Node SkolemCache::mkTypedSkolemCached(
   a = a.isNull() ? a : Rewriter::rewrite(a);
   b = b.isNull() ? b : Rewriter::rewrite(b);
 
-  if (tn == d_strType)
+  if (options::skolemSharing() && tn == d_strType)
   {
     std::tie(id, a, b) = normalizeStringSkolem(id, a, b);
   }
@@ -59,6 +61,11 @@ Node SkolemCache::mkTypedSkolemCached(
     d_skolemCache[a][b][id] = sk;
     return sk;
   }
+  else
+  {
+    d_statistics.d_numCachedSkolems += 1;
+    d_statistics.d_numSkolems += 1;
+  }
   return it->second;
 }
 Node SkolemCache::mkTypedSkolemCached(TypeNode tn,
@@ -78,6 +85,7 @@ Node SkolemCache::mkTypedSkolem(TypeNode tn, const char* c)
 {
   Node n = NodeManager::currentNM()->mkSkolem(c, tn, "string skolem");
   d_allSkolems.insert(n);
+  d_statistics.d_numSkolems += 1;
   return n;
 }
 
@@ -94,6 +102,15 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
 
   NodeManager* nm = NodeManager::currentNM();
 
+  if (id == SK_FIRST_CTN_IOPRE || id == SK_FIRST_CTN_RFCPRE)
+  {
+    id = SK_FIRST_CTN_PRE;
+  }
+  else if (id == SK_FIRST_CTN_IOPOST || id == SK_FIRST_CTN_RFCPOST)
+  {
+    id = SK_FIRST_CTN_POST;
+  }
+
   if (id == SK_FIRST_CTN_POST)
   {
     // SK_FIRST_CTN_POST(x, y) --->
@@ -196,6 +213,19 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
   return std::make_tuple(id, a, b);
 }
 
+SkolemCache::Statistics::Statistics()
+    : d_numSkolems("theory::strings::NumSkolems", 0),
+      d_numCachedSkolems("theory::strings::NumCachedSkolems", 0)
+{
+  smtStatisticsRegistry()->registerStat(&d_numSkolems);
+  smtStatisticsRegistry()->registerStat(&d_numCachedSkolems);
+}
+
+SkolemCache::Statistics::~Statistics() {
+  smtStatisticsRegistry()->unregisterStat(&d_numSkolems);
+  smtStatisticsRegistry()->unregisterStat(&d_numCachedSkolems);
+}
+
 }  // namespace strings
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h
index c1e3c7214..3612f8503 100644
--- a/src/theory/strings/skolem_cache.h
+++ b/src/theory/strings/skolem_cache.h
@@ -22,6 +22,7 @@
 #include <unordered_set>
 
 #include "expr/node.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
@@ -94,6 +95,13 @@ class SkolemCache
     // of b in a as the witness for contains( a, b ).
     SK_FIRST_CTN_PRE,
     SK_FIRST_CTN_POST,
+
+    SK_FIRST_CTN_IOPRE,
+    SK_FIRST_CTN_IOPOST,
+
+    SK_FIRST_CTN_RFCPRE,
+    SK_FIRST_CTN_RFCPOST,
+
     // For integer b,
     // len( a ) > b =>
     //    exists k. a = k ++ a' ^ len( k ) = b
@@ -162,6 +170,17 @@ class SkolemCache
   std::map<Node, std::map<Node, std::map<SkolemId, Node> > > d_skolemCache;
   /** the set of all skolems we have generated */
   std::unordered_set<Node, NodeHashFunction> d_allSkolems;
+
+  struct Statistics
+  {
+    IntStat d_numSkolems;
+    IntStat d_numCachedSkolems;
+
+    Statistics();
+    ~Statistics();
+  };
+
+  Statistics d_statistics;
 };
 
 }  // namespace strings
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 9949bcea4..8b88af3c0 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -4418,10 +4418,12 @@ Node TheoryStrings::ppRewrite(TNode atom) {
   Node atomElim;
   if (options::regExpElim() && atom.getKind() == STRING_IN_REGEXP)
   {
+    d_statistics.d_numStrInRe += 1;
     // aggressive elimination of regular expression membership
     atomElim = d_regexp_elim.eliminate(atom);
     if (!atomElim.isNull())
     {
+      d_statistics.d_numStrInReElim += 1;
       Trace("strings-ppr") << "  rewrote " << atom << " -> " << atomElim
                            << " via regular expression elimination."
                            << std::endl;
@@ -4451,12 +4453,16 @@ TheoryStrings::Statistics::Statistics()
     : d_splits("theory::strings::NumOfSplitOnDemands", 0),
       d_eq_splits("theory::strings::NumOfEqSplits", 0),
       d_deq_splits("theory::strings::NumOfDiseqSplits", 0),
-      d_loop_lemmas("theory::strings::NumOfLoops", 0)
+      d_loop_lemmas("theory::strings::NumOfLoops", 0),
+      d_numStrInRe("theory::strings::NumStrInRe", 0),
+      d_numStrInReElim("theory::strings::NumStrInReElim", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_splits);
   smtStatisticsRegistry()->registerStat(&d_eq_splits);
   smtStatisticsRegistry()->registerStat(&d_deq_splits);
   smtStatisticsRegistry()->registerStat(&d_loop_lemmas);
+  smtStatisticsRegistry()->registerStat(&d_numStrInRe);
+  smtStatisticsRegistry()->registerStat(&d_numStrInReElim);
 }
 
 TheoryStrings::Statistics::~Statistics(){
@@ -4464,6 +4470,8 @@ TheoryStrings::Statistics::~Statistics(){
   smtStatisticsRegistry()->unregisterStat(&d_eq_splits);
   smtStatisticsRegistry()->unregisterStat(&d_deq_splits);
   smtStatisticsRegistry()->unregisterStat(&d_loop_lemmas);
+  smtStatisticsRegistry()->unregisterStat(&d_numStrInRe);
+  smtStatisticsRegistry()->unregisterStat(&d_numStrInReElim);
 }
 
 /** run the given inference step */
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 8e2af8434..aeba210f9 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -683,6 +683,8 @@ private:
     IntStat d_eq_splits;
     IntStat d_deq_splits;
     IntStat d_loop_lemmas;
+    IntStat d_numStrInRe;
+    IntStat d_numStrInReElim;
     Statistics();
     ~Statistics();
   };/* class TheoryStrings::Statistics */
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 6272ad129..f93c09cd4 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -134,9 +134,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                          n,
                          nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, x), n));
     Node io2 =
-        d_sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_PRE, "iopre");
+        d_sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_IOPRE, "iopre");
     Node io4 =
-        d_sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_POST, "iopost");
+        d_sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_IOPOST, "iopost");
 
     // ~contains( substr( x, n, len( x ) - n ), y )
     Node c11 = nm->mkNode(STRING_STRCTN, st, y).negate();
@@ -355,9 +355,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     Node z = t[2];
     TypeNode tn = t[0].getType();
     Node rp1 =
-        d_sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_PRE, "rfcpre");
+        d_sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_RFCPRE, "rfcpre");
     Node rp2 =
-        d_sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_POST, "rfcpost");
+        d_sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_RFCPOST, "rfcpost");
     Node rpw = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "rpw");
 
     // y = ""