Bug fixes

diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc
index 77709b6b0918fc63398ae5ddaf7fb98230caf1ad..db79c255247c3371b9c0c1b68b607b0f02014d42 100644 (file)
--- a/src/AST/boolean.cc
+++ b/src/AST/boolean.cc
@@ -50,7 +50,6 @@ Boolean *BooleanVar::clone(CSolver *solver, CloneMap *map) {
        Boolean *bvar = solver->getBooleanVar(type);
        map->put(this, bvar);
        return bvar;
-
 }
 
 Boolean *BooleanOrder::clone(CSolver *solver, CloneMap *map) {

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index bc247c2f558eaee155ddd2a091d7d8bdeede93ae..fb81e2f91c7c9e369cb718de26204fd448861cea 100644 (file)
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -21,7 +21,7 @@ class Boolean : public ASTNode {
 public:
        Boolean(ASTNodeType _type);
        virtual ~Boolean() {}
-       virtual Boolean *clone(CSolver *solver, CloneMap *map);
+       virtual Boolean *clone(CSolver *solver, CloneMap *map) { ASSERT(0); return NULL; }
        Polarity polarity;
        BooleanValue boolVal;
        Vector<Boolean *> parents;

diff --git a/src/AST/element.h b/src/AST/element.h
index 267f133f1beff89633bf4fffa540b2eb7ead6acf..d0cec9fbaaa5d262b61c4c419b40b904b61bde7c 100644 (file)
--- a/src/AST/element.h
+++ b/src/AST/element.h
@@ -16,7 +16,7 @@ public:
        virtual ~Element() {}
        Vector<ASTNode *> parents;
        ElementEncoding encoding;
-       virtual Element *clone(CSolver *solver, CloneMap *map);
+       virtual Element *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;};
        MEMALLOC;
 };
 

diff --git a/src/AST/function.h b/src/AST/function.h
index 6b0cd134f4660663e4d59e24f959f9a42a6e0029..0ed79cec7a09058f06be76ffd58c9582711df20f 100644 (file)
--- a/src/AST/function.h
+++ b/src/AST/function.h
@@ -12,7 +12,7 @@ public:
        Function(FunctionType _type) : type(_type) {}
        FunctionType type;
        virtual ~Function() {}
-       virtual Function *clone(CSolver *solver, CloneMap *map);
+       virtual Function *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;}
        MEMALLOC;
 };
 

diff --git a/src/AST/predicate.h b/src/AST/predicate.h
index 047ef138145328891d5b44cb9762ff2324248454..85ca7f1e798bc528359840d1b6d5e537406c2cbe 100644 (file)
--- a/src/AST/predicate.h
+++ b/src/AST/predicate.h
@@ -4,6 +4,7 @@
 #include "mymemory.h"
 #include "ops.h"
 #include "structs.h"
+#include "common.h"
 
 #define GETPREDICATETYPE(o) (((Predicate *)(o))->type)
 
@@ -11,7 +12,7 @@ class Predicate {
 public:
        Predicate(PredicateType _type) : type(_type) {}
        virtual ~Predicate() {}
-       virtual Predicate *clone(CSolver *solver, CloneMap *map);
+       virtual Predicate *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;}
        PredicateType type;
        MEMALLOC;
 };

