summaryrefslogtreecommitdiff
path: root/src/expr/kind_template.h
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/expr/kind_template.h
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/expr/kind_template.h')
-rw-r--r--src/expr/kind_template.h1
1 files changed, 1 insertions, 0 deletions
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback