diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-22 21:10:51 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-22 21:10:51 +0000 |
commit | e2611a54c5479086df0c4a80f56597aae80b5c4e (patch) | |
tree | b0d98600bd70147f28197883d3481614b87d76f6 /src/smt/smt_engine.h | |
parent | 8b106b77c11d12d16abac845ed704845ef888bd2 (diff) |
Separate public-facing and internal-facing interfaces to Statistics.
The external interface (e.g., what's answered by ExprManager::getStatistics() and SmtEngine::getStatistics()) is a snapshot of the current statistics (rather than a reference to the actual StatisticsRegistry).
The StatisticsRegistry is now internal-only. However, it's built as a convenience library so that the parser and driver can use it too (by re-linking against it).
This is part of the ongoing effort to clean up the public interface.
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/smt/smt_engine.h')
-rw-r--r-- | src/smt/smt_engine.h | 44 |
1 files changed, 16 insertions, 28 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 2fa60104c..cbb97f9f7 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -35,7 +35,7 @@ #include "options/options.h" #include "util/result.h" #include "util/sexpr.h" -#include "util/stats.h" +#include "util/statistics.h" #include "theory/logic_info.h" // In terms of abstraction, this is below (and provides services to) @@ -51,6 +51,7 @@ class NodeHashFunction; class Command; +class SmtEngine; class DecisionEngine; class TheoryEngine; @@ -74,6 +75,7 @@ namespace smt { */ class DefinedFunction; + class SmtEngineStatistics; class SmtEnginePrivate; class SmtScope; @@ -83,6 +85,10 @@ namespace smt { typedef context::CDList<Command*, CommandCleanup> CommandList; }/* CVC4::smt namespace */ +namespace stats { + StatisticsRegistry* getStatisticsRegistry(SmtEngine*); +}/* CVC4::stats namespace */ + // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the // hood): use a type parameter and have check() delegate, or subclass // SmtEngine and override check()? @@ -273,6 +279,7 @@ class CVC4_PUBLIC SmtEngine { friend class ::CVC4::smt::SmtEnginePrivate; friend class ::CVC4::smt::SmtScope; + friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(SmtEngine*); friend void ::CVC4::smt::beforeSearch(std::string, bool, SmtEngine*) throw(ModalException); // to access d_modelCommands friend size_t ::CVC4::Model::getNumCommands() const; @@ -280,31 +287,7 @@ class CVC4_PUBLIC SmtEngine { StatisticsRegistry* d_statisticsRegistry; - // === STATISTICS === - /** time spent in definition-expansion */ - TimerStat d_definitionExpansionTime; - /** time spent in non-clausal simplification */ - TimerStat d_nonclausalSimplificationTime; - /** Num of constant propagations found during nonclausal simp */ - IntStat d_numConstantProps; - /** time spent in static learning */ - TimerStat d_staticLearningTime; - /** time spent in simplifying ITEs */ - TimerStat d_simpITETime; - /** time spent in simplifying ITEs */ - TimerStat d_unconstrainedSimpTime; - /** time spent removing ITEs */ - TimerStat d_iteRemovalTime; - /** time spent in theory preprocessing */ - TimerStat d_theoryPreprocessTime; - /** time spent converting to CNF */ - TimerStat d_cnfConversionTime; - /** Num of assertions before ite removal */ - IntStat d_numAssertionsPre; - /** Num of assertions after ite removal */ - IntStat d_numAssertionsPost; - /** time spent in checkModel() */ - TimerStat d_checkModelTime; + smt::SmtEngineStatistics* d_stats; /** * Add to Model command. This is used for recording a command that should be reported @@ -567,9 +550,14 @@ public: } /** - * Permit access to the underlying StatisticsRegistry. + * Export statistics from this SmtEngine. + */ + Statistics getStatistics() const throw(); + + /** + * Get the value of one named statistic from this SmtEngine. */ - StatisticsRegistry* getStatisticsRegistry() const; + SExpr getStatistic(std::string name) const throw(); Result getStatusOfLastCommand() const { return d_status; |