From: Andrew Reynolds Date: Fri, 5 Feb 2021 16:04:30 +0000 (-0600) Subject: Miscellaneous cleaning in theory engine (#5854) X-Git-Tag: cvc5-1.0.0~2319 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3783c06132f60c490fb40fd08ffd068f87729d2b;p=cvc5.git Miscellaneous cleaning in theory engine (#5854) This statistic is unused, I believe it is leftover from deleted code. --- 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 */