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.

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index af95ca20f51512c5d21d8bdc2449660c8026433f..fe4af6361c45b6aa7adacc4e54e433f290f66e8b 100644 (file)
--- 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 db2248454df18d0e52616fdde10c1b8e937775a0..433cebf33925fffc0a83d87b01fad0a34bc24aad 100644 (file)
--- 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 9b0fc81be0a25def35308fa2430aaec57b8e688d..7228bc167c1ba99f8adae86e373895acae4a96f2 100644 (file)
--- 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 e08898905aa2f19180542d14c522418da63c969b..a2f1194149e774d0fe5f3792e424b37eec2639b8 100644 (file)
--- 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 37916f769a67fa3cab22bc7de69e5f7344ac4802..fbcd28385db9b6b46ff9885f2dca53cc81faae77 100644 (file)
--- 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"
 

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 81294722f85069536f343498912831173541d02b..b1f56ea375e45c5dcfffd921d4df9a499a714aea 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1765,7 +1765,15 @@ SExpr SmtEngine::getStatistic(std::string name) const
   return d_statisticsRegistry->getStatistic(name);
 }
 
-void SmtEngine::safeFlushStatistics(int fd) const {
+void SmtEngine::flushStatistics(std::ostream& out) const
+{
+  d_nodeManager->getStatisticsRegistry()->flushInformation(out);
+  d_statisticsRegistry->flushInformation(out);
+}
+
+void SmtEngine::safeFlushStatistics(int fd) const
+{
+  d_nodeManager->getStatisticsRegistry()->safeFlushInformation(fd);
   d_statisticsRegistry->safeFlushInformation(fd);
 }
 

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index bce08620227ba5d6b1aa3a0c0952deb1f7121724..f8a74597b8184d8818786d3525f9b403a3478ced 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -801,7 +801,13 @@ class CVC4_PUBLIC SmtEngine
   /** Get the value of one named statistic from this SmtEngine. */
   SExpr getStatistic(std::string name) const;
 
-  /** Flush statistic from this SmtEngine. Safe to use in a signal handler. */
+  /** Flush statistics from this SmtEngine and the NodeManager it uses. */
+  void flushStatistics(std::ostream& out) const;
+
+  /**
+   * Flush statistics from this SmtEngine and the NodeManager it uses. Safe to
+   * use in a signal handler.
+   */
   void safeFlushStatistics(int fd) const;
 
   /**