From: Aina Niemetz 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 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 */