X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FTuner%2Fautotuner.cc;h=1bf29d82cb2e46a89fa6c9bbfaf29103d4b219b3;hb=ec4122e6d43e951feb8b344bf3511a50e08a3615;hp=9082ae4d027b950d4b713e8f5eeae8a05d91f7e9;hpb=d46ee65a6767e2016cab629220a60c3e39b366f1;p=satune.git

diff --git a/src/Tuner/autotuner.cc b/src/Tuner/autotuner.cc
index 9082ae4..1bf29d8 100644
--- a/src/Tuner/autotuner.cc
+++ b/src/Tuner/autotuner.cc
@@ -5,10 +5,14 @@
 #include <stdlib.h>
 #include <float.h>
 
+#define UNSETVALUE -1
+#define TIMEOUTSEC 5000
 AutoTuner::AutoTuner(uint _budget) :
-	budget(_budget) {
+	budget(_budget), result(UNSETVALUE) {
 }
 
+AutoTuner::~AutoTuner() {}
+
 void AutoTuner::addProblem(CSolver *solver) {
 	solvers.push(solver);
 }
@@ -16,14 +20,16 @@ void AutoTuner::addProblem(CSolver *solver) {
 long long AutoTuner::evaluate(CSolver *problem, SearchTuner *tuner) {
 	CSolver *copy = problem->clone();
 	copy->setTuner(tuner);
-	int result = copy->solve();
-	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);
+	copy->setSatSolverTimeout(TIMEOUTSEC);
+	model_print("**********************\n");
+	int sat = copy->solve();
+	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;
 }
@@ -41,8 +47,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);
@@ -52,7 +57,6 @@ SearchTuner *AutoTuner::mutateTuner(SearchTuner *oldTuner, uint k) {
 	return newTuner;
 }
 
-
 void AutoTuner::tune() {
 	SearchTuner *bestTuner = NULL;
 	double bestScore = DBL_MAX;
@@ -92,6 +96,7 @@ void AutoTuner::tune() {
 	}
 	model_print("Best tuner:\n");
 	bestTuner->print();
+	bestTuner->serialize("TUNER.conf");
 	model_print("Received score %f\n", bestScore);
 	if (bestTuner != NULL)
 		delete bestTuner;