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 709b1e7770bbf48aecf3b06ee896161f55184461..36ddecee97ce32e0574068f7c80ae8acdfe79f20 100644 (file)
--- 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 77031ee1cf386cbc9aef64d46013205032c49294..a6b68d644b08701aeaa857208d03d88876b1ece0 100644 (file)
--- 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 eb5804e6bee94670b5ad2576198520e088d7c4cb..ee12f941eee13078a1bdacfb988da6ba0d1afcf8 100644 (file)
--- 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 5d3dd845cfd7b319d9d3928a4b78e14b835f92d0..f869d83a43c95150211ad04229ef783326dfdd76 100644 (file)
--- 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