Bug fixes
authorBrian Demsky <bdemsky@uci.edu>
Mon, 28 Aug 2017 23:30:16 +0000 (16:30 -0700)
committerbdemsky <bdemsky@uci.edu>
Mon, 28 Aug 2017 23:30:25 +0000 (16:30 -0700)
17 files changed:
src/AST/boolean.cc
src/AST/boolean.h
src/AST/element.h
src/AST/function.h
src/AST/predicate.h
src/ASTAnalyses/orderanalysis.cc
src/ASTTransform/orderdecompose.cc
src/Backend/constraint.cc
src/Backend/inc_solver.cc
src/Backend/satencoder.cc
src/Backend/satencoder.h
src/Backend/satorderencoder.cc
src/Test/ordergraphtest.cc
src/Tuner/autotuner.cc
src/Tuner/searchtuner.cc
src/Tuner/tunable.h
src/csolver.cc

index 77709b6..db79c25 100644 (file)
@@ -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) {
index bc247c2..fb81e2f 100644 (file)
@@ -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;
index 267f133..d0cec9f 100644 (file)
@@ -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;
 };
 
index 6b0cd13..0ed79ce 100644 (file)
@@ -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;
 };
 
index 047ef13..85ca7f1 100644 (file)
@@ -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;
 };
index 57443c1..6010375 100644 (file)
@@ -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;
index 9a60497..15c6de6 100644 (file)
@@ -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) {
index 201d7db..dd536e0 100644 (file)
@@ -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) {
index 85528dc..7d0fd65 100644 (file)
@@ -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) {
index 838170f..b1eeb50 100644 (file)
@@ -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);
        }
index d750c9e..b6bce01 100644 (file)
@@ -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
index 750be42..3bff52b 100644 (file)
@@ -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);
index 4562176..c6f5918 100644 (file)
@@ -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;
 }
index 78d16c8..f450967 100644 (file)
@@ -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;
 }
index e964f45..0459206 100644 (file)
@@ -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
index 8d696af..a1e165a 100644 (file)
@@ -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;
 };
 
index a9a4f62..3fd77a3 100644 (file)
@@ -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;
 }