diff options
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/command_executor.h | 2 | ||||
-rw-r--r-- | src/main/command_executor_portfolio.cpp | 8 | ||||
-rw-r--r-- | src/main/driver_unified.cpp | 2 | ||||
-rw-r--r-- | src/main/main.cpp | 2 | ||||
-rw-r--r-- | src/main/main.h | 4 | ||||
-rw-r--r-- | src/main/portfolio.cpp | 3 | ||||
-rw-r--r-- | src/main/portfolio.h | 2 | ||||
-rw-r--r-- | src/main/util.cpp | 2 |
8 files changed, 12 insertions, 13 deletions
diff --git a/src/main/command_executor.h b/src/main/command_executor.h index df9c9e19f..7b6c2fab5 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -19,10 +19,10 @@ #include <string> #include "expr/expr_manager.h" -#include "expr/statistics_registry.h" #include "options/options.h" #include "smt/smt_engine.h" #include "smt_util/command.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace main { diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index cdd20c05a..9d0042694 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -63,8 +63,8 @@ CommandExecutorPortfolio::CommandExecutorPortfolio assert(d_threadOptions.size() == d_numThreads); d_statLastWinner.setData(d_lastWinner); - d_stats.registerStat_(&d_statLastWinner); - d_stats.registerStat_(&d_statWaitTime); + d_stats.registerStat(&d_statLastWinner); + d_stats.registerStat(&d_statWaitTime); /* Duplication, individualization */ d_exprMgrs.push_back(&d_exprMgr); @@ -99,8 +99,8 @@ CommandExecutorPortfolio::~CommandExecutorPortfolio() d_exprMgrs.clear(); d_smts.clear(); - d_stats.unregisterStat_(&d_statLastWinner); - d_stats.unregisterStat_(&d_statWaitTime); + d_stats.unregisterStat(&d_statLastWinner); + d_stats.unregisterStat(&d_statWaitTime); } void CommandExecutorPortfolio::lemmaSharingInit() diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index c110ffa4f..71f47906d 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -28,7 +28,6 @@ #include "base/output.h" #include "expr/expr_iomanip.h" #include "expr/expr_manager.h" -#include "expr/statistics_registry.h" #include "main/command_executor.h" #ifdef PORTFOLIO_BUILD @@ -50,6 +49,7 @@ #include "smt_util/command.h" #include "util/configuration.h" #include "util/result.h" +#include "util/statistics_registry.h" using namespace std; using namespace CVC4; diff --git a/src/main/main.cpp b/src/main/main.cpp index f8cb0677c..92902ac11 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -24,7 +24,6 @@ #include "base/output.h" #include "expr/expr_manager.h" -#include "expr/statistics.h" #include "main/command_executor.h" #include "main/interactive_shell.h" #include "options/base_options.h" @@ -37,6 +36,7 @@ #include "smt_util/command.h" #include "util/configuration.h" #include "util/result.h" +#include "util/statistics.h" using namespace std; using namespace CVC4; diff --git a/src/main/main.h b/src/main/main.h index 7dda429af..2ba688a98 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -21,10 +21,10 @@ #include "base/tls.h" #include "cvc4autoconfig.h" #include "expr/expr_manager.h" -#include "expr/statistics.h" -#include "expr/statistics_registry.h" #include "options/options.h" #include "smt/smt_engine.h" +#include "util/statistics.h" +#include "util/statistics_registry.h" #ifndef __CVC4__MAIN__MAIN_H #define __CVC4__MAIN__MAIN_H diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp index ea7e3d458..22f3a67ae 100644 --- a/src/main/portfolio.cpp +++ b/src/main/portfolio.cpp @@ -20,11 +20,10 @@ #include <boost/exception_ptr.hpp> #include "base/output.h" -#include "expr/statistics_registry.h" #include "options/options.h" #include "smt/smt_engine.h" #include "util/result.h" - +#include "util/statistics_registry.h" namespace CVC4 { diff --git a/src/main/portfolio.h b/src/main/portfolio.h index 5a730c005..cab8bda3c 100644 --- a/src/main/portfolio.h +++ b/src/main/portfolio.h @@ -19,10 +19,10 @@ #include <boost/function.hpp> #include <utility> -#include "expr/statistics_registry.h" #include "options/options.h" #include "smt/smt_engine.h" #include "smt_util/command.h" +#include "util/statistics_registry.h" namespace CVC4 { diff --git a/src/main/util.cpp b/src/main/util.cpp index bc3d45287..abcdcc7c5 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -31,12 +31,12 @@ #include "base/exception.h" #include "base/tls.h" #include "cvc4autoconfig.h" -#include "expr/statistics.h" #include "main/command_executor.h" #include "main/main.h" #include "options/base_options.h" #include "options/options.h" #include "smt/smt_engine.h" +#include "util/statistics.h" using CVC4::Exception; using namespace std; |