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/smt_engine.h | |
| 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/smt_engine.h')
| -rw-r--r-- | src/smt/smt_engine.h | 8 |
1 files changed, 7 insertions, 1 deletions
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; /** |