summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/api/cvc4cpp.cpp6
-rw-r--r--src/api/cvc4cpp.h4
-rw-r--r--src/expr/node_manager.cpp7
-rw-r--r--src/expr/node_manager.h9
-rw-r--r--src/main/command_executor.cpp8
-rw-r--r--src/main/command_executor.h8
-rw-r--r--src/main/driver_unified.cpp34
-rw-r--r--src/main/main.cpp2
-rw-r--r--src/main/main.h6
-rw-r--r--src/main/signal_handlers.cpp5
-rw-r--r--src/smt/smt_engine.cpp23
-rw-r--r--src/smt/smt_engine.h11
-rw-r--r--src/smt/smt_engine_stats.cpp11
-rw-r--r--src/smt/smt_engine_stats.h7
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback