Restructure transforms a little and run make tabbing
authorbdemsky <bdemsky@uci.edu>
Sat, 2 Sep 2017 06:47:41 +0000 (23:47 -0700)
committerbdemsky <bdemsky@uci.edu>
Sat, 2 Sep 2017 06:47:41 +0000 (23:47 -0700)
43 files changed:
src/AST/asthash.cc
src/AST/asthash.h
src/AST/boolean.h
src/AST/element.h
src/AST/order.cc
src/AST/order.h
src/AST/set.cc
src/AST/set.h
src/ASTAnalyses/ordergraph.cc
src/ASTTransform/decomposeordertransform.cc
src/ASTTransform/decomposeordertransform.h
src/ASTTransform/integerencoding.cc
src/ASTTransform/integerencoding.h
src/ASTTransform/integerencodingrecord.cc
src/ASTTransform/integerencodingrecord.h
src/ASTTransform/pass.h [deleted file]
src/ASTTransform/transform.cc
src/ASTTransform/transform.h
src/ASTTransform/transformer.cc [deleted file]
src/ASTTransform/transformer.h [deleted file]
src/Backend/constraint.cc
src/Backend/orderelement.h
src/Backend/satencoder.cc
src/Backend/satencoder.h
src/Collections/hashset.h
src/Collections/hashtable.h
src/Collections/structs.h
src/Encoders/orderencoding.h
src/Test/ordergraphtest.cc
src/Translator/decomposeorderresolver.cc
src/Translator/decomposeorderresolver.h
src/Translator/integerencorderresolver.cc
src/Translator/integerencorderresolver.h
src/Translator/orderpairresolver.cc
src/Translator/orderpairresolver.h
src/Translator/orderresolver.h
src/Tuner/autotuner.cc
src/Tuner/autotuner.h
src/Tuner/searchtuner.cc
src/Tuner/searchtuner.h
src/common.h
src/csolver.cc
src/csolver.h

index 503ca0e..9fed236 100644 (file)
@@ -4,29 +4,29 @@
 #include "boolean.h"
 #include "element.h"
 
-bool compareArray(Array<Boolean *> * inputs1, Array<Boolean *> *inputs2) {
+bool compareArray(Array<Boolean *> *inputs1, Array<Boolean *> *inputs2) {
        if (inputs1->getSize() != inputs2->getSize())
                return false;
-       for(uint i=0;i<inputs1->getSize();i++) {
+       for (uint i = 0; i < inputs1->getSize(); i++) {
                if (inputs1->get(i) != inputs2->get(i))
                        return false;
        }
        return true;
 }
 
-bool compareArray(Array<Element *> * inputs1, Array<Element *> *inputs2) {
+bool compareArray(Array<Element *> *inputs1, Array<Element *> *inputs2) {
        if (inputs1->getSize() != inputs2->getSize())
                return false;
-       for(uint i=0;i<inputs1->getSize();i++) {
+       for (uint i = 0; i < inputs1->getSize(); i++) {
                if (inputs1->get(i) != inputs2->get(i))
                        return false;
        }
        return true;
 }
 
-uint hashArray(Array<Boolean *> * inputs) {
+uint hashArray(Array<Boolean *> *inputs) {
        uint hash = inputs->getSize();
-       for(uint i=0;i<inputs->getSize();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<Boolean *> * inputs) {
        return hash;
 }
 
-uint hashArray(Array<Element *> * inputs) {
+uint hashArray(Array<Element *> *inputs) {
        uint hash = inputs->getSize();
-       for(uint i=0;i<inputs->getSize();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<Element *> * 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:
index 6dd50dc..a80d67e 100644 (file)
@@ -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);
index afcf512..5a4b5af 100644 (file)
@@ -24,7 +24,7 @@ public:
 };
 
 class BooleanConst : public Boolean {
- public:
+public:
        BooleanConst(bool isTrue);
        Boolean *clone(CSolver *solver, CloneMap *map);
        bool isTrue() {return istrue;}
index 2622437..f1ba4eb 100644 (file)
@@ -15,7 +15,7 @@ public:
        Vector<ASTNode *> parents;
        ElementEncoding encoding;
        virtual Element *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;};
-       
+
        CMEMALLOC;
 };
 
index 908d691..35bca4a 100644 (file)
@@ -41,7 +41,7 @@ Order::~Order() {
                orderPairTable->resetanddelete();
                delete orderPairTable;
        }
-       
+
        if (graph != NULL) {
                delete graph;
        }
index 65291aa..d922235 100644 (file)
@@ -19,7 +19,7 @@ public:
        Order *clone(CSolver *solver, CloneMap *map);
        Vector<BooleanOrder *> 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);
index e33bad0..4e7383a 100644 (file)
@@ -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);
        }
 }
index 056794e..5a5cdab 100644 (file)
@@ -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<uint64_t> *members;
-       
+
 };
 
 #endif/* SET_H */
index 62d4846..f797f5e 100644 (file)
@@ -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;
        }
index 6be7bea..ec8b020 100644 (file)
@@ -1,7 +1,7 @@
-/* 
+/*
  * File:   ordertransform.cc
  * Author: hamed
- * 
+ *
  * Created on August 28, 2017, 10:35 AM
  */
 
 #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<Order *> *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<Order *> ordervec;
        Vector<Order *> 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);
                }
        }
 }
index 3d7d6e8..69f7a1f 100644 (file)
@@ -1,4 +1,4 @@
-/* 
+/*
  * File:   ordertransform.h
  * Author: hamed
  *
 
 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:
-       OrdercurrOrder;
-       OrderGraphcurrGraph;
+private:
+       Order *currOrder;
+       OrderGraph *currGraph;
 };
 
-#endif /* ORDERTRANSFORM_H */
+#endif/* ORDERTRANSFORM_H */
 
index f1b9919..d8150b3 100644 (file)
@@ -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<Order *> *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(){
-       IntegerEncodingRecordencodingRecord = 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; i<size; i++){
+       for (uint i = 0; i < size; i++) {
                orderIntegerEncodingSATEncoder(currOrder->constraints.get(i));
        }
        currOrder->setOrderResolver(new IntegerEncOrderResolver(solver, encodingRecord));
@@ -40,7 +45,7 @@ void IntegerEncodingTransform::doTransform(){
 
 
 void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder) {
-       IntegerEncodingRecordierec = 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);
index 3bfb289..f051a41 100644 (file)
@@ -1,4 +1,4 @@
-/* 
+/*
  * File:   integerencoding.h
  * Author: hamed
  *
 #include "transform.h"
 #include "order.h"
 
-class IntegerEncodingTransform : public Transform{
+class IntegerEncodingTransform : public Transform {
 public:
-       IntegerEncodingTransform(CSolversolver);
+       IntegerEncodingTransform(CSolver *solver);
        void orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder);
-       void setCurrentOrder(Order* _curr) {currOrder = _curr;}
        void doTransform();
-       bool canExecuteTransform();
+       void integerEncode(Order *currOrder);
+
        virtual ~IntegerEncodingTransform();
 private:
-       OrdercurrOrder;
+       Order *currOrder;
        //FIXME:We can remove it, because we don't need it for translating anymore... -HG
-       HashTableOrderIntEncodingorderIntEncoding;
+       HashTableOrderIntEncoding *orderIntEncoding;
 };
 
 
-#endif /* INTEGERENCODING_H */
+#endif/* INTEGERENCODING_H */
 
index abd763f..f8690d7 100644 (file)
@@ -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();
index a85e98a..556e6c5 100644 (file)
@@ -1,4 +1,4 @@
-/* 
+/*
  * File:   integerencodingrecord.h
  * Author: hamed
  *
 
 class IntegerEncodingRecord {
 public:
-       IntegerEncodingRecord(Setset);
+       IntegerEncodingRecord(Set *set);
        ~IntegerEncodingRecord();
-       ElementgetOrderIntegerElement(CSolver *This, uint64_t item, bool create = true);
-       inline SetgetSecondarySet() { return secondarySet; }
+       Element *getOrderIntegerElement(CSolver *This, uint64_t item, bool create = true);
+       inline Set *getSecondarySet() { return secondarySet; }
        CMEMALLOC;
-       
+
 private:
-       SetsecondarySet;
+       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 (file)
index 211bd4e..0000000
+++ /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 */
-
index bf04575..99a181f 100644 (file)
@@ -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() {
 }
index 678c732..976c2c8 100644 (file)
@@ -1,4 +1,4 @@
-/* 
+/*
  * File:   transform.h
  * Author: hamed
  *
 #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 ...
-       CSolversolver;
+       CSolver *solver;
 };
 
-#endif /* TRANSFORM_H */
+#endif/* TRANSFORM_H */
 
diff --git a/src/ASTTransform/transformer.cc b/src/ASTTransform/transformer.cc
deleted file mode 100644 (file)
index 2c814ea..0000000
+++ /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<Order *> *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 (file)
index 4e9f427..0000000
+++ /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 */
-
index 8c247cc..b90ec4a 100644 (file)
@@ -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;
 }
 
index 07913c9..d56a3a7 100644 (file)
@@ -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 ElementgetElement() { return elem; }
+       inline bool equals(OrderElement *oe) { return item == oe->item;}
+       inline Element *getElement() { return elem; }
        CMEMALLOC;
 private:
        uint64_t item;
index 0de0ae4..1d6b4f4 100644 (file)
@@ -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:
index 94115ce..25f6918 100644 (file)
@@ -9,18 +9,18 @@
 typedef Hashtable<Boolean *, Node *, uintptr_t, 4> 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;
index 47b6f50..cdba3b2 100644 (file)
@@ -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--;
                        }
index 18d7353..44b984d 100644 (file)
@@ -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;
index c2ed0e9..ea7fa1f 100644 (file)
@@ -27,7 +27,7 @@ typedef Hashset<OrderElement *, uintptr_t, 4, order_element_hash_function, order
 typedef Hashtable<OrderNode *, HashsetOrderNode *, uintptr_t, 4> HashtableNodeToNodeSet;
 typedef Hashtable<OrderPair *, OrderPair *, uintptr_t, 4, order_pair_hash_function, order_pair_equals> HashtableOrderPair;
 typedef Hashtable<void *, void *, uintptr_t, 4> CloneMap;
-typedef Hashtable<Order* , IntegerEncodingRecord*, uintptr_t, 4> HashTableOrderIntEncoding; 
+typedef Hashtable<Order *, IntegerEncodingRecord *, uintptr_t, 4> HashTableOrderIntEncoding;
 
 typedef SetIterator<TableEntry *, uintptr_t, 4, table_entry_hash_function, table_entry_equals> SetIteratorTableEntry;
 typedef SetIterator<OrderEdge *, uintptr_t, 4, order_edge_hash_function, order_edge_equals> SetIteratorOrderEdge;
index 90a97eb..0792d4a 100644 (file)
@@ -11,8 +11,8 @@ typedef enum OrderEncodingType OrderEncodingType;
 class OrderEncoding {
 public:
        OrderEncoding(Order *order);
-       
-       OrderResolverresolver;
+
+       OrderResolver *resolver;
        OrderEncodingType type;
        Order *order;
        CMEMALLOC;
index 72ad021..092e0ed 100644 (file)
@@ -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;
 }
