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").

12 files changed, 58 insertions, 57 deletions

diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index a36ec2e16..c04e8bde9 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -1111,9 +1111,10 @@ AbstractionModule::ArgsTableEntry& AbstractionModule::ArgsTable::getEntry(TNode
 }
 
 AbstractionModule::Statistics::Statistics(const std::string& name)
-  : d_numFunctionsAbstracted(name + "theory::bv::AbstractioModule::NumFunctionsAbstracted", 0)
-  , d_numArgsSkolemized(name + "theory::bv::AbstractioModule::NumArgsSkolemized", 0)
-  , d_abstractionTime(name + "theory::bv::AbstractioModule::AbstractionTime")
+    : d_numFunctionsAbstracted(name + "::abstraction::NumFunctionsAbstracted",
+                               0),
+      d_numArgsSkolemized(name + "::abstraction::NumArgsSkolemized", 0),
+      d_abstractionTime(name + "::abstraction::AbstractionTime")
 {
   smtStatisticsRegistry()->registerStat(&d_numFunctionsAbstracted);
   smtStatisticsRegistry()->registerStat(&d_numArgsSkolemized);
diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp
index 354b58376..101b64173 100644
--- a/src/theory/bv/bv_quick_check.cpp
+++ b/src/theory/bv/bv_quick_check.cpp
@@ -353,13 +353,13 @@ Node QuickXPlain::minimizeConflict(TNode confl) {
 }
 
 QuickXPlain::Statistics::Statistics(const std::string& name)
-  : d_xplainTime("theory::bv::"+name+"::QuickXplain::Time")
-  , d_numSolved("theory::bv::"+name+"::QuickXplain::NumSolved", 0)
-  , d_numUnknown("theory::bv::"+name+"::QuickXplain::NumUnknown", 0)
-  , d_numUnknownWasUnsat("theory::bv::"+name+"::QuickXplain::NumUnknownWasUnsat", 0)
-  , d_numConflictsMinimized("theory::bv::"+name+"::QuickXplain::NumConflictsMinimized", 0)
-  , d_finalPeriod("theory::bv::"+name+"::QuickXplain::FinalPeriod", 0)
-  , d_avgMinimizationRatio("theory::bv::"+name+"::QuickXplain::AvgMinRatio")
+  : d_xplainTime(name + "::QuickXplain::Time")
+  , d_numSolved(name + "::QuickXplain::NumSolved", 0)
+  , d_numUnknown(name + "::QuickXplain::NumUnknown", 0)
+  , d_numUnknownWasUnsat(name + "::QuickXplain::NumUnknownWasUnsat", 0)
+  , d_numConflictsMinimized(name + "::QuickXplain::NumConflictsMinimized", 0)
+  , d_finalPeriod(name + "::QuickXplain::FinalPeriod", 0)
+  , d_avgMinimizationRatio(name + "::QuickXplain::AvgMinRatio")
 {
   smtStatisticsRegistry()->registerStat(&d_xplainTime);
   smtStatisticsRegistry()->registerStat(&d_numSolved);
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index d163bf7f9..d941d018f 100644
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -117,7 +117,7 @@ class QuickXPlain {
     IntStat d_numConflictsMinimized;
     IntStat d_finalPeriod;
     AverageStat d_avgMinimizationRatio;
-    Statistics(const std::string&);
+    Statistics(const std::string& name);
     ~Statistics();
   };
   BVQuickCheck* d_solver;
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 888c95692..456f627d0 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -229,7 +229,7 @@ void SubstitutionEx::storeCache(TNode from, TNode to, Node reason) {
 AlgebraicSolver::AlgebraicSolver(context::Context* c, TheoryBV* bv)
   : SubtheorySolver(c, bv)
   , d_modelMap(NULL)
-  , d_quickSolver(new BVQuickCheck("alg", bv))
+  , d_quickSolver(new BVQuickCheck("theory::bv::algebraic", bv))
   , d_isComplete(c, false)
   , d_isDifficult(c, false)
   , d_budget(options::bitvectorAlgebraicBudget())
@@ -239,7 +239,7 @@ AlgebraicSolver::AlgebraicSolver(context::Context* c, TheoryBV* bv)
   , d_numSolved(0)
   , d_numCalls(0)
   , d_ctx(new context::Context())
-  , d_quickXplain(options::bitvectorQuickXplain() ? new QuickXPlain("alg", d_quickSolver) : NULL)
+  , d_quickXplain(options::bitvectorQuickXplain() ? new QuickXPlain("theory::bv::algebraic", d_quickSolver) : NULL)
   , d_statistics()
 {}
 
@@ -778,14 +778,14 @@ Node AlgebraicSolver::getModelValue(TNode node) {
 }
 
 AlgebraicSolver::Statistics::Statistics()
-  : d_numCallstoCheck("theory::bv::AlgebraicSolver::NumCallsToCheck", 0)
-  , d_numSimplifiesToTrue("theory::bv::AlgebraicSolver::NumSimplifiesToTrue", 0)
-  , d_numSimplifiesToFalse("theory::bv::AlgebraicSolver::NumSimplifiesToFalse", 0)
-  , d_numUnsat("theory::bv::AlgebraicSolver::NumUnsat", 0)
-  , d_numSat("theory::bv::AlgebraicSolver::NumSat", 0)
-  , d_numUnknown("theory::bv::AlgebraicSolver::NumUnknown", 0)
-  , d_solveTime("theory::bv::AlgebraicSolver::SolveTime")
-  , d_useHeuristic("theory::bv::AlgebraicSolver::UseHeuristic", 0.2)
+  : d_numCallstoCheck("theory::bv::algebraic::NumCallsToCheck", 0)
+  , d_numSimplifiesToTrue("theory::bv::algebraic::NumSimplifiesToTrue", 0)
+  , d_numSimplifiesToFalse("theory::bv::algebraic::NumSimplifiesToFalse", 0)
+  , d_numUnsat("theory::bv::algebraic::NumUnsat", 0)
+  , d_numSat("theory::bv::algebraic::NumSat", 0)
+  , d_numUnknown("theory::bv::algebraic::NumUnknown", 0)
+  , d_solveTime("theory::bv::algebraic::SolveTime")
+  , d_useHeuristic("theory::bv::algebraic::UseHeuristic", 0.2)
 {
   smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
   smtStatisticsRegistry()->registerStat(&d_numSimplifiesToTrue);
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 61bbf667d..902a4dbe0 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -36,9 +36,9 @@ namespace bv {
 
 BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv)
   : SubtheorySolver(c, bv),
-    d_bitblaster(new TLazyBitblaster(c, bv, bv->getFullInstanceName() + "lazy")),
+    d_bitblaster(new TLazyBitblaster(c, bv, "theory::bv::lazy")),
     d_bitblastQueue(c),
-    d_statistics(bv->getFullInstanceName()),
+    d_statistics(),
     d_validModelCache(c, true),
     d_lemmaAtomsQueue(c),
     d_useSatPropagation(options::bitvectorPropagate()),
@@ -54,9 +54,9 @@ BitblastSolver::~BitblastSolver() {
   delete d_bitblaster;
 }
 
-BitblastSolver::Statistics::Statistics(const std::string &instanceName)
-  : d_numCallstoCheck(instanceName + "theory::bv::BitblastSolver::NumCallsToCheck", 0)
-  , d_numBBLemmas(instanceName + "theory::bv::BitblastSolver::NumTimesLemmasBB", 0)
+BitblastSolver::Statistics::Statistics()
+  : d_numCallstoCheck("theory::bv::BitblastSolver::NumCallsToCheck", 0)
+  , d_numBBLemmas("theory::bv::BitblastSolver::NumTimesLemmasBB", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
   smtStatisticsRegistry()->registerStat(&d_numBBLemmas);
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index f88810fca..509e59b19 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -39,7 +39,7 @@ class BitblastSolver : public SubtheorySolver {
   struct Statistics {
     IntStat d_numCallstoCheck;
     IntStat d_numBBLemmas;
-    Statistics(const std::string &instanceName);
+    Statistics();
     ~Statistics();
   };
   /** Bitblaster */
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 2c543b3da..bd4040dd7 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -34,7 +34,7 @@ using namespace CVC4::theory::bv::utils;
 CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv)
   : SubtheorySolver(c, bv),
     d_notify(*this),
-    d_equalityEngine(d_notify, c, "theory::bv::TheoryBV", true),
+    d_equalityEngine(d_notify, c, "theory::bv::ee", true),
     d_slicer(new Slicer()),
     d_isComplete(c, true),
     d_lemmaThreshold(16),
diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp
index bed922830..54c9cb08a 100644
--- a/src/theory/bv/bv_to_bool.cpp
+++ b/src/theory/bv/bv_to_bool.cpp
@@ -241,12 +241,12 @@ void BvToBoolPreprocessor::liftBvToBool(const std::vector<Node>& assertions, std
 }
 
 BvToBoolPreprocessor::Statistics::Statistics()
-  : d_numTermsLifted("theory::bv::BvToBoolPreprocess::NumberOfTermsLifted", 0)
-  , d_numAtomsLifted("theory::bv::BvToBoolPreprocess::NumberOfAtomsLifted", 0)
-  , d_numTermsForcedLifted("theory::bv::BvToBoolPreprocess::NumberOfTermsForcedLifted", 0)
-  , d_numTermsLowered("theory::bv::BvToBoolPreprocess::NumberOfTermsLowered", 0)
-  , d_numAtomsLowered("theory::bv::BvToBoolPreprocess::NumberOfAtomsLowered", 0)    
-  , d_numTermsForcedLowered("theory::bv::BvToBoolPreprocess::NumberOfTermsForcedLowered", 0)
+  : d_numTermsLifted("theory::bv::BvToBool::NumTermsLifted", 0)
+  , d_numAtomsLifted("theory::bv::BvToBool::NumAtomsLifted", 0)
+  , d_numTermsForcedLifted("theory::bv::BvToBool::NumTermsForcedLifted", 0)
+  , d_numTermsLowered("theory::bv::BvToBool::NumTermsLowered", 0)
+  , d_numAtomsLowered("theory::bv::BvToBool::NumAtomsLowered", 0)
+  , d_numTermsForcedLowered("theory::bv::BvToBool::NumTermsForcedLowered", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_numTermsLifted);
   smtStatisticsRegistry()->registerStat(&d_numAtomsLifted);
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index 6cd4a3314..189898c0c 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -369,13 +369,13 @@ void TLazyBitblaster::getConflict(std::vector<TNode>& conflict)
 }
 
 TLazyBitblaster::Statistics::Statistics(const std::string& prefix) :
-  d_numTermClauses("theory::bv::"+prefix+"::NumberOfTermSatClauses", 0),
-  d_numAtomClauses("theory::bv::"+prefix+"::NumberOfAtomSatClauses", 0),
-  d_numTerms("theory::bv::"+prefix+"::NumberOfBitblastedTerms", 0),
-  d_numAtoms("theory::bv::"+prefix+"::NumberOfBitblastedAtoms", 0),
-  d_numExplainedPropagations("theory::bv::"+prefix+"::NumberOfExplainedPropagations", 0),
-  d_numBitblastingPropagations("theory::bv::"+prefix+"::NumberOfBitblastingPropagations", 0),
-  d_bitblastTimer("theory::bv::"+prefix+"::BitblastTimer")
+  d_numTermClauses(prefix + "::NumTermSatClauses", 0),
+  d_numAtomClauses(prefix + "::NumAtomSatClauses", 0),
+  d_numTerms(prefix + "::NumBitblastedTerms", 0),
+  d_numAtoms(prefix + "::NumBitblastedAtoms", 0),
+  d_numExplainedPropagations(prefix + "::NumExplainedPropagations", 0),
+  d_numBitblastingPropagations(prefix + "::NumBitblastingPropagations", 0),
+  d_bitblastTimer(prefix + "::BitblastTimer")
 {
   smtStatisticsRegistry()->registerStat(&d_numTermClauses);
   smtStatisticsRegistry()->registerStat(&d_numAtomClauses);
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index fa234fcde..4c4b7c723 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -640,12 +640,12 @@ std::string UnionFind::debugPrint(TermId id) {
 }
 
 UnionFind::Statistics::Statistics():
-  d_numNodes("theory::bv::slicer::NumberOfNodes", 0),
-  d_numRepresentatives("theory::bv::slicer::NumberOfRepresentatives", 0),
-  d_numSplits("theory::bv::slicer::NumberOfSplits", 0),
-  d_numMerges("theory::bv::slicer::NumberOfMerges", 0),
+  d_numNodes("theory::bv::slicer::NumNodes", 0),
+  d_numRepresentatives("theory::bv::slicer::NumRepresentatives", 0),
+  d_numSplits("theory::bv::slicer::NumSplits", 0),
+  d_numMerges("theory::bv::slicer::NumMerges", 0),
   d_avgFindDepth("theory::bv::slicer::AverageFindDepth"),
-  d_numAddedEqualities("theory::bv::slicer::NumberOfEqualitiesAdded", Slicer::d_numAddedEqualities)
+  d_numAddedEqualities("theory::bv::slicer::NumEqualitiesAdded", Slicer::d_numAddedEqualities)
 {
   smtStatisticsRegistry()->registerStat(&d_numRepresentatives);
   smtStatisticsRegistry()->registerStat(&d_numSplits);
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index fd9ad0c6a..47f2b9245 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -51,7 +51,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u,
     d_sharedTermsSet(c),
     d_subtheories(),
     d_subtheoryMap(),
-    d_statistics(getFullInstanceName()),
+    d_statistics(),
     d_staticLearnCache(),
     d_BVDivByZero(),
     d_BVRemByZero(),
@@ -64,7 +64,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u,
     d_literalsToPropagateIndex(c, 0),
     d_propagatedBy(c),
     d_eagerSolver(NULL),
-    d_abstractionModule(new AbstractionModule(getFullInstanceName())),
+    d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV))),
     d_isCoreTheory(false),
     d_calledPreregister(false),
     d_needsLastCallCheck(false),
@@ -130,14 +130,14 @@ void TheoryBV::spendResource(unsigned amount)
   getOutputChannel().spendResource(amount);
 }
 
-TheoryBV::Statistics::Statistics(const std::string &name):
-  d_avgConflictSize(name + "theory::bv::AvgBVConflictSize"),
-  d_solveSubstitutions(name + "theory::bv::NumberOfSolveSubstitutions", 0),
-  d_solveTimer(name + "theory::bv::solveTimer"),
-  d_numCallsToCheckFullEffort(name + "theory::bv::NumberOfFullCheckCalls", 0),
-  d_numCallsToCheckStandardEffort(name + "theory::bv::NumberOfStandardCheckCalls", 0),
-  d_weightComputationTimer(name + "theory::bv::weightComputationTimer"),
-  d_numMultSlice(name + "theory::bv::NumMultSliceApplied", 0)
+TheoryBV::Statistics::Statistics():
+  d_avgConflictSize("theory::bv::AvgBVConflictSize"),
+  d_solveSubstitutions("theory::bv::NumSolveSubstitutions", 0),
+  d_solveTimer("theory::bv::solveTimer"),
+  d_numCallsToCheckFullEffort("theory::bv::NumFullCheckCalls", 0),
+  d_numCallsToCheckStandardEffort("theory::bv::NumStandardCheckCalls", 0),
+  d_weightComputationTimer("theory::bv::weightComputationTimer"),
+  d_numMultSlice("theory::bv::NumMultSliceApplied", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_avgConflictSize);
   smtStatisticsRegistry()->registerStat(&d_solveSubstitutions);
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 1992c0ae3..90bd6275c 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -117,7 +117,7 @@ private:
     IntStat     d_numCallsToCheckStandardEffort;
     TimerStat   d_weightComputationTimer;
     IntStat     d_numMultSlice;
-    Statistics(const std::string &name);
+    Statistics();
     ~Statistics();
   };