diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-04-28 20:01:15 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-28 18:01:15 +0000 |
commit | 0683b708c4752c1d0e894f19e8011a256ef6df7e (patch) | |
tree | 2f832d72c3b7b83519bf030a692bc0b91278b2d6 /src/util | |
parent | b5ac06abf4b2cc6b027dedd045595187589bcc35 (diff) |
Make sure reference stats are reset properly (#6457)
This PR adds a reset() method to the ReferenceStat class. It then uses it to properly reset such statistics in the minisat solvers where lifetime is an issue.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/statistics_stats.h | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/util/statistics_stats.h b/src/util/statistics_stats.h index 4821dda60..982190b79 100644 --- a/src/util/statistics_stats.h +++ b/src/util/statistics_stats.h @@ -131,6 +131,15 @@ class ReferenceStat d_data->d_value = &t; } } + /** Commit the value currently pointed to and release it. */ + void reset() + { + if constexpr (Configuration::isStatisticsBuild()) + { + d_data->commit(); + d_data->d_value = nullptr; + } + } /** Copy the current value of the referenced object. */ ~ReferenceStat() { |