summaryrefslogtreecommitdiff
path: root/src/main
diff options
context:
space:
mode:
Diffstat (limited to 'src/main')
-rw-r--r--src/main/command_executor.h6
-rw-r--r--src/main/command_executor_portfolio.cpp30
-rw-r--r--src/main/driver_unified.cpp21
-rw-r--r--src/main/main.cpp2
-rw-r--r--src/main/portfolio.cpp3
5 files changed, 32 insertions, 30 deletions
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index 8ef1a6a5f..df9c9e19f 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -65,6 +65,8 @@ public:
d_stats.flushInformation(out);
}
+ SmtGlobals* globals() { return d_smtEngine->globals(); }
+
protected:
/** Executes treating cmd as a singleton */
virtual bool doCommandSingleton(CVC4::Command* cmd);
@@ -74,9 +76,7 @@ private:
};/* class CommandExecutor */
-bool smtEngineInvoke(SmtEngine* smt,
- Command* cmd,
- std::ostream *out);
+bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out);
}/* CVC4::main namespace */
}/* CVC4 namespace */
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index c471ae585..cdd20c05a 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -117,24 +117,24 @@ void CommandExecutorPortfolio::lemmaSharingInit()
const unsigned int sharingChannelSize = 1000000;
for(unsigned i = 0; i < d_numThreads; ++i){
- d_channelsOut.push_back
- (new SynchronizedSharedChannel<ChannelFormat>(sharingChannelSize));
- d_channelsIn.push_back
- (new SynchronizedSharedChannel<ChannelFormat>(sharingChannelSize));
+ d_channelsOut.push_back(
+ new SynchronizedSharedChannel<ChannelFormat>(sharingChannelSize));
+ d_channelsIn.push_back(
+ new SynchronizedSharedChannel<ChannelFormat>(sharingChannelSize));
}
/* Lemma I/O channels */
for(unsigned i = 0; i < d_numThreads; ++i) {
string tag = "thread #" +
boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]);
- d_threadOptions[i].set
- (options::lemmaOutputChannel,
- new PortfolioLemmaOutputChannel(tag, d_channelsOut[i], d_exprMgrs[i],
- d_vmaps[i]->d_from, d_vmaps[i]->d_to));
- d_threadOptions[i].set
- (options::lemmaInputChannel,
- new PortfolioLemmaInputChannel(tag, d_channelsIn[i], d_exprMgrs[i],
- d_vmaps[i]->d_from, d_vmaps[i]->d_to));
+ LemmaOutputChannel* outputChannel =
+ new PortfolioLemmaOutputChannel(tag, d_channelsOut[i], d_exprMgrs[i],
+ d_vmaps[i]->d_from, d_vmaps[i]->d_to);
+ LemmaInputChannel* inputChannel =
+ new PortfolioLemmaInputChannel(tag, d_channelsIn[i], d_exprMgrs[i],
+ d_vmaps[i]->d_from, d_vmaps[i]->d_to);
+ d_smts[i]->globals()->setLemmaInputChannel(inputChannel);
+ d_smts[i]->globals()->setLemmaOutputChannel(outputChannel);
}
/* Output to string stream */
@@ -163,8 +163,10 @@ void CommandExecutorPortfolio::lemmaSharingCleanup()
for(unsigned i = 0; i < d_numThreads; ++i) {
delete d_channelsIn[i];
delete d_channelsOut[i];
- d_threadOptions[i].set(options::lemmaInputChannel, NULL);
- d_threadOptions[i].set(options::lemmaOutputChannel, NULL);
+ delete d_smts[i]->globals()->getLemmaInputChannel();
+ d_smts[i]->globals()->setLemmaInputChannel(NULL);
+ delete d_smts[i]->globals()->getLemmaOutputChannel();
+ d_smts[i]->globals()->setLemmaOutputChannel(NULL);
}
d_channelsIn.clear();
d_channelsOut.clear();
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index fd5aec7d0..c110ffa4f 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -28,7 +28,6 @@
#include "base/output.h"
#include "expr/expr_iomanip.h"
#include "expr/expr_manager.h"
-#include "expr/result.h"
#include "expr/statistics_registry.h"
#include "main/command_executor.h"
@@ -50,6 +49,7 @@
#include "smt/smt_options_handler.h"
#include "smt_util/command.h"
#include "util/configuration.h"
+#include "util/result.h"
using namespace std;
using namespace CVC4;
@@ -285,11 +285,11 @@ int runCvc4(int argc, char* argv[], Options& opts) {
replayParserBuilder.withStreamInput(cin);
}
replayParser = replayParserBuilder.build();
- opts.set(options::replayStream, new Parser::ExprStream(replayParser));
+ pExecutor->globals()->setReplayStream(new Parser::ExprStream(replayParser));
}
- if( opts[options::replayLog] != NULL ) {
- *opts[options::replayLog] << language::SetLanguage(opts[options::outputLanguage])
- << expr::ExprSetDepth(-1);
+ if( pExecutor->globals()->getReplayLog() != NULL ) {
+ *(pExecutor->globals()->getReplayLog()) <<
+ language::SetLanguage(opts[options::outputLanguage]) << expr::ExprSetDepth(-1);
}
int returnValue = 0;
@@ -569,10 +569,11 @@ int runCvc4(int argc, char* argv[], Options& opts) {
delete parser;
}
- if( opts[options::replayStream] != NULL ) {
+ if( pExecutor->globals()->getReplayStream() != NULL ) {
+ ExprStream* replayStream = pExecutor->globals()->getReplayStream();
+ pExecutor->globals()->setReplayStream(NULL);
// this deletes the expression parser too
- delete opts[options::replayStream];
- opts.set(options::replayStream, NULL);
+ delete replayStream;
}
Result result;
@@ -610,8 +611,8 @@ int runCvc4(int argc, char* argv[], Options& opts) {
}
// make sure to flush replay output log before early-exit
- if( opts[options::replayLog] != NULL ) {
- *opts[options::replayLog] << flush;
+ if( pExecutor->globals()->getReplayLog() != NULL ) {
+ *(pExecutor->globals()->getReplayLog()) << flush;
}
// make sure out and err streams are flushed too
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 3f0842cc5..f8cb0677c 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -24,7 +24,6 @@
#include "base/output.h"
#include "expr/expr_manager.h"
-#include "expr/result.h"
#include "expr/statistics.h"
#include "main/command_executor.h"
#include "main/interactive_shell.h"
@@ -37,6 +36,7 @@
#include "smt/smt_engine.h"
#include "smt_util/command.h"
#include "util/configuration.h"
+#include "util/result.h"
using namespace std;
using namespace CVC4;
diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp
index 884c3eda7..ea7e3d458 100644
--- a/src/main/portfolio.cpp
+++ b/src/main/portfolio.cpp
@@ -20,11 +20,10 @@
#include <boost/exception_ptr.hpp>
#include "base/output.h"
-#include "expr/result.h"
#include "expr/statistics_registry.h"
#include "options/options.h"
#include "smt/smt_engine.h"
-
+#include "util/result.h"
namespace CVC4 {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback