diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-11 22:54:50 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-11 22:54:50 -0600 |
| commit | a49efc8c32020b7c2285fa744ae61a576801c51d (patch) | |
| tree | e261da599172d1bc767da066e25e15b9cf4eaec5 /src/smt | |
| parent | 107b1422f9549eb2128729c3fd173441029ba443 (diff) | |
Flush statistics through NodeManager in SmtEngine (#5652)
This removes the dependency on the Expr layer from src/main.
This requires moving the flushing of NodeManager statistics within SmtEngine.
This is a temporary solution until we have a permanent solution for statistics.
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 10 | ||||
| -rw-r--r-- | src/smt/smt_engine.h | 8 |
2 files changed, 16 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 81294722f..b1f56ea37 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1765,7 +1765,15 @@ SExpr SmtEngine::getStatistic(std::string name) const return d_statisticsRegistry->getStatistic(name); } -void SmtEngine::safeFlushStatistics(int fd) const { +void SmtEngine::flushStatistics(std::ostream& out) const +{ + d_nodeManager->getStatisticsRegistry()->flushInformation(out); + d_statisticsRegistry->flushInformation(out); +} + +void SmtEngine::safeFlushStatistics(int fd) const +{ + d_nodeManager->getStatisticsRegistry()->safeFlushInformation(fd); d_statisticsRegistry->safeFlushInformation(fd); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index bce086202..f8a74597b 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -801,7 +801,13 @@ class CVC4_PUBLIC SmtEngine /** Get the value of one named statistic from this SmtEngine. */ SExpr getStatistic(std::string name) const; - /** Flush statistic from this SmtEngine. Safe to use in a signal handler. */ + /** Flush statistics from this SmtEngine and the NodeManager it uses. */ + void flushStatistics(std::ostream& out) const; + + /** + * Flush statistics from this SmtEngine and the NodeManager it uses. Safe to + * use in a signal handler. + */ void safeFlushStatistics(int fd) const; /** |