Commiting my local changes ...

[satune.git] / src / Tuner / autotuner.cc

diff --git a/src/Tuner/autotuner.cc b/src/Tuner/autotuner.cc
index e5ec2fb7839bf30c4749147a7202948f2963d19b..29c3289ec2d371f71f9e47f0ea2745e8ee71e023 100644 (file)
--- a/src/Tuner/autotuner.cc
+++ b/src/Tuner/autotuner.cc
@@ -4,8 +4,51 @@
 #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), result(UNSETVALUE) {
@@ -18,22 +61,23 @@ void AutoTuner::addProblem(CSolver *solver) {
 long long AutoTuner::evaluate(CSolver *problem, SearchTuner *tuner) {
        CSolver *copy = problem->clone();
        copy->setTuner(tuner);
-        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);
+       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;
 }
@@ -51,8 +95,7 @@ double AutoTuner::evaluateAll(SearchTuner *tuner) {
 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);