Perform statistics printing via the API (#6952)

This PR changes how the command executor prints the statistics by moving stuff around a bit, eventually using only proper API methods of api::Solver. This PR also removes the smt_engine.h include from command_executor.cpp.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 4252cd45e5f313f669de2821a1351148bcd9af48..69aa720ea713e3a1a9b930282bd412831ba25569 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -4762,7 +4762,9 @@ struct Stat::StatData
 
 Stat::~Stat() {}
 Stat::Stat(const Stat& s)
-    : d_expert(s.d_expert), d_data(std::make_unique<StatData>(s.d_data->data))
+    : d_expert(s.d_expert),
+      d_default(s.d_default),
+      d_data(std::make_unique<StatData>(s.d_data->data))
 {
 }
 Stat& Stat::operator=(const Stat& s)
@@ -5387,6 +5389,11 @@ void Solver::resetStatistics()
   }
 }
 
+void Solver::printStatisticsSafe(int fd) const
+{
+  d_smtEngine->printStatisticsSafe(fd);
+}
+
 /* Helpers for mkTerm checks.                                                 */
 /* .......................................................................... */
 
@@ -6640,8 +6647,7 @@ Result Solver::checkEntailed(const Term& term) const
          "(try --incremental)";
   CVC5_API_SOLVER_CHECK_TERM(term);
   //////// all checks before this line
-  cvc5::Result r = d_smtEngine->checkEntailed(*term.d_node);
-  return Result(r);
+  return d_smtEngine->checkEntailed(*term.d_node);
   ////////
   CVC5_API_TRY_CATCH_END;
 }
@@ -6684,8 +6690,7 @@ Result Solver::checkSat(void) const
       << "Cannot make multiple queries unless incremental solving is enabled "
          "(try --incremental)";
   //////// all checks before this line
-  cvc5::Result r = d_smtEngine->checkSat();
-  return Result(r);
+  return d_smtEngine->checkSat();
   ////////
   CVC5_API_TRY_CATCH_END;
 }
@@ -6700,8 +6705,7 @@ Result Solver::checkSatAssuming(const Term& assumption) const
          "(try --incremental)";
   CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(assumption, getBooleanSort());
   //////// all checks before this line
-  cvc5::Result r = d_smtEngine->checkSat(*assumption.d_node);
-  return Result(r);
+  return d_smtEngine->checkSat(*assumption.d_node);
   ////////
   CVC5_API_TRY_CATCH_END;
 }
@@ -6721,8 +6725,7 @@ Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const
     CVC5_API_SOLVER_CHECK_TERM(term);
   }
   std::vector<Node> eassumptions = Term::termVectorToNodes(assumptions);
-  cvc5::Result r = d_smtEngine->checkSat(eassumptions);
-  return Result(r);
+  return d_smtEngine->checkSat(eassumptions);
   ////////
   CVC5_API_TRY_CATCH_END;
 }

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 672ccf8f8242f8bd7e28ea061f5594068b44f55a..e41df9593e4394b33a9779778fe81f12c4526176 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -4161,6 +4161,11 @@ class CVC5_EXPORT Solver
   /** Reset the API statistics */
   void resetStatistics();
 
+  /**
+   * Print the statistics to the given file descriptor, suitable for usage in signal handlers.
+   */
+  void printStatisticsSafe(int fd) const;
+
   /** Helper to check for API misuse in mkOp functions. */
   void checkMkTerm(Kind kind, uint32_t nchildren) const;
   /** Helper for mk-functions that call d_nodeMgr->mkConst(). */

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 55b93a15c26777ebc014949788e482503256dbdc..ce7a46b4e85dad7e055836616b24848ca429826b 100644 (file)
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -29,7 +29,6 @@
 #include "options/base_options.h"
 #include "options/main_options.h"
 #include "smt/command.h"
-#include "smt/smt_engine.h"
 
 namespace cvc5 {
 namespace main {
@@ -68,7 +67,7 @@ void CommandExecutor::printStatistics(std::ostream& out) const
 {
   if (d_solver->getOptions().base.statistics)
   {
-    getSmtEngine()->printStatistics(out);
+    out << d_solver->getStatistics();
   }
 }
 
@@ -76,7 +75,7 @@ void CommandExecutor::printStatisticsSafe(int fd) const
 {
   if (d_solver->getOptions().base.statistics)
   {
-    getSmtEngine()->printStatisticsSafe(fd);
+    d_solver->printStatisticsSafe(fd);
   }
 }
 
@@ -152,12 +151,6 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
     d_result = res = q->getResult();
   }
 
-  if ((cs != nullptr || q != nullptr)
-      && d_solver->getOptions().base.statisticsEveryQuery)
-  {
-    getSmtEngine()->printStatisticsDiff(*d_solver->getOptions().base.err);
-  }
-
   bool isResultUnsat = res.isUnsat() || res.isEntailed();
 
   // dump the model/proof/unsat core if option is set

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index bbd65c24f0fb6ecb5cb860b67eb3ee0ed3d97665..d3eb5c48a628cf10b9d7ad9f631c6e146d87188c 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -935,7 +935,10 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
         checkUnsatCore();
       }
     }
-
+    if (d_env->getOptions().base.statisticsEveryQuery)
+    {
+      printStatisticsDiff();
+    }
     return r;
   }
   catch (UnsafeInterruptException& e)
@@ -948,6 +951,11 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
     Result::UnknownExplanation why = getResourceManager()->outOfResources()
                                          ? Result::RESOURCEOUT
                                          : Result::TIMEOUT;
+
+    if (d_env->getOptions().base.statisticsEveryQuery)
+    {
+      printStatisticsDiff();
+    }
     return Result(Result::SAT_UNKNOWN, why, d_state->getFilename());
   }
 }
@@ -1925,9 +1933,9 @@ void SmtEngine::printStatisticsSafe(int fd) const
   d_env->getStatisticsRegistry().printSafe(fd);
 }
 
-void SmtEngine::printStatisticsDiff(std::ostream& out) const
+void SmtEngine::printStatisticsDiff() const
 {
-  d_env->getStatisticsRegistry().printDiff(out);
+  d_env->getStatisticsRegistry().printDiff(*d_env->getOptions().base.err);
   d_env->getStatisticsRegistry().storeSnapshot();
 }
 

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 02e5c6b064cc09466e1f9e51d2bbf8f55e7c446d..0e4e03f3adefc6a32de9566f572737a0d39edf1f 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -828,7 +828,7 @@ class CVC5_EXPORT SmtEngine
    * time. Internally prints the diff and then stores a snapshot for the next
    * call.
    */
-  void printStatisticsDiff(std::ostream&) const;
+  void printStatisticsDiff() const;
 
   /**
    * Set user attribute.