From: Brian Demsky <bdemsky@uci.edu>
Date: Mon, 28 Aug 2017 23:30:16 +0000 (-0700)
Subject: Bug fixes
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=3b751b303da242b1ebb2b7d4f2e7377d2c47e045;p=satune.git
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<Boolean *> 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<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 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;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 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;
}