diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-05 10:04:30 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-05 10:04:30 -0600 |
| commit | 3783c06132f60c490fb40fd08ffd068f87729d2b (patch) | |
| tree | 612bceda2064f34c101b8ac136165e457124050f /src/theory | |
| parent | 7ee5ed0feaaf524237d5e4632948aaa3f1ec3fb6 (diff) | |
Miscellaneous cleaning in theory engine (#5854)
This statistic is unused, I believe it is leftover from deleted code.
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/theory_engine.cpp | 6 | ||||
| -rw-r--r-- | src/theory/theory_engine.h | 2 |
2 files changed, 1 insertions, 7 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 9fb76ab44..0fd8347c8 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -242,8 +242,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_resourceManager(rm), d_inPreregister(false), d_factsAsserted(context, false), - d_attr_handle(), - d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0) + d_attr_handle() { for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) @@ -255,8 +254,6 @@ TheoryEngine::TheoryEngine(context::Context* context, smtStatisticsRegistry()->registerStat(&d_combineTheoriesTime); d_true = NodeManager::currentNM()->mkConst<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(false); - - smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded); } TheoryEngine::~TheoryEngine() { @@ -270,7 +267,6 @@ TheoryEngine::~TheoryEngine() { } smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime); - smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded); } void TheoryEngine::interrupt() { d_interrupted = true; } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index d72a999b2..e2e7850b5 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -671,8 +671,6 @@ private: * This function is called from the smt engine's checkModel routine. */ void checkTheoryAssertionsWithModel(bool hardFailure); - private: - IntStat d_arithSubstitutionsAdded; };/* class TheoryEngine */ }/* CVC4 namespace */ |