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/main/driver_unified.cpp | |
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/main/driver_unified.cpp')
-rw-r--r-- | src/main/driver_unified.cpp | 48 |
1 files changed, 24 insertions, 24 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 0c6496053..e2b1c21f0 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -20,6 +20,7 @@ #include <fstream> #include <iostream> #include <new> +#include <unistd.h> #include <stdio.h> #include <unistd.h> @@ -45,7 +46,6 @@ #include "util/output.h" #include "util/dump.h" #include "util/result.h" -#include "util/stats.h" using namespace std; using namespace CVC4; @@ -63,10 +63,11 @@ namespace CVC4 { /** Just the basename component of argv[0] */ const char *progName; - /** A pointer to the StatisticsRegistry (the signal handlers need it) */ - CVC4::StatisticsRegistry* pStatistics; - } -} + /** A pointer to the CommandExecutor (the signal handlers need it) */ + CVC4::main::CommandExecutor* pExecutor; + + }/* CVC4::main namespace */ +}/* CVC4 namespace */ void printUsage(Options& opts, bool full) { @@ -185,20 +186,18 @@ int runCvc4(int argc, char* argv[], Options& opts) { # ifndef PORTFOLIO_BUILD ExprManager exprMgr(opts); # else - vector<Options> threadOpts = parseThreadSpecificOptions(opts); + vector<Options> threadOpts = parseThreadSpecificOptions(opts); ExprManager exprMgr(threadOpts[0]); # endif - CommandExecutor* cmdExecutor = # ifndef PORTFOLIO_BUILD - new CommandExecutor(exprMgr, opts); + CommandExecutor cmdExecutor(exprMgr, opts); # else - new CommandExecutorPortfolio(exprMgr, opts, threadOpts); -#endif + CommandExecutorPortfolio cmdExecutor(exprMgr, opts, threadOpts); +# endif - // Create the SmtEngine - StatisticsRegistry driverStats("driver"); - pStatistics->registerStat_(&driverStats); + // give access to the signal handlers for stats output + pExecutor = &cmdExecutor; Parser* replayParser = NULL; if( opts[options::replayFilename] != "" ) { @@ -218,11 +217,11 @@ int runCvc4(int argc, char* argv[], Options& opts) { } // Timer statistic - RegisterStatistic statTotalTime(&driverStats, &s_totalTime); + RegisterStatistic statTotalTime(&cmdExecutor.getStatisticsRegistry(), &s_totalTime); // Filename statistics ReferenceStat< const char* > s_statFilename("filename", filename); - RegisterStatistic statFilenameReg(&driverStats, &s_statFilename); + RegisterStatistic statFilenameReg(&cmdExecutor.getStatisticsRegistry(), &s_statFilename); // Parse and execute commands until we are done Command* cmd; @@ -243,7 +242,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { replayParser->useDeclarationsFrom(shell.getParser()); } while((cmd = shell.readCommand())) { - status = cmdExecutor->doCommand(cmd) && status; + status = cmdExecutor.doCommand(cmd) && status; delete cmd; } } else { @@ -267,7 +266,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { delete cmd; break; } - status = cmdExecutor->doCommand(cmd); + status = cmdExecutor.doCommand(cmd); delete cmd; } // Remove the parser @@ -283,7 +282,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { int returnValue; string result = "unknown"; if(status) { - result = cmdExecutor->getSmtEngineStatus(); + result = cmdExecutor.getSmtEngineStatus(); if(result == "sat") { returnValue = 10; @@ -298,19 +297,20 @@ int runCvc4(int argc, char* argv[], Options& opts) { } #ifdef CVC4_COMPETITION_MODE - // exit, don't return - // (don't want destructors to run) - exit(returnValue); + // exit, don't return (don't want destructors to run) + // _exit() from unistd.h doesn't run global destructors + // or other on_exit/atexit stuff. + _exit(returnValue); #endif /* CVC4_COMPETITION_MODE */ ReferenceStat< Result > s_statSatResult("sat/unsat", result); - RegisterStatistic statSatResultReg(&driverStats, &s_statSatResult); + RegisterStatistic statSatResultReg(&cmdExecutor.getStatisticsRegistry(), &s_statSatResult); s_totalTime.stop(); if(opts[options::statistics]) { - pStatistics->flushInformation(*opts[options::err]); + cmdExecutor.flushStatistics(*opts[options::err]); } - exit(returnValue); + pExecutor = NULL; return returnValue; } |