summaryrefslogtreecommitdiff
path: root/src/theory/bv/bv_quick_check.h
diff options
context:
space:
mode:
authorGereon Kremer <gkremer@stanford.edu>2021-03-11 21:20:19 +0100
committerGitHub <noreply@github.com>2021-03-11 20:20:19 +0000
commit42d5d8950d849aa4b855aa62834cd5fdee1a91a8 (patch)
tree2cbb6d9b283c05fc12ba9ad8495fa84a57375af6 /src/theory/bv/bv_quick_check.h
parentdc679ed380aabc62aadfbb4033c02c5a27ae903c (diff)
First refactoring of statistics classes (#6105)
This PR does a first round of refactoring on the statistics, in particular the Stat class and derived classes. It significantly shrinks the class hierarchy, modernizes some code (e.g. use std::chrono instead of clock_gettime), removes unused features (e.g. nesting of statistics) and does some general cleanup and consolidation. Subsequent PRs are planned to change the ownership model (right now every module owns the Stat object) which makes the whole register / unregister mechanism obsolete.
Diffstat (limited to 'src/theory/bv/bv_quick_check.h')
-rw-r--r--src/theory/bv/bv_quick_check.h1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index b10eb2811..f509c3cb4 100644
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -27,6 +27,7 @@
#include "prop/sat_solver_types.h"
#include "theory/bv/theory_bv_utils.h"
#include "util/statistics_registry.h"
+#include "util/stats_timer.h"
namespace CVC4 {
namespace theory {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback