uint timeinsecs = problem->getBestTime() / NANOSEC;
uint adaptive = (timeinsecs > 30) ? timeinsecs * 5 : 150;
uint maxtime = (adaptive < timeout) ? adaptive : timeout;
-
+ uint satuneTimeout = (2*maxtime < maxtime + 600)?2*maxtime: maxtime + 600;
//Do run
- snprintf(buffer, sizeof(buffer), "./run.sh deserializerun %s %u tuner%u result%u > log%u", problem->getProblem(), maxtime, execnum, execnum, execnum);
+ snprintf(buffer, sizeof(buffer), "timeout %u ./run.sh deserializerun %s %u tuner%u result%u > log%u", satuneTimeout, problem->getProblem(), maxtime, execnum, execnum, execnum);
+ model_print("Running: %s\n", buffer);
int status = system(buffer);
long long metric = -1;
myfile >> sat;
myfile.close();
}
- updateTimeout(problem, metric);
+ if(sat != IS_INDETER){
+ updateTimeout(problem, metric);
+ }
snprintf(buffer, sizeof(buffer), "tuner%uused", execnum);
tuner->getTuner()->addUsed(buffer);
+ } else if (status == 124 << 8) {// timeout happens ...
+ tuner->getTuner()->copySettingstoUsedSettings();
}
+
//Increment execution count
execnum++;
if (problem->getResult() == TUNERUNSETVALUE && sat != IS_INDETER) {
problem->setResult( sat );
} else if (problem->getResult() != sat && sat != IS_INDETER) {
- model_print("******** Result has changed ********\n");
+ model_print("******** Result has changed ******** Found a bug!!\n");
+ ASSERT(0);
}
if (sat == IS_INDETER && metric != -1) {//The case when we have a timeout
metric = -1;