diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-11 22:54:50 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-11 22:54:50 -0600 |
| commit | a49efc8c32020b7c2285fa744ae61a576801c51d (patch) | |
| tree | e261da599172d1bc767da066e25e15b9cf4eaec5 /src/main | |
| parent | 107b1422f9549eb2128729c3fd173441029ba443 (diff) | |
Flush statistics through NodeManager in SmtEngine (#5652)
This removes the dependency on the Expr layer from src/main.
This requires moving the flushing of NodeManager statistics within SmtEngine.
This is a temporary solution until we have a permanent solution for statistics.
Diffstat (limited to 'src/main')
| -rw-r--r-- | src/main/command_executor.cpp | 6 | ||||
| -rw-r--r-- | src/main/command_executor.h | 1 | ||||
| -rw-r--r-- | src/main/driver_unified.cpp | 2 | ||||
| -rw-r--r-- | src/main/main.cpp | 2 | ||||
| -rw-r--r-- | src/main/main.h | 2 |
5 files changed, 3 insertions, 10 deletions
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index af95ca20f..fe4af6361 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -66,14 +66,14 @@ CommandExecutor::~CommandExecutor() void CommandExecutor::flushStatistics(std::ostream& out) const { - d_solver->getExprManager()->getStatistics().flushInformation(out); - d_smtEngine->getStatistics().flushInformation(out); + // SmtEngine + node manager flush statistics is part of the call below + d_smtEngine->flushStatistics(out); d_stats.flushInformation(out); } void CommandExecutor::safeFlushStatistics(int fd) const { - d_solver->getExprManager()->safeFlushStatistics(fd); + // SmtEngine + node manager flush statistics is part of the call below d_smtEngine->safeFlushStatistics(fd); d_stats.safeFlushInformation(fd); } diff --git a/src/main/command_executor.h b/src/main/command_executor.h index db2248454..433cebf33 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -19,7 +19,6 @@ #include <string> #include "api/cvc4cpp.h" -#include "expr/expr_manager.h" #include "expr/symbol_manager.h" #include "options/options.h" #include "smt/smt_engine.h" diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 9b0fc81be..7228bc167 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -27,8 +27,6 @@ #include "api/cvc4cpp.h" #include "base/configuration.h" #include "base/output.h" -#include "expr/expr_iomanip.h" -#include "expr/expr_manager.h" #include "main/command_executor.h" #include "main/interactive_shell.h" #include "main/main.h" diff --git a/src/main/main.cpp b/src/main/main.cpp index e08898905..a2f119414 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -24,7 +24,6 @@ #include "base/configuration.h" #include "base/output.h" -#include "expr/expr_manager.h" #include "main/command_executor.h" #include "main/interactive_shell.h" #include "options/language.h" @@ -32,7 +31,6 @@ #include "parser/parser.h" #include "parser/parser_builder.h" #include "parser/parser_exception.h" -#include "smt/smt_engine.h" #include "util/result.h" #include "util/statistics.h" diff --git a/src/main/main.h b/src/main/main.h index 37916f769..fbcd28385 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -19,9 +19,7 @@ #include "base/exception.h" #include "cvc4autoconfig.h" -#include "expr/expr_manager.h" #include "options/options.h" -#include "smt/smt_engine.h" #include "util/statistics.h" #include "util/statistics_registry.h" |