src/main/portfolio_util.cpp

   1 /*********************                                                        */
   2 /*! \file portfolio_util.cpp
   3  ** \verbatim
   4  ** Original author: kshitij
   5  ** Major contributors: mdeters
   6  ** Minor contributors (to current version):
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Code relevant only for portfolio builds
  15  **/
  16
  17 #include <cassert>
  18 #include <vector>
  19 #include <unistd.h>
  20 #include "options/options.h"
  21 #include "main/options.h"
  22 #include "prop/options.h"
  23 #include "smt/options.h"
  24
  25 using namespace std;
  26
  27 namespace CVC4 {
  28
  29 vector<Options> parseThreadSpecificOptions(Options opts)
  30 {
  31   vector<Options> threadOptions;
  32
  33   unsigned numThreads = opts[options::threads];
  34
  35   /**
  36    * Use satRandomSeed for generating random numbers, in particular
  37    * satRandomSeed-s
  38    */
  39   srand((unsigned int)(-opts[options::satRandomSeed]));
  40
  41   for(unsigned i = 0; i < numThreads; ++i) {
  42     threadOptions.push_back(opts);
  43     Options& tOpts = threadOptions.back();
  44
  45     // Set thread identifier
  46     tOpts.set(options::thread_id, i);
  47
  48     // If the random-seed is negative, pick a random seed randomly
  49     if(opts[options::satRandomSeed] < 0) {
  50       tOpts.set(options::satRandomSeed, (double)rand());
  51     }
  52
  53     if(i < opts[options::threadArgv].size() &&
  54        !opts[options::threadArgv][i].empty()) {
  55
  56       // separate out the thread's individual configuration string
  57       stringstream optidss;
  58       optidss << "--thread" << i;
  59       string optid = optidss.str();
  60       int targc = 1;
  61       char* tbuf = strdup(opts[options::threadArgv][i].c_str());
  62       char* p = tbuf;
  63       // string length is certainly an upper bound on size needed
  64       char** targv = new char*[opts[options::threadArgv][i].size()];
  65       char** vp = targv;
  66       *vp++ = strdup(optid.c_str());
  67       p = strtok(p, " ");
  68       while(p != NULL) {
  69         *vp++ = p;
  70         ++targc;
  71         p = strtok(NULL, " ");
  72       }
  73       *vp++ = NULL;
  74       if(targc > 1) { // this is necessary in case you do e.g. --thread0="  "
  75         try {
  76           tOpts.parseOptions(targc, targv);
  77         } catch(OptionException& e) {
  78           stringstream ss;
  79           ss << optid << ": " << e.getMessage();
  80           throw OptionException(ss.str());
  81         }
  82         if(optind != targc) {
  83           stringstream ss;
  84           ss << "unused argument `" << targv[optind]
  85              << "' in thread configuration " << optid << " !";
  86           throw OptionException(ss.str());
  87         }
  88         if(tOpts[options::threads] != numThreads
  89            || tOpts[options::threadArgv] != opts[options::threadArgv]) {
  90           stringstream ss;
  91           ss << "not allowed to set thread options in " << optid << " !";
  92           throw OptionException(ss.str());
  93         }
  94       }
  95       free(targv[0]);
  96       delete targv;
  97       free(tbuf);
  98     }
  99   }
 100
 101   assert(numThreads >= 1);      //do we need this?
 102
 103   return threadOptions;
 104 }
 105
 106 }/*CVC4 namespace */