after merge (mostly tabbing issues)
[satune.git] / src / Tuner / autotuner.cc
index 9082ae4d027b950d4b713e8f5eeae8a05d91f7e9..ff3aa3f9f81b16b0ea368af69fbf94c72497e028 100644 (file)
@@ -5,8 +5,10 @@
 #include <stdlib.h>
 #include <float.h>
 
+#define UNSETVALUE -1
+
 AutoTuner::AutoTuner(uint _budget) :
-       budget(_budget) {
+       budget(_budget), result(UNSETVALUE) {
 }
 
 void AutoTuner::addProblem(CSolver *solver) {
@@ -16,14 +18,22 @@ 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("**********************\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 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("Elapsed Time: %llu\n", elapsedTime);
+//     model_print("Encode Time: %llu\n", encodeTime);
+//     model_print("Solve Time: %llu\n", solveTime);
        delete copy;
        return metric;
 }
@@ -92,6 +102,7 @@ void AutoTuner::tune() {
        }
        model_print("Best tuner:\n");
        bestTuner->print();
+       bestTuner->serialize();
        model_print("Received score %f\n", bestScore);
        if (bestTuner != NULL)
                delete bestTuner;