From c6b2e085d4eb2c232a528a96e13fc7b65fd98fea Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Tue, 6 Mar 2018 16:54:06 -0800 Subject: 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"). --- src/theory/bv/abstraction.cpp | 7 ++++--- src/theory/bv/bv_quick_check.cpp | 14 +++++++------- src/theory/bv/bv_quick_check.h | 2 +- src/theory/bv/bv_subtheory_algebraic.cpp | 20 ++++++++++---------- src/theory/bv/bv_subtheory_bitblast.cpp | 10 +++++----- src/theory/bv/bv_subtheory_bitblast.h | 2 +- src/theory/bv/bv_subtheory_core.cpp | 2 +- src/theory/bv/bv_to_bool.cpp | 12 ++++++------ src/theory/bv/lazy_bitblaster.cpp | 14 +++++++------- src/theory/bv/slicer.cpp | 10 +++++----- src/theory/bv/theory_bv.cpp | 20 ++++++++++---------- src/theory/bv/theory_bv.h | 2 +- 12 files changed, 58 insertions(+), 57 deletions(-) (limited to 'src/theory/bv') 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& 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& 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(); }; -- cgit v1.2.3