#include <math.h>
#include <stdlib.h>
#include <float.h>
+#include <iostream>
+#include <chrono>
+#include <thread>
+#include <mutex>
+#include <condition_variable>
+
+#define TIMEOUT 1000s
+#define UNSETVALUE -1
+#define POSINFINITY 9999999999L
+
+using namespace std::chrono_literals;
+
+int solve(CSolver *solver)
+{
+ try{
+ return solver->solve();
+ }
+ catch(std::runtime_error& e) {
+ return UNSETVALUE;
+ }
+}
+
+int solveWrapper(CSolver *solver)
+{
+ std::mutex m;
+ std::condition_variable cv;
+ int retValue;
+
+ std::thread t([&cv, &retValue, solver]()
+ {
+ retValue = solve(solver);
+ cv.notify_one();
+ });
+
+ t.detach();
+
+ {
+ std::unique_lock<std::mutex> l(m);
+ if(cv.wait_for(l, TIMEOUT) == std::cv_status::timeout)
+ throw std::runtime_error("Timeout");
+ }
+
+ return retValue;
+}
+
AutoTuner::AutoTuner(uint _budget) :
- budget(_budget) {
+ budget(_budget), result(UNSETVALUE) {
}
void AutoTuner::addProblem(CSolver *solver) {
long long AutoTuner::evaluate(CSolver *problem, SearchTuner *tuner) {
CSolver *copy = problem->clone();
copy->setTuner(tuner);
- int result = copy->solve();
- 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);
+ model_print("**********************\n");
+ long long metric = 0L;
+ try {
+ int sat = solveWrapper(copy);
+ if (result == UNSETVALUE)
+ result = sat;
+ else if (result != sat) {
+ model_print("&&&&&&&&&&&&&&&&&& Result has changed &&&&&&&&&&&&&\n");
+ copy->printConstraints();
+ }
+ metric = copy->getElapsedTime();
+ }
+ catch(std::runtime_error& e) {
+ metric = POSINFINITY;
+ model_print("TimeOut has hit\n");
+ }
+
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);
}
model_print("Best tuner:\n");
bestTuner->print();
+ bestTuner->serialize();
model_print("Received score %f\n", bestScore);
if (bestTuner != NULL)
delete bestTuner;