diff options
Diffstat (limited to 'src/main/portfolio_util.cpp')
-rw-r--r-- | src/main/portfolio_util.cpp | 81 |
1 files changed, 51 insertions, 30 deletions
diff --git a/src/main/portfolio_util.cpp b/src/main/portfolio_util.cpp index 1ec0b961c..e42787fea 100644 --- a/src/main/portfolio_util.cpp +++ b/src/main/portfolio_util.cpp @@ -19,45 +19,68 @@ #include <cassert> #include <vector> -#include "options/base_options.h" -#include "options/main_options.h" #include "options/options.h" -#include "options/prop_options.h" -#include "options/smt_options.h" -#include "smt/smt_options_handler.h" using namespace std; namespace CVC4 { -vector<Options> parseThreadSpecificOptions(Options opts) -{ - vector<Options> threadOptions; +OptionsList::OptionsList() : d_options() {} + +OptionsList::~OptionsList(){ + for(std::vector<Options*>::iterator i = d_options.begin(), + iend = d_options.end(); i != iend; ++i) + { + Options* current = *i; + delete current; + } + d_options.clear(); +} + +void OptionsList::push_back_copy(const Options& opts) { + Options* copy = new Options; + copy->copyValues(opts); + d_options.push_back(copy); +} + +Options& OptionsList::operator[](size_t position){ + return *(d_options[position]); +} + +const Options& OptionsList::operator[](size_t position) const { + return *(d_options[position]); +} -#warning "TODO: Check that the SmtEngine pointer should be NULL with Kshitij." - smt::SmtOptionsHandler optionsHandler(NULL); +Options& OptionsList::back() { + return *(d_options.back()); +} - unsigned numThreads = opts[options::threads]; +size_t OptionsList::size() const { + return d_options.size(); +} + +void parseThreadSpecificOptions(OptionsList& threadOptions, const Options& opts) +{ + + unsigned numThreads = opts.getThreads(); for(unsigned i = 0; i < numThreads; ++i) { - threadOptions.push_back(opts); + threadOptions.push_back_copy(opts); Options& tOpts = threadOptions.back(); // Set thread identifier - tOpts.set(options::thread_id, i); - - if(i < opts[options::threadArgv].size() && - !opts[options::threadArgv][i].empty()) { - + tOpts.setThreadId(i); + const std::vector<std::string>& optThreadArgvs = opts.getThreadArgv(); + if(i < optThreadArgvs.size() && (! optThreadArgvs[i].empty())) { // separate out the thread's individual configuration string stringstream optidss; optidss << "--thread" << i; string optid = optidss.str(); int targc = 1; - char* tbuf = strdup(opts[options::threadArgv][i].c_str()); + char* tbuf = strdup(optThreadArgvs[i].c_str()); char* p = tbuf; // string length is certainly an upper bound on size needed - char** targv = new char*[opts[options::threadArgv][i].size()]; + char** targv = new char*[optThreadArgvs[i].size()]; char** vp = targv; *vp++ = strdup(optid.c_str()); p = strtok(p, " "); @@ -69,7 +92,7 @@ vector<Options> parseThreadSpecificOptions(Options opts) *vp++ = NULL; if(targc > 1) { // this is necessary in case you do e.g. --thread0=" " try { - tOpts.parseOptions(targc, targv, &optionsHandler); + tOpts.parseOptions(targc, targv); } catch(OptionException& e) { stringstream ss; ss << optid << ": " << e.getMessage(); @@ -81,8 +104,8 @@ vector<Options> parseThreadSpecificOptions(Options opts) << "' in thread configuration " << optid << " !"; throw OptionException(ss.str()); } - if(tOpts[options::threads] != numThreads - || tOpts[options::threadArgv] != opts[options::threadArgv]) { + if(tOpts.getThreads() != numThreads || + tOpts.getThreadArgv() != opts.getThreadArgv()) { stringstream ss; ss << "not allowed to set thread options in " << optid << " !"; throw OptionException(ss.str()); @@ -95,12 +118,10 @@ vector<Options> parseThreadSpecificOptions(Options opts) } assert(numThreads >= 1); //do we need this? - - return threadOptions; } void PortfolioLemmaOutputChannel::notifyNewLemma(Expr lemma) { - if(int(lemma.getNumChildren()) > options::sharingFilterByLength()) { + if(int(lemma.getNumChildren()) > Options::currentGetSharingFilterByLength()) { return; } ++cnt; @@ -109,9 +130,9 @@ void PortfolioLemmaOutputChannel::notifyNewLemma(Expr lemma) { try { d_pickler.toPickle(lemma, pkl); d_sharedChannel->push(pkl); - if(Trace.isOn("showSharing") && options::thread_id() == 0) { - *options::out() << "thread #0: notifyNewLemma: " << lemma - << std::endl; + if(Trace.isOn("showSharing") && Options::currentGetThreadId() == 0) { + (*(Options::currentGetOut())) + << "thread #0: notifyNewLemma: " << lemma << std::endl; } } catch(expr::pickle::PicklingException& p){ Trace("sharing::blocked") << lemma << std::endl; @@ -137,8 +158,8 @@ Expr PortfolioLemmaInputChannel::getNewLemma() { expr::pickle::Pickle pkl = d_sharedChannel->pop(); Expr e = d_pickler.fromPickle(pkl); - if(Trace.isOn("showSharing") && options::thread_id() == 0) { - *options::out() << "thread #0: getNewLemma: " << e << std::endl; + if(Trace.isOn("showSharing") && Options::currentGetThreadId() == 0) { + (*Options::currentGetOut()) << "thread #0: getNewLemma: " << e << std::endl; } return e; } |