diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-03-06 16:54:06 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-03-06 16:54:06 -0800 |
| commit | c6b2e085d4eb2c232a528a96e13fc7b65fd98fea (patch) | |
| tree | 632708f158acc6a3b5b3201212fa2ba1a0606c30 /src/expr/mkkind | |
| parent | 612bb0013f180a7d414f0a4b1e770aaa7ed09152 (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/mkkind')
| -rwxr-xr-x | src/expr/mkkind | 5 |
1 files changed, 5 insertions, 0 deletions
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}}" |