Make statistics output consistent. (#1647)

* Fixes --hide-zero-stats (and really skips the 0 values)
* Removes the additional newline after each statistic
* Introduces theory::getStatsPrefix(TheoryId) to generate consistent
  prefixes for statistics based on the theory id
  (e.g., THEORY_BV -> "theory::bv").

3 files changed, 16 insertions, 0 deletions

diff --git a/src/expr/kind_template.cpp b/src/expr/kind_template.cpp
index 5f92af622..aa9107a18 100644
--- a/src/expr/kind_template.cpp
+++ b/src/expr/kind_template.cpp
@@ -91,5 +91,15 @@ ${type_constant_to_theory_id}
   throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad type constant");
 }
 
+std::string getStatsPrefix(TheoryId theoryId) {
+  switch(theoryId) {
+${theory_stats_prefixes}
+#line 98 "${template}"
+  default:
+    break;
+  }
+  return "unknown";
+}
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 9247f50dd..6ebbb32c2 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -99,6 +99,7 @@ CVC4_PUBLIC inline TheoryId& operator++(TheoryId& id) {
 std::ostream& operator<<(std::ostream& out, TheoryId theoryId);
 TheoryId kindToTheoryId(::CVC4::Kind k) CVC4_PUBLIC;
 TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant) CVC4_PUBLIC;
+std::string getStatsPrefix(TheoryId theoryId) CVC4_PUBLIC;
 
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/expr/mkkind b/src/expr/mkkind
index 2b1901f5d..5e5be7c45 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -75,6 +75,7 @@ seen_theory_builtin=false
 
 theory_enum=
 theory_descriptions=
+theory_stats_prefixes=
 
 function theory {
   # theory ID T header
@@ -109,6 +110,9 @@ function theory {
 "
   theory_descriptions="${theory_descriptions}  case ${theory_id}: out << \"${theory_id}\"; break;
 "
+  prefix=$(echo "$theory_id" | tr '[:upper:]' '[:lower:]')
+  theory_stats_prefixes="${theory_stats_prefixes}  case ${theory_id}: return \"theory::${prefix#theory_}\"; break;
+"
 }
 
 function alternate {
@@ -416,6 +420,7 @@ for var in \
     type_constant_groundterms \
     type_properties_includes \
     theory_descriptions \
+    theory_stats_prefixes \
     template \
     ; do
   eval text="\${text//\\\$\\{$var\\}/\${$var}}"