diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-02-15 09:08:47 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-15 09:08:47 +0100 |
commit | b05fae1fa9e46b63b22a41d8c32e944502366770 (patch) | |
tree | 3360088d27a19824cb276dc1cc63836c296b3321 | |
parent | 0ff53d70b3e0a11e4ae5c1c8f612d809dca2d004 (diff) |
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.
-rw-r--r-- | src/theory/arith/nl/nonlinear_extension.cpp | 11 | ||||
-rw-r--r-- | src/theory/arith/nl/nonlinear_extension.h | 5 | ||||
-rw-r--r-- | src/theory/arith/nl/stats.cpp | 5 | ||||
-rw-r--r-- | src/theory/arith/nl/stats.h | 2 |
4 files changed, 1 insertions, 22 deletions
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 |