Adding a directed search based config for the tuner
[satune.git] / src / Tuner / autotuner.cc
index e5ec2fb7839bf30c4749147a7202948f2963d19b..857b21cf6a5ad3c935d26f63a2d0d2b8e3db5191 100644 (file)
@@ -6,7 +6,7 @@
 #include <float.h>
 
 #define UNSETVALUE -1
-
+#define TIMEOUTSEC 5000
 AutoTuner::AutoTuner(uint _budget) :
        budget(_budget), result(UNSETVALUE) {
 }
@@ -18,22 +18,16 @@ void AutoTuner::addProblem(CSolver *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;
 }
@@ -51,8 +45,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);
@@ -62,6 +55,13 @@ SearchTuner *AutoTuner::mutateTuner(SearchTuner *oldTuner, uint k) {
        return newTuner;
 }
 
+#ifdef STATICENCGEN
+SearchTuner *AutoTuner::mutateTuner(SearchTuner *oldTuner) {
+       SearchTuner *newTuner = oldTuner->copyUsed();
+       result = newTuner->nextStaticTuner();
+       return result==EXIT_FAILURE? newTuner: NULL;
+}
+#endif
 
 void AutoTuner::tune() {
        SearchTuner *bestTuner = NULL;
@@ -71,6 +71,20 @@ void AutoTuner::tune() {
        double base_temperature = evaluateAll(oldTuner);
        double oldScore = base_temperature;
 
+#ifdef STATICENCGEN
+       while(true){
+               SearchTuner *newTuner = mutateTuner(oldTuner);
+               if(newTuner == NULL)
+                       return;
+               double newScore = evaluateAll(newTuner);
+               newTuner->printUsed();
+               model_print("Received score %f\n", newScore);
+               delete oldTuner;
+               oldScore = newScore;
+               oldTuner = newTuner;
+       }
+#endif
+       
        for (uint i = 0; i < budget; i++) {
                SearchTuner *newTuner = mutateTuner(oldTuner, i);
                double newScore = evaluateAll(newTuner);