From 18e52361a8109c62de3636b3a261b25e3991734b Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 11 Oct 2021 16:21:32 -0700 Subject: [PATCH] Rename SmtEngineStatistics to SolverEngineStatistics. (#7339) --- src/CMakeLists.txt | 4 ++-- src/smt/env.cpp | 2 +- src/smt/expand_definitions.cpp | 4 ++-- src/smt/expand_definitions.h | 6 +++--- src/smt/preprocessor.cpp | 2 +- src/smt/preprocessor.h | 2 +- src/smt/process_assertions.cpp | 4 ++-- src/smt/process_assertions.h | 6 +++--- src/smt/smt_solver.cpp | 4 ++-- src/smt/smt_solver.h | 6 +++--- src/smt/solver_engine.cpp | 4 ++-- src/smt/solver_engine.h | 4 ++-- .../{smt_engine_stats.cpp => solver_engine_stats.cpp} | 4 ++-- src/smt/{smt_engine_stats.h => solver_engine_stats.h} | 10 +++++----- 14 files changed, 31 insertions(+), 31 deletions(-) rename src/smt/{smt_engine_stats.cpp => solver_engine_stats.cpp} (94%) rename src/smt/{smt_engine_stats.h => solver_engine_stats.h} (87%) 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 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 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_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 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 d_commandVerbosity; /** The statistics class */ - std::unique_ptr d_stats; + std::unique_ptr d_stats; /** the output manager for commands */ mutable OutputManager d_outMgr; diff --git a/src/smt/smt_engine_stats.cpp b/src/smt/solver_engine_stats.cpp similarity index 94% rename from src/smt/smt_engine_stats.cpp rename to src/smt/solver_engine_stats.cpp index c76a8a2e7..645103327 100644 --- a/src/smt/smt_engine_stats.cpp +++ b/src/smt/solver_engine_stats.cpp @@ -13,14 +13,14 @@ * Implementation of statistics for SMT engine. */ -#include "smt/smt_engine_stats.h" +#include "smt/solver_engine_stats.h" #include "smt/smt_statistics_registry.h" namespace cvc5 { namespace smt { -SmtEngineStatistics::SmtEngineStatistics(const std::string& name) +SolverEngineStatistics::SolverEngineStatistics(const std::string& name) : d_definitionExpansionTime(smtStatisticsRegistry().registerTimer( name + "definitionExpansionTime")), d_numConstantProps( diff --git a/src/smt/smt_engine_stats.h b/src/smt/solver_engine_stats.h similarity index 87% rename from src/smt/smt_engine_stats.h rename to src/smt/solver_engine_stats.h index 31b479b5c..7701f7c07 100644 --- a/src/smt/smt_engine_stats.h +++ b/src/smt/solver_engine_stats.h @@ -15,17 +15,17 @@ #include "cvc5_private.h" -#ifndef CVC5__SMT__SMT_ENGINE_STATS_H -#define CVC5__SMT__SMT_ENGINE_STATS_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 SmtEngineStatistics +struct SolverEngineStatistics { - SmtEngineStatistics(const std::string& name = "smt::SolverEngine::"); + SolverEngineStatistics(const std::string& name = "smt::SolverEngine::"); /** time spent in definition-expansion */ TimerStat d_definitionExpansionTime; /** number of constant propagations found during nonclausal simp */ @@ -47,7 +47,7 @@ struct SmtEngineStatistics /** Has something simplified to false? */ IntStat d_simplifiedToFalse; -}; /* struct SmtEngineStatistics */ +}; /* struct SolverEngineStatistics */ } // namespace smt } // namespace cvc5 -- 2.30.2