summaryrefslogtreecommitdiff
path: root/src/theory/bv/bv_to_bool.cpp
diff options
context:
space:
mode:
authorMathias Preiner <mathias.preiner@gmail.com>2018-03-06 16:54:06 -0800
committerGitHub <noreply@github.com>2018-03-06 16:54:06 -0800
commitc6b2e085d4eb2c232a528a96e13fc7b65fd98fea (patch)
tree632708f158acc6a3b5b3201212fa2ba1a0606c30 /src/theory/bv/bv_to_bool.cpp
parent612bb0013f180a7d414f0a4b1e770aaa7ed09152 (diff)
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").
Diffstat (limited to 'src/theory/bv/bv_to_bool.cpp')
-rw-r--r--src/theory/bv/bv_to_bool.cpp12
1 files changed, 6 insertions, 6 deletions
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback