bug fixes
authorBrian Demsky <bdemsky@uci.edu>
Sun, 31 Dec 2017 08:55:12 +0000 (00:55 -0800)
committerBrian Demsky <bdemsky@uci.edu>
Sun, 31 Dec 2017 08:55:12 +0000 (00:55 -0800)
35 files changed:
src/AST/asthash.cc
src/AST/element.h
src/AST/order.cc
src/AST/set.cc
src/AST/set.h
src/ASTAnalyses/Order/orderanalysis.cc
src/ASTAnalyses/Order/orderanalysis.h
src/ASTAnalyses/Order/ordergraph.cc
src/ASTAnalyses/Order/ordernode.h
src/ASTTransform/decomposeordertransform.cc
src/Backend/cnfexpr.cc
src/Backend/constraint.cc
src/Backend/inc_solver.cc
src/Backend/satencoder.cc
src/Backend/satencoder.h
src/Collections/array.h
src/Collections/hashset.h
src/Collections/hashtable.h
src/Collections/qsort.cc
src/Collections/structs.cc
src/Collections/vector.h
src/Encoders/elementencoding.cc
src/Encoders/elementencoding.h
src/Serialize/deserializer.cc
src/Serialize/serializer.cc
src/Serialize/serializer.h
src/Test/deserializerautotune.cc [changed mode: 0755->0644]
src/Test/deserializersolveprint.cc [changed mode: 0755->0644]
src/Test/deserializersolveprintopt.cc [changed mode: 0755->0644]
src/Test/deserializersolvetest.cc [changed mode: 0755->0644]
src/Test/deserializertest.cc
src/common.h
src/csolver.cc
src/csolver.h
src/mymemory.h

index 7350a7e..347e5fa 100644 (file)
@@ -4,8 +4,8 @@
 #include "boolean.h"
 #include "element.h"
 
