diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/api/cvc4cpp.cpp | 6 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 4 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 7 | ||||
-rw-r--r-- | src/expr/node_manager.h | 9 | ||||
-rw-r--r-- | src/main/command_executor.cpp | 8 | ||||
-rw-r--r-- | src/main/command_executor.h | 8 | ||||
-rw-r--r-- | src/main/driver_unified.cpp | 34 | ||||
-rw-r--r-- | src/main/main.cpp | 2 | ||||
-rw-r--r-- | src/main/main.h | 6 | ||||
-rw-r--r-- | src/main/signal_handlers.cpp | 5 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 23 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 11 | ||||
-rw-r--r-- | src/smt/smt_engine_stats.cpp | 11 | ||||
-rw-r--r-- | src/smt/smt_engine_stats.h | 7 |
14 files changed, 53 insertions, 88 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index e87e6176b..dce190460 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -4040,9 +4040,9 @@ Solver::Solver(Options* opts) d_rng.reset(new Random(o[options::seed])); #if CVC4_STATISTICS_ON d_stats.reset(new Statistics()); - d_nodeMgr->getStatisticsRegistry()->registerStat(&d_stats->d_consts); - d_nodeMgr->getStatisticsRegistry()->registerStat(&d_stats->d_vars); - d_nodeMgr->getStatisticsRegistry()->registerStat(&d_stats->d_terms); + d_smtEngine->getStatisticsRegistry()->registerStat(&d_stats->d_consts); + d_smtEngine->getStatisticsRegistry()->registerStat(&d_stats->d_vars); + d_smtEngine->getStatisticsRegistry()->registerStat(&d_stats->d_terms); #endif } diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 2d2b8a2e5..a176744ef 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -3687,12 +3687,12 @@ class CVC4_EXPORT Solver /** The node manager of this solver. */ std::unique_ptr<NodeManager> d_nodeMgr; + /** The statistics collected on the Api level. */ + std::unique_ptr<Statistics> d_stats; /** The SMT engine of this solver. */ std::unique_ptr<SmtEngine> d_smtEngine; /** The random number generator of this solver. */ std::unique_ptr<Random> d_rng; - /** The statistics collected on the Api level. */ - std::unique_ptr<Statistics> d_stats; }; } // namespace api diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index fdd7e5f5a..599d3e8f7 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -18,6 +18,7 @@ #include "expr/node_manager.h" #include <algorithm> +#include <sstream> #include <stack> #include <utility> @@ -32,7 +33,6 @@ #include "expr/skolem_manager.h" #include "expr/type_checker.h" #include "util/resource_manager.h" -#include "util/statistics_registry.h" using namespace std; using namespace CVC4::expr; @@ -93,8 +93,7 @@ namespace attr { typedef expr::Attribute<attr::LambdaBoundVarListTag, Node> LambdaBoundVarListAttr; NodeManager::NodeManager() - : d_statisticsRegistry(new StatisticsRegistry()), - d_skManager(new SkolemManager), + : d_skManager(new SkolemManager), d_bvManager(new BoundVarManager), next_id(0), d_attrManager(new expr::attr::AttributeManager()), @@ -264,8 +263,6 @@ NodeManager::~NodeManager() { } // defensive coding, in case destruction-order issues pop up (they often do) - delete d_statisticsRegistry; - d_statisticsRegistry = NULL; delete d_attrManager; d_attrManager = NULL; } diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 348200b6e..ce89f5dc6 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -41,7 +41,6 @@ namespace api { class Solver; } -class StatisticsRegistry; class ResourceManager; class SkolemManager; class BoundVarManager; @@ -116,8 +115,6 @@ class NodeManager static thread_local NodeManager* s_current; - StatisticsRegistry* d_statisticsRegistry; - /** The skolem manager */ std::unique_ptr<SkolemManager> d_skManager; /** The bound variable manager */ @@ -390,12 +387,6 @@ class NodeManager /** Get this node manager's bound variable manager */ BoundVarManager* getBoundVarManager() { return d_bvManager.get(); } - /** Get this node manager's statistics registry */ - StatisticsRegistry* getStatisticsRegistry() const - { - return d_statisticsRegistry; - } - /** Subscribe to NodeManager events */ void subscribeEvents(NodeManagerListener* listener) { Assert(std::find(d_listeners.begin(), d_listeners.end(), listener) diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index a343b4a37..551880b98 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -50,9 +50,7 @@ void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString CommandExecutor::CommandExecutor(Options& options) : d_solver(new api::Solver(&options)), d_symman(new SymbolManager(d_solver.get())), - d_smtEngine(d_solver->getSmtEngine()), d_options(options), - d_stats(), d_result() { } @@ -66,15 +64,13 @@ CommandExecutor::~CommandExecutor() void CommandExecutor::flushStatistics(std::ostream& out) const { // SmtEngine + node manager flush statistics is part of the call below - d_smtEngine->flushStatistics(out); - d_stats.flushInformation(out); + getSmtEngine()->flushStatistics(out); } void CommandExecutor::safeFlushStatistics(int fd) const { // SmtEngine + node manager flush statistics is part of the call below - d_smtEngine->safeFlushStatistics(fd); - d_stats.safeFlushInformation(fd); + getSmtEngine()->safeFlushStatistics(fd); } bool CommandExecutor::doCommand(Command* cmd) diff --git a/src/main/command_executor.h b/src/main/command_executor.h index 48761b7ad..0dea41383 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -52,9 +52,7 @@ class CommandExecutor * symbol manager. */ std::unique_ptr<SymbolManager> d_symman; - SmtEngine* d_smtEngine; Options& d_options; - StatisticsRegistry d_stats; api::Result d_result; public: @@ -82,11 +80,7 @@ class CommandExecutor api::Result getResult() const { return d_result; } void reset(); - StatisticsRegistry& getStatisticsRegistry() { - return d_stats; - } - - SmtEngine* getSmtEngine() { return d_smtEngine; } + SmtEngine* getSmtEngine() const { return d_solver->getSmtEngine(); } /** * Flushes statistics to a file descriptor. diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 846bef5be..d2b676e82 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -15,6 +15,7 @@ #include <stdio.h> #include <unistd.h> +#include <chrono> #include <cstdlib> #include <cstring> #include <fstream> @@ -38,7 +39,6 @@ #include "parser/parser_builder.h" #include "smt/command.h" #include "util/result.h" -#include "util/statistics_registry.h" using namespace std; using namespace CVC4; @@ -59,9 +59,6 @@ namespace CVC4 { /** A pointer to the CommandExecutor (the signal handlers need it) */ CVC4::main::CommandExecutor* pExecutor = nullptr; - /** A pointer to the totalTime driver stat (the signal handlers need it) */ - CVC4::TimerStat* pTotalTime = nullptr; - }/* CVC4::main namespace */ }/* CVC4 namespace */ @@ -82,10 +79,7 @@ void printUsage(Options& opts, bool full) { int runCvc4(int argc, char* argv[], Options& opts) { - // Timer statistic - pTotalTime = new TimerStat("driver::totalTime"); - pTotalTime->start(); - + std::chrono::time_point totalTimeStart = std::chrono::steady_clock::now(); // For the signal handlers' benefit pOptions = &opts; @@ -186,14 +180,6 @@ int runCvc4(int argc, char* argv[], Options& opts) { int returnValue = 0; { - // Timer statistic - RegisterStatistic statTotalTime(&pExecutor->getStatisticsRegistry(), - pTotalTime); - - // Filename statistics - ReferenceStat<std::string> s_statFilename("driver::filename", filenameStr); - RegisterStatistic statFilenameReg(&pExecutor->getStatisticsRegistry(), - &s_statFilename); // notify SmtEngine that we are starting to parse pExecutor->getSmtEngine()->notifyStartParsing(filenameStr); @@ -471,16 +457,10 @@ int runCvc4(int argc, char* argv[], Options& opts) { // or other on_exit/atexit stuff. _exit(returnValue); #endif /* CVC4_COMPETITION_MODE */ + pExecutor->getSmtEngine()->setResultStatistic(result.toString()); + std::chrono::duration totalTime = std::chrono::steady_clock::now() - totalTimeStart; + pExecutor->getSmtEngine()->setTotalTimeStatistic(std::chrono::duration<double>(totalTime).count()); - ReferenceStat<api::Result> s_statSatResult("driver::sat/unsat", result); - RegisterStatistic statSatResultReg(&pExecutor->getStatisticsRegistry(), - &s_statSatResult); - - pTotalTime->stop(); - - // Tim: I think that following comment is out of date? - // Set the global executor pointer to nullptr first. If we get a - // signal while dumping statistics, we don't want to try again. pExecutor->flushOutputStreams(); #ifdef CVC4_DEBUG @@ -494,12 +474,8 @@ int runCvc4(int argc, char* argv[], Options& opts) { #endif /* CVC4_DEBUG */ } - // On exceptional exit, these are leaked, but that's okay... they - // need to be around in that case for main() to print statistics. - delete pTotalTime; delete pExecutor; - pTotalTime = nullptr; pExecutor = nullptr; signal_handlers::cleanup(); diff --git a/src/main/main.cpp b/src/main/main.cpp index 7e0ed1e83..eb313c3bd 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -32,7 +32,6 @@ #include "parser/parser_builder.h" #include "parser/parser_exception.h" #include "util/result.h" -#include "util/statistics.h" using namespace std; using namespace CVC4; @@ -68,7 +67,6 @@ int main(int argc, char* argv[]) { *opts.getErr() << "(error \"" << e << "\")" << endl; } if(opts.getStatistics() && pExecutor != NULL) { - pTotalTime->stop(); pExecutor->flushStatistics(*opts.getErr()); } } diff --git a/src/main/main.h b/src/main/main.h index 37430b507..b769bee7d 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -20,9 +20,6 @@ #include "base/exception.h" #include "cvc4autoconfig.h" #include "options/options.h" -#include "util/statistics.h" -#include "util/statistics_registry.h" -#include "util/stats_timer.h" #ifndef CVC4__MAIN__MAIN_H #define CVC4__MAIN__MAIN_H @@ -41,9 +38,6 @@ extern const std::string* progName; /** A reference for use by the signal handlers to print statistics */ extern CVC4::main::CommandExecutor* pExecutor; -/** A reference for use by the signal handlers to print statistics */ -extern CVC4::TimerStat* pTotalTime; - /** * If true, will not spin on segfault even when CVC4_DEBUG is on. * Useful for nightly regressions, noninteractive performance runs diff --git a/src/main/signal_handlers.cpp b/src/main/signal_handlers.cpp index f3f32c4cd..ccd6c0b19 100644 --- a/src/main/signal_handlers.cpp +++ b/src/main/signal_handlers.cpp @@ -40,7 +40,6 @@ #include "options/options.h" #include "smt/smt_engine.h" #include "util/safe_print.h" -#include "util/statistics.h" using CVC4::Exception; using namespace std; @@ -61,10 +60,6 @@ void print_statistics() { if (pOptions != NULL && pOptions->getStatistics() && pExecutor != NULL) { - if (pTotalTime != NULL && pTotalTime->running()) - { - pTotalTime->stop(); - } pExecutor->safeFlushStatistics(STDERR_FILENO); } } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8ec594faa..a5da782d0 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -410,9 +410,10 @@ LogicInfo SmtEngine::getUserLogicInfo() const return res; } -void SmtEngine::notifyStartParsing(std::string filename) +void SmtEngine::notifyStartParsing(const std::string& filename) { d_state->setFilename(filename); + d_stats->d_driverFilename.set(filename); // Copy the original options. This is called prior to beginning parsing. // Hence reset should revert to these options, which note is after reading // the command line. @@ -423,6 +424,15 @@ const std::string& SmtEngine::getFilename() const { return d_state->getFilename(); } + +void SmtEngine::setResultStatistic(const std::string& result) { + d_stats->d_driverResult.set(result); +} + +void SmtEngine::setTotalTimeStatistic(double seconds) { + d_stats->d_driverTotalTime.set(seconds); +} + void SmtEngine::setLogicInternal() { Assert(!d_state->isFullyInited()) @@ -508,15 +518,6 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const if (key == "all-statistics") { vector<SExpr> stats; - StatisticsRegistry* sr = getNodeManager()->getStatisticsRegistry(); - for (StatisticsRegistry::const_iterator i = sr->begin(); i != sr->end(); - ++i) - { - vector<SExpr> v; - v.push_back((*i).first); - v.push_back((*i).second); - stats.push_back(v); - } for (StatisticsRegistry::const_iterator i = d_env->getStatisticsRegistry()->begin(); i != d_env->getStatisticsRegistry()->end(); ++i) @@ -1896,13 +1897,11 @@ SExpr SmtEngine::getStatistic(std::string name) const void SmtEngine::flushStatistics(std::ostream& out) const { - getNodeManager()->getStatisticsRegistry()->flushInformation(out); d_env->getStatisticsRegistry()->flushInformation(out); } void SmtEngine::safeFlushStatistics(int fd) const { - getNodeManager()->getStatisticsRegistry()->safeFlushInformation(fd); d_env->getStatisticsRegistry()->safeFlushInformation(fd); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 16434d6d7..de3a64ff6 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -247,11 +247,20 @@ class CVC4_EXPORT SmtEngine * to a state where its options were prior to parsing but after e.g. * reading command line options. */ - void notifyStartParsing(std::string filename) CVC4_EXPORT; + void notifyStartParsing(const std::string& filename) CVC4_EXPORT; /** return the input name (if any) */ const std::string& getFilename() const; /** + * Helper method for the API to put the last check result into the statistics. + */ + void setResultStatistic(const std::string& result) CVC4_EXPORT; + /** + * Helper method for the API to put the total runtime into the statistics. + */ + void setTotalTimeStatistic(double seconds) CVC4_EXPORT; + + /** * Get the model (only if immediately preceded by a SAT or NOT_ENTAILED * query). Only permitted if produce-models is on. */ diff --git a/src/smt/smt_engine_stats.cpp b/src/smt/smt_engine_stats.cpp index d8c48fd1d..382dcba1f 100644 --- a/src/smt/smt_engine_stats.cpp +++ b/src/smt/smt_engine_stats.cpp @@ -30,7 +30,10 @@ SmtEngineStatistics::SmtEngineStatistics() d_solveTime("smt::SmtEngine::solveTime"), d_pushPopTime("smt::SmtEngine::pushPopTime"), d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"), - d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0) + d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0), + d_driverFilename("driver::filename", ""), + d_driverResult("driver::sat/unsat", ""), + d_driverTotalTime("driver::totalTime", 0.0) { smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime); smtStatisticsRegistry()->registerStat(&d_numConstantProps); @@ -43,6 +46,9 @@ SmtEngineStatistics::SmtEngineStatistics() smtStatisticsRegistry()->registerStat(&d_pushPopTime); smtStatisticsRegistry()->registerStat(&d_processAssertionsTime); smtStatisticsRegistry()->registerStat(&d_simplifiedToFalse); + smtStatisticsRegistry()->registerStat(&d_driverFilename); + smtStatisticsRegistry()->registerStat(&d_driverResult); + smtStatisticsRegistry()->registerStat(&d_driverTotalTime); } SmtEngineStatistics::~SmtEngineStatistics() @@ -58,6 +64,9 @@ SmtEngineStatistics::~SmtEngineStatistics() smtStatisticsRegistry()->unregisterStat(&d_pushPopTime); smtStatisticsRegistry()->unregisterStat(&d_processAssertionsTime); smtStatisticsRegistry()->unregisterStat(&d_simplifiedToFalse); + smtStatisticsRegistry()->unregisterStat(&d_driverFilename); + smtStatisticsRegistry()->unregisterStat(&d_driverResult); + smtStatisticsRegistry()->unregisterStat(&d_driverTotalTime); } } // namespace smt diff --git a/src/smt/smt_engine_stats.h b/src/smt/smt_engine_stats.h index 0f2e4fd50..9e3e7989e 100644 --- a/src/smt/smt_engine_stats.h +++ b/src/smt/smt_engine_stats.h @@ -50,6 +50,13 @@ struct SmtEngineStatistics /** Has something simplified to false? */ IntStat d_simplifiedToFalse; + + /** Name of the input file */ + BackedStat<std::string> d_driverFilename; + /** Result of the last check */ + BackedStat<std::string> d_driverResult; + /** Total time of the current run */ + BackedStat<double> d_driverTotalTime; }; /* struct SmtEngineStatistics */ } // namespace smt |