#include <float.h>
#define UNSETVALUE -1
-
+#define TIMEOUTSEC 5000
AutoTuner::AutoTuner(uint _budget) :
budget(_budget), result(UNSETVALUE) {
}
+AutoTuner::~AutoTuner() {}
+
void AutoTuner::addProblem(CSolver *solver) {
solvers.push(solver);
}
long long AutoTuner::evaluate(CSolver *problem, SearchTuner *tuner) {
CSolver *copy = problem->clone();
copy->setTuner(tuner);
- model_print("**********************\n");
+ copy->setSatSolverTimeout(TIMEOUTSEC);
+ model_print("**********************\n");
int sat = copy->solve();
- if(result == UNSETVALUE)
- result = sat;
- else if(result != sat){
- model_print("&&&&&&&&&&&&&&&&&& Result has changed &&&&&&&&&&&&&\n");
- copy->printConstraints();
- }
- //model_print("SAT %d\n", result);
- long long elapsedTime = copy->getElapsedTime();
-// long long encodeTime = copy->getEncodeTime();
-// long long solveTime = copy->getSolveTime();
- long long metric = elapsedTime;
-// model_print("Elapsed Time: %llu\n", elapsedTime);
-// model_print("Encode Time: %llu\n", encodeTime);
-// model_print("Solve Time: %llu\n", solveTime);
+ if (result == UNSETVALUE && sat != IS_INDETER)
+ result = sat;
+ else if (result != sat && sat != IS_INDETER) {
+ model_print("&&&&&&&&&&&&&&&&&& Result has changed &&&&&&&&&&&&&\n");
+ copy->printConstraints();
+ }
+ long long metric = copy->getElapsedTime();
delete copy;
return metric;
}
SearchTuner *AutoTuner::mutateTuner(SearchTuner *oldTuner, uint k) {
SearchTuner *newTuner = oldTuner->copyUsed();
uint numSettings = oldTuner->getSize();
- double factor = 0.3;//Adjust this factor...
- uint settingsToMutate = (uint)(factor * (((double)numSettings) * (budget - k)) / (budget));
+ uint settingsToMutate = (uint)(AUTOTUNERFACTOR * (((double)numSettings) * (budget - k)) / (budget));
if (settingsToMutate < 1)
settingsToMutate = 1;
model_print("Mutating %u settings\n", settingsToMutate);
return newTuner;
}
-
void AutoTuner::tune() {
SearchTuner *bestTuner = NULL;
double bestScore = DBL_MAX;
}
model_print("Best tuner:\n");
bestTuner->print();
- bestTuner->serialize();
+ bestTuner->serialize("TUNER.conf");
model_print("Received score %f\n", bestScore);
if (bestTuner != NULL)
delete bestTuner;