From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Mon, 15 Feb 2021 08:08:47 +0000 (+0100)
Subject: Remove now obsolete sendLemmas and inferences stat from arith::nl (#5903)
X-Git-Tag: cvc5-1.0.0~2278
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b05fae1fa9e46b63b22a41d8c32e944502366770;p=cvc5.git

Remove now obsolete sendLemmas and inferences stat from arith::nl (#5903)

This PR removes some obsolete code from the nonlinear solver.
The statistics will soon be replaced by a generic statistic in the theory inference manager.
---

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 709b1e777..36ddecee9 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -85,17 +85,6 @@ void NonlinearExtension::preRegisterTerm(TNode n)
   d_extTheory.registerTerm(n);
 }
 
-void NonlinearExtension::sendLemmas(const std::vector<NlLemma>& out)
-{
-  for (const NlLemma& nlem : out)
-  {
-    Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << nlem.getId()
-                          << " : " << nlem.d_node << std::endl;
-    d_im.addPendingArithLemma(nlem);
-    d_stats.d_inferences << nlem.getId();
-  }
-}
-
 void NonlinearExtension::processSideEffect(const NlLemma& se)
 {
   d_trSlv.processSideEffect(se);
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index 77031ee1c..a6b68d644 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -203,11 +203,6 @@ class NonlinearExtension
   /** singleton version of above */
   unsigned filterLemma(NlLemma lem, std::vector<NlLemma>& out);
 
-  /**
-   * Send lemmas in out on the output channel of theory of arithmetic.
-   */
-  void sendLemmas(const std::vector<NlLemma>& out);
-
   /** run check strategy
    *
    * Check assertions for consistency in the effort LAST_CALL with a subset of
diff --git a/src/theory/arith/nl/stats.cpp b/src/theory/arith/nl/stats.cpp
index eb5804e6b..ee12f941e 100644
--- a/src/theory/arith/nl/stats.cpp
+++ b/src/theory/arith/nl/stats.cpp
@@ -23,19 +23,16 @@ namespace nl {
 
 NlStats::NlStats()
     : d_mbrRuns("nl::mbrRuns", 0),
-      d_checkRuns("nl::checkRuns", 0),
-      d_inferences("nl::inferences")
+      d_checkRuns("nl::checkRuns", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_mbrRuns);
   smtStatisticsRegistry()->registerStat(&d_checkRuns);
-  smtStatisticsRegistry()->registerStat(&d_inferences);
 }
 
 NlStats::~NlStats()
 {
   smtStatisticsRegistry()->unregisterStat(&d_mbrRuns);
   smtStatisticsRegistry()->unregisterStat(&d_checkRuns);
-  smtStatisticsRegistry()->unregisterStat(&d_inferences);
 }
 
 }  // namespace nl
diff --git a/src/theory/arith/nl/stats.h b/src/theory/arith/nl/stats.h
index 5d3dd845c..f869d83a4 100644
--- a/src/theory/arith/nl/stats.h
+++ b/src/theory/arith/nl/stats.h
@@ -41,8 +41,6 @@ class NlStats
   IntStat d_mbrRuns;
   /** Number of calls to NonlinearExtension::checkLastCall */
   IntStat d_checkRuns;
-  /** Counts the number of applications of each type of inference */
-  HistogramStat<InferenceId> d_inferences;
 };
 
 }  // namespace nl