From: bdemsky Date: Sat, 2 Sep 2017 06:47:41 +0000 (-0700) Subject: Restructure transforms a little and run make tabbing X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=d46ee65a6767e2016cab629220a60c3e39b366f1;p=satune.git Restructure transforms a little and run make tabbing --- diff --git a/src/AST/asthash.cc b/src/AST/asthash.cc index 503ca0e..9fed236 100644 --- a/src/AST/asthash.cc +++ b/src/AST/asthash.cc @@ -4,29 +4,29 @@ #include "boolean.h" #include "element.h" -bool compareArray(Array * inputs1, Array *inputs2) { +bool compareArray(Array *inputs1, Array *inputs2) { if (inputs1->getSize() != inputs2->getSize()) return false; - for(uint i=0;igetSize();i++) { + for (uint i = 0; i < inputs1->getSize(); i++) { if (inputs1->get(i) != inputs2->get(i)) return false; } return true; } -bool compareArray(Array * inputs1, Array *inputs2) { +bool compareArray(Array *inputs1, Array *inputs2) { if (inputs1->getSize() != inputs2->getSize()) return false; - for(uint i=0;igetSize();i++) { + for (uint i = 0; i < inputs1->getSize(); i++) { if (inputs1->get(i) != inputs2->get(i)) return false; } return true; } -uint hashArray(Array * inputs) { +uint hashArray(Array *inputs) { uint hash = inputs->getSize(); - for(uint i=0;igetSize();i++) { + for (uint i = 0; i < inputs->getSize(); i++) { uint newval = (uint)(uintptr_t) inputs->get(i); hash ^= newval; hash = (hash << 3) | (hash >> 29); @@ -34,9 +34,9 @@ uint hashArray(Array * inputs) { return hash; } -uint hashArray(Array * inputs) { +uint hashArray(Array *inputs) { uint hash = inputs->getSize(); - for(uint i=0;igetSize();i++) { + for (uint i = 0; i < inputs->getSize(); i++) { uint newval = (uint)(uintptr_t) inputs->get(i); hash ^= newval; hash = (hash << 3) | (hash >> 29); @@ -44,24 +44,24 @@ uint hashArray(Array * inputs) { return hash; } -uint hashBoolean(Boolean * b) { - switch(b->type) { +uint hashBoolean(Boolean *b) { + switch (b->type) { case ORDERCONST: { - BooleanOrder * o=(BooleanOrder *)b; + BooleanOrder *o = (BooleanOrder *)b; return ((uint)(uintptr_t) o->order) ^ ((uint) o->first) ^ (((uint)(o->second)) << 2); } case BOOLEANVAR: { return (uint)(uintptr_t) b; } case LOGICOP: { - BooleanLogic * l=(BooleanLogic *)b; + BooleanLogic *l = (BooleanLogic *)b; return ((uint)l->op) ^ hashArray(&l->inputs); } case PREDICATEOP: { - BooleanPredicate * p=(BooleanPredicate *)b; + BooleanPredicate *p = (BooleanPredicate *)b; return ((uint)(uintptr_t) p->predicate) ^ - (((uint)(uintptr_t) p->undefStatus) << 1) ^ - hashArray(&p->inputs); + (((uint)(uintptr_t) p->undefStatus) << 1) ^ + hashArray(&p->inputs); } default: ASSERT(0); @@ -71,26 +71,26 @@ uint hashBoolean(Boolean * b) { bool compareBoolean(Boolean *b1, Boolean *b2) { if (b1->type != b2->type) return false; - switch(b1->type) { + switch (b1->type) { case ORDERCONST: { - BooleanOrder * o1=(BooleanOrder *)b1; - BooleanOrder * o2=(BooleanOrder *)b2; + BooleanOrder *o1 = (BooleanOrder *)b1; + BooleanOrder *o2 = (BooleanOrder *)b2; return (o1->order == o2->order) && (o1->first == o2->first) && (o1->second == o2->second); } case BOOLEANVAR: { return b1 == b2; } case LOGICOP: { - BooleanLogic * l1=(BooleanLogic *)b1; - BooleanLogic * l2=(BooleanLogic *)b2; + BooleanLogic *l1 = (BooleanLogic *)b1; + BooleanLogic *l2 = (BooleanLogic *)b2; return (l1->op == l2->op) && compareArray(&l1->inputs, &l2->inputs); } case PREDICATEOP: { - BooleanPredicate * p1=(BooleanPredicate *)b1; - BooleanPredicate * p2=(BooleanPredicate *)b2; + BooleanPredicate *p1 = (BooleanPredicate *)b1; + BooleanPredicate *p2 = (BooleanPredicate *)b2; return (p1->predicate == p2->predicate) && - p1->undefStatus == p2->undefStatus && - compareArray(&p1->inputs, &p2->inputs); + p1->undefStatus == p2->undefStatus && + compareArray(&p1->inputs, &p2->inputs); } default: ASSERT(0); @@ -98,18 +98,18 @@ bool compareBoolean(Boolean *b1, Boolean *b2) { } uint hashElement(Element *e) { - switch(e->type) { + switch (e->type) { case ELEMSET: { return (uint)(uintptr_t) e; } case ELEMFUNCRETURN: { - ElementFunction * ef=(ElementFunction *) e; + ElementFunction *ef = (ElementFunction *) e; return ((uint)(uintptr_t) ef->function) ^ - ((uint)(uintptr_t) ef->overflowstatus) ^ - hashArray(&ef->inputs); + ((uint)(uintptr_t) ef->overflowstatus) ^ + hashArray(&ef->inputs); } case ELEMCONST: { - ElementConst * ec=(ElementConst *) e; + ElementConst *ec = (ElementConst *) e; return ((uint) ec->value); } default: @@ -120,20 +120,20 @@ uint hashElement(Element *e) { bool compareElement(Element *e1, Element *e2) { if (e1->type != e2->type) return false; - switch(e1->type) { + switch (e1->type) { case ELEMSET: { return e1 == e2; } case ELEMFUNCRETURN: { - ElementFunction * ef1=(ElementFunction *) e1; - ElementFunction * ef2=(ElementFunction *) e2; + ElementFunction *ef1 = (ElementFunction *) e1; + ElementFunction *ef2 = (ElementFunction *) e2; return (ef1->function == ef2->function) && - (ef1->overflowstatus == ef2->overflowstatus) && - compareArray(&ef1->inputs, &ef2->inputs); + (ef1->overflowstatus == ef2->overflowstatus) && + compareArray(&ef1->inputs, &ef2->inputs); } case ELEMCONST: { - ElementConst * ec1=(ElementConst *) e1; - ElementConst * ec2=(ElementConst *) e2; + ElementConst *ec1 = (ElementConst *) e1; + ElementConst *ec2 = (ElementConst *) e2; return (ec1->value == ec2->value); } default: diff --git a/src/AST/asthash.h b/src/AST/asthash.h index 6dd50dc..a80d67e 100644 --- a/src/AST/asthash.h +++ b/src/AST/asthash.h @@ -3,7 +3,7 @@ #include "classes.h" #include "hashtable.h" -uint hashBoolean(Boolean * boolean); +uint hashBoolean(Boolean *boolean); bool compareBoolean(Boolean *b1, Boolean *b2); uint hashElement(Element *element); diff --git a/src/AST/boolean.h b/src/AST/boolean.h index afcf512..5a4b5af 100644 --- a/src/AST/boolean.h +++ b/src/AST/boolean.h @@ -24,7 +24,7 @@ public: }; class BooleanConst : public Boolean { - public: +public: BooleanConst(bool isTrue); Boolean *clone(CSolver *solver, CloneMap *map); bool isTrue() {return istrue;} diff --git a/src/AST/element.h b/src/AST/element.h index 2622437..f1ba4eb 100644 --- a/src/AST/element.h +++ b/src/AST/element.h @@ -15,7 +15,7 @@ public: Vector parents; ElementEncoding encoding; virtual Element *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;}; - + CMEMALLOC; }; diff --git a/src/AST/order.cc b/src/AST/order.cc index 908d691..35bca4a 100644 --- a/src/AST/order.cc +++ b/src/AST/order.cc @@ -41,7 +41,7 @@ Order::~Order() { orderPairTable->resetanddelete(); delete orderPairTable; } - + if (graph != NULL) { delete graph; } diff --git a/src/AST/order.h b/src/AST/order.h index 65291aa..d922235 100644 --- a/src/AST/order.h +++ b/src/AST/order.h @@ -19,7 +19,7 @@ public: Order *clone(CSolver *solver, CloneMap *map); Vector constraints; OrderEncoding encoding; - void setOrderResolver(OrderResolver* _resolver) { encoding.resolver = _resolver;}; + void setOrderResolver(OrderResolver *_resolver) { encoding.resolver = _resolver;}; void initializeOrderHashtable(); void initializeOrderElementsHashtable(); void addOrderConstraint(BooleanOrder *constraint); diff --git a/src/AST/set.cc b/src/AST/set.cc index e33bad0..4e7383a 100644 --- a/src/AST/set.cc +++ b/src/AST/set.cc @@ -41,10 +41,10 @@ uint Set::getSize() { } } -uint64_t Set::getMemberAt(uint index){ - if(isRange){ - return low+index; - }else { +uint64_t Set::getMemberAt(uint index) { + if (isRange) { + return low + index; + } else { return members->get(index); } } diff --git a/src/AST/set.h b/src/AST/set.h index 056794e..5a5cdab 100644 --- a/src/AST/set.h +++ b/src/AST/set.h @@ -20,8 +20,8 @@ public: virtual ~Set(); bool exists(uint64_t element); uint getSize(); - VarType getType(){return type;} - uint64_t getNewUniqueItem(){return low++;} + VarType getType() {return type;} + uint64_t getNewUniqueItem() {return low++;} uint64_t getMemberAt(uint index); uint64_t getElement(uint index); virtual Set *clone(CSolver *solver, CloneMap *map); @@ -32,7 +32,7 @@ protected: uint64_t low;//also used to count unique items uint64_t high; Vector *members; - + }; #endif/* SET_H */ diff --git a/src/ASTAnalyses/ordergraph.cc b/src/ASTAnalyses/ordergraph.cc index 62d4846..f797f5e 100644 --- a/src/ASTAnalyses/ordergraph.cc +++ b/src/ASTAnalyses/ordergraph.cc @@ -111,9 +111,9 @@ OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id, bool create) { if ( tmp != NULL) { delete node; node = tmp; - } else if(create) { + } else if (create) { nodes->add(node); - } else{ + } else { delete node; return NULL; } diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc index 6be7bea..ec8b020 100644 --- a/src/ASTTransform/decomposeordertransform.cc +++ b/src/ASTTransform/decomposeordertransform.cc @@ -1,7 +1,7 @@ -/* +/* * File: ordertransform.cc * Author: hamed - * + * * Created on August 28, 2017, 10:35 AM */ @@ -14,21 +14,65 @@ #include "ordergraph.h" #include "csolver.h" #include "decomposeorderresolver.h" +#include "tunable.h" +#include "orderanalysis.h" -DecomposeOrderTransform::DecomposeOrderTransform(CSolver* _solver) - :Transform(_solver) +DecomposeOrderTransform::DecomposeOrderTransform(CSolver *_solver) + : Transform(_solver) { } DecomposeOrderTransform::~DecomposeOrderTransform() { } -bool DecomposeOrderTransform::canExecuteTransform(){ - return canExecutePass(solver, currOrder->type, DECOMPOSEORDER, &onoff); +void DecomposeOrderTransform::doTransform() { + Vector *orders = solver->getOrders(); + uint size = orders->getSize(); + for (uint i = 0; i < size; i++) { + Order *order = orders->get(i); + + if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0) { + continue; + } + + OrderGraph *graph = buildOrderGraph(order); + if (order->type == SATC_PARTIAL) { + //Required to do SCC analysis for partial order graphs. It + //makes sure we don't incorrectly optimize graphs with negative + //polarity edges + completePartialOrderGraph(graph); + } + + bool mustReachGlobal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHGLOBAL, &onoff); + + if (mustReachGlobal) + reachMustAnalysis(solver, graph, false); + + bool mustReachLocal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHLOCAL, &onoff); + + if (mustReachLocal) { + //This pair of analysis is also optional + if (order->type == SATC_PARTIAL) { + localMustAnalysisPartial(solver, graph); + } else { + localMustAnalysisTotal(solver, graph); + } + } + + bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff); + + if (mustReachPrune) + removeMustBeTrueNodes(solver, graph); + + //This is needed for splitorder + computeStronglyConnectedComponentGraph(graph); + decomposeOrder(order, graph); + delete graph; + } } -void DecomposeOrderTransform::doTransform(){ +void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *currGraph) { Vector ordervec; Vector partialcandidatevec; uint size = currOrder->constraints.getSize(); @@ -36,7 +80,6 @@ void DecomposeOrderTransform::doTransform(){ BooleanOrder *orderconstraint = currOrder->constraints.get(i); OrderNode *from = currGraph->getOrderNodeFromOrderGraph(orderconstraint->first); OrderNode *to = currGraph->getOrderNodeFromOrderGraph(orderconstraint->second); - model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum); if (from->sccNum != to->sccNum) { OrderEdge *edge = currGraph->getOrderEdgeFromOrderGraph(from, to); if (edge->polPos) { @@ -84,7 +127,6 @@ void DecomposeOrderTransform::doTransform(){ Order *neworder = partialcandidatevec.get(i); if (neworder != NULL) { neworder->type = SATC_TOTAL; - model_print("i=%u\t", i); } } } diff --git a/src/ASTTransform/decomposeordertransform.h b/src/ASTTransform/decomposeordertransform.h index 3d7d6e8..69f7a1f 100644 --- a/src/ASTTransform/decomposeordertransform.h +++ b/src/ASTTransform/decomposeordertransform.h @@ -1,4 +1,4 @@ -/* +/* * File: ordertransform.h * Author: hamed * @@ -13,19 +13,16 @@ class DecomposeOrderTransform : public Transform { public: - DecomposeOrderTransform(CSolver* _solver); - virtual ~DecomposeOrderTransform(); + DecomposeOrderTransform(CSolver *_solver); + ~DecomposeOrderTransform(); void doTransform(); - void setOrderGraph(OrderGraph* _graph){ - currGraph = _graph; - } - void setCurrentOrder(Order* _current) { currOrder = _current;} - bool canExecuteTransform(); + void decomposeOrder (Order *currOrder, OrderGraph *currGraph); + CMEMALLOC; - private: - Order* currOrder; - OrderGraph* currGraph; +private: + Order *currOrder; + OrderGraph *currGraph; }; -#endif /* ORDERTRANSFORM_H */ +#endif/* ORDERTRANSFORM_H */ diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc index f1b9919..d8150b3 100644 --- a/src/ASTTransform/integerencoding.cc +++ b/src/ASTTransform/integerencoding.cc @@ -1,4 +1,3 @@ - #include "integerencoding.h" #include "set.h" #include "order.h" @@ -6,33 +5,39 @@ #include "csolver.h" #include "integerencodingrecord.h" #include "integerencorderresolver.h" +#include "tunable.h" - -IntegerEncodingTransform::IntegerEncodingTransform(CSolver* _solver) - :Transform(_solver) -{ +IntegerEncodingTransform::IntegerEncodingTransform(CSolver *_solver) + : Transform(_solver) +{ orderIntEncoding = new HashTableOrderIntEncoding(); } -IntegerEncodingTransform::~IntegerEncodingTransform(){ +IntegerEncodingTransform::~IntegerEncodingTransform() { orderIntEncoding->resetanddelete(); } -bool IntegerEncodingTransform::canExecuteTransform(){ - return canExecutePass(solver, currOrder->type, ORDERINTEGERENCODING, &offon); +void IntegerEncodingTransform::doTransform() { + Vector *orders = solver->getOrders(); + uint size = orders->getSize(); + for (uint i = 0; i < size; i++) { + Order *order = orders->get(i); + if (GETVARTUNABLE(solver->getTuner(), order->type, ORDERINTEGERENCODING, &onoff)) + integerEncode(order); + } } -void IntegerEncodingTransform::doTransform(){ - IntegerEncodingRecord* encodingRecord = NULL; +void IntegerEncodingTransform::integerEncode(Order *currOrder) { + IntegerEncodingRecord *encodingRecord = NULL; if (!orderIntEncoding->contains(currOrder)) { encodingRecord = new IntegerEncodingRecord( - solver->createRangeSet(currOrder->set->getType(), 0, (uint64_t) currOrder->set->getSize()-1)); + solver->createRangeSet(currOrder->set->getType(), 0, (uint64_t) currOrder->set->getSize() - 1)); orderIntEncoding->put(currOrder, encodingRecord); } else { encodingRecord = orderIntEncoding->get(currOrder); } uint size = currOrder->constraints.getSize(); - for(uint i=0; iconstraints.get(i)); } currOrder->setOrderResolver(new IntegerEncOrderResolver(solver, encodingRecord)); @@ -40,7 +45,7 @@ void IntegerEncodingTransform::doTransform(){ void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder) { - IntegerEncodingRecord* ierec = orderIntEncoding->get(currOrder); + IntegerEncodingRecord *ierec = orderIntEncoding->get(currOrder); //getting two elements and using LT predicate ... Element *elem1 = ierec->getOrderIntegerElement(solver, boolOrder->first); Element *elem2 = ierec->getOrderIntegerElement(solver, boolOrder->second); diff --git a/src/ASTTransform/integerencoding.h b/src/ASTTransform/integerencoding.h index 3bfb289..f051a41 100644 --- a/src/ASTTransform/integerencoding.h +++ b/src/ASTTransform/integerencoding.h @@ -1,4 +1,4 @@ -/* +/* * File: integerencoding.h * Author: hamed * @@ -11,20 +11,20 @@ #include "transform.h" #include "order.h" -class IntegerEncodingTransform : public Transform{ +class IntegerEncodingTransform : public Transform { public: - IntegerEncodingTransform(CSolver* solver); + IntegerEncodingTransform(CSolver *solver); void orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder); - void setCurrentOrder(Order* _curr) {currOrder = _curr;} void doTransform(); - bool canExecuteTransform(); + void integerEncode(Order *currOrder); + virtual ~IntegerEncodingTransform(); private: - Order* currOrder; + Order *currOrder; //FIXME:We can remove it, because we don't need it for translating anymore... -HG - HashTableOrderIntEncoding* orderIntEncoding; + HashTableOrderIntEncoding *orderIntEncoding; }; -#endif /* INTEGERENCODING_H */ +#endif/* INTEGERENCODING_H */ diff --git a/src/ASTTransform/integerencodingrecord.cc b/src/ASTTransform/integerencodingrecord.cc index abd763f..f8690d7 100644 --- a/src/ASTTransform/integerencodingrecord.cc +++ b/src/ASTTransform/integerencodingrecord.cc @@ -1,7 +1,7 @@ -/* +/* * File: integerencodingrecord.cpp * Author: hamed - * + * * Created on August 26, 2017, 6:19 PM */ @@ -9,19 +9,19 @@ #include "csolver.h" #include "orderelement.h" -IntegerEncodingRecord::IntegerEncodingRecord(Set* _set): +IntegerEncodingRecord::IntegerEncodingRecord(Set *_set) : secondarySet(_set) { elementTable = new HashsetOrderElement(); } -IntegerEncodingRecord::~IntegerEncodingRecord(){ +IntegerEncodingRecord::~IntegerEncodingRecord() { if (elementTable != NULL) { delete elementTable; } } -Element * IntegerEncodingRecord::getOrderIntegerElement(CSolver *This, uint64_t item, bool create) { +Element *IntegerEncodingRecord::getOrderIntegerElement(CSolver *This, uint64_t item, bool create) { OrderElement oelement(item, NULL); if ( elementTable->contains(&oelement)) { return elementTable->get(&oelement)->getElement(); diff --git a/src/ASTTransform/integerencodingrecord.h b/src/ASTTransform/integerencodingrecord.h index a85e98a..556e6c5 100644 --- a/src/ASTTransform/integerencodingrecord.h +++ b/src/ASTTransform/integerencodingrecord.h @@ -1,4 +1,4 @@ -/* +/* * File: integerencodingrecord.h * Author: hamed * @@ -13,16 +13,16 @@ class IntegerEncodingRecord { public: - IntegerEncodingRecord(Set* set); + IntegerEncodingRecord(Set *set); ~IntegerEncodingRecord(); - Element* getOrderIntegerElement(CSolver *This, uint64_t item, bool create = true); - inline Set* getSecondarySet() { return secondarySet; } + Element *getOrderIntegerElement(CSolver *This, uint64_t item, bool create = true); + inline Set *getSecondarySet() { return secondarySet; } CMEMALLOC; - + private: - Set* secondarySet; + Set *secondarySet; HashsetOrderElement *elementTable; }; -#endif /* INTEGERENCODINGRECORD_H */ +#endif/* INTEGERENCODINGRECORD_H */ diff --git a/src/ASTTransform/pass.h b/src/ASTTransform/pass.h deleted file mode 100644 index 211bd4e..0000000 --- a/src/ASTTransform/pass.h +++ /dev/null @@ -1,29 +0,0 @@ -/* - * File: pass.h - * Author: hamed - * - * Created on August 28, 2017, 6:23 PM - */ - -#ifndef PASS_H -#define PASS_H -#include "classlist.h" -#include "mymemory.h" -#include "structs.h" -#include "tunable.h" -#include "csolver.h" - -class Pass{ -public: - Pass(){}; - virtual ~Pass(){}; - virtual inline bool canExecutePass(CSolver* This, uint type, Tunables tunable, TunableDesc* desc){ - return GETVARTUNABLE(This->getTuner(), type, tunable, desc); - } - CMEMALLOC; - -}; - - -#endif /* PASS_H */ - diff --git a/src/ASTTransform/transform.cc b/src/ASTTransform/transform.cc index bf04575..99a181f 100644 --- a/src/ASTTransform/transform.cc +++ b/src/ASTTransform/transform.cc @@ -1,16 +1,16 @@ -/* +/* * File: transform.cc * Author: hamed - * + * * Created on August 26, 2017, 5:14 PM */ #include "transform.h" -Transform::Transform(CSolver* _solver) +Transform::Transform(CSolver *_solver) { solver = _solver; } -Transform::~Transform(){ +Transform::~Transform() { } diff --git a/src/ASTTransform/transform.h b/src/ASTTransform/transform.h index 678c732..976c2c8 100644 --- a/src/ASTTransform/transform.h +++ b/src/ASTTransform/transform.h @@ -1,4 +1,4 @@ -/* +/* * File: transform.h * Author: hamed * @@ -11,19 +11,17 @@ #include "classlist.h" #include "mymemory.h" #include "structs.h" -#include "pass.h" -class Transform : public Pass{ +class Transform { public: - Transform(CSolver* _solver); + Transform(CSolver *_solver); virtual ~Transform(); - virtual bool canExecuteTransform() = 0; virtual void doTransform() = 0; CMEMALLOC; - protected: +protected: // Need solver for translating back the result ... - CSolver* solver; + CSolver *solver; }; -#endif /* TRANSFORM_H */ +#endif/* TRANSFORM_H */ diff --git a/src/ASTTransform/transformer.cc b/src/ASTTransform/transformer.cc deleted file mode 100644 index 2c814ea..0000000 --- a/src/ASTTransform/transformer.cc +++ /dev/null @@ -1,86 +0,0 @@ -#include "transformer.h" -#include "common.h" -#include "order.h" -#include "boolean.h" -#include "ordergraph.h" -#include "ordernode.h" -#include "rewriter.h" -#include "orderedge.h" -#include "mutableset.h" -#include "ops.h" -#include "csolver.h" -#include "orderanalysis.h" -#include "tunable.h" -#include "transform.h" -#include "element.h" -#include "integerencoding.h" -#include "decomposeordertransform.h" - -Transformer::Transformer(CSolver *_solver): - integerEncoding(new IntegerEncodingTransform(_solver)), - decomposeOrder(new DecomposeOrderTransform(_solver)), - solver(_solver) -{ -} - -Transformer::~Transformer(){ - delete integerEncoding; - delete decomposeOrder; -} - -void Transformer::orderAnalysis() { - Vector *orders = solver->getOrders(); - uint size = orders->getSize(); - for (uint i = 0; i < size; i++) { - Order *order = orders->get(i); - decomposeOrder->setCurrentOrder(order); - - if (true) { - continue; - } - - OrderGraph *graph = buildOrderGraph(order); - if (order->type == SATC_PARTIAL) { - //Required to do SCC analysis for partial order graphs. It - //makes sure we don't incorrectly optimize graphs with negative - //polarity edges - completePartialOrderGraph(graph); - } - - - bool mustReachGlobal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHGLOBAL, &onoff); - - if (mustReachGlobal) - reachMustAnalysis(solver, graph, false); - - bool mustReachLocal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHLOCAL, &onoff); - - if (mustReachLocal) { - //This pair of analysis is also optional - if (order->type == SATC_PARTIAL) { - localMustAnalysisPartial(solver, graph); - } else { - localMustAnalysisTotal(solver, graph); - } - } - - bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff); - - if (mustReachPrune) - removeMustBeTrueNodes(solver, graph); - - //This is needed for splitorder - computeStronglyConnectedComponentGraph(graph); - decomposeOrder->setOrderGraph(graph); - decomposeOrder->doTransform(); - delete graph; - - integerEncoding->setCurrentOrder(order); - if(!integerEncoding->canExecuteTransform()){ - continue; - } - integerEncoding->doTransform(); - } -} - - diff --git a/src/ASTTransform/transformer.h b/src/ASTTransform/transformer.h deleted file mode 100644 index 4e9f427..0000000 --- a/src/ASTTransform/transformer.h +++ /dev/null @@ -1,33 +0,0 @@ -/* - * File: transformer.h - * Author: hamed - * - * Created on August 24, 2017, 5:33 PM - */ - -#ifndef ORDERDECOMPOSE_H -#define ORDERDECOMPOSE_H -#include "classlist.h" -#include "structs.h" -#include "transform.h" -#include "integerencoding.h" -#include "decomposeordertransform.h" - -class Transformer{ -public: - Transformer(CSolver* solver); - ~Transformer(); - IntegerEncodingTransform* getIntegerEncodingTransform(){ return integerEncoding; } - void orderAnalysis(); - CMEMALLOC; - private: - //For now we can just add transforms here, but in future we may want take a smarter approach. - IntegerEncodingTransform* integerEncoding; - DecomposeOrderTransform* decomposeOrder; - - CSolver* solver; -}; - - -#endif/* ORDERDECOMPOSE_H */ - diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc index 8c247cc..b90ec4a 100644 --- a/src/Backend/constraint.cc +++ b/src/Backend/constraint.cc @@ -333,15 +333,15 @@ Edge constraintNewVar(CNF *cnf) { } int solveCNF(CNF *cnf) { - long long startTime=getTimeNano(); + long long startTime = getTimeNano(); countPass(cnf); convertPass(cnf, false); finishedClauses(cnf->solver); - long long startSolve=getTimeNano(); + long long startSolve = getTimeNano(); int result = solve(cnf->solver); - long long finishTime=getTimeNano(); - cnf->encodeTime=startSolve-startTime; - cnf->solveTime=finishTime-startSolve; + long long finishTime = getTimeNano(); + cnf->encodeTime = startSolve - startTime; + cnf->solveTime = finishTime - startSolve; return result; } diff --git a/src/Backend/orderelement.h b/src/Backend/orderelement.h index 07913c9..d56a3a7 100644 --- a/src/Backend/orderelement.h +++ b/src/Backend/orderelement.h @@ -16,8 +16,8 @@ class OrderElement { public: OrderElement(uint64_t item, Element *elem); inline uint getHash() {return (uint) item;} - inline bool equals(OrderElement* oe){ return item == oe->item;} - inline Element* getElement() { return elem; } + inline bool equals(OrderElement *oe) { return item == oe->item;} + inline Element *getElement() { return elem; } CMEMALLOC; private: uint64_t item; diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc index 0de0ae4..1d6b4f4 100644 --- a/src/Backend/satencoder.cc +++ b/src/Backend/satencoder.cc @@ -12,7 +12,7 @@ #include "predicate.h" #include "set.h" -SATEncoder::SATEncoder(CSolver * _solver) : +SATEncoder::SATEncoder(CSolver *_solver) : cnf(createCNF()), solver(_solver) { } @@ -38,22 +38,22 @@ void SATEncoder::encodeAllSATEncoder(CSolver *csolver) { Edge SATEncoder::encodeConstraintSATEncoder(Boolean *constraint) { Edge result; if (booledgeMap.contains(constraint)) { - Edge e={(Node *) booledgeMap.get(constraint)}; + Edge e = {(Node *) booledgeMap.get(constraint)}; return e; } - + switch (constraint->type) { case ORDERCONST: - result=encodeOrderSATEncoder((BooleanOrder *) constraint); + result = encodeOrderSATEncoder((BooleanOrder *) constraint); break; case BOOLEANVAR: - result=encodeVarSATEncoder((BooleanVar *) constraint); + result = encodeVarSATEncoder((BooleanVar *) constraint); break; case LOGICOP: - result=encodeLogicSATEncoder((BooleanLogic *) constraint); + result = encodeLogicSATEncoder((BooleanLogic *) constraint); break; case PREDICATEOP: - result=encodePredicateSATEncoder((BooleanPredicate *) constraint); + result = encodePredicateSATEncoder((BooleanPredicate *) constraint); break; default: model_print("Unhandled case in encodeConstraintSATEncoder %u", constraint->type); @@ -133,7 +133,7 @@ void SATEncoder::encodeElementSATEncoder(Element *element) { /* Check to see if we have already encoded this element. */ if (getElementEncoding(element)->variables != NULL) return; - + /* Need to encode. */ switch ( element->type) { case ELEMFUNCRETURN: diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h index 94115ce..25f6918 100644 --- a/src/Backend/satencoder.h +++ b/src/Backend/satencoder.h @@ -9,18 +9,18 @@ typedef Hashtable BooleanToEdgeMap; class SATEncoder { - public: +public: int solve(); SATEncoder(CSolver *solver); ~SATEncoder(); void encodeAllSATEncoder(CSolver *csolver); Edge encodeConstraintSATEncoder(Boolean *constraint); - CNF * getCNF() { return cnf;} + CNF *getCNF() { return cnf;} long long getSolveTime() { return cnf->solveTime; } long long getEncodeTime() { return cnf->encodeTime; } - + CMEMALLOC; - private: +private: Edge getNewVarSATEncoder(); void getArrayNewVarsSATEncoder(uint num, Edge *carray); Edge encodeVarSATEncoder(BooleanVar *constraint); @@ -56,7 +56,7 @@ class SATEncoder { Edge encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint); void encodeEnumTableElemFunctionSATEncoder(ElementFunction *This); void encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *This); - + CNF *cnf; CSolver *solver; BooleanToEdgeMap booledgeMap; diff --git a/src/Collections/hashset.h b/src/Collections/hashset.h index 47b6f50..cdba3b2 100644 --- a/src/Collections/hashset.h +++ b/src/Collections/hashset.h @@ -148,15 +148,15 @@ public: return false; } - /** @brief Return random key from set. */ + /** @brief Return random key from set. */ - _Key getRandomElement() { + _Key getRandomElement() { if (getSize() == 0) return NULL; else if (getSize() < 6) { uint count = random() % getSize(); - Linknode<_Key> *ptr=list; - while(count > 0) { + Linknode<_Key> *ptr = list; + while (count > 0) { ptr = ptr->next; count--; } diff --git a/src/Collections/hashtable.h b/src/Collections/hashtable.h index 18d7353..44b984d 100644 --- a/src/Collections/hashtable.h +++ b/src/Collections/hashtable.h @@ -115,10 +115,10 @@ public: size = 0; } - /** Doesn't work with zero value */ - _Val getRandomValue() { - while(true) { - unsigned int index=random() & capacitymask; + /** Doesn't work with zero value */ + _Val getRandomValue() { + while (true) { + unsigned int index = random() & capacitymask; struct Hashlistnode<_Key, _Val> *bin = &table[index]; if (bin->key != NULL && bin->val != NULL) { return bin->val; diff --git a/src/Collections/structs.h b/src/Collections/structs.h index c2ed0e9..ea7fa1f 100644 --- a/src/Collections/structs.h +++ b/src/Collections/structs.h @@ -27,7 +27,7 @@ typedef Hashset HashtableNodeToNodeSet; typedef Hashtable HashtableOrderPair; typedef Hashtable CloneMap; -typedef Hashtable HashTableOrderIntEncoding; +typedef Hashtable HashTableOrderIntEncoding; typedef SetIterator SetIteratorTableEntry; typedef SetIterator SetIteratorOrderEdge; diff --git a/src/Encoders/orderencoding.h b/src/Encoders/orderencoding.h index 90a97eb..0792d4a 100644 --- a/src/Encoders/orderencoding.h +++ b/src/Encoders/orderencoding.h @@ -11,8 +11,8 @@ typedef enum OrderEncodingType OrderEncodingType; class OrderEncoding { public: OrderEncoding(Order *order); - - OrderResolver* resolver; + + OrderResolver *resolver; OrderEncodingType type; Order *order; CMEMALLOC; diff --git a/src/Test/ordergraphtest.cc b/src/Test/ordergraphtest.cc index 72ad021..092e0ed 100644 --- a/src/Test/ordergraphtest.cc +++ b/src/Test/ordergraphtest.cc @@ -16,41 +16,41 @@ int main(int numargs, char **argv) { Boolean *o58 = solver->orderConstraint(order, 5, 8); Boolean *o81 = solver->orderConstraint(order, 8, 1); - Boolean * array1[]={o12, o13, o24, o34}; + Boolean *array1[] = {o12, o13, o24, o34}; solver->addConstraint(solver->applyLogicalOperation(SATC_OR, array1, 4) ); - Boolean * array2[]={o41, o57}; - + Boolean *array2[] = {o41, o57}; + Boolean *b1 = solver->applyLogicalOperation(SATC_XOR, array2, 2); - Boolean * array3[]={o34}; + Boolean *array3[] = {o34}; Boolean *o34n = solver->applyLogicalOperation(SATC_NOT, array3, 1); - Boolean * array4[]={o24}; + Boolean *array4[] = {o24}; Boolean *o24n = solver->applyLogicalOperation(SATC_NOT, array4, 1); - Boolean * array5[]={o34n, o24n}; + Boolean *array5[] = {o34n, o24n}; Boolean *b2 = solver->applyLogicalOperation(SATC_OR, array5, 2); - Boolean * array6[] = {b1, b2}; + Boolean *array6[] = {b1, b2}; solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, array6, 2) ); - Boolean * array7[] = {o12, o13}; + Boolean *array7[] = {o12, o13}; solver->addConstraint(solver->applyLogicalOperation(SATC_AND, array7, 2) ); - Boolean * array8[] = {o76, o65}; + Boolean *array8[] = {o76, o65}; solver->addConstraint(solver->applyLogicalOperation(SATC_OR, array8, 2) ); - Boolean * array9[] = {o76, o65}; - Boolean* b3= solver->applyLogicalOperation(SATC_AND, array9, 2) ; - Boolean * array10[] = {o57}; - Boolean* o57n= solver->applyLogicalOperation(SATC_NOT, array10, 1); - Boolean * array11[] = {b3, o57n}; + Boolean *array9[] = {o76, o65}; + Boolean *b3 = solver->applyLogicalOperation(SATC_AND, array9, 2) ; + Boolean *array10[] = {o57}; + Boolean *o57n = solver->applyLogicalOperation(SATC_NOT, array10, 1); + Boolean *array11[] = {b3, o57n}; solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, array11, 2)); - Boolean * array12[] = {o58, o81}; + Boolean *array12[] = {o58, o81}; solver->addConstraint(solver->applyLogicalOperation(SATC_AND, array12, 2) ); - + /* if (solver->solve() == 1) - printf("SAT\n"); - else - printf("UNSAT\n");*/ - + printf("SAT\n"); + else + printf("UNSAT\n");*/ + solver->autoTune(100); delete solver; } diff --git a/src/Translator/decomposeorderresolver.cc b/src/Translator/decomposeorderresolver.cc index 28e3b56..798bb30 100644 --- a/src/Translator/decomposeorderresolver.cc +++ b/src/Translator/decomposeorderresolver.cc @@ -1,8 +1,8 @@ -/* +/* * File: DecomposeOrderResolver.cc * Author: hamed - * + * * Created on September 1, 2017, 10:36 AM */ @@ -11,7 +11,7 @@ #include "ordernode.h" #include "ordergraph.h" -DecomposeOrderResolver::DecomposeOrderResolver(OrderGraph* _graph, Vector& _orders): +DecomposeOrderResolver::DecomposeOrderResolver(OrderGraph *_graph, Vector &_orders) : graph(_graph), orders(_orders.getSize(), _orders.expose()) { @@ -20,30 +20,30 @@ DecomposeOrderResolver::DecomposeOrderResolver(OrderGraph* _graph, VectorgetOrderNodeFromOrderGraph(first, false /*Don't create new node if doesn't exist*/); - if(from == NULL){ + if (from == NULL) { return SATC_UNORDERED; } OrderNode *to = graph->getOrderNodeFromOrderGraph(second, false); - if(from == NULL){ + if (from == NULL) { return SATC_UNORDERED; } if (from->sccNum != to->sccNum) { - OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to, false /* Don't create a new edge*/); - if (edge != NULL && edge->mustPos){ + OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to, false /* Don't create a new edge*/); + if (edge != NULL && edge->mustPos) { return SATC_FIRST; - } else if( edge != NULL && edge->mustNeg){ + } else if ( edge != NULL && edge->mustNeg) { return SATC_SECOND; - }else { - switch(graph->getOrder()->type){ - case SATC_TOTAL: - return from->sccNum < to->sccNum? SATC_FIRST: SATC_SECOND; - case SATC_PARTIAL: - //Adding support for partial order ... - default: - ASSERT(0); - } + } else { + switch (graph->getOrder()->type) { + case SATC_TOTAL: + return from->sccNum < to->sccNum ? SATC_FIRST : SATC_SECOND; + case SATC_PARTIAL: + //Adding support for partial order ... + default: + ASSERT(0); + } } } else { Order *suborder = NULL; diff --git a/src/Translator/decomposeorderresolver.h b/src/Translator/decomposeorderresolver.h index 590c565..0ca8264 100644 --- a/src/Translator/decomposeorderresolver.h +++ b/src/Translator/decomposeorderresolver.h @@ -1,5 +1,5 @@ -/* +/* * File: DecomposeOrderResolver.h * Author: hamed * @@ -13,15 +13,15 @@ #include "structs.h" #include "orderresolver.h" -class DecomposeOrderResolver : public OrderResolver{ +class DecomposeOrderResolver : public OrderResolver { public: - DecomposeOrderResolver(OrderGraph* graph, Vector & orders); + DecomposeOrderResolver(OrderGraph *graph, Vector &orders); HappenedBefore resolveOrder(uint64_t first, uint64_t second); virtual ~DecomposeOrderResolver(); private: - OrderGraph* graph; - Vector orders; + OrderGraph *graph; + Vector orders; }; -#endif /* DECOMPOSEORDERRESOLVER_H */ +#endif/* DECOMPOSEORDERRESOLVER_H */ diff --git a/src/Translator/integerencorderresolver.cc b/src/Translator/integerencorderresolver.cc index a9048ef..4f67018 100644 --- a/src/Translator/integerencorderresolver.cc +++ b/src/Translator/integerencorderresolver.cc @@ -1,8 +1,8 @@ -/* +/* * File: integerencorderresolver.cpp * Author: hamed - * + * * Created on September 1, 2017, 4:58 PM */ @@ -10,7 +10,7 @@ #include "integerencodingrecord.h" #include "sattranslator.h" -IntegerEncOrderResolver::IntegerEncOrderResolver(CSolver* _solver, IntegerEncodingRecord* _ierecord): +IntegerEncOrderResolver::IntegerEncOrderResolver(CSolver *_solver, IntegerEncodingRecord *_ierecord) : solver(_solver), ierecord(_ierecord) { @@ -20,15 +20,15 @@ IntegerEncOrderResolver::~IntegerEncOrderResolver() { } -HappenedBefore IntegerEncOrderResolver::resolveOrder(uint64_t first, uint64_t second){ - Element* elem1 = ierecord->getOrderIntegerElement(solver, first, false); - if(elem1 == NULL) +HappenedBefore IntegerEncOrderResolver::resolveOrder(uint64_t first, uint64_t second) { + Element *elem1 = ierecord->getOrderIntegerElement(solver, first, false); + if (elem1 == NULL) return SATC_UNORDERED; - Element* elem2 = ierecord->getOrderIntegerElement(solver, second, false); - if(elem2 == NULL) + Element *elem2 = ierecord->getOrderIntegerElement(solver, second, false); + if (elem2 == NULL) return SATC_UNORDERED; - + uint64_t val1 = getElementValueSATTranslator(solver, elem1); uint64_t val2 = getElementValueSATTranslator(solver, elem2); - return val1 < val2? SATC_FIRST : val1> val2? SATC_SECOND: SATC_UNORDERED; + return val1 < val2 ? SATC_FIRST : val1> val2 ? SATC_SECOND : SATC_UNORDERED; } diff --git a/src/Translator/integerencorderresolver.h b/src/Translator/integerencorderresolver.h index e517881..56941e9 100644 --- a/src/Translator/integerencorderresolver.h +++ b/src/Translator/integerencorderresolver.h @@ -1,5 +1,5 @@ -/* +/* * File: integerencorderresolver.h * Author: hamed * @@ -10,15 +10,15 @@ #define INTEGERENCORDERRESOLVER_H #include "orderresolver.h" -class IntegerEncOrderResolver : public OrderResolver{ +class IntegerEncOrderResolver : public OrderResolver { public: - IntegerEncOrderResolver(CSolver* _solver, IntegerEncodingRecord* _ierecord); + IntegerEncOrderResolver(CSolver *_solver, IntegerEncodingRecord *_ierecord); HappenedBefore resolveOrder(uint64_t first, uint64_t second); virtual ~IntegerEncOrderResolver(); private: - CSolver* solver; - IntegerEncodingRecord* ierecord; + CSolver *solver; + IntegerEncodingRecord *ierecord; }; -#endif /* INTEGERENCORDERRESOLVER_H */ +#endif/* INTEGERENCORDERRESOLVER_H */ diff --git a/src/Translator/orderpairresolver.cc b/src/Translator/orderpairresolver.cc index fa147d0..3f50077 100644 --- a/src/Translator/orderpairresolver.cc +++ b/src/Translator/orderpairresolver.cc @@ -1,8 +1,8 @@ -/* +/* * File: orderpairresolver.cc * Author: hamed - * + * * Created on September 1, 2017, 3:36 PM */ @@ -14,7 +14,7 @@ #include "satencoder.h" #include "csolver.h" -OrderPairResolver::OrderPairResolver(CSolver* _solver, Order* _order) : +OrderPairResolver::OrderPairResolver(CSolver *_solver, Order *_order) : solver(_solver), order(_order) { @@ -23,37 +23,37 @@ OrderPairResolver::OrderPairResolver(CSolver* _solver, Order* _order) : OrderPairResolver::~OrderPairResolver() { } -HappenedBefore OrderPairResolver::resolveOrder(uint64_t first, uint64_t second){ - if(order->graph != NULL){ +HappenedBefore OrderPairResolver::resolveOrder(uint64_t first, uint64_t second) { + if (order->graph != NULL) { // For the cases that tuning framework decides no to build a graph for order ... - OrderGraph* graph = order->graph; + OrderGraph *graph = order->graph; OrderNode *from = graph->getOrderNodeFromOrderGraph(first, false /*Don't create new node if doesn't exist*/); - if(from == NULL){ + if (from == NULL) { return SATC_UNORDERED; } OrderNode *to = graph->getOrderNodeFromOrderGraph(second, false); - if(from == NULL){ + if (from == NULL) { return SATC_UNORDERED; } - OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to, false /* Don't create a new edge*/); - if (edge != NULL && edge->mustPos){ + OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to, false /* Don't create a new edge*/); + if (edge != NULL && edge->mustPos) { return SATC_FIRST; - } else if( edge != NULL && edge->mustNeg){ + } else if ( edge != NULL && edge->mustNeg) { return SATC_SECOND; } } //Couldn't infer from graph. Should call the SAT Solver ... - switch( order->type){ - case SATC_TOTAL: - resolveTotalOrder(first, second); - case SATC_PARTIAL: - //TODO: Support for partial order ... - default: - ASSERT(0); + switch ( order->type) { + case SATC_TOTAL: + resolveTotalOrder(first, second); + case SATC_PARTIAL: + //TODO: Support for partial order ... + default: + ASSERT(0); } - + } diff --git a/src/Translator/orderpairresolver.h b/src/Translator/orderpairresolver.h index 8063a90..80ef7e4 100644 --- a/src/Translator/orderpairresolver.h +++ b/src/Translator/orderpairresolver.h @@ -1,5 +1,5 @@ -/* +/* * File: orderpairresolver.h * Author: hamed * @@ -11,16 +11,16 @@ #include "orderresolver.h" -class OrderPairResolver : public OrderResolver{ +class OrderPairResolver : public OrderResolver { public: - OrderPairResolver(CSolver* _solver, Order* _order); + OrderPairResolver(CSolver *_solver, Order *_order); HappenedBefore resolveOrder(uint64_t first, uint64_t second); virtual ~OrderPairResolver(); private: - CSolver* solver; - Order* order; + CSolver *solver; + Order *order; HappenedBefore resolveTotalOrder(uint64_t first, uint64_t second); }; -#endif /* ORDERPAIRRESOLVER_H */ +#endif/* ORDERPAIRRESOLVER_H */ diff --git a/src/Translator/orderresolver.h b/src/Translator/orderresolver.h index 35498ff..7e5ea61 100644 --- a/src/Translator/orderresolver.h +++ b/src/Translator/orderresolver.h @@ -1,5 +1,5 @@ -/* +/* * File: orderresolver.h * Author: hamed * @@ -14,11 +14,11 @@ class OrderResolver { public: - OrderResolver(){}; + OrderResolver() {}; virtual HappenedBefore resolveOrder(uint64_t first, uint64_t second) = 0; - virtual ~OrderResolver(){}; + virtual ~OrderResolver() {}; CMEMALLOC; }; -#endif /* ORDERRESOLVER_H */ +#endif/* ORDERRESOLVER_H */ diff --git a/src/Tuner/autotuner.cc b/src/Tuner/autotuner.cc index 3765759..9082ae4 100644 --- a/src/Tuner/autotuner.cc +++ b/src/Tuner/autotuner.cc @@ -13,14 +13,14 @@ void AutoTuner::addProblem(CSolver *solver) { solvers.push(solver); } -long long AutoTuner::evaluate(CSolver * problem, SearchTuner *tuner) { - CSolver * copy=problem->clone(); +long long AutoTuner::evaluate(CSolver *problem, SearchTuner *tuner) { + CSolver *copy = problem->clone(); copy->setTuner(tuner); int result = copy->solve(); - long long elapsedTime=copy->getElapsedTime(); - long long encodeTime=copy->getEncodeTime(); - long long solveTime=copy->getSolveTime(); - long long metric=elapsedTime; + long long elapsedTime = copy->getElapsedTime(); + 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); @@ -29,24 +29,24 @@ long long AutoTuner::evaluate(CSolver * problem, SearchTuner *tuner) { } double AutoTuner::evaluateAll(SearchTuner *tuner) { - double product=1; - for(uint i=0;icopyUsed(); - uint numSettings=oldTuner->getSize(); - double factor=0.3;//Adjust this factor... - uint settingsToMutate=(uint)(factor*(((double)numSettings) * (budget - k))/(budget)); +SearchTuner *AutoTuner::mutateTuner(SearchTuner *oldTuner, uint k) { + SearchTuner *newTuner = oldTuner->copyUsed(); + uint numSettings = oldTuner->getSize(); + double factor = 0.3;//Adjust this factor... + uint settingsToMutate = (uint)(factor * (((double)numSettings) * (budget - k)) / (budget)); if (settingsToMutate < 1) - settingsToMutate=1; + settingsToMutate = 1; model_print("Mutating %u settings\n", settingsToMutate); - while(settingsToMutate-- != 0) { + while (settingsToMutate-- != 0) { newTuner->randomMutate(); } return newTuner; @@ -54,19 +54,19 @@ SearchTuner * AutoTuner::mutateTuner(SearchTuner * oldTuner, uint k) { void AutoTuner::tune() { - SearchTuner * bestTuner = NULL; - double bestScore=DBL_MAX; + SearchTuner *bestTuner = NULL; + double bestScore = DBL_MAX; - SearchTuner * oldTuner=new SearchTuner(); - double base_temperature=evaluateAll(oldTuner); - double oldScore=base_temperature; + SearchTuner *oldTuner = new SearchTuner(); + double base_temperature = evaluateAll(oldTuner); + double oldScore = base_temperature; - for (uint i=0;iprintUsed(); model_print("Received score %f\n", newScore); - double scoreDiff=newScore - oldScore; //smaller is better + double scoreDiff = newScore - oldScore; //smaller is better if (newScore < bestScore) { if (bestTuner != NULL) delete bestTuner; @@ -78,7 +78,7 @@ void AutoTuner::tune() { if (scoreDiff < 0) { acceptanceP = 1; } else { - double currTemp=base_temperature * (((double)budget - i) / budget); + double currTemp = base_temperature * (((double)budget - i) / budget); acceptanceP = exp(-scoreDiff / currTemp); } double ran = ((double)random()) / RAND_MAX; diff --git a/src/Tuner/autotuner.h b/src/Tuner/autotuner.h index 9e36732..d9fb430 100644 --- a/src/Tuner/autotuner.h +++ b/src/Tuner/autotuner.h @@ -4,17 +4,17 @@ #include "structs.h" class AutoTuner { - public: +public: AutoTuner(uint budget); void addProblem(CSolver *solver); void tune(); CMEMALLOC; - private: +private: long long evaluate(CSolver *problem, SearchTuner *tuner); double evaluateAll(SearchTuner *tuner); - SearchTuner * mutateTuner(SearchTuner * oldTuner, uint k); + SearchTuner *mutateTuner(SearchTuner *oldTuner, uint k); - Vector solvers; + Vector solvers; uint budget; }; #endif diff --git a/src/Tuner/searchtuner.cc b/src/Tuner/searchtuner.cc index c3c1af7..52c7a70 100644 --- a/src/Tuner/searchtuner.cc +++ b/src/Tuner/searchtuner.cc @@ -12,11 +12,11 @@ TunableSetting::TunableSetting(TunableParam _param) : param(_param) { } -TunableSetting::TunableSetting(TunableSetting * ts) : +TunableSetting::TunableSetting(TunableSetting *ts) : hasVar(ts->hasVar), type(ts->type), param(ts->param), - lowValue(ts->lowValue), + lowValue(ts->lowValue), highValue(ts->highValue), defaultValue(ts->defaultValue), selectedValue(ts->selectedValue) @@ -43,19 +43,19 @@ unsigned int tunableSettingHash(TunableSetting *setting) { bool tunableSettingEquals(TunableSetting *setting1, TunableSetting *setting2) { return setting1->hasVar == setting2->hasVar && - setting1->type == setting2->type && - setting1->param == setting2->param; + setting1->type == setting2->type && + setting1->param == setting2->param; } SearchTuner::SearchTuner() { } -SearchTuner * SearchTuner::copyUsed() { - SearchTuner * tuner = new SearchTuner(); - SetIteratorTunableSetting *iterator=usedSettings.iterator(); - while(iterator->hasNext()) { - TunableSetting *setting=iterator->next(); - TunableSetting *copy=new TunableSetting(setting); +SearchTuner *SearchTuner::copyUsed() { + SearchTuner *tuner = new SearchTuner(); + SetIteratorTunableSetting *iterator = usedSettings.iterator(); + while (iterator->hasNext()) { + TunableSetting *setting = iterator->next(); + TunableSetting *copy = new TunableSetting(setting); tuner->settings.add(copy); } delete iterator; @@ -63,9 +63,9 @@ SearchTuner * SearchTuner::copyUsed() { } SearchTuner::~SearchTuner() { - SetIteratorTunableSetting *iterator=settings.iterator(); - while(iterator->hasNext()) { - TunableSetting *setting=iterator->next(); + SetIteratorTunableSetting *iterator = settings.iterator(); + while (iterator->hasNext()) { + TunableSetting *setting = iterator->next(); delete setting; } delete iterator; @@ -73,12 +73,12 @@ SearchTuner::~SearchTuner() { int SearchTuner::getTunable(TunableParam param, TunableDesc *descriptor) { TunableSetting setting(param); - TunableSetting * result = usedSettings.get(&setting); + TunableSetting *result = usedSettings.get(&setting); if (result == NULL) { result = settings.get(&setting); if ( result == NULL) { - result=new TunableSetting(param); - uint value = descriptor->lowValue + (random() % (1+ descriptor->highValue - descriptor->lowValue)); + result = new TunableSetting(param); + uint value = descriptor->lowValue + (random() % (1 + descriptor->highValue - descriptor->lowValue)); result->setDecision(descriptor->lowValue, descriptor->highValue, descriptor->defaultValue, value); settings.add(result); } @@ -89,12 +89,12 @@ int SearchTuner::getTunable(TunableParam param, TunableDesc *descriptor) { int SearchTuner::getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor) { TunableSetting setting(vartype, param); - TunableSetting * result = usedSettings.get(&setting); + TunableSetting *result = usedSettings.get(&setting); if (result == NULL) { result = settings.get(&setting); if ( result == NULL) { - result=new TunableSetting(vartype, param); - uint value = descriptor->lowValue + (random() % (1+ descriptor->highValue - descriptor->lowValue)); + result = new TunableSetting(vartype, param); + uint value = descriptor->lowValue + (random() % (1 + descriptor->highValue - descriptor->lowValue)); result->setDecision(descriptor->lowValue, descriptor->highValue, descriptor->defaultValue, value); settings.add(result); } @@ -104,9 +104,9 @@ int SearchTuner::getVarTunable(VarType vartype, TunableParam param, TunableDesc } void SearchTuner::randomMutate() { - TunableSetting * randomSetting = settings.getRandomElement(); - int range=randomSetting->highValue-randomSetting->lowValue; - int randomchoice=(random() % range) + randomSetting->lowValue; + TunableSetting *randomSetting = settings.getRandomElement(); + int range = randomSetting->highValue - randomSetting->lowValue; + int randomchoice = (random() % range) + randomSetting->lowValue; if (randomchoice < randomSetting->selectedValue) randomSetting->selectedValue = randomchoice; else @@ -114,9 +114,9 @@ void SearchTuner::randomMutate() { } void SearchTuner::print() { - SetIteratorTunableSetting *iterator=settings.iterator(); - while(iterator->hasNext()) { - TunableSetting *setting=iterator->next(); + SetIteratorTunableSetting *iterator = settings.iterator(); + while (iterator->hasNext()) { + TunableSetting *setting = iterator->next(); setting->print(); } delete iterator; @@ -124,9 +124,9 @@ void SearchTuner::print() { } void SearchTuner::printUsed() { - SetIteratorTunableSetting *iterator=usedSettings.iterator(); - while(iterator->hasNext()) { - TunableSetting *setting=iterator->next(); + SetIteratorTunableSetting *iterator = usedSettings.iterator(); + while (iterator->hasNext()) { + TunableSetting *setting = iterator->next(); setting->print(); } delete iterator; diff --git a/src/Tuner/searchtuner.h b/src/Tuner/searchtuner.h index 862faf6..20edb7d 100644 --- a/src/Tuner/searchtuner.h +++ b/src/Tuner/searchtuner.h @@ -5,14 +5,14 @@ #include "structs.h" class TunableSetting { - public: - TunableSetting(VarType type, TunableParam param); +public: + TunableSetting(VarType type, TunableParam param); TunableSetting(TunableParam param); - TunableSetting(TunableSetting * ts); + TunableSetting(TunableSetting *ts); void setDecision(int _low, int _high, int _default, int _selection); void print(); CMEMALLOC; - private: +private: bool hasVar; VarType type; TunableParam param; @@ -32,22 +32,22 @@ typedef Hashset SetIteratorTunableSetting; class SearchTuner : public Tuner { - public: +public: SearchTuner(); ~SearchTuner(); int getTunable(TunableParam param, TunableDesc *descriptor); int getVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor); - SearchTuner * copyUsed(); + SearchTuner *copyUsed(); void randomMutate(); uint getSize() { return usedSettings.getSize();} void print(); void printUsed(); CMEMALLOC; - private: +private: /** Used Settings keeps track of settings that were actually used by - the example. Mutating settings may cause the Constraint Compiler - not to query other settings.*/ + the example. Mutating settings may cause the Constraint Compiler + not to query other settings.*/ HashsetTunableSetting usedSettings; /** Settings contains all settings. */ HashsetTunableSetting settings; diff --git a/src/common.h b/src/common.h index 3fffb34..4ebd816 100644 --- a/src/common.h +++ b/src/common.h @@ -69,7 +69,7 @@ void print_trace(void); static inline long long getTimeNano() { struct timespec time; - clock_gettime(CLOCK_REALTIME, & time); + clock_gettime(CLOCK_REALTIME, &time); return time.tv_sec * 1000000000 + time.tv_nsec; } #endif/* __COMMON_H__ */ diff --git a/src/csolver.cc b/src/csolver.cc index a2081b8..de9543e 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -11,11 +11,12 @@ #include "sattranslator.h" #include "tunable.h" #include "polarityassignment.h" -#include "transformer.h" +#include "decomposeordertransform.h" #include "autotuner.h" #include "astops.h" #include "structs.h" #include "orderresolver.h" +#include "integerencoding.h" CSolver::CSolver() : boolTrue(new BooleanConst(true)), @@ -25,7 +26,6 @@ CSolver::CSolver() : elapsedTime(0) { satEncoder = new SATEncoder(this); - transformer = new Transformer(this); } /** This function tears down the solver and the entire AST */ @@ -69,7 +69,6 @@ CSolver::~CSolver() { delete boolTrue; delete boolFalse; delete satEncoder; - delete transformer; } CSolver *CSolver::clone() { @@ -211,7 +210,7 @@ Boolean *CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint nu Boolean *CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus) { BooleanPredicate *boolean = new BooleanPredicate(predicate, inputs, numInputs, undefinedStatus); - Boolean * b = boolMap.get(boolean); + Boolean *b = boolMap.get(boolean); if (b == NULL) { boolMap.put(boolean, boolean); allBooleans.push(boolean); @@ -230,22 +229,22 @@ bool CSolver::isFalse(Boolean *b) { return b->isFalse(); } -Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean * arg1, Boolean * arg2) { - Boolean * array[] = {arg1, arg2}; +Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean *arg1, Boolean *arg2) { + Boolean *array[] = {arg1, arg2}; return applyLogicalOperation(op, array, 2); } Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean *arg) { - Boolean * array[] = {arg}; + Boolean *array[] = {arg}; return applyLogicalOperation(op, array, 1); } Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) { - Boolean * newarray[asize]; - switch(op) { + Boolean *newarray[asize]; + switch (op) { case SATC_NOT: { - if (array[0]->type == LOGICOP && ((BooleanLogic *)array[0])->op==SATC_NOT) { + if (array[0]->type == LOGICOP && ((BooleanLogic *)array[0])->op == SATC_NOT) { return ((BooleanLogic *) array[0])->inputs.get(0); } else if (array[0]->type == BOOLCONST) { return array[0]->isTrue() ? boolFalse : boolTrue; @@ -253,12 +252,12 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) break; } case SATC_IFF: { - for(uint i=0;i<2;i++) { + for (uint i = 0; i < 2; i++) { if (array[i]->type == BOOLCONST) { if (array[i]->isTrue()) { - return array[1-i]; + return array[1 - i]; } else { - newarray[0]=array[1-i]; + newarray[0] = array[1 - i]; return applyLogicalOperation(SATC_NOT, newarray, 1); } } @@ -266,36 +265,36 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) break; } case SATC_XOR: { - for(uint i=0;i<2;i++) { + for (uint i = 0; i < 2; i++) { if (array[i]->type == BOOLCONST) { if (array[i]->isTrue()) { - newarray[0]=array[1-i]; + newarray[0] = array[1 - i]; return applyLogicalOperation(SATC_NOT, newarray, 1); } else - return array[1-i]; + return array[1 - i]; } } break; } case SATC_OR: { - uint newindex=0; - for(uint i=0;itype == BOOLCONST) { if (b->isTrue()) return boolTrue; else continue; } else - newarray[newindex++]=b; + newarray[newindex++] = b; } - if (newindex==0) { + if (newindex == 0) { return boolFalse; - } else if (newindex==1) + } else if (newindex == 1) return newarray[0]; else if (newindex == 2) { - bool isNot0 = (newarray[0]->type==BOOLCONST) && ((BooleanLogic *)newarray[0])->op == SATC_NOT; - bool isNot1 = (newarray[1]->type==BOOLCONST) && ((BooleanLogic *)newarray[1])->op == SATC_NOT; + bool isNot0 = (newarray[0]->type == BOOLCONST) && ((BooleanLogic *)newarray[0])->op == SATC_NOT; + bool isNot1 = (newarray[1]->type == BOOLCONST) && ((BooleanLogic *)newarray[1])->op == SATC_NOT; if (isNot0 != isNot1) { if (isNot0) { @@ -314,20 +313,20 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) break; } case SATC_AND: { - uint newindex=0; - for(uint i=0;itype == BOOLCONST) { if (b->isTrue()) continue; else return boolFalse; } else - newarray[newindex++]=b; + newarray[newindex++] = b; } - if (newindex==0) { + if (newindex == 0) { return boolTrue; - } else if(newindex==1) { + } else if (newindex == 1) { return newarray[0]; } else { array = newarray; @@ -352,14 +351,14 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) break; } } - + ASSERT(asize != 0); Boolean *boolean = new BooleanLogic(this, op, array, asize); Boolean *b = boolMap.get(boolean); if (b == NULL) { boolMap.put(boolean, boolean); allBooleans.push(boolean); - return boolean; + return boolean; } else { delete boolean; return b; @@ -393,10 +392,16 @@ int CSolver::solve() { tuner = new DefaultTuner(); deleteTuner = true; } - + long long startTime = getTimeNano(); computePolarities(this); - transformer->orderAnalysis(); + + DecomposeOrderTransform dot(this); + dot.doTransform(); + + IntegerEncodingTransform iet(this); + iet.doTransform(); + naiveEncodingDecision(this); satEncoder->encodeAllSATEncoder(this); int result = unsat ? IS_UNSAT : satEncoder->solve(); @@ -432,7 +437,7 @@ bool CSolver::getBooleanValue(Boolean *boolean) { } HappenedBefore CSolver::getOrderConstraintValue(Order *order, uint64_t first, uint64_t second) { - return order->encoding.resolver->resolveOrder(first, second); + return order->encoding.resolver->resolveOrder(first, second); } long long CSolver::getEncodeTime() { return satEncoder->getEncodeTime(); } @@ -440,7 +445,7 @@ long long CSolver::getEncodeTime() { return satEncoder->getEncodeTime(); } long long CSolver::getSolveTime() { return satEncoder->getSolveTime(); } void CSolver::autoTune(uint budget) { - AutoTuner * autotuner=new AutoTuner(budget); + AutoTuner *autotuner = new AutoTuner(budget); autotuner->addProblem(this); autotuner->tune(); delete autotuner; diff --git a/src/csolver.h b/src/csolver.h index 7942839..1ff4cd1 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -19,7 +19,7 @@ public: Set *createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange); Element *createRangeVar(VarType type, uint64_t lowrange, uint64_t highrange); - + /** This function creates a mutable set. */ MutableSet *createMutableSet(VarType type); @@ -44,7 +44,7 @@ public: Boolean *getBooleanTrue(); Boolean *getBooleanFalse(); - + /** This function creates a boolean variable. */ Boolean *getBooleanVar(VarType type); @@ -87,9 +87,9 @@ public: Boolean *applyLogicalOperation(LogicOp op, Boolean **array, uint asize); - /** This function applies a logical operation to the Booleans in its input. */ + /** This function applies a logical operation to the Booleans in its input. */ - Boolean *applyLogicalOperation(LogicOp op, Boolean * arg1, Boolean * arg2); + Boolean *applyLogicalOperation(LogicOp op, Boolean *arg1, Boolean *arg2); /** This function applies a logical operation to the Booleans in its input. */ @@ -119,7 +119,7 @@ public: bool isTrue(Boolean *b); bool isFalse(Boolean *b); - + void setUnSAT() { unsat = true; } bool isUnSAT() { return unsat; } @@ -127,8 +127,7 @@ public: Vector *getOrders() { return &allOrders;} Tuner *getTuner() { return tuner; } - Transformer* getTransformer() {return transformer;} - + SetIteratorBoolean *getConstraints() { return constraints.iterator(); } SATEncoder *getSATEncoder() {return satEncoder;} @@ -139,12 +138,11 @@ public: CSolver *clone(); void autoTune(uint budget); - void setTransformer(Transformer * _transformer) { transformer = _transformer; } - void setTuner(Tuner * _tuner) { tuner = _tuner; } + void setTuner(Tuner *_tuner) { tuner = _tuner; } long long getElapsedTime() { return elapsedTime; } long long getEncodeTime(); long long getSolveTime(); - + CMEMALLOC; private: @@ -178,17 +176,16 @@ private: /** This is a vector of all function structs that we have allocated. */ Vector allFunctions; - Boolean * boolTrue; - Boolean * boolFalse; - + Boolean *boolTrue; + Boolean *boolFalse; + /** These two tables are used for deduplicating entries. */ BooleanMatchMap boolMap; ElementMatchMap elemMap; - + SATEncoder *satEncoder; bool unsat; Tuner *tuner; - Transformer* transformer; long long elapsedTime; }; #endif