From 7aa87517562e993e530a1da323b724d8e30e9fbe Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 4 Mar 2013 19:58:15 -0500 Subject: [PATCH] New --tear-down-incremental mode, useful for debugging and performance profiling. --- src/main/command_executor.cpp | 15 ++++- src/main/command_executor.h | 9 ++- src/main/command_executor_portfolio.cpp | 2 +- src/main/driver_unified.cpp | 76 +++++++++++++++++++++++++ src/main/options | 3 + 5 files changed, 98 insertions(+), 7 deletions(-) diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index a1410d910..4644c91a7 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -28,7 +28,7 @@ void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options) : d_exprMgr(exprMgr), - d_smtEngine(SmtEngine(&exprMgr)), + d_smtEngine(new SmtEngine(&exprMgr)), d_options(options), d_stats("driver"), d_result() { @@ -61,13 +61,22 @@ bool CommandExecutor::doCommand(Command* cmd) } } +void CommandExecutor::reset() +{ + if(d_options[options::statistics]) { + flushStatistics(*d_options[options::err]); + } + delete d_smtEngine; + d_smtEngine = new SmtEngine(&d_exprMgr); +} + bool CommandExecutor::doCommandSingleton(Command* cmd) { bool status = true; if(d_options[options::verbosity] >= -1) { - status = smtEngineInvoke(&d_smtEngine, cmd, d_options[options::out]); + status = smtEngineInvoke(d_smtEngine, cmd, d_options[options::out]); } else { - status = smtEngineInvoke(&d_smtEngine, cmd, NULL); + status = smtEngineInvoke(d_smtEngine, cmd, NULL); } Result res; diff --git a/src/main/command_executor.h b/src/main/command_executor.h index 5395cc804..e6e3d3411 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -33,7 +33,7 @@ private: protected: ExprManager& d_exprMgr; - SmtEngine d_smtEngine; + SmtEngine* d_smtEngine; Options& d_options; StatisticsRegistry d_stats; Result d_result; @@ -41,7 +41,9 @@ protected: public: CommandExecutor(ExprManager &exprMgr, Options &options); - virtual ~CommandExecutor() {} + virtual ~CommandExecutor() { + delete d_smtEngine; + } /** * Executes a command. Recursively handles if cmd is a command @@ -51,6 +53,7 @@ public: bool doCommand(CVC4::Command* cmd); Result getResult() const { return d_result; } + void reset(); StatisticsRegistry& getStatisticsRegistry() { return d_stats; @@ -58,7 +61,7 @@ public: virtual void flushStatistics(std::ostream& out) const { d_exprMgr.getStatistics().flushInformation(out); - d_smtEngine.getStatistics().flushInformation(out); + d_smtEngine->getStatistics().flushInformation(out); d_stats.flushInformation(out); } diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index 61447afe2..9de3b2134 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -63,7 +63,7 @@ CommandExecutorPortfolio::CommandExecutorPortfolio } // Create the SmtEngine(s) - d_smts.push_back(&d_smtEngine); + d_smts.push_back(d_smtEngine); for(unsigned i = 1; i < d_numThreads; ++i) { d_smts.push_back(new SmtEngine(d_exprMgrs[i])); } diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index c2b879a6b..8117dbc05 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -238,6 +238,9 @@ int runCvc4(int argc, char* argv[], Options& opts) { Command* cmd; bool status = true; if(opts[options::interactive] && inputFromStdin) { + if( opts[options::tearDownIncremental] ) { + throw OptionException("--tear-down-incremental incompatible with --interactive"); + } #ifndef PORTFOLIO_BUILD if(!opts.wasSetByUser(options::incrementalSolving)) { cmd = new SetOptionCommand("incremental", true); @@ -267,6 +270,79 @@ int runCvc4(int argc, char* argv[], Options& opts) { status = pExecutor->doCommand(cmd) && status; delete cmd; } + } else if(opts[options::tearDownIncremental]) { + if(opts[options::incrementalSolving]) { + throw OptionException("--tear-down-incremental incompatible with --incremental"); + } + + ParserBuilder parserBuilder(exprMgr, filename, opts); + + if( inputFromStdin ) { +#if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK) + parserBuilder.withStreamInput(cin); +#else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ + parserBuilder.withLineBufferedStreamInput(cin); +#endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ + } + + vector< vector > allCommands; + allCommands.push_back(vector()); + Parser *parser = parserBuilder.build(); + if(replayParser != NULL) { + // have the replay parser use the file's declarations + replayParser->useDeclarationsFrom(parser); + } + bool needReset = false; + while(status && (cmd = parser->nextCommand())) { + if(dynamic_cast(cmd) != NULL) { + if(needReset) { + pExecutor->reset(); + for(size_t i = 0; i < allCommands.size(); ++i) { + for(size_t j = 0; j < allCommands[i].size(); ++j) { + Command* cmd = allCommands[i][j]->clone(); + pExecutor->doCommand(cmd); + delete cmd; + } + } + needReset = false; + } + allCommands.push_back(vector()); + } else if(dynamic_cast(cmd) != NULL) { + allCommands.pop_back(); // fixme leaks cmds here + pExecutor->reset(); + for(size_t i = 0; i < allCommands.size(); ++i) { + for(size_t j = 0; j < allCommands[i].size(); ++j) { + Command* cmd = allCommands[i][j]->clone(); + pExecutor->doCommand(cmd); + delete cmd; + } + } + } else if(dynamic_cast(cmd) != NULL || + dynamic_cast(cmd) != NULL) { + if(needReset) { + pExecutor->reset(); + for(size_t i = 0; i < allCommands.size(); ++i) { + for(size_t j = 0; j < allCommands[i].size(); ++j) { + Command* cmd = allCommands[i][j]->clone(); + pExecutor->doCommand(cmd); + delete cmd; + } + } + } + status = pExecutor->doCommand(cmd); + needReset = true; + } else { + allCommands.back().push_back(cmd->clone()); + if(dynamic_cast(cmd) != NULL) { + delete cmd; + break; + } + status = pExecutor->doCommand(cmd); + } + delete cmd; + } + // Remove the parser + delete parser; } else { if(!opts.wasSetByUser(options::incrementalSolving)) { cmd = new SetOptionCommand("incremental", false); diff --git a/src/main/options b/src/main/options index 8733011f7..fdb172c18 100644 --- a/src/main/options +++ b/src/main/options @@ -50,6 +50,9 @@ option segvSpin --segv-spin bool :default false spin on segfault/other crash waiting for gdb undocumented-alias --segv-nospin = --no-segv-spin +expert-option tearDownIncremental --tear-down-incremental bool :default false + implement PUSH/POP/multi-query by destroying and recreating SmtEngine + expert-option waitToJoin --wait-to-join bool :default true wait for other threads to join before quitting -- 2.30.2