X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FTuner%2Fautotuner.cc;h=857b21cf6a5ad3c935d26f63a2d0d2b8e3db5191;hp=e9bd7731e1b5030e97eb3c786c5312d322558bd8;hb=9eb16333c26996a97567f88d0f2e62e72eb9a9e6;hpb=5a644b3c50aadf6c0a1cfdb06dd1fbed8375d955

diff --git a/src/Tuner/autotuner.cc b/src/Tuner/autotuner.cc
index e9bd773..857b21c 100644
--- a/src/Tuner/autotuner.cc
+++ b/src/Tuner/autotuner.cc
@@ -5,68 +5,92 @@
 #include <stdlib.h>
 #include <float.h>
 
+#define UNSETVALUE -1
+#define TIMEOUTSEC 5000
 AutoTuner::AutoTuner(uint _budget) :
-	budget(_budget) {
+	budget(_budget), result(UNSETVALUE) {
 }
 
 void AutoTuner::addProblem(CSolver *solver) {
 	solvers.push(solver);
 }
 
-long long AutoTuner::evaluate(CSolver * problem, SearchTuner *tuner) {
-	CSolver * copy=problem->clone();
+long long AutoTuner::evaluate(CSolver *problem, SearchTuner *tuner) {
+	CSolver *copy = problem->clone();
 	copy->setTuner(tuner);
-	int result = copy->startEncoding();
-	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;
 }
 
 double AutoTuner::evaluateAll(SearchTuner *tuner) {
-	double product=1;
-	for(uint i=0;i<solvers.getSize();i++) {
-		CSolver * problem=solvers.get(i);
-		double score=evaluate(problem, tuner);
-		product*=score;
+	double product = 1;
+	for (uint i = 0; i < solvers.getSize(); i++) {
+		CSolver *problem = solvers.get(i);
+		double score = evaluate(problem, tuner);
+		product *= score;
 	}
-	return pow(product, 1/((double)solvers.getSize()));
+	return pow(product, 1 / ((double)solvers.getSize()));
 }
 
-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));
+SearchTuner *AutoTuner::mutateTuner(SearchTuner *oldTuner, uint k) {
+	SearchTuner *newTuner = oldTuner->copyUsed();
+	uint numSettings = oldTuner->getSize();
+	uint settingsToMutate = (uint)(AUTOTUNERFACTOR * (((double)numSettings) * (budget - k)) / (budget));
 	if (settingsToMutate < 1)
-		settingsToMutate=1;
+		settingsToMutate = 1;
 	model_print("Mutating %u settings\n", settingsToMutate);
-	while(settingsToMutate-- != 0) {
+	while (settingsToMutate-- != 0) {
 		newTuner->randomMutate();
 	}
 	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;
-	double bestScore=DBL_MAX;
+	SearchTuner *bestTuner = NULL;
+	double bestScore = DBL_MAX;
 
-	SearchTuner * oldTuner=new SearchTuner();
-	double base_temperature=evaluateAll(oldTuner);
-	double oldScore=base_temperature;
+	SearchTuner *oldTuner = new SearchTuner();
+	double base_temperature = evaluateAll(oldTuner);
+	double oldScore = base_temperature;
 
-	for (uint i=0;i<budget;i++) {
-		SearchTuner *newTuner=mutateTuner(oldTuner, i);
-		double newScore=evaluateAll(newTuner);
+#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);
 		newTuner->printUsed();
 		model_print("Received score %f\n", newScore);
-		double scoreDiff=newScore - oldScore; //smaller is better
+		double scoreDiff = newScore - oldScore;	//smaller is better
 		if (newScore < bestScore) {
 			if (bestTuner != NULL)
 				delete bestTuner;
@@ -78,7 +102,7 @@ void AutoTuner::tune() {
 		if (scoreDiff < 0) {
 			acceptanceP = 1;
 		} else {
-			double currTemp=base_temperature * (((double)budget - i) / budget);
+			double currTemp = base_temperature * (((double)budget - i) / budget);
 			acceptanceP = exp(-scoreDiff / currTemp);
 		}
 		double ran = ((double)random()) / RAND_MAX;
@@ -92,6 +116,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;