summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/CMakeLists.txt4
-rw-r--r--src/smt/env.cpp2
-rw-r--r--src/smt/expand_definitions.cpp4
-rw-r--r--src/smt/expand_definitions.h6
-rw-r--r--src/smt/preprocessor.cpp2
-rw-r--r--src/smt/preprocessor.h2
-rw-r--r--src/smt/process_assertions.cpp4
-rw-r--r--src/smt/process_assertions.h6
-rw-r--r--src/smt/smt_solver.cpp4
-rw-r--r--src/smt/smt_solver.h6
-rw-r--r--src/smt/solver_engine.cpp4
-rw-r--r--src/smt/solver_engine.h4
-rw-r--r--src/smt/solver_engine_stats.cpp (renamed from src/smt/smt_engine_stats.cpp)4
-rw-r--r--src/smt/solver_engine_stats.h (renamed from src/smt/smt_engine_stats.h)10
14 files changed, 31 insertions, 31 deletions
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<TConvProofGenerator> 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<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_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<TheoryEngine> 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<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/smt_engine_stats.cpp b/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
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback