From: Brian Demsky Date: Mon, 28 Aug 2017 23:30:16 +0000 (-0700) Subject: Bug fixes X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=3b751b303da242b1ebb2b7d4f2e7377d2c47e045 Bug fixes --- diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc index 77709b6..db79c25 100644 --- 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 bc247c2..fb81e2f 100644 --- 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 parents; diff --git a/src/AST/element.h b/src/AST/element.h index 267f133..d0cec9f 100644 --- a/src/AST/element.h +++ b/src/AST/element.h @@ -16,7 +16,7 @@ public: virtual ~Element() {} Vector 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 6b0cd13..0ed79ce 100644 --- 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 047ef13..85ca7f1 100644 --- 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 57443c1..6010375 100644 --- 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 9a60497..15c6de6 100644 --- 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 201d7db..dd536e0 100644 --- 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 85528dc..7d0fd65 100644 --- 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 838170f..b1eeb50 100644 --- 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 d750c9e..b6bce01 100644 --- 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 750be42..3bff52b 100644 --- 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 4562176..c6f5918 100644 --- 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 78d16c8..f450967 100644 --- 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;iprintUsed(); + 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 e964f45..0459206 100644 --- 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 8d696af..a1e165a 100644 --- 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 a9a4f62..3fd77a3 100644 --- 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; }