From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 12 Oct 2021 18:09:22 +0000 (-0700)
Subject: Get rid of unused member d_smtStats in ExpandDefs. (#7346)
X-Git-Tag: cvc5-1.0.0~1077
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=08d3d5bb9ea5164fd21764ddce445ee73bb56401;p=cvc5.git

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 126896786..54aba6b71 100644
--- 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 f36c1769f..8ecf276e2 100644
--- 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 9312deb97..4b16b9391 100644
--- 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 8c4998e30..e522b45dd 100644
--- 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 7f7ce9cca..84c5d1d43 100644
--- 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 */