From 63647b1d79df6f287ea6599958b16fce44b8271d Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 15 Apr 2021 21:30:49 +0200 Subject: [PATCH] Fix printing of stats when aborted. (#6362) This PR improves/fixes printing of statistics when the solver has been aborted, i.e. when we use printSafe(), and a few other minor issues with the new statistics setup. add toString() methods for TypeConstant, api::Kind to allow for automatic printing by print_safe<>() improve kindToString() to avoid std::stringstream fix newlines between statistics in printSafe() make printing of histograms consistent make --stats-all, --stats-expert and --stats-every-check automatically enable --stats (and vice versa) --- src/api/cpp/cvc5.cpp | 6 ++++++ src/expr/kind_template.cpp | 24 +++++++++++------------- src/expr/kind_template.h | 1 + src/expr/mkkind | 2 +- src/options/base_options.toml | 26 +++++++++++++------------- src/options/options_handler.cpp | 29 +++++++++++++++++++++++++++-- src/options/options_handler.h | 2 +- src/util/statistics_registry.cpp | 2 +- src/util/statistics_value.h | 2 -- 9 files changed, 61 insertions(+), 33 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 2a8e0f4c7..5c3cbd3f5 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -762,6 +762,12 @@ std::string kindToString(Kind k) : cvc5::kind::kindToString(extToIntKind(k)); } +const char* toString(Kind k) +{ + return k == INTERNAL_KIND ? "INTERNAL_KIND" + : cvc5::kind::toString(extToIntKind(k)); +} + std::ostream& operator<<(std::ostream& out, Kind k) { switch (k) diff --git a/src/expr/kind_template.cpp b/src/expr/kind_template.cpp index 0674a61b0..da1a75499 100644 --- a/src/expr/kind_template.cpp +++ b/src/expr/kind_template.cpp @@ -62,23 +62,21 @@ bool isAssociative(::cvc5::Kind k) } } -std::string kindToString(::cvc5::Kind k) -{ - std::stringstream ss; - ss << k; - return ss.str(); -} +std::string kindToString(::cvc5::Kind k) { return toString(k); } } // namespace kind -std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) { - switch(typeConstant) { -${type_constant_descriptions} - default: - out << "UNKNOWN_TYPE_CONSTANT"; - break; +const char* toString(TypeConstant tc) +{ + switch (tc) + { + ${type_constant_descriptions} + default: return "UNKNOWN_TYPE_CONSTANT"; } - return out; +} +std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) +{ + return out << toString(typeConstant); } namespace theory { diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index d5fc3967c..5fa1d99ff 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -92,6 +92,7 @@ struct TypeConstantHashFunction { } };/* struct TypeConstantHashFunction */ +const char* toString(TypeConstant tc); std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant); namespace theory { diff --git a/src/expr/mkkind b/src/expr/mkkind index bf0da1073..53e63af6e 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -256,7 +256,7 @@ function register_sort { type_constant_list="${type_constant_list} ${id}, /**< ${comment} */ " - type_constant_descriptions="${type_constant_descriptions} case $id: out << \"${comment}\"; break; + type_constant_descriptions="${type_constant_descriptions} case $id: return \"${comment}\"; " type_constant_to_theory_id="${type_constant_to_theory_id} case $id: return $theory_id; " diff --git a/src/options/base_options.toml b/src/options/base_options.toml index 9c02a51d1..4ebb71b76 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -85,33 +85,33 @@ header = "options/base_options.h" [[option]] name = "statistics" - smt_name = "statistics" + smt_name = "stats" long = "stats" category = "common" type = "bool" - predicates = ["statsEnabledBuild"] + predicates = ["setStats"] read_only = true help = "give statistics on exit" [[option]] - name = "statisticsExpert" - smt_name = "stats-expert" - long = "stats-expert" + name = "statisticsAll" + smt_name = "stats-all" + long = "stats-all" category = "expert" type = "bool" - predicates = ["statsEnabledBuild"] + predicates = ["setStats"] read_only = true - help = "print expert (non-public) statistics as well" + help = "print unchanged (defaulted) statistics as well" [[option]] - name = "statisticsAll" - smt_name = "stats-all" - long = "stats-all" + name = "statisticsExpert" + smt_name = "stats-expert" + long = "stats-expert" category = "expert" type = "bool" - predicates = ["statsEnabledBuild"] + predicates = ["setStats"] read_only = true - help = "print unchanged (defaulted) statistics as well" + help = "print expert (non-public) statistics as well" [[option]] name = "statisticsEveryQuery" @@ -119,7 +119,7 @@ header = "options/base_options.h" long = "stats-every-query" category = "regular" type = "bool" - predicates = ["statsEnabledBuild"] + predicates = ["setStats"] default = "false" read_only = true help = "in incremental mode, print stats after every satisfiability or validity query" diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 28b8073b9..86ab9c0b3 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -259,15 +259,40 @@ void OptionsHandler::setProduceAssertions(std::string option, bool value) options::interactiveMode.set(value); } -void OptionsHandler::statsEnabledBuild(std::string option, bool value) +void OptionsHandler::setStats(const std::string& option, bool value) { #ifndef CVC5_STATISTICS_ON - if(value) { + if (value) + { std::stringstream ss; ss << "option `" << option << "' requires a statistics-enabled build of CVC4; this binary was not built with statistics support"; throw OptionException(ss.str()); } #endif /* CVC5_STATISTICS_ON */ + if (value) + { + if (option == options::statisticsAll.getName()) + { + d_options->d_holder->statistics = true; + } + else if (option == options::statisticsEveryQuery.getName()) + { + d_options->d_holder->statistics = true; + } + else if (option == options::statisticsExpert.getName()) + { + d_options->d_holder->statistics = true; + } + } + else + { + if (option == options::statistics.getName()) + { + d_options->d_holder->statisticsAll = false; + d_options->d_holder->statisticsEveryQuery = false; + d_options->d_holder->statisticsExpert = false; + } + } } void OptionsHandler::threadN(std::string option) { diff --git a/src/options/options_handler.h b/src/options/options_handler.h index f8b818f0f..6fd9a398b 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -86,7 +86,7 @@ public: */ void setProduceAssertions(std::string option, bool value); - void statsEnabledBuild(std::string option, bool value); + void setStats(const std::string& option, bool value); unsigned long limitHandler(std::string option, std::string optarg); void setResourceWeight(std::string option, std::string optarg); diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp index ebd16ebc0..51da36aba 100644 --- a/src/util/statistics_registry.cpp +++ b/src/util/statistics_registry.cpp @@ -97,7 +97,7 @@ void StatisticsRegistry::printSafe(int fd) const safe_print(fd, s.first); safe_print(fd, " = "); s.second->printSafe(fd); - safe_print(fd, '\n'); + safe_print(fd, "\n"); } } } diff --git a/src/util/statistics_value.h b/src/util/statistics_value.h index 09f429187..950bdd4ab 100644 --- a/src/util/statistics_value.h +++ b/src/util/statistics_value.h @@ -154,11 +154,9 @@ struct StatisticHistogramValue : StatisticBaseValue { safe_print(fd, ", "); } - safe_print(fd, "("); safe_print(fd, static_cast(i + d_offset)); safe_print(fd, ": "); safe_print(fd, d_hist[i]); - safe_print(fd, ")"); } } safe_print(fd, " }"); -- 2.30.2