diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-02-20 08:57:39 -0500 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-02-20 08:57:39 -0500 |
| commit | 531ec6e52b75cd2f600a3fc781383e7539f2335a (patch) | |
| tree | 2a78deb202f6886b6524f3852dc81f46c0eff36a /src/main/portfolio.h | |
| parent | 046fd1e02c1330b207bda99f8121b11562dd619c (diff) | |
portfolio: add stat to track time spent waiting for interrupted threads to stop
Diffstat (limited to 'src/main/portfolio.h')
| -rw-r--r-- | src/main/portfolio.h | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/main/portfolio.h b/src/main/portfolio.h index 61a4c055f..c2d313a44 100644 --- a/src/main/portfolio.h +++ b/src/main/portfolio.h @@ -22,14 +22,16 @@ #include "smt/smt_engine.h" #include "expr/command.h" #include "options/options.h" +#include "util/statistics_registry.h" namespace CVC4 { template<typename T, typename S> std::pair<int, S> runPortfolio(int numThreads, - boost::function<T()> driverFn, - boost::function<S()> threadFns[], - bool optionWaitToJoin); + boost::function<T()> driverFn, + boost::function<S()> threadFns[], + bool optionWaitToJoin, + TimerStat& statWaitTime); // as we have defined things, S=void would give compile errors // do we want to fix this? yes, no, maybe? |