Get rid of unused member d_smtStats in ExpandDefs. (#7346)

This further renames d_smtStats to d_slvStats in ProcessAssertions.

diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp
index 12689678662cfdf6a22860b010ea2e861cc59ebd..54aba6b71dbc6319e06d145ffb99e0319473638f 100644 (file)
--- a/src/smt/expand_definitions.cpp
+++ b/src/smt/expand_definitions.cpp
@@ -23,7 +23,6 @@
 #include "proof/conv_proof_generator.h"
 #include "smt/env.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,10 +34,7 @@ using namespace cvc5::kind;
 namespace cvc5 {
 namespace smt {
 
-ExpandDefs::ExpandDefs(Env& env, SolverEngineStatistics& stats)
-    : d_env(env), d_smtStats(stats), d_tpg(nullptr)
-{
-}
+ExpandDefs::ExpandDefs(Env& env) : d_env(env), d_tpg(nullptr) {}
 
 ExpandDefs::~ExpandDefs() {}
 

diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h
index f36c1769fbaa28f8b405e37a06a6e43c7e879d05..8ecf276e245c529264964db639516cd1cf3bb7e3 100644 (file)
--- a/src/smt/expand_definitions.h
+++ b/src/smt/expand_definitions.h
@@ -31,8 +31,6 @@ class TConvProofGenerator;
 
 namespace smt {
 
-struct SolverEngineStatistics;
-
 /**
  * Module in charge of expanding definitions for an SMT engine.
  *
@@ -42,7 +40,7 @@ struct SolverEngineStatistics;
 class ExpandDefs
 {
  public:
-  ExpandDefs(Env& env, SolverEngineStatistics& stats);
+  ExpandDefs(Env& env);
   ~ExpandDefs();
   /**
    * Expand definitions in term n. Return the expanded form of n.
@@ -69,8 +67,6 @@ class ExpandDefs
                               TConvProofGenerator* tpg);
   /** Reference to the environment. */
   Env& d_env;
-  /** Reference to the SMT stats */
-  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 9312deb97f903221feb86e1c090eb70cf512d01b..4b16b93910ea487ad5f5f207f29fa0ac326613c1 100644 (file)
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -42,7 +42,7 @@ Preprocessor::Preprocessor(Env& env,
       d_absValues(abs),
       d_propagator(true, true),
       d_assertionsProcessed(env.getUserContext(), false),
-      d_exDefs(env, stats),
+      d_exDefs(env),
       d_processor(env, stats),
       d_pnm(nullptr)
 {

diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 8c4998e30cdffce1a67a2f9d070bab272d3a5250..e522b45ddcaf1892fba15edef734da435a017c93 100644 (file)
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -58,7 +58,7 @@ class ScopeCounter
 };
 
 ProcessAssertions::ProcessAssertions(Env& env, SolverEngineStatistics& stats)
-    : EnvObj(env), d_smtStats(stats), d_preprocessingPassContext(nullptr)
+    : EnvObj(env), d_slvStats(stats), d_preprocessingPassContext(nullptr)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
 }
@@ -268,7 +268,7 @@ bool ProcessAssertions::apply(Assertions& as)
   noConflict = simplifyAssertions(as);
   if (!noConflict)
   {
-    ++(d_smtStats.d_simplifiedToFalse);
+    ++(d_slvStats.d_simplifiedToFalse);
   }
   Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-simplify"
                     << endl;
@@ -287,13 +287,13 @@ bool ProcessAssertions::apply(Assertions& as)
 
   if (options().smt.earlyIteRemoval)
   {
-    d_smtStats.d_numAssertionsPre += assertions.size();
+    d_slvStats.d_numAssertionsPre += assertions.size();
     d_passes["ite-removal"]->apply(&assertions);
     // This is needed because when solving incrementally, removeITEs may
     // introduce skolems that were solved for earlier and thus appear in the
     // substitution map.
     d_passes["apply-substs"]->apply(&assertions);
-    d_smtStats.d_numAssertionsPost += assertions.size();
+    d_slvStats.d_numAssertionsPost += assertions.size();
   }
 
   dumpAssertions("pre-repeat-simplify", as);

diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h
index 7f7ce9cca5c7f1adef489f086820a45652f6a84d..84c5d1d43726cb9a3f0b261dee889b47ae2e9fdb 100644 (file)
--- a/src/smt/process_assertions.h
+++ b/src/smt/process_assertions.h
@@ -81,7 +81,7 @@ class ProcessAssertions : protected EnvObj
 
  private:
   /** Reference to the SMT stats */
-  SolverEngineStatistics& d_smtStats;
+  SolverEngineStatistics& d_slvStats;
   /** The preprocess context */
   preprocessing::PreprocessingPassContext* d_preprocessingPassContext;
   /** True node */