From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 12 Dec 2020 04:54:50 +0000 (-0600)
Subject: Flush statistics through NodeManager in SmtEngine (#5652)
X-Git-Tag: cvc5-1.0.0~2453
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a49efc8c32020b7c2285fa744ae61a576801c51d;p=cvc5.git

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 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"
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 81294722f..b1f56ea37 100644
--- 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 bce086202..f8a74597b 100644
--- 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;
 
   /**