From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Thu, 18 Oct 2018 00:52:00 +0000 (-0700)
Subject: Adoptive timeout ...
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=e7c4e5bf8b7030d84af472b9fc81930b704dd9bd

Adoptive timeout ...
---

e7c4e5bf8b7030d84af472b9fc81930b704dd9bd
diff --cc src/Tuner/multituner.cc
index 3961d2b,a9fe693..ec8bcb7
--- a/src/Tuner/multituner.cc
+++ b/src/Tuner/multituner.cc
@@@ -39,7 -39,7 +39,7 @@@ TunerRecord *TunerRecord::changeTuner(S
  }
  
  MultiTuner::MultiTuner(uint _budget, uint _rounds, uint _timeout) :
--	budget(_budget), rounds(_rounds), timeout(_timeout), execnum(0) {
++	budget(_budget), rounds(_rounds), timeout(_timeout), besttime(_timeout), execnum(0) {
  }
  
  MultiTuner::~MultiTuner() {
@@@ -193,7 -193,7 +193,7 @@@ long long MultiTuner::evaluate(Problem 
  			myfile >> sat;
  			myfile.close();
  		}
--
++		updateTimeout(metric);
  		snprintf(buffer, sizeof(buffer), "tuner%uused", execnum);
  		tuner->getTuner()->addUsed(buffer);
  	}
@@@ -205,9 -205,9 +205,28 @@@
  	} else if (problem->result != sat && sat != IS_INDETER) {
  		model_print("******** Result has changed ********\n");
  	}
++	if(sat == IS_INDETER && metric != -1){ //The case when we have a timeout
++		metric = -1; 
++	}
  	return metric;
  }
  
++void MultiTuner::updateTimeout(long long metric){
++	double currentTime= metric / NANOSEC;
++	if(currentTime < besttime){
++		besttime = currentTime;
++	}
++	uint adoptive;
++	if(besttime > 30){
++		adoptive = besttime * 5;
++	}else {
++		adoptive = 150;
++	}
++	if(adoptive < timeout){
++		timeout = adoptive;
++	}
++}
++
  void MultiTuner::tuneComp() {
  	Vector<TunerRecord *> *tunerV = new Vector<TunerRecord *>(&tuners);
  	for (uint b = 0; b < budget; b++) {
@@@ -277,11 -277,11 +296,11 @@@
  				if (score > tscore)
  					break;
  			}
- 			LOG("ranking[%u]=tuner<%d>(Score=%d)\n", j, tuner->tunernumber, score);
- 			LOG("************************\n");
+ 			DEBUG("ranking[%u]=tuner<%p,%u>(Score=%d)\n", j, tuner, tuner->tunernumber, score);
+ 			DEBUG("************************\n");
  			ranking.insertAt(j, tuner);
  		}
 -		DEBUG("tunerSize=%u\trankingSize=%u\ttunerVSize=%u\n", tuners.getSize(), ranking.getSize(), tunerV->getSize());
 +		LOG("tunerSize=%u\trankingSize=%u\ttunerVSize=%u\n", tuners.getSize(), ranking.getSize(), tunerV->getSize());
  		for (uint i = tuners.getSize(); i < ranking.getSize(); i++) {
  			TunerRecord *tuner = ranking.get(i);
  			model_print("Removing tuner %u\n", tuner->tunernumber);
diff --cc src/Tuner/multituner.h
index 1c654eb,1c654eb..f566828
--- a/src/Tuner/multituner.h
+++ b/src/Tuner/multituner.h
@@@ -42,6 -42,6 +42,7 @@@ public
  	void addProblem(const char *filename);
  	void addTuner(SearchTuner *tuner);
  	void readData(uint numRuns);
++        void updateTimeout(long long metric);
  	void tuneK();
  	void tuneComp();
  	void printData();
@@@ -60,6 -60,6 +61,7 @@@ protected
  	uint budget;
  	uint rounds;
  	uint timeout;
++	double besttime;
  	int execnum;
  };
  #endif
diff --cc src/common.h
index 2b67e04,48b2a7e..39d4ea4
--- a/src/common.h
+++ b/src/common.h
@@@ -18,6 -18,6 +18,7 @@@
  #include "config.h"
  #include "time.h"
  
++#define NANOSEC 1000000000.0
  
  #if 0
  extern int model_out;
diff --cc src/csolver.cc
index 51f0943,51f0943..fbe0dd0
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@@ -577,7 -577,7 +577,6 @@@ void CSolver::inferFixedOrders() 
  	}
  }
  
--#define NANOSEC 1000000000.0
  int CSolver::solve() {
  	long long startTime = getTimeNano();
  	bool deleteTuner = false;