diff options
| author | Tim King <taking@cs.nyu.edu> | 2018-01-08 22:04:02 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-01-08 22:04:02 -0800 |
| commit | 3c6398194b01372720964590b2b07d93590e511d (patch) | |
| tree | 1e1f40d79eeabe8b30524fe96d279a4f3d5b8fd7 /src/util/statistics_registry.cpp | |
| parent | 707e27e61addafdbcce5e7b6d32a61985f563dfb (diff) | |
Removing more miscellaneous throw specifiers. (#1488)
Removing more miscellaneous throw specifiers.
Diffstat (limited to 'src/util/statistics_registry.cpp')
| -rw-r--r-- | src/util/statistics_registry.cpp | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp index 016bd2184..11afb99ed 100644 --- a/src/util/statistics_registry.cpp +++ b/src/util/statistics_registry.cpp @@ -140,10 +140,8 @@ std::ostream& operator<<(std::ostream& os, const timespec& t) { /** Construct a statistics registry */ -StatisticsRegistry::StatisticsRegistry(const std::string& name) - throw(CVC4::IllegalArgumentException) : - Stat(name) { - +StatisticsRegistry::StatisticsRegistry(const std::string& name) : Stat(name) +{ d_prefix = name; if(__CVC4_USE_STATISTICS) { PrettyCheckArgument(d_name.find(s_regDelim) == std::string::npos, name, @@ -152,7 +150,8 @@ StatisticsRegistry::StatisticsRegistry(const std::string& name) } } -void StatisticsRegistry::registerStat(Stat* s) throw(CVC4::IllegalArgumentException) { +void StatisticsRegistry::registerStat(Stat* s) +{ #ifdef CVC4_STATISTICS_ON PrettyCheckArgument(d_stats.find(s) == d_stats.end(), s, "Statistic `%s' was not registered with this registry.", @@ -161,7 +160,8 @@ void StatisticsRegistry::registerStat(Stat* s) throw(CVC4::IllegalArgumentExcept #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::registerStat_() */ -void StatisticsRegistry::unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException) { +void StatisticsRegistry::unregisterStat(Stat* s) +{ #ifdef CVC4_STATISTICS_ON PrettyCheckArgument(d_stats.find(s) != d_stats.end(), s, "Statistic `%s' was not registered with this registry.", |