index 28e3b56..798bb30 100644 (file)
@@ -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<Order*>& _orders):
+DecomposeOrderResolver::DecomposeOrderResolver(OrderGraph *_graph, Vector<Order *> &_orders) :
        graph(_graph),
        orders(_orders.getSize(), _orders.expose())
 {
@@ -20,30 +20,30 @@ DecomposeOrderResolver::DecomposeOrderResolver(OrderGraph* _graph, Vector<Order*
 DecomposeOrderResolver::~DecomposeOrderResolver() {
 }
 
-HappenedBefore DecomposeOrderResolver::resolveOrder(uint64_t first, uint64_t second){
+HappenedBefore DecomposeOrderResolver::resolveOrder(uint64_t first, uint64_t second) {
        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;
        }
        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;
index 590c565..0ca8264 100644 (file)
@@ -1,5 +1,5 @@
 
-/* 
+/*
  * File:   DecomposeOrderResolver.h
  * Author: hamed
  *
 #include "structs.h"
 #include "orderresolver.h"
 
-class DecomposeOrderResolver : public OrderResolver{
+class DecomposeOrderResolver : public OrderResolver {
 public:
-       DecomposeOrderResolver(OrderGraph* graph, Vector<Order *> & orders);
+       DecomposeOrderResolver(OrderGraph *graph, Vector<Order *> &orders);
        HappenedBefore resolveOrder(uint64_t first, uint64_t second);
        virtual ~DecomposeOrderResolver();
 private:
-       OrderGraphgraph;
-       Vector<Order*> orders;
+       OrderGraph *graph;
+       Vector<Order *> orders;
 };
 
-#endif /* DECOMPOSEORDERRESOLVER_H */
+#endif/* DECOMPOSEORDERRESOLVER_H */
 
index a9048ef..4f67018 100644 (file)
@@ -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){
-       Elementelem1 = 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;
-       Elementelem2 = 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;
 }
index e517881..56941e9 100644 (file)
@@ -1,5 +1,5 @@
 
-/* 
+/*
  * File:   integerencorderresolver.h
  * Author: hamed
  *
 #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:
-       CSolversolver;
-       IntegerEncodingRecordierecord;
+       CSolver *solver;
+       IntegerEncodingRecord *ierecord;
 };
 
-#endif /* INTEGERENCORDERRESOLVER_H */
+#endif/* INTEGERENCORDERRESOLVER_H */
 
index fa147d0..3f50077 100644 (file)
@@ -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 ...
-               OrderGraphgraph = 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);
        }
-       
+
 
 }
 
index 8063a90..80ef7e4 100644 (file)
@@ -1,5 +1,5 @@
 
-/* 
+/*
  * File:   orderpairresolver.h
  * Author: hamed
  *
 
 #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:
-       CSolversolver;
-       Orderorder;
+       CSolver *solver;
+       Order *order;
        HappenedBefore resolveTotalOrder(uint64_t first, uint64_t second);
 };
 
-#endif /* ORDERPAIRRESOLVER_H */
+#endif/* ORDERPAIRRESOLVER_H */
 
index 35498ff..7e5ea61 100644 (file)
@@ -1,5 +1,5 @@
 
-/* 
+/*
  * File:   orderresolver.h
  * Author: hamed
  *
 
 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 */
 
index 3765759..9082ae4 100644 (file)
@@ -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;i<solvers.getSize();i++) {
-               CSolver * problem=solvers.get(i);
-               double score=evaluate(problem, tuner);
-               product*=score;
+       double product = 1;
+       for (uint i = 0; i < solvers.getSize(); i++) {
+               CSolver *problem = solvers.get(i);
+               double score = evaluate(problem, tuner);
+               product *= score;
        }
-       return pow(product, 1/((double)solvers.getSize()));
+       return pow(product, 1 / ((double)solvers.getSize()));
 }
 
-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));
+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;i<budget;i++) {
-               SearchTuner *newTuner=mutateTuner(oldTuner, i);
-               double newScore=evaluateAll(newTuner);
+       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
+               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;
index 9e36732..d9fb430 100644 (file)
@@ -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<CSolver *> solvers;      
+       Vector<CSolver *> solvers;
        uint budget;
 };
 #endif
index c3c1af7..52c7a70 100644 (file)
@@ -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;
index 862faf6..20edb7d 100644 (file)
@@ -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<TunableSetting *, uintptr_t, 4, tunableSettingHash, tunableSetti
 typedef SetIterator<TunableSetting *, uintptr_t, 4, tunableSettingHash, tunableSettingEquals> 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;
index 3fffb34..4ebd816 100644 (file)
@@ -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__ */
index a2081b8..de9543e 100644 (file)
 #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;i<asize;i++) {
-                       Boolean *b=array[i];
+               uint newindex = 0;
+               for (uint i = 0; i < asize; i++) {
+                       Boolean *b = array[i];
                        if (b->type == 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;i<asize;i++) {
-                       Boolean *b=array[i];
+               uint newindex = 0;
+               for (uint i = 0; i < asize; i++) {
+                       Boolean *b = array[i];
                        if (b->type == 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;
index 7942839..1ff4cd1 100644 (file)
@@ -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<Order *> *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<Function *> 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