diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-09-08 14:25:25 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-09-08 14:25:25 +0000 |
commit | cfa9e2cbbdf77a325791b5548b41093a0781311c (patch) | |
tree | e843d38afe4b197a2dd81316998477cedac26c52 /src/main/portfolio.cpp | |
parent | 6935324f45bd7f2c735ca4120a9e800ef8903442 (diff) |
Single driver for both sequential and portfolio
A "command executer" layer between parsing commands and invoking them.
New implementation of portfolio driver splits only when check-sat or query
command is encountered, and then switches back to sequential till the next
one. As side effect, restores functionality of interactive mode and
push/pops.
Diffstat (limited to 'src/main/portfolio.cpp')
-rw-r--r-- | src/main/portfolio.cpp | 36 |
1 files changed, 19 insertions, 17 deletions
diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp index 10c387b14..90af26458 100644 --- a/src/main/portfolio.cpp +++ b/src/main/portfolio.cpp @@ -11,10 +11,8 @@ ** 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 + ** \brief Provides (somewhat) generic functionality to simulate a + ** (potentially cooperative) race **/ #include <boost/function.hpp> @@ -27,19 +25,18 @@ #include "util/result.h" #include "options/options.h" -using namespace boost; - namespace CVC4 { -mutex mutex_done; -mutex mutex_main_wait; -condition condition_var_main_wait; +boost::mutex mutex_done; +boost::mutex mutex_main_wait; +boost::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) { +void runThread(int thread_id, boost::function<S()> threadFn, S& returnValue) +{ returnValue = threadFn(); if( mutex_done.try_lock() ) { @@ -54,15 +51,17 @@ void runThread(int thread_id, function<S()> threadFn, S& returnValue) { template<typename T, typename S> std::pair<int, S> runPortfolio(int numThreads, - function<T()> driverFn, - function<S()> threadFns[], + boost::function<T()> driverFn, + boost::function<S()> threadFns[], bool optionWaitToJoin) { - thread thread_driver; - thread threads[numThreads]; + boost::thread thread_driver; + boost::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]) )); + threads[t] = + boost::thread(boost::bind(runThread<S>, t, threadFns[t], + boost::ref(threads_returnValue[t]) ) ); } if(not driverFn.empty()) @@ -87,7 +86,10 @@ std::pair<int, S> runPortfolio(int numThreads, // instantiation template -std::pair<int, Result> -runPortfolio<void, Result>(int, boost::function<void()>, boost::function<Result()>*, bool); +std::pair<int, bool> +runPortfolio<void, bool>(int, + boost::function<void()>, + boost::function<bool()>*, + bool); }/* CVC4 namespace */ |