From cd362e8c49a8ac25e3f0324e89d139285cb71c3d Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Sun, 31 Dec 2017 00:55:12 -0800 Subject: [PATCH] bug fixes --- src/AST/asthash.cc | 6 +- src/AST/element.h | 6 +- src/AST/order.cc | 2 +- src/AST/set.cc | 24 +-- src/AST/set.h | 2 +- src/ASTAnalyses/Order/orderanalysis.cc | 14 +- src/ASTAnalyses/Order/orderanalysis.h | 4 +- src/ASTAnalyses/Order/ordergraph.cc | 10 +- src/ASTAnalyses/Order/ordernode.h | 12 +- src/ASTTransform/decomposeordertransform.cc | 5 +- src/Backend/cnfexpr.cc | 3 +- src/Backend/constraint.cc | 34 ++-- src/Backend/inc_solver.cc | 5 +- src/Backend/satencoder.cc | 6 +- src/Backend/satencoder.h | 2 +- src/Collections/array.h | 4 +- src/Collections/hashset.h | 6 +- src/Collections/hashtable.h | 32 ++-- src/Collections/qsort.cc | 96 +++++----- src/Collections/structs.cc | 10 +- src/Collections/vector.h | 202 ++++++++++---------- src/Encoders/elementencoding.cc | 2 +- src/Encoders/elementencoding.h | 2 +- src/Serialize/deserializer.cc | 30 +-- src/Serialize/serializer.cc | 14 +- src/Serialize/serializer.h | 4 +- src/Test/deserializerautotune.cc | 20 +- src/Test/deserializersolveprint.cc | 14 +- src/Test/deserializersolveprintopt.cc | 14 +- src/Test/deserializersolvetest.cc | 14 +- src/Test/deserializertest.cc | 12 +- src/common.h | 6 +- src/csolver.cc | 84 ++++---- src/csolver.h | 6 +- src/mymemory.h | 30 +-- 35 files changed, 373 insertions(+), 364 deletions(-) mode change 100755 => 100644 src/Test/deserializerautotune.cc mode change 100755 => 100644 src/Test/deserializersolveprint.cc mode change 100755 => 100644 src/Test/deserializersolveprintopt.cc mode change 100755 => 100644 src/Test/deserializersolvetest.cc diff --git a/src/AST/asthash.cc b/src/AST/asthash.cc index 7350a7e..347e5fa 100644 --- a/src/AST/asthash.cc +++ b/src/AST/asthash.cc @@ -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 *inputs1, Array *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; diff --git a/src/AST/element.h b/src/AST/element.h index 1e7b1f2..5259c09 100644 --- a/src/AST/element.h +++ b/src/AST/element.h @@ -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 inputs; BooleanEdge overflowstatus; diff --git a/src/AST/order.cc b/src/AST/order.cc index 315b112..2b3184a 100644 --- a/src/AST/order.cc +++ b/src/AST/order.cc @@ -33,7 +33,7 @@ Order *Order::clone(CSolver *solver, CloneMap *map) { HashtableOrderPair *Order::getOrderPairTable() { ASSERT( encoding.resolver != NULL); - if (OrderPairResolver *t = dynamic_cast(encoding.resolver)) { + if (OrderPairResolver * t = dynamic_cast(encoding.resolver)) { return t->getOrderPairTable(); } else { ASSERT(0); diff --git a/src/AST/set.cc b/src/AST/set.cc index d45791a..e019b12 100644 --- a/src/AST/set.cc +++ b/src/AST/set.cc @@ -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; iget(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() { diff --git a/src/AST/set.h b/src/AST/set.h index c647af5..34784d3 100644 --- a/src/AST/set.h +++ b/src/AST/set.h @@ -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 *members; }; diff --git a/src/ASTAnalyses/Order/orderanalysis.cc b/src/ASTAnalyses/Order/orderanalysis.cc index 8a991a4..cd50ed9 100644 --- a/src/ASTAnalyses/Order/orderanalysis.cc +++ b/src/ASTAnalyses/Order/orderanalysis.cc @@ -12,15 +12,15 @@ #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 *finishNodes) { +HashtableNodeToNodeSet *getMustReachMap(CSolver *solver, OrderGraph *graph, Vector *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 *finishNodes, bool computeTransitiveClosure) { +void DFSClearContradictions(CSolver *solver, OrderGraph *graph, HashtableNodeToNodeSet *table, Vector *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(); diff --git a/src/ASTAnalyses/Order/orderanalysis.h b/src/ASTAnalyses/Order/orderanalysis.h index a371c85..72f389c 100644 --- a/src/ASTAnalyses/Order/orderanalysis.h +++ b/src/ASTAnalyses/Order/orderanalysis.h @@ -4,8 +4,8 @@ #include "structs.h" #include "mymemory.h" -void DFSClearContradictions(CSolver *solver, OrderGraph *graph, HashtableNodeToNodeSet * table, Vector *finishNodes, bool computeTransitiveClosure); -HashtableNodeToNodeSet * getMustReachMap(CSolver *solver, OrderGraph *graph, Vector *finishNodes); +void DFSClearContradictions(CSolver *solver, OrderGraph *graph, HashtableNodeToNodeSet *table, Vector *finishNodes, bool computeTransitiveClosure); +HashtableNodeToNodeSet *getMustReachMap(CSolver *solver, OrderGraph *graph, Vector *finishNodes); void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure); void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph); diff --git a/src/ASTAnalyses/Order/ordergraph.cc b/src/ASTAnalyses/Order/ordergraph.cc index 9f50949..cbc2e25 100644 --- a/src/ASTAnalyses/Order/ordergraph.cc +++ b/src/ASTAnalyses/Order/ordergraph.cc @@ -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 *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 *finishNodes) { void OrderGraph::DFSMust(Vector *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 *finishNodes, void OrderGraph::resetNodeInfoStatusSCC() { SetIteratorOrderNode *iterator = getNodes(); while (iterator->hasNext()) { - ((OrderNode*)iterator->next())->status = NOTVISITED; + ((OrderNode *)iterator->next())->status = NOTVISITED; } delete iterator; } diff --git a/src/ASTAnalyses/Order/ordernode.h b/src/ASTAnalyses/Order/ordernode.h index 4a40466..1303a5a 100644 --- a/src/ASTAnalyses/Order/ordernode.h +++ b/src/ASTAnalyses/Order/ordernode.h @@ -17,18 +17,18 @@ 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); diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc index 525a03c..c75fbec 100644 --- a/src/ASTTransform/decomposeordertransform.cc +++ b/src/ASTTransform/decomposeordertransform.cc @@ -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 diff --git a/src/Backend/cnfexpr.cc b/src/Backend/cnfexpr.cc index b04044a..e8af3b8 100644 --- a/src/Backend/cnfexpr.cc +++ b/src/Backend/cnfexpr.cc @@ -1,5 +1,6 @@ #include "cnfexpr.h" #include +#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 */ diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc index 8486282..386706d 100644 --- a/src/Backend/constraint.cc +++ b/src/Backend/constraint.cc @@ -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; } diff --git a/src/Backend/inc_solver.cc b/src/Backend/inc_solver.cc index 7d0fd65..d295cee 100644 --- a/src/Backend/inc_solver.cc +++ b/src/Backend/inc_solver.cc @@ -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) { diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc index 206d2b7..bf8ede4 100644 --- a/src/Backend/satencoder.cc +++ b/src/Backend/satencoder.cc @@ -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() { diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h index dcf3b86..0347164 100644 --- a/src/Backend/satencoder.h +++ b/src/Backend/satencoder.h @@ -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;} diff --git a/src/Collections/array.h b/src/Collections/array.h index 03d83cd..f4ae3a5 100644 --- a/src/Collections/array.h +++ b/src/Collections/array.h @@ -5,13 +5,13 @@ template 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)); } diff --git a/src/Collections/hashset.h b/src/Collections/hashset.h index 86cbce9..009c047 100644 --- a/src/Collections/hashset.h +++ b/src/Collections/hashset.h @@ -18,10 +18,10 @@ struct Linknode { Linknode<_Key> *next; }; -template +template class Hashset; -template, bool (*equals)(_Key, _Key) = defaultEquals<_Key> > +template, 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, bool (*equals)(_Key, _Key) = defaultEquals<_Key> > +template, bool (*equals) (_Key, _Key) = defaultEquals<_Key> > class Hashset { public: Hashset(unsigned int initialcapacity = 16, double factor = 0.5) : diff --git a/src/Collections/hashtable.h b/src/Collections/hashtable.h index 9f5f3b3..0a50bb9 100644 --- a/src/Collections/hashtable.h +++ b/src/Collections/hashtable.h @@ -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, bool (*equals)(_Key, _Key) = defaultEquals<_Key> > +template, 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; diff --git a/src/Collections/qsort.cc b/src/Collections/qsort.cc index f4e7ec9..d384220 100644 --- a/src/Collections/qsort.cc +++ b/src/Collections/qsort.cc @@ -76,19 +76,19 @@ * 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); \ @@ -102,18 +102,18 @@ * 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); \ + } \ } /* @@ -133,27 +133,27 @@ * * 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) diff --git a/src/Collections/structs.cc b/src/Collections/structs.cc index ac69f9d..7673474 100644 --- a/src/Collections/structs.cc +++ b/src/Collections/structs.cc @@ -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); diff --git a/src/Collections/vector.h b/src/Collections/vector.h index 6c53253..3cf0010 100644 --- a/src/Collections/vector.h +++ b/src/Collections/vector.h @@ -2,112 +2,112 @@ #define VECTOR_H #include -#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 diff --git a/src/Encoders/elementencoding.cc b/src/Encoders/elementencoding.cc index 19439dc..cc96889 100644 --- a/src/Encoders/elementencoding.cc +++ b/src/Encoders/elementencoding.cc @@ -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); } diff --git a/src/Encoders/elementencoding.h b/src/Encoders/elementencoding.h index b066de3..17314e9 100644 --- a/src/Encoders/elementencoding.h +++ b/src/Encoders/elementencoding.h @@ -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; diff --git a/src/Serialize/deserializer.cc b/src/Serialize/deserializer.cc index ddac4c9..3f9c97d 100644 --- a/src/Serialize/deserializer.cc +++ b/src/Serialize/deserializer.cc @@ -18,14 +18,14 @@ #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 members; - for(uint i=0; iaddElementMSet(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); diff --git a/src/Serialize/serializer.cc b/src/Serialize/serializer.cc index daa8ba0..35bae4c 100644 --- a/src/Serialize/serializer.cc +++ b/src/Serialize/serializer.cc @@ -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); } } diff --git a/src/Serialize/serializer.h b/src/Serialize/serializer.h index 7030438..79012c7 100644 --- a/src/Serialize/serializer.h +++ b/src/Serialize/serializer.h @@ -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 */ diff --git a/src/Test/deserializerautotune.cc b/src/Test/deserializerautotune.cc old mode 100755 new mode 100644 index 9e21eb5..d3f2440 --- a/src/Test/deserializerautotune.cc +++ b/src/Test/deserializerautotune.cc @@ -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; diff --git a/src/Test/deserializersolveprint.cc b/src/Test/deserializersolveprint.cc old mode 100755 new mode 100644 index 1d1148b..8f71e6f --- a/src/Test/deserializersolveprint.cc +++ b/src/Test/deserializersolveprint.cc @@ -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++) { - CSolver* solver = 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]); diff --git a/src/Test/deserializersolveprintopt.cc b/src/Test/deserializersolveprintopt.cc old mode 100755 new mode 100644 index 4e9637d..0c707ce --- a/src/Test/deserializersolveprintopt.cc +++ b/src/Test/deserializersolveprintopt.cc @@ -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++) { - CSolver* solver = 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]); diff --git a/src/Test/deserializersolvetest.cc b/src/Test/deserializersolvetest.cc old mode 100755 new mode 100644 index 7a938cf..0f35d12 --- a/src/Test/deserializersolvetest.cc +++ b/src/Test/deserializersolvetest.cc @@ -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++) { - CSolver* solver = 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]); diff --git a/src/Test/deserializertest.cc b/src/Test/deserializertest.cc index bbef427..c8d35c9 100644 --- a/src/Test/deserializertest.cc +++ b/src/Test/deserializertest.cc @@ -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); } - CSolver* solver = CSolver::deserialize(argv[1]); + CSolver *solver = CSolver::deserialize(argv[1]); solver->printConstraints(); - delete solver; + delete solver; return 1; - + } diff --git a/src/common.h b/src/common.h index cc12ef8..7343c83 100644 --- a/src/common.h +++ b/src/common.h @@ -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) \ diff --git a/src/csolver.cc b/src/csolver.cc index e4e0452..b74df47 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -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; diff --git a/src/csolver.h b/src/csolver.h index ffbfe35..523ac30 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -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(); diff --git a/src/mymemory.h b/src/mymemory.h index 92fb0fe..b87e2c8 100644 --- a/src/mymemory.h +++ b/src/mymemory.h @@ -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 */ -- 2.34.1