From: bdemsky <bdemsky@uci.edu>
Date: Thu, 18 Oct 2018 18:35:53 +0000 (-0700)
Subject: Generally it is good not to have redundant information which introduces new consisten... 
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=9392806929b8fc95a9f9a65ffd22e6867911b420

Generally it is good not to have redundant information which introduces new consistency constraints
---

diff --git a/src/Tuner/multituner.cc b/src/Tuner/multituner.cc
index 64f67ae..9d8e121 100644
--- a/src/Tuner/multituner.cc
+++ b/src/Tuner/multituner.cc
@@ -11,11 +11,10 @@
 
 #define UNSETVALUE -1
 
-Problem::Problem(const char *_problem, uint _timeout) : 
+Problem::Problem(const char *_problem) :
 	problemnumber(-1),
-	result(UNSETVALUE) , 
-	besttime(std::numeric_limits<double>::infinity()),
-	timeout(_timeout)
+	result(UNSETVALUE),
+	besttime(LLONG_MAX)
 {
 	uint len = strlen(_problem);
 	problem = (char *) ourmalloc(len + 1);
@@ -56,7 +55,7 @@ MultiTuner::~MultiTuner() {
 }
 
 void MultiTuner::addProblem(const char *filename) {
-	Problem *p = new Problem(filename, timeout);
+	Problem *p = new Problem(filename);
 	p->problemnumber = problems.getSize();
 	problems.push(p);
 }
@@ -115,7 +114,7 @@ void MultiTuner::readData(uint numRuns) {
 		if (problems.getSize() <= problemnumber)
 			problems.setSize(problemnumber + 1);
 		if (problems.get(problemnumber) == NULL)
-			problems.set(problemnumber, new Problem(problemname, timeout));
+			problems.set(problemnumber, new Problem(problemname));
 		Problem *problem = problems.get(problemnumber);
 		long long metric = -1;
 		int sat = IS_INDETER;
@@ -179,8 +178,13 @@ long long MultiTuner::evaluate(Problem *problem, TunerRecord *tuner) {
 	snprintf(buffer, sizeof(buffer), "tuner%u", execnum);
 	tuner->getTuner()->serialize(buffer);
 
+	//compute timeout
+	uint timeinsecs = problem->besttime / NANOSEC;
+	uint adaptive = (timeinsecs > 30) ? timeinsecs * 5 : 150;
+	uint maxtime = (adaptive < timeout) ? adaptive : timeout;
+
 	//Do run
-	snprintf(buffer, sizeof(buffer), "./run.sh deserializerun %s %u tuner%u result%u > log%u", problem->getProblem(), problem->timeout, execnum, execnum, execnum);
+	snprintf(buffer, sizeof(buffer), "./run.sh deserializerun %s %u tuner%u result%u > log%u", problem->getProblem(), maxtime, execnum, execnum, execnum);
 	int status = system(buffer);
 
 	long long metric = -1;
@@ -211,27 +215,16 @@ long long MultiTuner::evaluate(Problem *problem, TunerRecord *tuner) {
 	} 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; 
+	if (sat == IS_INDETER && metric != -1) {//The case when we have a timeout
+		metric = -1;
 	}
 	return metric;
 }
 
-void MultiTuner::updateTimeout(Problem *problem, long long metric){
-	double currentTime= metric / NANOSEC;
-	if(currentTime < problem->besttime){
-		problem->besttime = currentTime;
-	}
-	uint adoptive;
-	if(problem->besttime > 30){
-		adoptive = problem->besttime * 5;
-	}else {
-		adoptive = 150;
-	}
-	if(adoptive < problem->timeout){
-		problem->timeout = adoptive;
+void MultiTuner::updateTimeout(Problem *problem, long long metric) {
+	if (metric < problem->besttime) {
+		problem->besttime = metric;
 	}
-	LOG("Timeout=%u\tadoptive%u\tcurrentTime=%f\n", problem->timeout, adoptive, currentTime);
 }
 
 void MultiTuner::tuneComp() {
diff --git a/src/Tuner/multituner.h b/src/Tuner/multituner.h
index 85b028b..1e878ee 100644
--- a/src/Tuner/multituner.h
+++ b/src/Tuner/multituner.h
@@ -7,7 +7,7 @@
 
 class Problem {
 public:
-	Problem(const char *problem, uint timeout);
+	Problem(const char *problem);
 	char *getProblem() {return problem;}
 	~Problem();
 	CMEMALLOC;
@@ -15,8 +15,7 @@ private:
 	int problemnumber;
 	int result;
 	char *problem;
-        double besttime;
-        uint timeout;
+	long long besttime;
 	friend class MultiTuner;
 };
 
@@ -44,7 +43,7 @@ public:
 	void addProblem(const char *filename);
 	void addTuner(SearchTuner *tuner);
 	void readData(uint numRuns);
-        void updateTimeout(Problem *problem, long long metric);
+	void updateTimeout(Problem *problem, long long metric);
 	void tuneK();
 	void tuneComp();
 	void printData();
diff --git a/src/common.h b/src/common.h
index 39d4ea4..879c1f2 100644
--- a/src/common.h
+++ b/src/common.h
@@ -41,7 +41,7 @@ extern int switch_alloc;
 #ifdef CONFIG_DEBUG
 #define DEBUG(fmt, ...) do { model_print("*** %15s:%-4d %25s() *** " fmt, __FILE__, __LINE__, __func__, ## __VA_ARGS__); } while (0)
 #define DBG() DEBUG("\n")
-#define LOG(fmt, ...) do{model_print(fmt, ## __VA_ARGS__);}while(0)
+#define LOG(fmt, ...) do {model_print(fmt, ## __VA_ARGS__);} while (0)
 #define DBG_ENABLED() (1)
 #else
 #define DEBUG(fmt, ...)