diff options
Diffstat (limited to 'src/main/portfolio.cpp')
-rw-r--r-- | src/main/portfolio.cpp | 93 |
1 files changed, 93 insertions, 0 deletions
diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp new file mode 100644 index 000000000..fc22374cf --- /dev/null +++ b/src/main/portfolio.cpp @@ -0,0 +1,93 @@ +/********************* */ +/*! \file portfolio.cpp + ** \verbatim + ** Original author: kshitij + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include <boost/function.hpp> +#include <boost/thread.hpp> +#include <boost/bind.hpp> +#include <boost/thread/condition.hpp> +#include <boost/exception_ptr.hpp> + +#include "smt/smt_engine.h" +#include "util/result.h" +#include "util/options.h" + +using namespace boost; + +namespace CVC4 { + +mutex mutex_done; +mutex mutex_main_wait; +condition condition_var_main_wait; + +bool global_flag_done = false; +int global_winner = -1; + +template<typename S> +void runThread(int thread_id, function<S()> threadFn, S& returnValue) { + returnValue = threadFn(); + + if( mutex_done.try_lock() ) { + if(global_flag_done == false) { + global_flag_done = true; + global_winner = thread_id; + } + mutex_done.unlock(); + condition_var_main_wait.notify_all(); // we want main thread to quit + } +} + +template<typename T, typename S> +std::pair<int, S> runPortfolio(int numThreads, + function<T()> driverFn, + function<S()> threadFns[], + bool optionWaitToJoin) { + thread thread_driver; + thread threads[numThreads]; + S threads_returnValue[numThreads]; + + for(int t = 0; t < numThreads; ++t) { + threads[t] = thread(bind(runThread<S>, t, threadFns[t], ref(threads_returnValue[t]) )); + } + + if(not driverFn.empty()) + thread_driver = boost::thread(driverFn); + + while(global_flag_done == false) + condition_var_main_wait.wait(mutex_main_wait); + + if(not driverFn.empty()) { + thread_driver.interrupt(); + thread_driver.join(); + } + + for(int t = 0; t < numThreads; ++t) { + if(optionWaitToJoin) { + threads[t].join(); + } + } + + return std::pair<int, S>(global_winner,threads_returnValue[global_winner]); +} + +// instantiation +template +std::pair<int, Result> +runPortfolio<void, Result>(int, boost::function<void()>, boost::function<Result()>*, bool); + +}/* CVC4 namespace */ |