Rename SmtEngineStatistics to SolverEngineStatistics. (#7339)
authorAina Niemetz <aina.niemetz@gmail.com>
Mon, 11 Oct 2021 23:21:32 +0000 (16:21 -0700)
committerGitHub <noreply@github.com>
Mon, 11 Oct 2021 23:21:32 +0000 (23:21 +0000)
16 files changed:
src/CMakeLists.txt
src/smt/env.cpp
src/smt/expand_definitions.cpp
src/smt/expand_definitions.h
src/smt/preprocessor.cpp
src/smt/preprocessor.h
src/smt/process_assertions.cpp
src/smt/process_assertions.h
src/smt/smt_engine_stats.cpp [deleted file]
src/smt/smt_engine_stats.h [deleted file]
src/smt/smt_solver.cpp
src/smt/smt_solver.h
src/smt/solver_engine.cpp
src/smt/solver_engine.h
src/smt/solver_engine_stats.cpp [new file with mode: 0644]
src/smt/solver_engine_stats.h [new file with mode: 0644]

index 61be39f97c2a451195476995d24cebc779764378..c00e92c8309f2193e65e8ee3be96bad267b9f298 100644 (file)
@@ -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
index f63747ebda52eca2d1dc19788f4f5522291093ff..9334732fe10ed639a92271e5b890d91b9d077922 100644 (file)
@@ -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"
index 3ee08848d44fff915970dd424ba465bdbfcbda84..12689678662cfdf6a22860b010ea2e861cc59ebd 100644 (file)
@@ -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)
 {
 }
index 997e973916261a276ddaf11b961b80c3ac6ae5a2..f36c1769fbaa28f8b405e37a06a6e43c7e879d05 100644 (file)
@@ -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;
 };
index bdf80718130542388b94477389b8193bc0e52ced..9312deb97f903221feb86e1c090eb70cf512d01b 100644 (file)
@@ -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),
index b455fb3ca6f7ab71891c71bb3b95436ca1fd4a44..40a84981aa9f6cbadecc2584a0477f31aacaad67 100644 (file)
@@ -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
index 73578f2cb94bcd4c214e2aa2ecba6ec29ea7dc49..8c4998e30cdffce1a67a2f9d070bab272d3a5250 100644 (file)
@@ -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);
index 00b57813f4193846d9eecb77d6775d4d88b6ead2..7f7ce9cca5c7f1adef489f086820a45652f6a84d 100644 (file)
@@ -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 (file)
index c76a8a2..0000000
+++ /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 (file)
index 31b479b..0000000
+++ /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 */
index 0f98c58664f7eab94fa438aede0cda6bfecb0c54..41f9a67b1f3109e95c1308a9f7a7d7227e45483b 100644 (file)
@@ -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),
index 04093443eeee398bdecf9e48a817f570365a311a..83e591835179701801d1cc5f18b2c34c9c8c9f40 100644 (file)
@@ -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 */
index 4c8ec4ff2f4b1ee076b76ceae950378306a124b2..cefc59631b0edbc4e1058f4a069afd3127a172c6 100644 (file)
@@ -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
index 8ec0b15f37c501f399335b487ed112826d4de6aa..c627a63d6b9cabf6c7fa0e2c3c223b62c16e409b 100644 (file)
@@ -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 (file)
index 0000000..6451033
--- /dev/null
@@ -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 (file)
index 0000000..7701f7c
--- /dev/null
@@ -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 */