diff --git a/src/ASTAnalyses/orderanalysis.cc b/src/ASTAnalyses/orderanalysis.cc
index 57443c12cee8136980058cc880596b226f62cced..60103759b0bfc61b5d060c412312c57cf3011b0f 100644 (file)
--- a/src/ASTAnalyses/orderanalysis.cc
+++ b/src/ASTAnalyses/orderanalysis.cc
@@ -84,15 +84,19 @@ bool isMustBeTrueNode(OrderNode *node) {
        HSIteratorOrderEdge *iterator = node->inEdges.iterator();
        while (iterator->hasNext()) {
                OrderEdge *edge = iterator->next();
-               if (!edge->mustPos)
+               if (!edge->mustPos) {
+                       delete iterator;
                        return false;
+               }
        }
        delete iterator;
        iterator = node->outEdges.iterator();
        while (iterator->hasNext()) {
                OrderEdge *edge = iterator->next();
-               if (!edge->mustPos)
+               if (!edge->mustPos) {
+                       delete iterator;
                        return false;
+               }
        }
        delete iterator;
        return true;

diff --git a/src/ASTTransform/orderdecompose.cc b/src/ASTTransform/orderdecompose.cc
index 9a60497ee39d009c6b2877877996f9e86bee5f46..15c6de61bef29eb4463baa9891500367f30960ce 100644 (file)
--- a/src/ASTTransform/orderdecompose.cc
+++ b/src/ASTTransform/orderdecompose.cc
@@ -79,7 +79,6 @@ void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
                BooleanOrder *orderconstraint = order->constraints.get(i);
                OrderNode *from = graph->getOrderNodeFromOrderGraph(orderconstraint->first);
                OrderNode *to = graph->getOrderNodeFromOrderGraph(orderconstraint->second);
-               model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
                if (from->sccNum != to->sccNum) {
                        OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
                        if (edge->polPos) {

diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
index 201d7dba172f77db67b0bfbfb1a9ae51ef5ba0c6..dd536e02e5989b7903eb872908194c1ec4f352f4 100644 (file)
--- a/src/Backend/constraint.cc
+++ b/src/Backend/constraint.cc
@@ -316,9 +316,11 @@ Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) {
 
 void addConstraintCNF(CNF *cnf, Edge constraint) {
        pushVectorEdge(&cnf->constraints, constraint);
+#ifdef CONFIG_DEBUG
        model_print("****ADDING NEW Constraint*****\n");
        printCNF(constraint);
        model_print("\n******************************\n");
+#endif
 }
 
 Edge constraintNewVar(CNF *cnf) {

diff --git a/src/Backend/inc_solver.cc b/src/Backend/inc_solver.cc
index 85528dc2c73d4a2d6a18ce12e86d236089f7a277..7d0fd6513d86379fb96385db7c67d654a157133f 100644 (file)
--- a/src/Backend/inc_solver.cc
+++ b/src/Backend/inc_solver.cc
@@ -180,7 +180,7 @@ bool first = true;
 void flushBufferSolver(IncrementalSolver *This) {
        ssize_t bytestowrite = sizeof(int) * This->offset;
        ssize_t byteswritten = 0;
-       //DEBUGGING CODE STARTS
+#ifdef CONFIG_DEBUG
        for (uint i = 0; i < This->offset; i++) {
                if (first)
                        printf("(");
@@ -194,7 +194,7 @@ void flushBufferSolver(IncrementalSolver *This) {
                        printf("%d", This->buffer[i]);
                }
        }
-       //DEBUGGING CODE ENDS
+#endif
        do {
                ssize_t n = write(This->to_solver_fd, &((char *)This->buffer)[byteswritten], bytestowrite);
                if (n == -1) {

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index 838170f69452d62967cf1b7511bcefc1462adbd9..b1eeb50a893e2b45d79b1efa4423b872e66d94e9 100644 (file)
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -31,9 +31,13 @@ void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
        HSIteratorBoolean *iterator = csolver->getConstraints();
        while (iterator->hasNext()) {
                Boolean *constraint = iterator->next();
+#ifdef CONFIG_DEBUG
                model_print("Encoding All ...\n\n");
+#endif
                Edge c = encodeConstraintSATEncoder(constraint);
+#ifdef CONFIG_DEBUG
                model_print("Returned Constraint in EncodingAll:\n");
+#endif
                ASSERT( !equalsEdge(c, E_BOGUS));
                addConstraintCNF(cnf, c);
        }

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index d750c9ec6c465e16286f663328466323328c5b5f..b6bce0182a64004a73ef447d9b4e880665c3ce05 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -33,7 +33,6 @@ class SATEncoder {
        Edge getElementValueBinaryIndexConstraint(Element *element, uint64_t value);
        Edge getElementValueBinaryValueConstraint(Element *element, uint64_t value);
        Edge getElementValueConstraint(Element *element, uint64_t value);
-       void allocElementConstraintVariables(ElementEncoding *ee, uint numVars);
        void generateOneHotEncodingVars(ElementEncoding *encoding);
        void generateUnaryEncodingVars(ElementEncoding *encoding);
        void generateBinaryIndexEncodingVars(ElementEncoding *encoding);
@@ -60,5 +59,6 @@ class SATEncoder {
        CSolver *solver;
 };
 
+void allocElementConstraintVariables(ElementEncoding *ee, uint numVars);
 Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair);
 #endif

diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc
index 750be42a73d954bd53d57fbc945850393954a57e..3bff52bd885f02410c599c7ef4bcd5b20f4a1a2d 100644 (file)
--- a/src/Backend/satorderencoder.cc
+++ b/src/Backend/satorderencoder.cc
@@ -25,7 +25,7 @@ Edge SATEncoder::encodeOrderSATEncoder(BooleanOrder *constraint) {
        return E_BOGUS;
 }
 
-Edge inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _second) {
+Edge SATEncoder::inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _second) {
        if (order->graph != NULL) {
                OrderGraph *graph = order->graph;
                OrderNode *first = graph->lookupOrderNodeFromOrderGraph(_first);
@@ -93,7 +93,7 @@ Edge SATEncoder::encodeTotalOrderSATEncoder(BooleanOrder *boolOrder) {
 
 
 void SATEncoder::createAllTotalOrderConstraintsSATEncoder(Order *order) {
-#ifdef TRACE_DEBUG
+#ifdef CONFIG_DEBUG
        model_print("in total order ...\n");
 #endif
        ASSERT(order->type == TOTAL);

diff --git a/src/Test/ordergraphtest.cc b/src/Test/ordergraphtest.cc
index 4562176d0bc937a9ac79669f98a16dc0dce5b090..c6f59186ca2013559a1c113aa083f8545484644a 100644 (file)
--- a/src/Test/ordergraphtest.cc
+++ b/src/Test/ordergraphtest.cc
@@ -16,24 +16,41 @@ int main(int numargs, char **argv) {
        Boolean *o58 =  solver->orderConstraint(order, 5, 8);
        Boolean *o81 =  solver->orderConstraint(order, 8, 1);
 
-       /* Not Valid c++...Let Hamed fix...
-          addConstraint(solver, applyLogicalOperation(solver, L_OR,(Boolean *[]) {o12, o13, o24, o34}, 4) );
-          Boolean *b1 = applyLogicalOperation(solver, L_XOR, (Boolean *[]) {o41, o57}, 2);
-          Boolean *o34n = applyLogicalOperation(solver, L_NOT, (Boolean *[]) {o34}, 1);
-          Boolean *o24n = applyLogicalOperation(solver, L_NOT, (Boolean *[]) {o24}, 1);
-          Boolean *b2 = applyLogicalOperation(solver, L_OR, (Boolean *[]) {o34n, o24n}, 2);
-          addConstraint(solver, applyLogicalOperation(solver, L_IMPLIES,(Boolean *[]) {b1, b2}, 2) );
-          addConstraint(solver, applyLogicalOperation(solver, L_AND,(Boolean *[]) {o12, o13}, 2) );
-          addConstraint(solver, applyLogicalOperation(solver, L_OR,(Boolean *[]) {o76, o65}, 2) );
-          Boolean* b3= applyLogicalOperation(solver, L_AND,(Boolean *[]) {o76, o65}, 2) ;
-          Boolean* o57n= applyLogicalOperation(solver, L_NOT,(Boolean *[]) {o57}, 1);
-          addConstraint(solver, applyLogicalOperation(solver, L_IMPLIES,(Boolean *[]) {b3, o57n}, 2) );
-          addConstraint(solver, applyLogicalOperation(solver, L_AND,(Boolean *[]) {o58, o81}, 2) );
+       Boolean * array1[]={o12, o13, o24, o34};
+       solver->addConstraint(solver->applyLogicalOperation(L_OR, array1, 4) );
+       Boolean * array2[]={o41, o57};
+       
+       Boolean *b1 = solver->applyLogicalOperation(L_XOR, array2, 2);
+       Boolean * array3[]={o34};
+       Boolean *o34n = solver->applyLogicalOperation(L_NOT, array3, 1);
+       Boolean * array4[]={o24};
+       Boolean *o24n = solver->applyLogicalOperation(L_NOT, array4, 1);
+       Boolean * array5[]={o34n, o24n};
+       Boolean *b2 = solver->applyLogicalOperation(L_OR, array5, 2);
+       Boolean * array6[] = {b1, b2};
+       solver->addConstraint(solver->applyLogicalOperation(L_IMPLIES, array6, 2) );
 
-          if (solver->startEncoding() == 1)
-          printf("SAT\n");
-          else
-          printf("UNSAT\n");
-        */
+       Boolean * array7[] = {o12, o13};
+       solver->addConstraint(solver->applyLogicalOperation(L_AND, array7, 2) );
+
+       Boolean * array8[] = {o76, o65};
+       solver->addConstraint(solver->applyLogicalOperation(L_OR, array8, 2) );
+
+       Boolean * array9[] = {o76, o65};
+       Boolean* b3= solver->applyLogicalOperation(L_AND, array9, 2) ;
+       Boolean * array10[] = {o57};
+       Boolean* o57n= solver->applyLogicalOperation(L_NOT, array10, 1);
+       Boolean * array11[] = {b3, o57n};
+       solver->addConstraint(solver->applyLogicalOperation(L_IMPLIES, array11, 2));
+
+       Boolean * array12[] = {o58, o81};
+       solver->addConstraint(solver->applyLogicalOperation(L_AND, array12, 2) );
+       
+       /*      if (solver->startEncoding() == 1)
+               printf("SAT\n");
+       else
+       printf("UNSAT\n");*/
+       
+       solver->autoTune(100);
        delete solver;
 }

diff --git a/src/Tuner/autotuner.cc b/src/Tuner/autotuner.cc
index 78d16c82f78911c7b42e4790b193dde72d2ab818..f4509677eed754d27d63ed2bb8cea63d929f1a46 100644 (file)
--- a/src/Tuner/autotuner.cc
+++ b/src/Tuner/autotuner.cc
@@ -21,6 +21,9 @@ long long AutoTuner::evaluate(CSolver * problem, SearchTuner *tuner) {
        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);
        delete copy;
        return metric;
 }
@@ -61,8 +64,12 @@ void AutoTuner::tune() {
        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
                if (newScore < bestScore) {
+                       if (bestTuner != NULL)
+                               delete bestTuner;
                        bestScore = newScore;
                        bestTuner = newTuner->copyUsed();
                }
@@ -76,10 +83,17 @@ void AutoTuner::tune() {
                }
                double ran = ((double)random()) / RAND_MAX;
                if (ran <= acceptanceP) {
+                       delete oldTuner;
                        oldScore = newScore;
                        oldTuner = newTuner;
                } else {
                        delete newTuner;
                }
        }
+       model_print("Best tuner:\n");
+       bestTuner->print();
+       model_print("Received score %f\n", bestScore);
+       if (bestTuner != NULL)
+               delete bestTuner;
+       delete oldTuner;
 }

diff --git a/src/Tuner/searchtuner.cc b/src/Tuner/searchtuner.cc
index e964f4564471609f7bdd17f2f34ef9dd54af9aff..045920628620bf9bf526e95375486ba011f81475 100644 (file)
--- a/src/Tuner/searchtuner.cc
+++ b/src/Tuner/searchtuner.cc
@@ -32,7 +32,7 @@ void TunableSetting::setDecision(int _low, int _high, int _default, int _selecti
 
 void TunableSetting::print() {
        if (hasVar) {
-               model_print("Type %llu, ", type);
+               model_print("Type %" PRIu64 ", ", type);
        }
        model_print("Param %u = %u\n", param, selectedValue);
 }
@@ -105,8 +105,8 @@ int SearchTuner::getVarTunable(VarType vartype, TunableParam param, TunableDesc
 
 void SearchTuner::randomMutate() {
        TunableSetting * randomSetting = settings.getRandomElement();
-       uint range=randomSetting->highValue-randomSetting->lowValue;
-       uint randomchoice=(random() % range) + randomSetting->lowValue;
+       int range=randomSetting->highValue-randomSetting->lowValue;
+       int randomchoice=(random() % range) + randomSetting->lowValue;
        if (randomchoice < randomSetting->selectedValue)
                randomSetting->selectedValue = randomchoice;
        else

diff --git a/src/Tuner/tunable.h b/src/Tuner/tunable.h
index 8d696af0c58197576697beb64ada3e9f43482e15..a1e165a3cf6afa21b5b68dd8079e4390b7303755 100644 (file)
--- a/src/Tuner/tunable.h
+++ b/src/Tuner/tunable.h
@@ -1,13 +1,13 @@
 #ifndef TUNABLE_H
 #define TUNABLE_H
 #include "classlist.h"
-
+#include "common.h"
 
 class Tuner {
 public:
-       virtual int getTunable(TunableParam param, TunableDesc *descriptor);
-       virtual int getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor);
-       virtual ~Tuner();
+       virtual int getTunable(TunableParam param, TunableDesc *descriptor) {ASSERT(0); return 0;}
+       virtual int getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor) {ASSERT(0); return 0;}
+       virtual ~Tuner() {}
        MEMALLOC;
 };
 

diff --git a/src/csolver.cc b/src/csolver.cc
index a9a4f624820e6f64adfdb145750c4378399a62b4..3fd77a3b45145c415dca79d64edf24dcdb58aea2 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -16,7 +16,7 @@
 
 CSolver::CSolver() :
        unsat(false),
-       tuner(new DefaultTuner()),
+       tuner(NULL),
        elapsedTime(0)
 {
        satEncoder = new SATEncoder(this);
@@ -61,7 +61,6 @@ CSolver::~CSolver() {
        }
 
        delete satEncoder;
-       delete tuner;
 }
 
 CSolver *CSolver::clone() {
@@ -70,7 +69,7 @@ CSolver *CSolver::clone() {
        HSIteratorBoolean *it = getConstraints();
        while (it->hasNext()) {
                Boolean *b = it->next();
-               b->clone(copy, &map);
+               copy->addConstraint(b->clone(copy, &map));
        }
        delete it;
        return copy;
@@ -202,6 +201,12 @@ Boolean *CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second)
 }
 
 int CSolver::startEncoding() {
+       bool deleteTuner = false;
+       if (tuner == NULL) {
+               tuner = new DefaultTuner();
+               deleteTuner = true;
+       }
+               
        long long startTime = getTimeNano();
        computePolarities(this);
        orderAnalysis(this);
@@ -210,6 +215,10 @@ int CSolver::startEncoding() {
        int result = satEncoder->solve();
        long long finishTime = getTimeNano();
        elapsedTime = finishTime - startTime;
+       if (deleteTuner) {
+               delete tuner;
+               tuner = NULL;
+       }
        return result;
 }
 
@@ -247,4 +256,5 @@ void CSolver::autoTune(uint budget) {
        AutoTuner * autotuner=new AutoTuner(budget);
        autotuner->addProblem(this);
        autotuner->tune();
+       delete autotuner;
 }