From 3783c06132f60c490fb40fd08ffd068f87729d2b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 5 Feb 2021 10:04:30 -0600 Subject: [PATCH] Miscellaneous cleaning in theory engine (#5854) This statistic is unused, I believe it is leftover from deleted code. --- src/theory/theory_engine.cpp | 6 +----- src/theory/theory_engine.h | 2 -- 2 files changed, 1 insertion(+), 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(true); d_false = NodeManager::currentNM()->mkConst(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 */ -- 2.30.2