From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Mon, 11 Oct 2021 23:21:32 +0000 (-0700)
Subject: Rename SmtEngineStatistics to SolverEngineStatistics. (#7339)
X-Git-Tag: cvc5-1.0.0~1087
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=18e52361a8109c62de3636b3a261b25e3991734b;p=cvc5.git

Rename SmtEngineStatistics to SolverEngineStatistics. (#7339)
---

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 61be39f97..c00e92c83 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -353,8 +353,8 @@ libcvc5_add_sources(
   smt/solver_engine_scope.h
   smt/smt_engine_state.cpp
   smt/smt_engine_state.h
-  smt/smt_engine_stats.cpp
-  smt/smt_engine_stats.h
+  smt/solver_engine_stats.cpp
+  smt/solver_engine_stats.h
   smt/smt_mode.cpp
   smt/smt_mode.h
   smt/smt_solver.cpp
diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index f63747ebd..9334732fe 100644
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -25,7 +25,7 @@
 #include "printer/printer.h"
 #include "proof/conv_proof_generator.h"
 #include "smt/dump_manager.h"
-#include "smt/smt_engine_stats.h"
+#include "smt/solver_engine_stats.h"
 #include "theory/evaluator.h"
 #include "theory/rewriter.h"
 #include "theory/trust_substitutions.h"
diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp
index 3ee08848d..126896786 100644
--- a/src/smt/expand_definitions.cpp
+++ b/src/smt/expand_definitions.cpp
@@ -22,8 +22,8 @@
 #include "preprocessing/assertion_pipeline.h"
 #include "proof/conv_proof_generator.h"
 #include "smt/env.h"
-#include "smt/smt_engine_stats.h"
 #include "smt/solver_engine.h"
+#include "smt/solver_engine_stats.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 #include "util/resource_manager.h"
@@ -35,7 +35,7 @@ using namespace cvc5::kind;
 namespace cvc5 {
 namespace smt {
 
-ExpandDefs::ExpandDefs(Env& env, SmtEngineStatistics& stats)
+ExpandDefs::ExpandDefs(Env& env, SolverEngineStatistics& stats)
     : d_env(env), d_smtStats(stats), d_tpg(nullptr)
 {
 }
diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h
index 997e97391..f36c1769f 100644
--- a/src/smt/expand_definitions.h
+++ b/src/smt/expand_definitions.h
@@ -31,7 +31,7 @@ class TConvProofGenerator;
 
 namespace smt {
 
-struct SmtEngineStatistics;
+struct SolverEngineStatistics;
 
 /**
  * Module in charge of expanding definitions for an SMT engine.
@@ -42,7 +42,7 @@ struct SmtEngineStatistics;
 class ExpandDefs
 {
  public:
-  ExpandDefs(Env& env, SmtEngineStatistics& stats);
+  ExpandDefs(Env& env, SolverEngineStatistics& stats);
   ~ExpandDefs();
   /**
    * Expand definitions in term n. Return the expanded form of n.
@@ -70,7 +70,7 @@ class ExpandDefs
   /** Reference to the environment. */
   Env& d_env;
   /** Reference to the SMT stats */
-  SmtEngineStatistics& d_smtStats;
+  SolverEngineStatistics& d_smtStats;
   /** A proof generator for the term conversion. */
   std::unique_ptr<TConvProofGenerator> d_tpg;
 };
diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index bdf807181..9312deb97 100644
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -37,7 +37,7 @@ namespace smt {
 
 Preprocessor::Preprocessor(Env& env,
                            AbstractValues& abs,
-                           SmtEngineStatistics& stats)
+                           SolverEngineStatistics& stats)
     : EnvObj(env),
       d_absValues(abs),
       d_propagator(true, true),
diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h
index b455fb3ca..40a84981a 100644
--- a/src/smt/preprocessor.h
+++ b/src/smt/preprocessor.h
@@ -53,7 +53,7 @@ class PreprocessProofGenerator;
 class Preprocessor : protected EnvObj
 {
  public:
-  Preprocessor(Env& env, AbstractValues& abs, SmtEngineStatistics& stats);
+  Preprocessor(Env& env, AbstractValues& abs, SolverEngineStatistics& stats);
   ~Preprocessor();
   /**
    * Finish initialization
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 73578f2cb..8c4998e30 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -34,7 +34,7 @@
 #include "smt/dump.h"
 #include "smt/expand_definitions.h"
 #include "smt/print_benchmark.h"
-#include "smt/smt_engine_stats.h"
+#include "smt/solver_engine_stats.h"
 #include "theory/logic_info.h"
 #include "theory/theory_engine.h"
 
@@ -57,7 +57,7 @@ class ScopeCounter
   unsigned& d_depth;
 };
 
-ProcessAssertions::ProcessAssertions(Env& env, SmtEngineStatistics& stats)
+ProcessAssertions::ProcessAssertions(Env& env, SolverEngineStatistics& stats)
     : EnvObj(env), d_smtStats(stats), d_preprocessingPassContext(nullptr)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h
index 00b57813f..7f7ce9cca 100644
--- a/src/smt/process_assertions.h
+++ b/src/smt/process_assertions.h
@@ -36,7 +36,7 @@ class PreprocessingPassContext;
 namespace smt {
 
 class Assertions;
-struct SmtEngineStatistics;
+struct SolverEngineStatistics;
 
 /**
  * Module in charge of processing assertions for an SMT engine.
@@ -59,7 +59,7 @@ class ProcessAssertions : protected EnvObj
   typedef std::unordered_map<Node, bool> NodeToBoolHashMap;
 
  public:
-  ProcessAssertions(Env& env, SmtEngineStatistics& stats);
+  ProcessAssertions(Env& env, SolverEngineStatistics& stats);
   ~ProcessAssertions();
   /** Finish initialize
    *
@@ -81,7 +81,7 @@ class ProcessAssertions : protected EnvObj
 
  private:
   /** Reference to the SMT stats */
-  SmtEngineStatistics& d_smtStats;
+  SolverEngineStatistics& d_smtStats;
   /** The preprocess context */
   preprocessing::PreprocessingPassContext* d_preprocessingPassContext;
   /** True node */
diff --git a/src/smt/smt_engine_stats.cpp b/src/smt/smt_engine_stats.cpp
deleted file mode 100644
index c76a8a2e7..000000000
--- a/src/smt/smt_engine_stats.cpp
+++ /dev/null
@@ -1,47 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Tim King, Gereon Kremer, Andrew Reynolds
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * Implementation of statistics for SMT engine.
- */
-
-#include "smt/smt_engine_stats.h"
-
-#include "smt/smt_statistics_registry.h"
-
-namespace cvc5 {
-namespace smt {
-
-SmtEngineStatistics::SmtEngineStatistics(const std::string& name)
-    : d_definitionExpansionTime(smtStatisticsRegistry().registerTimer(
-        name + "definitionExpansionTime")),
-      d_numConstantProps(
-          smtStatisticsRegistry().registerInt(name + "numConstantProps")),
-      d_numAssertionsPre(smtStatisticsRegistry().registerInt(
-          name + "numAssertionsPreITERemoval")),
-      d_numAssertionsPost(smtStatisticsRegistry().registerInt(
-          name + "numAssertionsPostITERemoval")),
-      d_checkModelTime(
-          smtStatisticsRegistry().registerTimer(name + "checkModelTime")),
-      d_checkUnsatCoreTime(
-          smtStatisticsRegistry().registerTimer(name + "checkUnsatCoreTime")),
-      d_solveTime(smtStatisticsRegistry().registerTimer(name + "solveTime")),
-      d_pushPopTime(
-          smtStatisticsRegistry().registerTimer(name + "pushPopTime")),
-      d_processAssertionsTime(smtStatisticsRegistry().registerTimer(
-          name + "processAssertionsTime")),
-      d_simplifiedToFalse(
-          smtStatisticsRegistry().registerInt(name + "simplifiedToFalse"))
-{
-}
-
-}  // namespace smt
-}  // namespace cvc5
diff --git a/src/smt/smt_engine_stats.h b/src/smt/smt_engine_stats.h
deleted file mode 100644
index 31b479b5c..000000000
--- a/src/smt/smt_engine_stats.h
+++ /dev/null
@@ -1,55 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Morgan Deters, Andrew Reynolds, Gereon Kremer
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * Statistics for SMT engine.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__SMT__SMT_ENGINE_STATS_H
-#define CVC5__SMT__SMT_ENGINE_STATS_H
-
-#include "util/statistics_stats.h"
-
-namespace cvc5 {
-namespace smt {
-
-struct SmtEngineStatistics
-{
-  SmtEngineStatistics(const std::string& name = "smt::SolverEngine::");
-  /** time spent in definition-expansion */
-  TimerStat d_definitionExpansionTime;
-  /** number of constant propagations found during nonclausal simp */
-  IntStat d_numConstantProps;
-  /** Number of assertions before ite removal */
-  IntStat d_numAssertionsPre;
-  /** Number of assertions after ite removal */
-  IntStat d_numAssertionsPost;
-  /** time spent in checkModel() */
-  TimerStat d_checkModelTime;
-  /** time spent in checkUnsatCore() */
-  TimerStat d_checkUnsatCoreTime;
-  /** time spent in PropEngine::checkSat() */
-  TimerStat d_solveTime;
-  /** time spent in pushing/popping */
-  TimerStat d_pushPopTime;
-  /** time spent in processAssertions() */
-  TimerStat d_processAssertionsTime;
-
-  /** Has something simplified to false? */
-  IntStat d_simplifiedToFalse;
-}; /* struct SmtEngineStatistics */
-
-}  // namespace smt
-}  // namespace cvc5
-
-#endif /* CVC5__SMT__SMT_ENGINE_STATS_H */
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 0f98c5866..41f9a67b1 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -22,8 +22,8 @@
 #include "smt/env.h"
 #include "smt/preprocessor.h"
 #include "smt/smt_engine_state.h"
-#include "smt/smt_engine_stats.h"
 #include "smt/solver_engine.h"
+#include "smt/solver_engine_stats.h"
 #include "theory/logic_info.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_traits.h"
@@ -36,7 +36,7 @@ namespace smt {
 SmtSolver::SmtSolver(Env& env,
                      SmtEngineState& state,
                      AbstractValues& abs,
-                     SmtEngineStatistics& stats)
+                     SolverEngineStatistics& stats)
     : d_env(env),
       d_state(state),
       d_pp(env, abs, stats),
diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h
index 04093443e..83e591835 100644
--- a/src/smt/smt_solver.h
+++ b/src/smt/smt_solver.h
@@ -45,7 +45,7 @@ namespace smt {
 
 class Assertions;
 class SmtEngineState;
-struct SmtEngineStatistics;
+struct SolverEngineStatistics;
 
 /**
  * A solver for SMT queries.
@@ -67,7 +67,7 @@ class SmtSolver
   SmtSolver(Env& env,
             SmtEngineState& state,
             AbstractValues& abs,
-            SmtEngineStatistics& stats);
+            SolverEngineStatistics& stats);
   ~SmtSolver();
   /**
    * Create theory engine, prop engine based on the environment.
@@ -131,7 +131,7 @@ class SmtSolver
   /** The preprocessor of this SMT solver */
   Preprocessor d_pp;
   /** Reference to the statistics of SolverEngine */
-  SmtEngineStatistics& d_stats;
+  SolverEngineStatistics& d_stats;
   /** The theory engine */
   std::unique_ptr<TheoryEngine> d_theoryEngine;
   /** The propositional engine */
diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index 4c8ec4ff2..cefc59631 100644
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -54,9 +54,9 @@
 #include "smt/quant_elim_solver.h"
 #include "smt/set_defaults.h"
 #include "smt/smt_engine_state.h"
-#include "smt/smt_engine_stats.h"
 #include "smt/smt_solver.h"
 #include "smt/solver_engine_scope.h"
+#include "smt/solver_engine_stats.h"
 #include "smt/sygus_solver.h"
 #include "smt/unsat_core_manager.h"
 #include "theory/quantifiers/instantiation_list.h"
@@ -121,7 +121,7 @@ SolverEngine::SolverEngine(NodeManager* nm, const Options* optr)
   // listen to resource out
   getResourceManager()->registerListener(d_routListener.get());
   // make statistics
-  d_stats.reset(new SmtEngineStatistics());
+  d_stats.reset(new SolverEngineStatistics());
   // make the SMT solver
   d_smtSolver.reset(new SmtSolver(*d_env, *d_state, *d_absValues, *d_stats));
   // make the SyGuS solver
diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h
index 8ec0b15f3..c627a63d6 100644
--- a/src/smt/solver_engine.h
+++ b/src/smt/solver_engine.h
@@ -93,7 +93,7 @@ class AbductionSolver;
 class InterpolationSolver;
 class QuantElimSolver;
 
-struct SmtEngineStatistics;
+struct SolverEngineStatistics;
 class SolverEngineScope;
 class PfManager;
 class UnsatCoreManager;
@@ -1102,7 +1102,7 @@ class CVC5_EXPORT SolverEngine
   std::map<std::string, int> d_commandVerbosity;
 
   /** The statistics class */
-  std::unique_ptr<smt::SmtEngineStatistics> d_stats;
+  std::unique_ptr<smt::SolverEngineStatistics> d_stats;
 
   /** the output manager for commands */
   mutable OutputManager d_outMgr;
diff --git a/src/smt/solver_engine_stats.cpp b/src/smt/solver_engine_stats.cpp
new file mode 100644
index 000000000..645103327
--- /dev/null
+++ b/src/smt/solver_engine_stats.cpp
@@ -0,0 +1,47 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Tim King, Gereon Kremer, Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Implementation of statistics for SMT engine.
+ */
+
+#include "smt/solver_engine_stats.h"
+
+#include "smt/smt_statistics_registry.h"
+
+namespace cvc5 {
+namespace smt {
+
+SolverEngineStatistics::SolverEngineStatistics(const std::string& name)
+    : d_definitionExpansionTime(smtStatisticsRegistry().registerTimer(
+        name + "definitionExpansionTime")),
+      d_numConstantProps(
+          smtStatisticsRegistry().registerInt(name + "numConstantProps")),
+      d_numAssertionsPre(smtStatisticsRegistry().registerInt(
+          name + "numAssertionsPreITERemoval")),
+      d_numAssertionsPost(smtStatisticsRegistry().registerInt(
+          name + "numAssertionsPostITERemoval")),
+      d_checkModelTime(
+          smtStatisticsRegistry().registerTimer(name + "checkModelTime")),
+      d_checkUnsatCoreTime(
+          smtStatisticsRegistry().registerTimer(name + "checkUnsatCoreTime")),
+      d_solveTime(smtStatisticsRegistry().registerTimer(name + "solveTime")),
+      d_pushPopTime(
+          smtStatisticsRegistry().registerTimer(name + "pushPopTime")),
+      d_processAssertionsTime(smtStatisticsRegistry().registerTimer(
+          name + "processAssertionsTime")),
+      d_simplifiedToFalse(
+          smtStatisticsRegistry().registerInt(name + "simplifiedToFalse"))
+{
+}
+
+}  // namespace smt
+}  // namespace cvc5
diff --git a/src/smt/solver_engine_stats.h b/src/smt/solver_engine_stats.h
new file mode 100644
index 000000000..7701f7c07
--- /dev/null
+++ b/src/smt/solver_engine_stats.h
@@ -0,0 +1,55 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, Andrew Reynolds, Gereon Kremer
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Statistics for SMT engine.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__SMT__SOLVER_ENGINE_STATS_H
+#define CVC5__SMT__SOLVER_ENGINE_STATS_H
+
+#include "util/statistics_stats.h"
+
+namespace cvc5 {
+namespace smt {
+
+struct SolverEngineStatistics
+{
+  SolverEngineStatistics(const std::string& name = "smt::SolverEngine::");
+  /** time spent in definition-expansion */
+  TimerStat d_definitionExpansionTime;
+  /** number of constant propagations found during nonclausal simp */
+  IntStat d_numConstantProps;
+  /** Number of assertions before ite removal */
+  IntStat d_numAssertionsPre;
+  /** Number of assertions after ite removal */
+  IntStat d_numAssertionsPost;
+  /** time spent in checkModel() */
+  TimerStat d_checkModelTime;
+  /** time spent in checkUnsatCore() */
+  TimerStat d_checkUnsatCoreTime;
+  /** time spent in PropEngine::checkSat() */
+  TimerStat d_solveTime;
+  /** time spent in pushing/popping */
+  TimerStat d_pushPopTime;
+  /** time spent in processAssertions() */
+  TimerStat d_processAssertionsTime;
+
+  /** Has something simplified to false? */
+  IntStat d_simplifiedToFalse;
+}; /* struct SolverEngineStatistics */
+
+}  // namespace smt
+}  // namespace cvc5
+
+#endif /* CVC5__SMT__SMT_ENGINE_STATS_H */