-#define HASHNEXT(hash, newval) {hash+=newval; hash += hash << 10; hash ^= hash >>6;}
-#define HASHFINAL(hash) {hash += hash <<3; hash ^= hash >> 11; hash += hash << 15;}
+#define HASHNEXT(hash, newval) {hash += newval; hash += hash << 10; hash ^= hash >> 6;}
+#define HASHFINAL(hash) {hash += hash << 3; hash ^= hash >> 11; hash += hash << 15;}
 
 bool compareArray(Array<BooleanEdge> *inputs1, Array<BooleanEdge> *inputs2) {
        if (inputs1->getSize() != inputs2->getSize())
@@ -64,7 +64,7 @@ uint hashBoolean(Boolean *b) {
        }
        case LOGICOP: {
                BooleanLogic *l = (BooleanLogic *)b;
-               return ((uint)l->op) + 43* hashArray(&l->inputs);
+               return ((uint)l->op) + 43 * hashArray(&l->inputs);
        }
        case PREDICATEOP: {
                BooleanPredicate *p = (BooleanPredicate *)b;
index 1e7b1f2..5259c09 100644 (file)
@@ -26,7 +26,7 @@ public:
 class ElementSet : public Element {
 public:
        ElementSet(ASTNodeType type, Set *s);
-        virtual ~ElementSet(){}
+       virtual ~ElementSet() {}
        ElementSet(Set *s);
        virtual Element *clone(CSolver *solver, CloneMap *map);
        virtual void serialize(Serializer *serializer);
@@ -41,7 +41,7 @@ protected:
 class ElementConst : public ElementSet {
 public:
        ElementConst(uint64_t value, Set *_set);
-        virtual ~ElementConst(){}
+       virtual ~ElementConst() {}
        uint64_t value;
        virtual void serialize(Serializer *serializer);
        virtual void print();
@@ -51,7 +51,7 @@ public:
 
 class ElementFunction : public Element {
 public:
-        virtual ~ElementFunction(){}
+       virtual ~ElementFunction() {}
        ElementFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus);
        Array<Element *> inputs;
        BooleanEdge overflowstatus;
index 315b112..2b3184a 100644 (file)
@@ -33,7 +33,7 @@ Order *Order::clone(CSolver *solver, CloneMap *map) {
 
 HashtableOrderPair *Order::getOrderPairTable() {
        ASSERT( encoding.resolver != NULL);
-       if (OrderPairResolver *t = dynamic_cast<OrderPairResolver *>(encoding.resolver)) {
+       if (OrderPairResolver * t = dynamic_cast<OrderPairResolver *>(encoding.resolver)) {
                return t->getOrderPairTable();
        } else {
                ASSERT(0);
index d45791a..e019b12 100644 (file)
@@ -139,19 +139,19 @@ void Set::serialize(Serializer *serializer) {
        serializer->mywrite(&This, sizeof(Set *));
        serializer->mywrite(&type, sizeof(VarType));
        serializer->mywrite(&isRange, sizeof(bool));
-        bool isMutable = isMutableSet();
+       bool isMutable = isMutableSet();
        serializer->mywrite(&isMutable, sizeof(bool));
-        if(isRange){
-                serializer->mywrite(&low, sizeof(uint64_t));
-                serializer->mywrite(&high, sizeof(uint64_t));
-        }else {
-                uint size = members->getSize();
-                serializer->mywrite(&size, sizeof(uint));
-                for(uint i=0; i<size; i++){
-                        uint64_t mem = members->get(i);
-                        serializer->mywrite(&mem, sizeof(uint64_t));
-                }
-        }
+       if (isRange) {
+               serializer->mywrite(&low, sizeof(uint64_t));
+               serializer->mywrite(&high, sizeof(uint64_t));
+       else {
+               uint size = members->getSize();
+               serializer->mywrite(&size, sizeof(uint));
+               for (uint i = 0; i < size; i++) {
+                       uint64_t mem = members->get(i);
+                       serializer->mywrite(&mem, sizeof(uint64_t));
+               }
+       }
 }
 
 void Set::print() {
index c647af5..34784d3 100644 (file)
@@ -33,7 +33,7 @@ public:
 protected:
        VarType type;
        bool isRange;
-       uint64_t low;//also used to count unique items
+       uint64_t low;   //also used to count unique items
        uint64_t high;
        Vector<uint64_t> *members;
 };
index 8a991a4..cd50ed9 100644 (file)
 #include "tunable.h"
 
 /** Returns a table that maps a node to the set of nodes that can reach the node. */
-HashtableNodeToNodeSet * getMustReachMap(CSolver  *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
+HashtableNodeToNodeSet *getMustReachMap(CSolver  *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
        uint size = finishNodes->getSize();
        HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
-       
+
        for (int i = size - 1; i >= 0; i--) {
                OrderNode *node = finishNodes->get(i);
                HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
                table->put(node, sources);
-               
+
                {
                        //Compute source sets
                        SetIteratorOrderEdge *iterator = node->inEdges.iterator();
@@ -39,18 +39,18 @@ HashtableNodeToNodeSet * getMustReachMap(CSolver  *solver, OrderGraph *graph, Ve
        return table;
 }
 
-void DFSClearContradictions(CSolver *solver, OrderGraph *graph, HashtableNodeToNodeSet * table, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure) {
+void DFSClearContradictions(CSolver *solver, OrderGraph *graph, HashtableNodeToNodeSet *table, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure) {
        uint size = finishNodes->getSize();
 
        for (int i = size - 1; i >= 0; i--) {
                OrderNode *node = finishNodes->get(i);
                HashsetOrderNode *sources = table->get(node);
-               
+
                if (computeTransitiveClosure) {
                        //Compute full transitive closure for nodes
                        SetIteratorOrderNode *srciterator = sources->iterator();
                        while (srciterator->hasNext()) {
-                               OrderNode *srcnode = (OrderNode*)srciterator->next();
+                               OrderNode *srcnode = (OrderNode *)srciterator->next();
                                OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(srcnode, node);
                                newedge->mustPos = true;
                                newedge->polPos = true;
@@ -105,7 +105,7 @@ void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiv
        //Topologically sort the mustPos edge graph
        graph->DFSMust(&finishNodes);
        graph->resetNodeInfoStatusSCC();
-       HashtableNodeToNodeSet * table=getMustReachMap(solver, graph, & finishNodes);
+       HashtableNodeToNodeSet *table = getMustReachMap(solver, graph, &finishNodes);
        //Find any backwards edges that complete cycles and force them to be mustNeg
        DFSClearContradictions(solver, graph, table, &finishNodes, computeTransitiveClosure);
        table->resetAndDeleteVals();
index a371c85..72f389c 100644 (file)
@@ -4,8 +4,8 @@
 #include "structs.h"
 #include "mymemory.h"
 
-void DFSClearContradictions(CSolver *solver, OrderGraph *graph, HashtableNodeToNodeSet * table, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure);
-HashtableNodeToNodeSet * getMustReachMap(CSolver  *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes);
+void DFSClearContradictions(CSolver *solver, OrderGraph *graph, HashtableNodeToNodeSet *table, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure);
+HashtableNodeToNodeSet *getMustReachMap(CSolver  *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes);
 
 void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure);
 void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph);
index 9f50949..cbc2e25 100644 (file)
@@ -117,7 +117,7 @@ void OrderGraph::addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrd
 
 OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) {
        OrderNode *node = new OrderNode(id);
-       OrderNode *tmp = (OrderNode*)nodes.get(node);
+       OrderNode *tmp = (OrderNode *)nodes.get(node);
        if ( tmp != NULL) {
                delete node;
                node = tmp;
@@ -129,7 +129,7 @@ OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) {
 
 OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) {
        OrderNodeKey node(id);
-       OrderNode *tmp = (OrderNode*)nodes.get(&node);
+       OrderNode *tmp = (OrderNode *)nodes.get(&node);
        return tmp;
 }
 
@@ -225,7 +225,7 @@ bool OrderGraph::isTherePathVisit(HashsetOrderNode &visited, OrderNode *current,
 void OrderGraph::DFS(Vector<OrderNode *> *finishNodes) {
        SetIteratorOrderNode *iterator = getNodes();
        while (iterator->hasNext()) {
-               OrderNode *node = (OrderNode*)iterator->next();
+               OrderNode *node = (OrderNode *)iterator->next();
                if (node->status == NOTVISITED && !node->removed) {
                        node->status = VISITED;
                        DFSNodeVisit(node, finishNodes, false, false, 0);
@@ -239,7 +239,7 @@ void OrderGraph::DFS(Vector<OrderNode *> *finishNodes) {
 void OrderGraph::DFSMust(Vector<OrderNode *> *finishNodes) {
        SetIteratorOrderNode *iterator = getNodes();
        while (iterator->hasNext()) {
-               OrderNode *node = (OrderNode*)iterator->next();
+               OrderNode *node = (OrderNode *)iterator->next();
                if (node->status == NOTVISITED && !node->removed) {
                        node->status = VISITED;
                        DFSNodeVisit(node, finishNodes, false, true, 0);
@@ -294,7 +294,7 @@ void OrderGraph::DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes,
 void OrderGraph::resetNodeInfoStatusSCC() {
        SetIteratorOrderNode *iterator = getNodes();
        while (iterator->hasNext()) {
-               ((OrderNode*)iterator->next())->status = NOTVISITED;
+               ((OrderNode *)iterator->next())->status = NOTVISITED;
        }
        delete iterator;
 }
index 4a40466..1303a5a 100644 (file)
 enum NodeStatus {NOTVISITED, VISITED, FINISHED, ADDEDTOSET};
 typedef enum NodeStatus NodeStatus;
 
-class OrderNodeKey{
+class OrderNodeKey {
 public:
-    OrderNodeKey(uint64_t id) : id(id){}
-    virtual ~OrderNodeKey(){}
-    uint64_t getID() {return id;}
-    uint64_t id;
+       OrderNodeKey(uint64_t id) : id(id) {}
+       virtual ~OrderNodeKey() {}
+       uint64_t getID() {return id;}
+       uint64_t id;
 };
 
 class OrderNode : public OrderNodeKey {
 public:
        OrderNode(uint64_t id);
-        virtual ~OrderNode(){}
+       virtual ~OrderNode() {}
        void addNewIncomingEdge(OrderEdge *edge);
        void addNewOutgoingEdge(OrderEdge *edge);
 
index 525a03c..c75fbec 100644 (file)
@@ -244,7 +244,7 @@ void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode
 void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, DecomposeOrderResolver *dor) {
        SetIteratorOrderNode *iterator = graph->getNodes();
        while (iterator->hasNext()) {
-               OrderNode *node = (OrderNode*)iterator->next();
+               OrderNode *node = (OrderNode *)iterator->next();
                if (node->removed)
                        continue;
                if (isMustBeTrueNode(node)) {
@@ -257,7 +257,7 @@ void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, Decompose
 void DecomposeOrderTransform::mustEdgePrune(OrderGraph *graph, DecomposeOrderResolver *dor) {
        SetIteratorOrderNode *iterator = graph->getNodes();
        while (iterator->hasNext()) {
-               OrderNode *node = (OrderNode*)iterator->next();
+               OrderNode *node = (OrderNode *)iterator->next();
                if (node->removed)
                        continue;
                attemptNodeMerge(graph, node, dor);
@@ -339,6 +339,7 @@ void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, Ord
                sink->inEdges.remove(outedge);
                //save the remapping that we did
                dor->remapEdge(dstnode->getID(), sink->getID(), node->getID(), sink->getID());
+
                //create the new edge
                OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(node, sink);
                //update the flags
index b04044a..e8af3b8 100644 (file)
@@ -1,5 +1,6 @@
 #include "cnfexpr.h"
 #include <stdio.h>
+#include "common.h"
 /*
    V2 Copyright (c) 2014 Ben Chambers, Eugene Goldberg, Pete Manolios,
    Vasilis Papavasileiou, Sudarshan Srinivasan, and Daron Vroon.
@@ -417,7 +418,7 @@ void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
                                mergeArray[mergeIndex++] = merge;
                        }
                }
-               deleteLitVector(lThis);//Done with this litVector
+               deleteLitVector(lThis); //Done with this litVector
        }
 
        /** Finally do the singleton, singleton pairs */
index 8486282..386706d 100644 (file)
@@ -78,22 +78,21 @@ void deleteCNF(CNF *cnf) {
        ourfree(cnf);
 }
 
-void resetCNF(CNF *cnf){
-        for (uint i = 0; i < cnf->capacity; i++) {
+void resetCNF(CNF *cnf) {
+       for (uint i = 0; i < cnf->capacity; i++) {
                Node *n = cnf->node_array[i];
                if (n != NULL)
                        ourfree(n);
        }
-        clearVectorEdge(&cnf->constraints);
-        clearVectorEdge(&cnf->args);
-        deleteIncrementalSolver(cnf->solver);
-        memset(cnf->node_array, 0, sizeof(Node *) * cnf->capacity);
-        
-        cnf->varcount = 1;
-        cnf->size = 0;
-        cnf->enableMatching = true;
-        cnf->solver = allocIncrementalSolver();
-        cnf->solveTime = 0;
+       clearVectorEdge(&cnf->constraints);
+       clearVectorEdge(&cnf->args);
+       resetSolver(cnf->solver);
+       memset(cnf->node_array, 0, sizeof(Node *) * cnf->capacity);
+
+       cnf->varcount = 1;
+       cnf->size = 0;
+       cnf->enableMatching = true;
+       cnf->solveTime = 0;
        cnf->encodeTime = 0;
 }
 
@@ -209,7 +208,12 @@ Edge constraintOR2(CNF *cnf, Edge left, Edge right) {
 }
 
 int comparefunction(const Edge *e1, const Edge *e2) {
-       return ((uintptr_t)e1->node_ptr) - ((uintptr_t)e2->node_ptr);
+       if (e1->node_ptr == e2->node_ptr)
+               return 0;
+       if (((uintptr_t)e1->node_ptr) < ((uintptr_t) e2->node_ptr))
+               return -1;
+       else
+               return 1;
 }
 
 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
@@ -370,9 +374,9 @@ int solveCNF(CNF *cnf) {
        int result = solve(cnf->solver);
        long long finishTime = getTimeNano();
        cnf->encodeTime = startSolve - startTime;
-        model_print("CNF Encode time: %f\n", cnf->encodeTime/1000000000.0);
+       model_print("CNF Encode time: %f\n", cnf->encodeTime / 1000000000.0);
        cnf->solveTime = finishTime - startSolve;
-       model_print("Solve time: %f\n", cnf->solveTime/ 1000000000.0);
+       model_print("Solve time: %f\n", cnf->solveTime / 1000000000.0);
        return result;
 }
 
index 7d0fd65..d295cee 100644 (file)
@@ -67,7 +67,10 @@ void addArrayClauseLiteral(IncrementalSolver *This, uint numliterals, int *liter
 }
 
 void finishedClauses(IncrementalSolver *This) {
-       addClauseLiteral(This, 0);
+       This->buffer[This->offset++] = 0;
+       if (This->offset == IS_BUFFERSIZE) {
+               flushBufferSolver(This);
+       }
 }
 
 void freeze(IncrementalSolver *This, int variable) {
index 206d2b7..bf8ede4 100644 (file)
@@ -21,9 +21,9 @@ SATEncoder::~SATEncoder() {
        deleteCNF(cnf);
 }
 
-void SATEncoder::resetSATEncoder(){
-        resetCNF(cnf);
-        booledgeMap.reset();
+void SATEncoder::resetSATEncoder() {
+       resetCNF(cnf);
+       booledgeMap.reset();
 }
 
 int SATEncoder::solve() {
index dcf3b86..0347164 100644 (file)
@@ -13,7 +13,7 @@ public:
        int solve();
        SATEncoder(CSolver *solver);
        ~SATEncoder();
-        void resetSATEncoder();
+       void resetSATEncoder();
        void encodeAllSATEncoder(CSolver *csolver);
        Edge encodeConstraintSATEncoder(BooleanEdge constraint);
        CNF *getCNF() { return cnf;}
index 03d83cd..f4ae3a5 100644 (file)
@@ -5,13 +5,13 @@ template<typename type>
 class Array {
 public:
        Array(uint _size) :
-               array((type *)ourcalloc(1, sizeof(type) * _size)),
+               array((type *) ourcalloc(1, sizeof(type) * _size)),
                size(_size)
        {
        }
 
        Array(type *_array, uint _size) :
-               array((type *)ourcalloc(1, sizeof(type) * _size)),
+               array((type *) ourcalloc(1, sizeof(type) * _size)),
                size(_size) {
                memcpy(array, _array, _size * sizeof(type));
        }
index 86cbce9..009c047 100644 (file)
@@ -18,10 +18,10 @@ struct Linknode {
        Linknode<_Key> *next;
 };
 
-template<typename _Key, typename _KeyInt, int _Shift, unsigned int (*hash_function)(_Key), bool (*equals)(_Key, _Key)>
+template<typename _Key, typename _KeyInt, int _Shift, unsigned int (*hash_function) (_Key), bool (*equals) (_Key, _Key)>
 class Hashset;
 
-template<typename _Key, typename _KeyInt, int _Shift, unsigned int (*hash_function)(_Key) = defaultHashFunction<_Key, _Shift, _KeyInt>, bool (*equals)(_Key, _Key) = defaultEquals<_Key> >
+template<typename _Key, typename _KeyInt, int _Shift, unsigned int (*hash_function) (_Key) = defaultHashFunction<_Key, _Shift, _KeyInt>, bool (*equals) (_Key, _Key) = defaultEquals<_Key> >
 class SetIterator {
 public:
        SetIterator(Linknode<_Key> *_curr, Hashset <_Key, _KeyInt, _Shift, hash_function, equals> *_set) :
@@ -76,7 +76,7 @@ private:
        Hashset <_Key, _KeyInt, _Shift, hash_function, equals> *set;
 };
 
-template<typename _Key, typename _KeyInt, int _Shift = 0, unsigned int (*hash_function)(_Key) = defaultHashFunction<_Key, _Shift, _KeyInt>, bool (*equals)(_Key, _Key) = defaultEquals<_Key> >
+template<typename _Key, typename _KeyInt, int _Shift = 0, unsigned int (*hash_function) (_Key) = defaultHashFunction<_Key, _Shift, _KeyInt>, bool (*equals) (_Key, _Key) = defaultEquals<_Key> >
 class Hashset {
 public:
        Hashset(unsigned int initialcapacity = 16, double factor = 0.5) :
index 9f5f3b3..0a50bb9 100644 (file)
@@ -57,7 +57,7 @@ inline bool defaultEquals(_Key key1, _Key key2) {
  *                 manipulation and storage.
  * @tparam _Shift  Logical shift to apply to all keys. Default 0.
  */
-template<typename _Key, typename _Val, typename _KeyInt, int _Shift = 0, unsigned int (*hash_function)(_Key) = defaultHashFunction<_Key, _Shift, _KeyInt>, bool (*equals)(_Key, _Key) = defaultEquals<_Key> >
+template<typename _Key, typename _Val, typename _KeyInt, int _Shift = 0, unsigned int (*hash_function) (_Key) = defaultHashFunction<_Key, _Shift, _KeyInt>, bool (*equals) (_Key, _Key) = defaultEquals<_Key> >
 class Hashtable {
 public:
        /**
@@ -255,9 +255,9 @@ public:
                                if (!search->val)
                                        break;
                        } else
-                               if (hashcode == search->hashcode)
-                                       if (equals(search->key, key))
-                                               return search->val;
+                       if (hashcode == search->hashcode)
+                               if (equals(search->key, key))
+                                       return search->val;
                        index++;
                        index &= capacitymask;
                        if (index == oindex)
@@ -297,15 +297,15 @@ public:
                                if (!search->val)
                                        break;
                        } else
-                               if (hashcode == search->hashcode)
-                                       if (equals(search->key, key)) {
-                                               _Val v = search->val;
-                                               //empty out this bin
-                                               search->val = (_Val) 1;
-                                               search->key = 0;
-                                               size--;
-                                               return v;
-                                       }
+                       if (hashcode == search->hashcode)
+                               if (equals(search->key, key)) {
+                                       _Val v = search->val;
+                                       //empty out this bin
+                                       search->val = (_Val) 1;
+                                       search->key = 0;
+                                       size--;
+                                       return v;
+                               }
                        index++;
                } while (true);
                return (_Val)0;
@@ -338,9 +338,9 @@ public:
                                if (!search->val)
                                        break;
                        } else
-                               if (hashcode == search->hashcode)
-                                       if (equals(search->key, key))
-                                               return true;
+                       if (hashcode == search->hashcode)
+                               if (equals(search->key, key))
+                                       return true;
                        index++;
                } while (true);
                return false;
index f4e7ec9..d384220 100644 (file)
  * arithmetic gets lost in the time required for comparison function calls.
  */
 #define SWAP(a, b, count, size, tmp) { \
-               count = size; \
+               count = size;   \
                do { \
-                       tmp = *a; \
+                       tmp = *a;       \
                        *a++ = *b; \
-                       *b++ = tmp; \
+                       *b++ = tmp;     \
                } while (--count); \
 }
 
 /* Copy one block of size size to another. */
-#define COPY(a, b, count, size, tmp1, tmp2) { \
-               count = size; \
-               tmp1 = a; \
-               tmp2 = b; \
+#define COPY(a, b, count, size, tmp1, tmp2) {  \
+               count = size;   \
+               tmp1 = a;       \
+               tmp2 = b;       \
                do { \
                        *tmp1++ = *tmp2++; \
                } while (--count); \
  * j < nmemb, select largest of Ki, Kj and Kj+1.
  */
 #define CREATE(initval, nmemb, par_i, child_i, par, child, size, count, tmp) { \
-               for (par_i = initval; (child_i = par_i * 2) <= nmemb; \
-                                par_i = child_i) { \
+               for (par_i = initval; (child_i = par_i * 2) <= nmemb;   \
+                                par_i = child_i) {     \
                        child = base + child_i * size; \
-                       if (child_i < nmemb && compar(child, child + size) < 0) { \
+                       if (child_i < nmemb && compar(child, child + size) < 0) {       \
                                child += size; \
                                ++child_i; \
-                       } \
+                       }       \
                        par = base + par_i * size; \
                        if (compar(child, par) <= 0) \
                                break; \
-                       SWAP(par, child, count, size, tmp); \
-               } \
+                       SWAP(par, child, count, size, tmp);     \
+               }       \
 }
 
 /*
  *
  * XXX Don't break the #define SELECT line, below.  Reiser cpp gets upset.
  */
-#define SELECT(par_i, child_i, nmemb, par, child, size, k, count, tmp1, tmp2) { \
+#define SELECT(par_i, child_i, nmemb, par, child, size, k, count, tmp1, tmp2) {        \
                for (par_i = 1; (child_i = par_i * 2) <= nmemb; par_i = child_i) { \
                        child = base + child_i * size; \
-                       if (child_i < nmemb && compar(child, child + size) < 0) { \
+                       if (child_i < nmemb && compar(child, child + size) < 0) {       \
                                child += size; \
                                ++child_i; \
-                       } \
+                       }       \
                        par = base + par_i * size; \
                        COPY(par, child, count, size, tmp1, tmp2); \
-               } \
-               for (;; ) { \
+               }       \
+               for (;; ) {     \
                        child_i = par_i; \
                        par_i = child_i / 2; \
                        child = base + child_i * size; \
                        par = base + par_i * size; \
-                       if (child_i == 1 || compar(k, par) < 0) { \
+                       if (child_i == 1 || compar(k, par) < 0) {       \
                                COPY(child, k, count, size, tmp1, tmp2); \
                                break; \
-                       } \
+                       }       \
                        COPY(child, par, count, size, tmp1, tmp2); \
-               } \
+               }       \
 }
 
 /*
@@ -236,18 +236,18 @@ static __inline void swapfunc(char *, char *, size_t, int);
 #define SWAPTYPE_INT  4
 #define SWAPTYPE_LONG 5
 
-#define TYPE_ALIGNED(TYPE, a, es)     \
+#define TYPE_ALIGNED(TYPE, a, es)                      \
        (((char *)a - (char *)0) % sizeof(TYPE) == 0 && es % sizeof(TYPE) == 0)
 
-#define swapcode(TYPE, parmi, parmj, n) {     \
-               size_t i = (n) / sizeof (TYPE);     \
-               TYPE *pi = (TYPE *) (parmi);      \
-               TYPE *pj = (TYPE *) (parmj);      \
-               do {            \
-                       TYPE t = *pi;      \
-                       *pi++ = *pj;        \
-                       *pj++ = t;        \
-               } while (--i > 0);        \
+#define swapcode(TYPE, parmi, parmj, n) {                      \
+               size_t i = (n) / sizeof (TYPE);                 \
+               TYPE *pi = (TYPE *) (parmi);                    \
+               TYPE *pj = (TYPE *) (parmj);                    \
+               do {                                            \
+                       TYPE t = *pi;                    \
+                       *pi++ = *pj;                            \
+                       *pj++ = t;                              \
+               } while (--i > 0);                              \
 }
 
 static __inline void
@@ -268,23 +268,23 @@ swapfunc(char *a, char *b, size_t n, int swaptype)
        }
 }
 
-#define swap(a, b)  do {        \
-               switch (swaptype) {       \
-               case SWAPTYPE_INT: {        \
-                       int t = *(int *)(a);      \
-                       *(int *)(a) = *(int *)(b);    \
-                       *(int *)(b) = t;      \
-                       break;          \
-               }           \
-               case SWAPTYPE_LONG: {       \
-                       long t = *(long *)(a);      \
-                       *(long *)(a) = *(long *)(b);    \
-                       *(long *)(b) = t;     \
-                       break;          \
-               }           \
-               default:          \
-                       swapfunc(a, b, es, swaptype);   \
-               }           \
+#define swap(a, b)  do {                               \
+               switch (swaptype) {                             \
+               case SWAPTYPE_INT: {                            \
+                       int t = *(int *)(a);                    \
+                       *(int *)(a) = *(int *)(b);              \
+                       *(int *)(b) = t;                        \
+                       break;                                  \
+               }                                               \
+               case SWAPTYPE_LONG: {                           \
+                       long t = *(long *)(a);                  \
+                       *(long *)(a) = *(long *)(b);            \
+                       *(long *)(b) = t;                       \
+                       break;                                  \
+               }                                               \
+               default:                                        \
+                       swapfunc(a, b, es, swaptype);           \
+               }                                               \
 } while (0)
 
 #define vecswap(a, b, n)  if ((n) > 0) swapfunc(a, b, n, swaptype)
index ac69f9d..7673474 100644 (file)
@@ -8,8 +8,8 @@
 #include "structs.h"
 #include "decomposeorderresolver.h"
 
-#define HASHNEXT(hash, newval) {hash+=newval; hash += hash << 10; hash ^= hash >>6;}
-#define HASHFINAL(hash) {hash += hash <<3; hash ^= hash >> 11; hash += hash << 15;}
+#define HASHNEXT(hash, newval) {hash += newval; hash += hash << 10; hash ^= hash >> 6;}
+#define HASHFINAL(hash) {hash += hash << 3; hash ^= hash >> 11; hash += hash << 15;}
 
 unsigned int table_entry_hash_function(TableEntry *This) {
        unsigned int h = 0;
@@ -38,7 +38,7 @@ bool order_node_equals(OrderNodeKey *key1, OrderNodeKey *key2) {
 }
 
 unsigned int order_edge_hash_function(OrderEdge *This) {
-       uint hash=0;
+       uint hash = 0;
        HASHNEXT(hash, (uint)(uintptr_t) This->sink);
        HASHNEXT(hash, (uint)(uintptr_t) This->source);
        HASHFINAL(hash);
@@ -58,7 +58,7 @@ bool order_element_equals(OrderElement *key1, OrderElement *key2) {
 }
 
 unsigned int order_pair_hash_function(OrderPair *This) {
-       uint hash=0;
+       uint hash = 0;
        HASHNEXT(hash, This->first);
        HASHNEXT(hash, This->second);
        HASHFINAL(hash);
@@ -70,7 +70,7 @@ bool order_pair_equals(OrderPair *key1, OrderPair *key2) {
 }
 
 unsigned int doredge_hash_function(DOREdge *key) {
-       uint hash=0;
+       uint hash = 0;
        HASHNEXT(hash, (uint) key->newfirst);
        HASHNEXT(hash, (uint) key->newsecond);
        HASHFINAL(hash);
index 6c53253..3cf0010 100644 (file)
 #define VECTOR_H
 #include <string.h>
 
-#define VectorDef(name, type)                                           \
-       struct Vector ## name {                                               \
-               uint size;                                                          \
-               uint capacity;                                                      \
-               type *array;                                                       \
-       };                                                                    \
-       typedef struct Vector ## name Vector ## name;                         \
-       Vector ## name * allocVector ## name(uint capacity);                  \
-       Vector ## name * allocDefVector ## name();                            \
-       Vector ## name * allocVectorArray ## name(uint capacity, type * array); \
-       void pushVector ## name(Vector ## name * vector, type item);           \
-       type lastVector ## name(Vector ## name * vector);                      \
-       void popVector ## name(Vector ## name * vector);                       \
-       type getVector ## name(Vector ## name * vector, uint index);           \
-       void setExpandVector ## name(Vector ## name * vector, uint index, type item); \
-       void setVector ## name(Vector ## name * vector, uint index, type item); \
-       uint getSizeVector ## name(const Vector ## name * vector);                   \
-       void setSizeVector ## name(Vector ## name * vector, uint size);        \
-       void deleteVector ## name(Vector ## name * vector);                    \
-       void clearVector ## name(Vector ## name * vector);                     \
-       void deleteVectorArray ## name(Vector ## name * vector);               \
-       type *exposeArray ## name(Vector ## name * vector);                  \
+#define VectorDef(name, type)                                                                                                                                                                          \
+       struct Vector ## name {                                                                                                                                                                                         \
+               uint size;                                                                                                                                                                                                                                      \
+               uint capacity;                                                                                                                                                                                                                  \
+               type *array;                                                                                                                                                                                                                     \
+       };                                                                                                                                                                                                                                                                              \
+       typedef struct Vector ## name Vector ## name;                                                                                                   \
+       Vector ## name * allocVector ## name(uint capacity);                                                                    \
+       Vector ## name * allocDefVector ## name();                                                                                                              \
+       Vector ## name * allocVectorArray ## name(uint capacity, type * array); \
+       void pushVector ## name(Vector ## name * vector, type item);                                     \
+       type lastVector ## name(Vector ## name * vector);                                                                                        \
+       void popVector ## name(Vector ## name * vector);                                                                                         \
+       type getVector ## name(Vector ## name * vector, uint index);                                     \
+       void setExpandVector ## name(Vector ## name * vector, uint index, type item);   \
+       void setVector ## name(Vector ## name * vector, uint index, type item); \
+       uint getSizeVector ## name(const Vector ## name * vector);                                                                       \
+       void setSizeVector ## name(Vector ## name * vector, uint size);                          \
+       void deleteVector ## name(Vector ## name * vector);                                                                              \
+       void clearVector ## name(Vector ## name * vector);                                                                               \
+       void deleteVectorArray ## name(Vector ## name * vector);                                                         \
+       type *exposeArray ## name(Vector ## name * vector);                                                                      \
        void initVector ## name(Vector ## name * vector, uint capacity); \
-       void initDefVector ## name(Vector ## name * vector);            \
+       void initDefVector ## name(Vector ## name * vector);                                            \
        void initVectorArray ## name(Vector ## name * vector, uint capacity, type * array);
 
-#define VectorImpl(name, type, defcap)                                  \
-       Vector ## name * allocDefVector ## name() {                           \
-               return allocVector ## name(defcap);                                 \
-       }                                                                     \
-       Vector ## name * allocVector ## name(uint capacity) {                 \
-               Vector ## name * tmp = (Vector ## name *)ourmalloc(sizeof(Vector ## name));  \
-               tmp->size = 0;                                                      \
-               tmp->capacity = capacity;                                           \
-               tmp->array = (type *) ourmalloc(sizeof(type) * capacity);           \
-               return tmp;                                                         \
-       }                                                                     \
-       Vector ## name * allocVectorArray ## name(uint capacity, type * array)  { \
-               Vector ## name * tmp = allocVector ## name(capacity);               \
-               tmp->size = capacity;                                                 \
-               memcpy(tmp->array, array, capacity * sizeof(type));                 \
-               return tmp;                                                         \
-       }                                                                     \
-       void popVector ## name(Vector ## name * vector) {                      \
-               vector->size--;                                                     \
-       }                                                                     \
-       type lastVector ## name(Vector ## name * vector) {                     \
-               return vector->array[vector->size - 1];                               \
-       }                                                                     \
-       void setSizeVector ## name(Vector ## name * vector, uint size) {       \
-               if (size <= vector->size) {                                         \
-                       vector->size = size;                                                \
-                       return;                                                           \
-               } else if (size > vector->capacity) {                               \
-                       vector->array = (type *)ourrealloc(vector->array, size * sizeof(type)); \
-                       vector->capacity = size;                                            \
-               }                                                                   \
+#define VectorImpl(name, type, defcap)                                                                                                                                 \
+       Vector ## name * allocDefVector ## name() {                                                                                                             \
+               return allocVector ## name(defcap);                                                                                                                                     \
+       }                                                                                                                                                                                                                                                                                       \
+       Vector ## name * allocVector ## name(uint capacity) {                                                                   \
+               Vector ## name * tmp = (Vector ## name *)ourmalloc(sizeof(Vector ## name));      \
+               tmp->size = 0;                                                                                                                                                                                                                  \
+               tmp->capacity = capacity;                                                                                                                                                                               \
+               tmp->array = (type *) ourmalloc(sizeof(type) * capacity);                                               \
+               return tmp;                                                                                                                                                                                                                                     \
+       }                                                                                                                                                                                                                                                                                       \
+       Vector ## name * allocVectorArray ## name(uint capacity, type * array)  {       \
+               Vector ## name * tmp = allocVector ## name(capacity);                                                           \
+               tmp->size = capacity;                                                                                                                                                                                                   \
+               memcpy(tmp->array, array, capacity * sizeof(type));                                                                     \
+               return tmp;                                                                                                                                                                                                                                     \
+       }                                                                                                                                                                                                                                                                                       \
+       void popVector ## name(Vector ## name * vector) {                                                                                        \
+               vector->size--;                                                                                                                                                                                                                 \
+       }                                                                                                                                                                                                                                                                                       \
+       type lastVector ## name(Vector ## name * vector) {                                                                               \
+               return vector->array[vector->size - 1];                                                                                                                         \
+       }                                                                                                                                                                                                                                                                                       \
+       void setSizeVector ## name(Vector ## name * vector, uint size) {                         \
+               if (size <= vector->size) {                                                                                                                                                                     \
+                       vector->size = size;                                                                                                                                                                                            \
+                       return;                                                                                                                                                                                                                                         \
+               } else if (size > vector->capacity) {                                                                                                                           \
+                       vector->array = (type *)ourrealloc(vector->array, size * sizeof(type)); \
+                       vector->capacity = size;                                                                                                                                                                                \
+               }                                                                                                                                                                                                                                                                               \
                bzero(&vector->array[vector->size], (size - vector->size) * sizeof(type)); \
-               vector->size = size;                                                  \
-       }                                                                     \
-       void pushVector ## name(Vector ## name * vector, type item) {          \
-               if (vector->size >= vector->capacity) {                             \
-                       uint newcap = vector->capacity << 1;                                \
-                       vector->array = (type *)ourrealloc(vector->array, newcap * sizeof(type)); \
-                       vector->capacity = newcap;                                          \
-               }                                                                   \
-               vector->array[vector->size++] = item;                               \
-       }                                                                     \
-       type getVector ## name(Vector ## name * vector, uint index) {         \
-               return vector->array[index];                                        \
-       }                                                                     \
+               vector->size = size;                                                                                                                                                                                                    \
+       }                                                                                                                                                                                                                                                                                       \
+       void pushVector ## name(Vector ## name * vector, type item) {                                    \
+               if (vector->size >= vector->capacity) {                                                                                                                 \
+                       uint newcap = vector->capacity << 1;                                                                                                                            \
+                       vector->array = (type *)ourrealloc(vector->array, newcap * sizeof(type));       \
+                       vector->capacity = newcap;                                                                                                                                                                      \
+               }                                                                                                                                                                                                                                                                               \
+               vector->array[vector->size++] = item;                                                                                                                           \
+       }                                                                                                                                                                                                                                                                                       \
+       type getVector ## name(Vector ## name * vector, uint index) {                                   \
+               return vector->array[index];                                                                                                                                                            \
+       }                                                                                                                                                                                                                                                                                       \
        void setExpandVector ## name(Vector ## name * vector, uint index, type item) { \
-               if (index >= vector->size)                                            \
-                       setSizeVector ## name(vector, index + 1);                         \
-               setVector ## name(vector, index, item);                             \
-       }                                                                     \
+               if (index >= vector->size)                                                                                                                                                                              \
+                       setSizeVector ## name(vector, index + 1);                                                                                                       \
+               setVector ## name(vector, index, item);                                                                                                                 \
+       }                                                                                                                                                                                                                                                                                       \
        void setVector ## name(Vector ## name * vector, uint index, type item) { \
-               vector->array[index] = item;                                          \
-       }                                                                     \
-       uint getSizeVector ## name(const Vector ## name * vector) {           \
-               return vector->size;                                                \
-       }                                                                     \
-       void deleteVector ## name(Vector ## name * vector) {                     \
-               ourfree(vector->array);                                             \
-               ourfree(vector);                                                    \
-       }                                                                     \
-       void clearVector ## name(Vector ## name * vector) {                     \
-               vector->size = 0;                                                     \
-       }                                                                     \
-       type *exposeArray ## name(Vector ## name * vector) {                 \
-               return vector->array;                                               \
-       }                                                                     \
-       void deleteVectorArray ## name(Vector ## name * vector) {              \
-               ourfree(vector->array);                                             \
-       }                                                                     \
-       void initVector ## name(Vector ## name * vector, uint capacity) { \
-               vector->size = 0;                                                      \
-               vector->capacity = capacity;                                              \
-               vector->array = (type *) ourmalloc(sizeof(type) * capacity);        \
-       }                                                                     \
-       void initDefVector ## name(Vector ## name * vector) {         \
-               initVector ## name(vector, defcap);                         \
-       }                                                                     \
-       void initVectorArray ## name(Vector ## name * vector, uint capacity, type * array) {  \
-               initVector ## name(vector, capacity);                          \
-               vector->size = capacity;                                              \
-               memcpy(vector->array, array, capacity * sizeof(type));  \
+               vector->array[index] = item;                                                                                                                                                                    \
+       }                                                                                                                                                                                                                                                                                       \
+       uint getSizeVector ## name(const Vector ## name * vector) {                                             \
+               return vector->size;                                                                                                                                                                                            \
+       }                                                                                                                                                                                                                                                                                       \
+       void deleteVector ## name(Vector ## name * vector) {                                                                             \
+               ourfree(vector->array);                                                                                                                                                                                 \
+               ourfree(vector);                                                                                                                                                                                                                \
+       }                                                                                                                                                                                                                                                                                       \
+       void clearVector ## name(Vector ## name * vector) {                                                                                     \
+               vector->size = 0;                                                                                                                                                                                                                       \
+       }                                                                                                                                                                                                                                                                                       \
+       type *exposeArray ## name(Vector ## name * vector) {                                                             \
+               return vector->array;                                                                                                                                                                                           \
+       }                                                                                                                                                                                                                                                                                       \
+       void deleteVectorArray ## name(Vector ## name * vector) {                                                        \
+               ourfree(vector->array);                                                                                                                                                                                 \
+       }                                                                                                                                                                                                                                                                                       \
+       void initVector ## name(Vector ## name * vector, uint capacity) {       \
+               vector->size = 0;                                                                                                                                                                                                                        \
+               vector->capacity = capacity;                                                                                                                                                                                    \
+               vector->array = (type *) ourmalloc(sizeof(type) * capacity);                            \
+       }                                                                                                                                                                                                                                                                                       \
+       void initDefVector ## name(Vector ## name * vector) {                                   \
+               initVector ## name(vector, defcap);                                                                                                     \
+       }                                                                                                                                                                                                                                                                                       \
+       void initVectorArray ## name(Vector ## name * vector, uint capacity, type * array) {    \
+               initVector ## name(vector, capacity);                                                                                                    \
+               vector->size = capacity;                                                                                                                                                                                        \
+               memcpy(vector->array, array, capacity * sizeof(type));  \
        }
 #endif
index 19439dc..cc96889 100644 (file)
@@ -32,7 +32,7 @@ void ElementEncoding::allocEncodingArrayElement(uint size) {
 }
 
 void ElementEncoding::allocInUseArrayElement(uint size) {
-       uint bytes = ((size + ((1 << 9) - 1)) >> 6) & ~7;//Depends on size of inUseArray
+       uint bytes = ((size + 63) >> 3) & ~7;   //Depends on size of inUseArray
        inUseArray = (uint64_t *) ourcalloc(1, bytes);
 }
 
index b066de3..17314e9 100644 (file)
@@ -42,7 +42,7 @@ public:
                };
                struct {
                        uint64_t offset;/* Value = offset + encoded number (interpretted according to isBinaryValSigned) */
-                       uint64_t low;/* Lowest value to encode */
+                       uint64_t low;   /* Lowest value to encode */
                        uint64_t high;/* High value to encode.   If low > high, we assume wrap around to include 0. */
                        uint numBits;
                        bool isBinaryValSigned;
index ddac4c9..3f9c97d 100644 (file)
 #define READBUFFERSIZE 16384
 
 Deserializer::Deserializer(const char *file) :
-       buffer((char *)ourmalloc(READBUFFERSIZE)),
+       buffer((char *) ourmalloc(READBUFFERSIZE)),
        bufferindex(0),
        bufferbytes(0),
        buffercap(READBUFFERSIZE),
        solver(new CSolver())
 {
        filedesc = open(file, O_RDONLY);
-       
+
        if (filedesc < 0) {
                exit(-1);
        }
@@ -39,7 +39,7 @@ Deserializer::~Deserializer() {
 }
 
 ssize_t Deserializer::myread(void *__buf, size_t bytestoread) {
-       char * out = (char * ) __buf;
+       char *out = (char * ) __buf;
        size_t totalbytesread = 0;
        while (bytestoread) {
                if (bufferbytes != 0) {
@@ -53,7 +53,7 @@ ssize_t Deserializer::myread(void *__buf, size_t bytestoread) {
                        out += bytestocopy;
                        bytestoread -= bytestocopy;
                } else {
-                       size_t bytesread=read (filedesc, buffer, buffercap);
+                       size_t bytesread = read (filedesc, buffer, buffercap);
                        bufferindex = 0;
                        bufferbytes = bytesread;
                        if (bytesread == 0) {
@@ -130,11 +130,11 @@ void Deserializer::deserializeBooleanEdge() {
        ASSERT(map.contains(tmp.getBoolean()));
        b_ptr = (Boolean *) map.get(tmp.getBoolean());
        BooleanEdge res(b_ptr);
-        bool isTopLevel;
-        myread(&isTopLevel, sizeof(bool));
-        if(isTopLevel){
-                solver->addConstraint(isNegated ? res.negate() : res);
-        }
+       bool isTopLevel;
+       myread(&isTopLevel, sizeof(bool));
+       if (isTopLevel) {
+               solver->addConstraint(isNegated ? res.negate() : res);
+       }
 }
 
 void Deserializer::deserializeBooleanVar() {
@@ -180,7 +180,7 @@ void Deserializer::deserializeSet() {
        myread(&isRange, sizeof(bool));
        bool isMutable;
        myread(&isMutable, sizeof(bool));
-       if(isRange){
+       if (isRange) {
                uint64_t low;
                myread(&low, sizeof(uint64_t));
                uint64_t high;
@@ -188,22 +188,22 @@ void Deserializer::deserializeSet() {
                map.put(s_ptr, new Set(type, low, high));
        } else {
                Set *set = NULL;
-               if(isMutable) {
+               if (isMutable) {
                        set = new MutableSet(type);
                }
                uint size;
                myread(&size, sizeof(uint));
                Vector<uint64_t> members;
-               for(uint i=0; i<size; i++) {
+               for (uint i = 0; i < size; i++) {
                        uint64_t mem;
                        myread(&mem, sizeof(uint64_t));
-                       if(isMutable) {
-                               ((MutableSet*) set)->addElementMSet(mem);
+                       if (isMutable) {
+                               ((MutableSet *) set)->addElementMSet(mem);
                        } else {
                                members.push(mem);
                        }
                }
-               if(!isMutable) {
+               if (!isMutable) {
                        set = solver->createSet(type, members.expose(), size);
                }
                map.put(s_ptr, set);
index daa8ba0..35bae4c 100644 (file)
@@ -26,14 +26,14 @@ Serializer::Serializer(const char *file) :
 void Serializer::flushBuffer() {
        ssize_t datatowrite = bufferoffset;
        ssize_t index = 0;
-       while(datatowrite) {
+       while (datatowrite) {
                ssize_t byteswritten = write(filedesc, &buffer[index], datatowrite);
                if (byteswritten == -1)
                        exit(-1);
                datatowrite -= byteswritten;
                index += byteswritten;
        }
-       bufferoffset=0;
+       bufferoffset = 0;
 }
 
 Serializer::~Serializer() {
@@ -45,12 +45,12 @@ Serializer::~Serializer() {
 }
 
 void Serializer::mywrite(const void *__buf, size_t __n) {
-       char *towrite=(char *) __buf;
-       if (__n > SERIALBUFFERLENGTH *2) {
+       char *towrite = (char *) __buf;
+       if (__n > SERIALBUFFERLENGTH * 2) {
                if (bufferoffset != 0)
                        flushBuffer();
                while (__n > 0) {
-                       ssize_t result=write(filedesc, &towrite, __n);
+                       ssize_t result = write(filedesc, &towrite, __n);
                        if (result != (ssize_t) __n)
                                exit(-1);
                        towrite += result;
@@ -58,7 +58,7 @@ void Serializer::mywrite(const void *__buf, size_t __n) {
                }
        } else {
                do  {
-                       uint spacefree = bufferlength-bufferoffset;
+                       uint spacefree = bufferlength - bufferoffset;
                        uint datatowrite = spacefree > __n ? __n : spacefree;
                        memcpy(&buffer[bufferoffset], towrite, datatowrite);
                        bufferoffset += datatowrite;
@@ -73,7 +73,7 @@ void Serializer::mywrite(const void *__buf, size_t __n) {
                        } else {
                                return;
                        }
-               } while(true);
+               } while (true);
        }
 }
 
index 7030438..79012c7 100644 (file)
@@ -23,7 +23,7 @@ public:
        CMEMALLOC;
 private:
        void flushBuffer();
-       char * buffer;
+       char *buffer;
        uint bufferoffset;
        uint bufferlength;
        int filedesc;
@@ -37,7 +37,7 @@ inline bool Serializer::isSerialized(void *obj) {
 
 
 
-void serializeBooleanEdge(Serializer *serializer, BooleanEdge be, bool isTopLevel=false);
+void serializeBooleanEdge(Serializer *serializer, BooleanEdge be, bool isTopLevel = false);
 
 #endif/* SERIALIZER_H */
 
old mode 100755 (executable)
new mode 100644 (file)
index 9e21eb5..d3f2440
@@ -1,23 +1,23 @@
 #include "csolver.h"
 #include "autotuner.h"
 
-int main(int argc, char ** argv){
-       if(argc < 2){
+int main(int argc, char **argv) {
+       if (argc < 2) {
                printf("You should specify file names ...");
-               exit(-1);       
+               exit(-1);
        }
-       CSolver * solvers[argc-1];
+       CSolver *solvers[argc - 1];
        AutoTuner *autotuner = new AutoTuner(100);
-       for(int i = 1; i < argc; i++) {
-               solvers[i-1] = CSolver::deserialize(argv[i]);
-               autotuner->addProblem(solvers[i-1]);
+       for (int i = 1; i < argc; i++) {
+               solvers[i - 1] = CSolver::deserialize(argv[i]);
+               autotuner->addProblem(solvers[i - 1]);
        }
 
        autotuner->tune();
        delete autotuner;
-       
-       for(int i = 1; i < argc; i++) {
-               delete solvers[i-1];
+
+       for (int i = 1; i < argc; i++) {
+               delete solvers[i - 1];
        }
 
        return 1;
old mode 100755 (executable)
new mode 100644 (file)
index 1d1148b..8f71e6f
@@ -1,16 +1,16 @@
 #include "csolver.h"
 
 
-int main(int argc, char ** argv){
-       if(argc < 2){
+int main(int argc, char **argv) {
+       if (argc < 2) {
                printf("You should specify file names ...");
-               exit(-1);       
+               exit(-1);
        }
-       for(int i = 1; i < argc; i++) {
-               CSolversolver = CSolver::deserialize(argv[i]);
+       for (int i = 1; i < argc; i++) {
+               CSolver *solver = CSolver::deserialize(argv[i]);
                solver->printConstraints();
-               int value=solver->solve();
-               if (value ==1) {
+               int value = solver->solve();
+               if (value == 1) {
                        printf("%s is SAT\n", argv[i]);
                } else {
                        printf("%s is UNSAT\n", argv[i]);
old mode 100755 (executable)
new mode 100644 (file)
index 4e9637d..0c707ce
@@ -1,15 +1,15 @@
 #include "csolver.h"
 
 
-int main(int argc, char ** argv){
-       if(argc < 2){
+int main(int argc, char **argv) {
+       if (argc < 2) {
                printf("You should specify file names ...");
-               exit(-1);       
+               exit(-1);
        }
-       for(int i = 1; i < argc; i++) {
-               CSolversolver = CSolver::deserialize(argv[i]);
-               int value=solver->solve();
-               if (value ==1) {
+       for (int i = 1; i < argc; i++) {
+               CSolver *solver = CSolver::deserialize(argv[i]);
+               int value = solver->solve();
+               if (value == 1) {
                        printf("%s is SAT\n", argv[i]);
                } else {
                        printf("%s is UNSAT\n", argv[i]);
old mode 100755 (executable)
new mode 100644 (file)
index 7a938cf..0f35d12
@@ -1,15 +1,15 @@
 #include "csolver.h"
 
 
-int main(int argc, char ** argv){
-       if(argc < 2){
+int main(int argc, char **argv) {
+       if (argc < 2) {
                printf("You should specify file names ...");
-               exit(-1);       
+               exit(-1);
        }
-       for(int i = 1; i < argc; i++) {
-               CSolversolver = CSolver::deserialize(argv[i]);
-               int value=solver->solve();
-               if (value ==1) {
+       for (int i = 1; i < argc; i++) {
+               CSolver *solver = CSolver::deserialize(argv[i]);
+               int value = solver->solve();
+               if (value == 1) {
                        printf("%s is SAT\n", argv[i]);
                } else {
                        printf("%s is UNSAT\n", argv[i]);
index bbef427..c8d35c9 100644 (file)
@@ -1,14 +1,14 @@
 #include "csolver.h"
 
 
-int main(int argc, char ** argv){
-       if(argc != 2){
+int main(int argc, char **argv) {
+       if (argc != 2) {
                printf("You only specify the name of the file ...");
-               exit(-1);       
+               exit(-1);
        }
-       CSolversolver = CSolver::deserialize(argv[1]);
+       CSolver *solver = CSolver::deserialize(argv[1]);
        solver->printConstraints();
-        delete solver;
+       delete solver;
        return 1;
-               
+
 }
index cc12ef8..7343c83 100644 (file)
@@ -55,9 +55,9 @@ void assert_hook(void);
                if (!(expr)) { \
                        fprintf(stderr, "Error: assertion failed in %s at line %d\n", __FILE__, __LINE__); \
                        /* print_trace(); // Trace printing may cause dynamic memory allocation */ \
-                       assert_hook();                           \
-                       exit(EXIT_FAILURE); \
-               } \
+                       assert_hook();                                                                                                   \
+                       exit(EXIT_FAILURE);     \
+               }       \
        } while (0)
 #else
 #define ASSERT(expr) \
index e4e0452..b74df47 100644 (file)
@@ -53,7 +53,7 @@ CSolver::~CSolver() {
 
        size = allElements.getSize();
        for (uint i = 0; i < size; i++) {
-                Element* el = allElements.get(i);
+               Element *el = allElements.get(i);
                delete el;
        }
 
@@ -80,9 +80,9 @@ CSolver::~CSolver() {
        delete satEncoder;
 }
 
-void CSolver::resetSolver(){
-        //serialize();
-        uint size = allBooleans.getSize();
+void CSolver::resetSolver() {
+       //serialize();
+       uint size = allBooleans.getSize();
        for (uint i = 0; i < size; i++) {
                delete allBooleans.get(i);
        }
@@ -94,7 +94,7 @@ void CSolver::resetSolver(){
 
        size = allElements.getSize();
        for (uint i = 0; i < size; i++) {
-                Element* el = allElements.get(i);
+               Element *el = allElements.get(i);
                delete el;
        }
 
@@ -117,25 +117,25 @@ void CSolver::resetSolver(){
                delete allFunctions.get(i);
        }
        delete boolTrue.getBoolean();
-        allBooleans.clear();
-        allSets.clear();
-        allElements.clear();
-        allTables.clear();
-        allPredicates.clear();
-        allOrders.clear();
-        allFunctions.clear();
-        constraints.reset();
-        activeOrders.reset();
-        boolMap.reset();
+       allBooleans.clear();
+       allSets.clear();
+       allElements.clear();
+       allTables.clear();
+       allPredicates.clear();
+       allOrders.clear();
+       allFunctions.clear();
+       constraints.reset();
+       activeOrders.reset();
+       boolMap.reset();
        elemMap.reset();
-        
-        boolTrue = BooleanEdge(new BooleanConst(true));
+
+       boolTrue = BooleanEdge(new BooleanConst(true));
        boolFalse = boolTrue.negate();
-        unsat = false;
-        elapsedTime = 0;
-        tuner = NULL;
-        satEncoder->resetSATEncoder();
-        
+       unsat = false;
+       elapsedTime = 0;
+       tuner = NULL;
+       satEncoder->resetSATEncoder();
+
 }
 
 CSolver *CSolver::clone() {
@@ -150,7 +150,7 @@ CSolver *CSolver::clone() {
        return copy;
 }
 
-CSolver* CSolver::deserialize(const char * file){
+CSolver *CSolver::deserialize(const char *file) {
        model_print("deserializing ...\n");
        Deserializer deserializer(file);
        return deserializer.deserialize();
@@ -159,8 +159,8 @@ CSolver* CSolver::deserialize(const char * file){
 void CSolver::serialize() {
        model_print("serializing ...\n");
        char buffer[255];
-       long long nanotime=getTimeNano();
-       int numchars=sprintf(buffer, "DUMP%llu", nanotime);
+       long long nanotime = getTimeNano();
+       int numchars = sprintf(buffer, "DUMP%llu", nanotime);
        Serializer serializer(buffer);
        SetIteratorBooleanEdge *it = getConstraints();
        while (it->hasNext()) {
@@ -468,19 +468,19 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
                boolMap.put(constraint, constraint);
                constraint->updateParents();
                if (order->graph != NULL) {
-                       OrderGraph *graph=order->graph;
-                       OrderNode *from=graph->lookupOrderNodeFromOrderGraph(first);
+                       OrderGraph *graph = order->graph;
+                       OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first);
                        if (from != NULL) {
-                               OrderNode *to=graph->lookupOrderNodeFromOrderGraph(second);
+                               OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second);
                                if (to != NULL) {
-                                       OrderEdge *edge=graph->lookupOrderEdgeFromOrderGraph(from, to);
+                                       OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to);
                                        OrderEdge *invedge;
 
                                        if (edge != NULL && edge->mustPos) {
                                                replaceBooleanWithTrueNoRemove(constraint);
                                        } else if (edge != NULL && edge->mustNeg) {
                                                replaceBooleanWithFalseNoRemove(constraint);
-                                       } else if ((invedge=graph->lookupOrderEdgeFromOrderGraph(to, from)) != NULL
+                                       } else if ((invedge = graph->lookupOrderEdgeFromOrderGraph(to, from)) != NULL
                                                                                 && invedge->mustPos) {
                                                replaceBooleanWithFalseNoRemove(constraint);
                                        }
@@ -539,7 +539,7 @@ Order *CSolver::createOrder(OrderType type, Set *set) {
 }
 
 /** Computes static ordering information to allow isTrue/isFalse
-               queries on newly created orders to work. */
+    queries on newly created orders to work. */
 
 void CSolver::inferFixedOrder(Order *order) {
        if (order->graph != NULL) {
@@ -548,7 +548,7 @@ void CSolver::inferFixedOrder(Order *order) {
        order->graph = buildMustOrderGraph(order);
        reachMustAnalysis(this, order->graph, true);
 }
-       
+
 void CSolver::inferFixedOrders() {
        SetIteratorOrder *orderit = activeOrders.iterator();
        while (orderit->hasNext()) {
@@ -559,7 +559,7 @@ void CSolver::inferFixedOrders() {
 
 #define NANOSEC 1000000000.0
 int CSolver::solve() {
-       long long starttime = getTimeNano();    
+       long long starttime = getTimeNano();
        bool deleteTuner = false;
        if (tuner == NULL) {
                tuner = new DefaultTuner();
@@ -581,16 +581,16 @@ int CSolver::solve() {
 
        computePolarities(this);
        long long time2 = getTimeNano();
-       model_print("Polarity time: %f\n", (time2-starttime)/NANOSEC);
+       model_print("Polarity time: %f\n", (time2 - starttime) / NANOSEC);
        Preprocess pp(this);
        pp.doTransform();
        long long time3 = getTimeNano();
-       model_print("Preprocess time: %f\n", (time3-time2)/NANOSEC);
-       
+       model_print("Preprocess time: %f\n", (time3 - time2) / NANOSEC);
+
        DecomposeOrderTransform dot(this);
        dot.doTransform();
        long long time4 = getTimeNano();
-       model_print("Decompose Order: %f\n", (time4-time3)/NANOSEC);
+       model_print("Decompose Order: %f\n", (time4 - time3) / NANOSEC);
 
        IntegerEncodingTransform iet(this);
        iet.doTransform();
@@ -601,19 +601,19 @@ int CSolver::solve() {
 
        naiveEncodingDecision(this);
        long long time5 = getTimeNano();
-       model_print("Encoding Graph Time: %f\n", (time5-time4)/NANOSEC);
-       
+       model_print("Encoding Graph Time: %f\n", (time5 - time4) / NANOSEC);
+
        long long startTime = getTimeNano();
        satEncoder->encodeAllSATEncoder(this);
        long long endTime = getTimeNano();
 
        elapsedTime = endTime - startTime;
-       model_print("Elapse Encode time: %f\n", elapsedTime/NANOSEC);
-       
+       model_print("Elapse Encode time: %f\n", elapsedTime / NANOSEC);
+
        model_print("Is problem UNSAT after encoding: %d\n", unsat);
        int result = unsat ? IS_UNSAT : satEncoder->solve();
        model_print("Result Computed in CSolver: %d\n", result);
-       
+
        if (deleteTuner) {
                delete tuner;
                tuner = NULL;
index ffbfe35..523ac30 100644 (file)
@@ -11,7 +11,7 @@ class CSolver {
 public:
        CSolver();
        ~CSolver();
-        void resetSolver();
+       void resetSolver();
        /** This function creates a set containing the elements passed in the array. */
        Set *createSet(VarType type, uint64_t *elements, uint num);
 
@@ -153,12 +153,12 @@ public:
        void replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb);
        CSolver *clone();
        void serialize();
-       static CSolver* deserialize(const char * file);
+       static CSolver *deserialize(const char *file);
        void autoTune(uint budget);
        void inferFixedOrders();
        void inferFixedOrder(Order *order);
 
-       
+
        void setTuner(Tuner *_tuner) { tuner = _tuner; }
        long long getElapsedTime() { return elapsedTime; }
        long long getEncodeTime();
index 92fb0fe..b87e2c8 100644 (file)
@@ -45,21 +45,21 @@ static inline void *ourcalloc(size_t count, size_t size) { return calloc(count,
 static inline void *ourrealloc(void *ptr, size_t size) { return realloc(ptr, size); }
 #endif
 
-#define CMEMALLOC                           \
-       void *operator new(size_t size) {       \
-               return ourmalloc(size);                \
-       }                                                  \
-       void operator delete(void *p, size_t size) {       \
-               ourfree(p);                                      \
-       }                                                  \
-       void *operator new[](size_t size) {               \
-               return ourmalloc(size);                          \
-       }                                                    \
-       void operator delete[](void *p, size_t size) {       \
-               ourfree(p);                                        \
-       }                                                                     \
-       void *operator new(size_t size, void *p) {                                                                                                                      /* placement new */ \
-               return p;                                                           \
+#define CMEMALLOC                                                                                                              \
+       void *operator new(size_t size) {                               \
+               return ourmalloc(size);                                                          \
+       }                                                                                                                                                                                                        \
+       void operator delete(void *p, size_t size) {                     \
+               ourfree(p);                                                                                                                                                      \
+       }                                                                                                                                                                                                        \
+       void *operator new[](size_t size) {                                                             \
+               return ourmalloc(size);                                                                                                  \
+       }                                                                                                                                                                                                                \
+       void operator delete[](void *p, size_t size) {                   \
+               ourfree(p);                                                                                                                                                              \
+       }                                                                                                                                                                                                                                                                                       \
+       void *operator new(size_t size, void *p) {                                                                                                                      /* placement new */     \
+               return p;                                                                                                                                                                                                                                               \
        }
 
 #endif/* _MY_MEMORY_H */