Generally it is good not to have redundant information which introduces new consisten...

diff --git a/src/Tuner/multituner.cc b/src/Tuner/multituner.cc
index 64f67aed459a93601886b0b21486e676115828b9..9d8e12129a522229e17da12341441e25525aa09d 100644 (file)
--- 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 85b028bc930b3e137eb586ba6ea5975239af8674..1e878eee0c2399a1686c1fb70b39a32a6680cccb 100644 (file)
--- 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 39d4ea4912675af08b3aee24a52a1ec44b53038a..879c1f2cf40613a7e3333a101a8d6f2be2ceba16 100644 (file)
--- 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, ...)