summaryrefslogtreecommitdiff
path: root/src/main
diff options
context:
space:
mode:
Diffstat (limited to 'src/main')
-rw-r--r--src/main/Makefile.am2
-rw-r--r--src/main/command_executor.cpp13
-rw-r--r--src/main/command_executor.h17
-rw-r--r--src/main/command_executor_portfolio.cpp54
-rw-r--r--src/main/command_executor_portfolio.h8
-rw-r--r--src/main/driver_unified.cpp48
-rw-r--r--src/main/main.cpp7
-rw-r--r--src/main/main.h10
-rw-r--r--src/main/util.cpp44
9 files changed, 118 insertions, 85 deletions
diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index 4524929d4..aa63846cf 100644
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -30,6 +30,7 @@ pcvc4_LDADD = \
libmain.a \
@builddir@/../parser/libcvc4parser.la \
@builddir@/../libcvc4.la \
+ @builddir@/../util/libstatistics.la \
@builddir@/../lib/libreplacements.la \
$(READLINE_LIBS)
pcvc4_CPPFLAGS = $(AM_CPPFLAGS) $(BOOST_CPPFLAGS) -DPORTFOLIO_BUILD
@@ -51,6 +52,7 @@ cvc4_LDADD = \
libmain.a \
@builddir@/../parser/libcvc4parser.la \
@builddir@/../libcvc4.la \
+ @builddir@/../util/libstatistics.la \
@builddir@/../lib/libreplacements.la \
$(READLINE_LIBS)
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 1bffd5e35..d283b2743 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -24,16 +24,11 @@
namespace CVC4 {
namespace main {
-
CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options):
d_exprMgr(exprMgr),
d_smtEngine(SmtEngine(&exprMgr)),
- d_options(options) {
-
- // signal handlers need access
- main::pStatistics = d_smtEngine.getStatisticsRegistry();
- d_exprMgr.getStatisticsRegistry()->setName("ExprManager");
- main::pStatistics->registerStat_(d_exprMgr.getStatisticsRegistry());
+ d_options(options),
+ d_stats("driver") {
}
bool CommandExecutor::doCommand(Command* cmd)
@@ -89,5 +84,5 @@ bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out)
return !cmd->fail();
}
-}/*main namespace*/
-}/*CVC4 namespace*/
+}/* CVC4::main namespace */
+}/* CVC4 namespace */
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index 273225e69..435299ce3 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -19,6 +19,12 @@
#include "expr/expr_manager.h"
#include "smt/smt_engine.h"
+#include "util/statistics_registry.h"
+#include "options/options.h"
+#include "expr/command.h"
+
+#include <string>
+#include <iostream>
namespace CVC4 {
namespace main {
@@ -29,6 +35,7 @@ protected:
ExprManager& d_exprMgr;
SmtEngine d_smtEngine;
Options& d_options;
+ StatisticsRegistry d_stats;
public:
// Note: though the options are not cached (instead a reference is
@@ -48,6 +55,16 @@ public:
virtual std::string getSmtEngineStatus();
+ StatisticsRegistry& getStatisticsRegistry() {
+ return d_stats;
+ }
+
+ virtual void flushStatistics(std::ostream& out) const {
+ d_exprMgr.getStatistics().flushInformation(out);
+ d_smtEngine.getStatistics().flushInformation(out);
+ d_stats.flushInformation(out);
+ }
+
protected:
/** Executes treating cmd as a singleton */
virtual bool doCommandSingleton(CVC4::Command* cmd);
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 045cac8f1..32a507d78 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -21,6 +21,7 @@
#include <boost/thread/condition.hpp>
#include <boost/exception_ptr.hpp>
#include <boost/lexical_cast.hpp>
+#include <string>
#include "expr/command.h"
#include "expr/pickler.h"
@@ -63,26 +64,10 @@ CommandExecutorPortfolio::CommandExecutorPortfolio
d_smts.push_back(new SmtEngine(d_exprMgrs[i]));
}
- for(unsigned i = 1; i < d_numThreads; ++i) {
- // Register the statistics registry of the thread
- string emTag = "ExprManager thread #"
- + boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]);
- string smtTag = "SmtEngine thread #"
- + boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]);
- d_exprMgrs[i]->getStatisticsRegistry()->setName(emTag);
- d_smts[i]->getStatisticsRegistry()->setName(smtTag);
- pStatistics->registerStat_
- (d_exprMgrs[i]->getStatisticsRegistry() );
- pStatistics->registerStat_
- (d_smts[i]->getStatisticsRegistry() );
- }
-
Assert(d_vmaps.size() == 0);
for(unsigned i = 0; i < d_numThreads; ++i) {
d_vmaps.push_back(new ExprManagerMapCollection());
}
-
-
}
CommandExecutorPortfolio::~CommandExecutorPortfolio()
@@ -116,7 +101,7 @@ void CommandExecutorPortfolio::lemmaSharingInit()
for(unsigned i = 0; i < d_numThreads; ++i){
if(Debug.isOn("channel-empty")) {
- d_channelsOut.push_back
+ d_channelsOut.push_back
(new EmptySharedChannel<ChannelFormat>(sharingChannelSize));
d_channelsIn.push_back
(new EmptySharedChannel<ChannelFormat>(sharingChannelSize));
@@ -143,7 +128,7 @@ void CommandExecutorPortfolio::lemmaSharingInit()
}
/* Output to string stream */
- if(d_options[options::verbosity] == 0
+ if(d_options[options::verbosity] == 0
|| d_options[options::separateOutput]) {
Assert(d_ostringstreams.size() == 0);
for(unsigned i = 0; i < d_numThreads; ++i) {
@@ -152,7 +137,7 @@ void CommandExecutorPortfolio::lemmaSharingInit()
}
}
}
-}
+}/* CommandExecutorPortfolio::lemmaSharingInit() */
void CommandExecutorPortfolio::lemmaSharingCleanup()
{
@@ -180,7 +165,8 @@ void CommandExecutorPortfolio::lemmaSharingCleanup()
d_ostringstreams.clear();
}
-}
+}/* CommandExecutorPortfolio::lemmaSharingCleanup() */
+
bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
{
@@ -200,7 +186,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
// } else if(dynamic_cast<GetValueCommand*>(cmd) != NULL) {
// mode = 2;
// }
-
+
if(mode == 0) {
d_seq->addCommand(cmd->clone());
return CommandExecutor::doCommandSingleton(cmd);
@@ -290,7 +276,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
*d_options[options::out]
<< d_ostringstreams[portfolioReturn.first]->str();
}
-
+
/* cleanup this check sat specific stuff */
lemmaSharingCleanup();
@@ -303,12 +289,30 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
Unreachable();
}
-}
+}/* CommandExecutorPortfolio::doCommandSingleton() */
std::string CommandExecutorPortfolio::getSmtEngineStatus()
{
return d_smts[d_lastWinner]->getInfo("status").getValue();
}
-}/*main namespace*/
-}/*CVC4 namespace*/
+void CommandExecutorPortfolio::flushStatistics(std::ostream& out) const {
+ Assert(d_numThreads == d_exprMgrs.size() && d_exprMgrs.size() == d_smts.size());
+ for(size_t i = 0; i < d_numThreads; ++i) {
+ string emTag = "ExprManager thread #"
+ + boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]);
+ Statistics stats = d_exprMgrs[i]->getStatistics();
+ stats.setPrefix(emTag);
+ stats.flushInformation(out);
+
+ string smtTag = "SmtEngine thread #"
+ + boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]);
+ stats = d_smts[i]->getStatistics();
+ stats.setPrefix(smtTag);
+ stats.flushInformation(out);
+ }
+ d_stats.flushInformation(out);
+}
+
+}/* CVC4::main namespace */
+}/* CVC4 namespace */
diff --git a/src/main/command_executor_portfolio.h b/src/main/command_executor_portfolio.h
index cc0a77698..72a677789 100644
--- a/src/main/command_executor_portfolio.h
+++ b/src/main/command_executor_portfolio.h
@@ -23,6 +23,11 @@
#include "main/command_executor.h"
#include "main/portfolio_util.h"
+#include <vector>
+#include <string>
+#include <iostream>
+#include <sstream>
+
namespace CVC4 {
class CommandSequence;
@@ -55,6 +60,9 @@ public:
~CommandExecutorPortfolio();
std::string getSmtEngineStatus();
+
+ void flushStatistics(std::ostream& out) const;
+
protected:
bool doCommandSingleton(Command* cmd);
private:
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;
}
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 70f2783a5..73936526f 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -26,6 +26,7 @@
#include "main/main.h"
#include "main/interactive_shell.h"
+#include "main/command_executor.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
#include "parser/parser_exception.h"
@@ -38,7 +39,7 @@
#include "theory/uf/options.h"
#include "util/output.h"
#include "util/result.h"
-#include "util/stats.h"
+#include "util/statistics.h"
using namespace std;
using namespace CVC4;
@@ -66,8 +67,8 @@ int main(int argc, char* argv[]) {
*opts[options::out] << "unknown" << endl;
#endif
*opts[options::err] << "CVC4 Error:" << endl << e << endl;
- if(opts[options::statistics] && pStatistics != NULL) {
- pStatistics->flushInformation(*opts[options::err]);
+ if(opts[options::statistics] && pExecutor != NULL) {
+ pExecutor->flushStatistics(*opts[options::err]);
}
}
exit(1);
diff --git a/src/main/main.h b/src/main/main.h
index 09ba60c94..8ed4da1cb 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -20,8 +20,10 @@
#include <string>
#include "options/options.h"
+#include "expr/expr_manager.h"
+#include "smt/smt_engine.h"
#include "util/exception.h"
-#include "util/stats.h"
+#include "util/statistics.h"
#include "util/tls.h"
#include "cvc4autoconfig.h"
@@ -31,14 +33,16 @@
namespace CVC4 {
namespace main {
+class CommandExecutor;
+
/** Full argv[0] */
extern const char* progPath;
/** Just the basename component of argv[0] */
extern const char* progName;
-/** A reference to the StatisticsRegistry for use by the signal handlers */
-extern CVC4::StatisticsRegistry* pStatistics;
+/** A reference for use by the signal handlers to print statistics */
+extern CVC4::main::CommandExecutor* pExecutor;
/**
* If true, will not spin on segfault even when CVC4_DEBUG is on.
diff --git a/src/main/util.cpp b/src/main/util.cpp
index 756c7d7a9..523486f80 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -28,10 +28,12 @@
#include "util/Assert.h"
#include "util/exception.h"
#include "options/options.h"
-#include "util/stats.h"
+#include "util/statistics.h"
+#include "smt/smt_engine.h"
#include "cvc4autoconfig.h"
#include "main/main.h"
+#include "main/command_executor.h"
using CVC4::Exception;
using namespace std;
@@ -52,8 +54,8 @@ bool segvNoSpin = false;
/** Handler for SIGXCPU, i.e., timeout. */
void timeout_handler(int sig, siginfo_t* info, void*) {
fprintf(stderr, "CVC4 interrupted by timeout.\n");
- if((*pOptions)[options::statistics] && pStatistics != NULL) {
- pStatistics->flushInformation(cerr);
+ if((*pOptions)[options::statistics] && pExecutor != NULL) {
+ pExecutor->flushStatistics(cerr);
}
abort();
}
@@ -61,8 +63,8 @@ void timeout_handler(int sig, siginfo_t* info, void*) {
/** Handler for SIGINT, i.e., when the user hits control C. */
void sigint_handler(int sig, siginfo_t* info, void*) {
fprintf(stderr, "CVC4 interrupted by user.\n");
- if((*pOptions)[options::statistics] && pStatistics != NULL) {
- pStatistics->flushInformation(cerr);
+ if((*pOptions)[options::statistics] && pExecutor != NULL) {
+ pExecutor->flushStatistics(cerr);
}
abort();
}
@@ -86,8 +88,8 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
if(segvNoSpin) {
fprintf(stderr, "No-spin requested, aborting...\n");
- if((*pOptions)[options::statistics] && pStatistics != NULL) {
- pStatistics->flushInformation(cerr);
+ if((*pOptions)[options::statistics] && pExecutor != NULL) {
+ pExecutor->flushStatistics(cerr);
}
abort();
} else {
@@ -106,8 +108,8 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
} else if(addr < 10*1024) {
cerr << "Looks like a NULL pointer was dereferenced." << endl;
}
- if((*pOptions)[options::statistics] && pStatistics != NULL) {
- pStatistics->flushInformation(cerr);
+ if((*pOptions)[options::statistics] && pExecutor != NULL) {
+ pExecutor->flushStatistics(cerr);
}
abort();
#endif /* CVC4_DEBUG */
@@ -119,8 +121,8 @@ void ill_handler(int sig, siginfo_t* info, void*) {
fprintf(stderr, "CVC4 executed an illegal instruction in DEBUG mode.\n");
if(segvNoSpin) {
fprintf(stderr, "No-spin requested, aborting...\n");
- if((*pOptions)[options::statistics] && pStatistics != NULL) {
- pStatistics->flushInformation(cerr);
+ if((*pOptions)[options::statistics] && pExecutor != NULL) {
+ pExecutor->flushStatistics(cerr);
}
abort();
} else {
@@ -132,8 +134,8 @@ void ill_handler(int sig, siginfo_t* info, void*) {
}
#else /* CVC4_DEBUG */
fprintf(stderr, "CVC4 executed an illegal instruction.\n");
- if((*pOptions)[options::statistics] && pStatistics != NULL) {
- pStatistics->flushInformation(cerr);
+ if((*pOptions)[options::statistics] && pExecutor != NULL) {
+ pExecutor->flushStatistics(cerr);
}
abort();
#endif /* CVC4_DEBUG */
@@ -156,8 +158,8 @@ void cvc4unexpected() {
}
if(segvNoSpin) {
fprintf(stderr, "No-spin requested.\n");
- if((*pOptions)[options::statistics] && pStatistics != NULL) {
- pStatistics->flushInformation(cerr);
+ if((*pOptions)[options::statistics] && pExecutor != NULL) {
+ pExecutor->flushStatistics(cerr);
}
set_terminate(default_terminator);
} else {
@@ -169,8 +171,8 @@ void cvc4unexpected() {
}
#else /* CVC4_DEBUG */
fprintf(stderr, "CVC4 threw an \"unexpected\" exception.\n");
- if((*pOptions)[options::statistics] && pStatistics != NULL) {
- pStatistics->flushInformation(cerr);
+ if((*pOptions)[options::statistics] && pExecutor != NULL) {
+ pExecutor->flushStatistics(cerr);
}
set_terminate(default_terminator);
#endif /* CVC4_DEBUG */
@@ -182,16 +184,16 @@ void cvc4terminate() {
"CVC4 was terminated by the C++ runtime.\n"
"Perhaps an exception was thrown during stack unwinding. "
"(Don't do that.)\n");
- if((*pOptions)[options::statistics] && pStatistics != NULL) {
- pStatistics->flushInformation(cerr);
+ if((*pOptions)[options::statistics] && pExecutor != NULL) {
+ pExecutor->flushStatistics(cerr);
}
default_terminator();
#else /* CVC4_DEBUG */
fprintf(stderr,
"CVC4 was terminated by the C++ runtime.\n"
"Perhaps an exception was thrown during stack unwinding.\n");
- if((*pOptions)[options::statistics] && pStatistics != NULL) {
- pStatistics->flushInformation(cerr);
+ if((*pOptions)[options::statistics] && pExecutor != NULL) {
+ pExecutor->flushStatistics(cerr);
}
default_terminator();
#endif /* CVC4_DEBUG */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback