Fix tabbing
authorbdemsky <bdemsky@uci.edu>
Fri, 17 Aug 2018 22:49:29 +0000 (15:49 -0700)
committerbdemsky <bdemsky@uci.edu>
Fri, 17 Aug 2018 22:49:29 +0000 (15:49 -0700)
36 files changed:
src/AST/boolean.h
src/AST/order.cc
src/AST/rewriter.cc
src/ASTAnalyses/Encoding/encodinggraph.cc
src/ASTAnalyses/Polarity/polarityassignment.cc
src/ASTTransform/elementopt.cc [changed mode: 0755->0644]
src/ASTTransform/elementopt.h [changed mode: 0755->0644]
src/Backend/constraint.cc
src/Backend/constraint.h
src/Backend/satelemencoder.cc
src/Backend/satencoder.cc
src/Backend/satencoder.h
src/Backend/satfuncopencoder.cc
src/Backend/satfunctableencoder.cc
src/Collections/corestructs.cc
src/Collections/hashset.h
src/Collections/hashtable.h
src/Collections/qsort.cc
src/Collections/vector.h
src/Encoders/elementencoding.h
src/Test/anyvaluetest.cc
src/Test/buglongclause.cc
src/Test/clonetest.cc
src/Test/deserializersolvetest.cc
src/Translator/decomposeorderresolver.cc
src/Translator/sattranslator.cc
src/Tuner/autotuner.cc
src/Tuner/autotuner.h
src/Tuner/tunable.cc
src/Tuner/tunable.h
src/ccsolver.cc
src/ccsolver.h
src/common.h
src/csolver.cc
src/csolver.h
src/mymemory.h

index de96bfc..77dc244 100644 (file)
@@ -12,7 +12,7 @@
 
 class Boolean : public ASTNode {
 private:
-    static uint64_t counter;
+       static uint64_t counter;
 public:
        Boolean(ASTNodeType _type);
        virtual ~Boolean() {}
@@ -25,7 +25,7 @@ public:
        BooleanValue boolVal;
        Vector<ASTNode *> parents;
        virtual void updateParents() {}
-        uint64_t id;
+       uint64_t id;
        CMEMALLOC;
 };
 
index 2b3184a..315b112 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 58ef96b..b5127c6 100644 (file)
@@ -51,7 +51,7 @@ void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
        }
 }
 
-void CSolver::handleFunction(ElementFunction * ef, BooleanEdge child) {
+void CSolver::handleFunction(ElementFunction *ef, BooleanEdge child) {
        BooleanEdge childNegate = child.negate();
        elemMap.remove(ef);
        if (ef->overflowstatus == child) {
@@ -106,7 +106,7 @@ void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) {
                } else {
                        BooleanLogic *logicop = (BooleanLogic *) parent;
                        boolMap.remove(logicop);        //could change parent's hash
-                       
+
                        uint parentsize = logicop->inputs.getSize();
                        for (uint j = 0; j < parentsize; j++) {
                                BooleanEdge b = logicop->inputs.get(j);
index 45ae01a..2a741ae 100644 (file)
@@ -79,8 +79,8 @@ void EncodingGraph::encode() {
                                        EncodingSubGraph *subgraph = graphMap.get(n);
                                        DEBUG("graphMap.get(subgraph=%p, n=%p)\n", subgraph, n);
                                        if (subgraph == NULL) {
-                                         encoding->encodingArrayInitialization();
-                                         continue;
+                                               encoding->encodingArrayInitialization();
+                                               continue;
                                        }
                                        uint encodingSize = subgraph->getEncodingMaxVal(n) + 1;
                                        uint paddedSize = encoding->getSizeEncodingArray(encodingSize);
@@ -255,9 +255,9 @@ void EncodingGraph::decideEdges() {
                        return;
 
                EncodingSubGraph *leftGraph = graphMap.get(left);
-                DEBUG("graphMap.get(left=%p, leftgraph=%p)\n", left, leftGraph);
+               DEBUG("graphMap.get(left=%p, leftgraph=%p)\n", left, leftGraph);
                EncodingSubGraph *rightGraph = graphMap.get(right);
-                DEBUG("graphMap.get(right=%p, rightgraph=%p)\n", right, rightGraph);
+               DEBUG("graphMap.get(right=%p, rightgraph=%p)\n", right, rightGraph);
                if (leftGraph == NULL && rightGraph != NULL) {
                        EncodingNode *tmp = left; left = right; right = tmp;
                        EncodingSubGraph *tmpsg = leftGraph; leftGraph = rightGraph; rightGraph = tmpsg;
index f941227..4a772ee 100644 (file)
@@ -24,7 +24,7 @@ void updateEdgePolarity(BooleanEdge dst, Polarity p) {
        Boolean *bdst = dst.getBoolean();
        bool isNegated = dst.isNegated();
        if (isNegated)
-               p=negatePolarity(p);
+               p = negatePolarity(p);
        updatePolarity(bdst, p);
 }
 
@@ -60,8 +60,8 @@ void computePredicatePolarity(BooleanPredicate *This) {
        if (This->undefStatus) {
                computePolarity(This->undefStatus.getBoolean(), P_BOTHTRUEFALSE);
        }
-       for(uint i=0; i < This->inputs.getSize(); i++) {
-               Element * e = This->inputs.get(i);
+       for (uint i = 0; i < This->inputs.getSize(); i++) {
+               Element *e = This->inputs.get(i);
                computeElement(e);
        }
 }
@@ -74,10 +74,10 @@ void computeElement(Element *e) {
                        computePolarity(ef->overflowstatus.getBoolean(), P_BOTHTRUEFALSE);
                }
 
-               for(uint i=0; i < ef->inputs.getSize(); i++) {
-                       Element * echild = ef->inputs.get(i);
+               for (uint i = 0; i < ef->inputs.getSize(); i++) {
+                       Element *echild = ef->inputs.get(i);
                        computeElement(echild);
-               }       
+               }
        }
 }
 
old mode 100755 (executable)
new mode 100644 (file)
index 3f1f892..6fec155
@@ -9,7 +9,7 @@
 
 ElementOpt::ElementOpt(CSolver *_solver)
        : Transform(_solver),
-               updateSets(solver->getTuner()->getTunable(ELEMENTOPTSETS, &onoff) == 1)
+       updateSets(solver->getTuner()->getTunable(ELEMENTOPTSETS, &onoff) == 1)
 {
 }
 
@@ -19,7 +19,7 @@ ElementOpt::~ElementOpt() {
 void ElementOpt::doTransform() {
        if (solver->getTuner()->getTunable(ELEMENTOPT, &onoff) == 0)
                return;
-       
+
        SetIteratorBooleanEdge *iterator = solver->getConstraints();
        while (iterator->hasNext()) {
                BooleanEdge constraint = iterator->next();
@@ -27,38 +27,38 @@ void ElementOpt::doTransform() {
                        workList.push((BooleanPredicate *)constraint.getBoolean());
        }
        while (workList.getSize() != 0) {
-               BooleanPredicate * pred = workList.last(); workList.pop();
+               BooleanPredicate *pred = workList.last(); workList.pop();
                processPredicate(pred);
        }
        delete iterator;
 }
 
-void ElementOpt::processPredicate(BooleanPredicate * pred) {
+void ElementOpt::processPredicate(BooleanPredicate *pred) {
        uint numInputs = pred->inputs.getSize();
        if (numInputs != 2)
                return;
 
-       Predicate * p = pred->getPredicate();
+       Predicate *p = pred->getPredicate();
        if (p->type == TABLEPRED)
-                       return;
+               return;
 
-       PredicateOperator * pop = (PredicateOperator *) p;
+       PredicateOperator *pop = (PredicateOperator *) p;
        CompOp op = pop->getOp();
 
-       Element * left = pred->inputs.get(0);
-       Element * right = pred->inputs.get(1);
+       Element *left = pred->inputs.get(0);
+       Element *right = pred->inputs.get(1);
 
        if (left->type == ELEMCONST) {
-               Element * tmp = left;
+               Element *tmp = left;
                left = right;
                right = tmp;
                op = flipOp(op);
        } else if (right->type != ELEMCONST)
                return;
 
-       if (left->type !=ELEMSET)
+       if (left->type != ELEMSET)
                return;
-       
+
        if (op == SATC_EQUALS) {
                handlePredicateEquals(pred, (ElementSet *) left, (ElementConst *) right);
        } else if (updateSets) {
@@ -75,8 +75,8 @@ void ElementOpt::handlePredicateEquals(BooleanPredicate *pred, ElementSet *left,
 }
 
 void ElementOpt::handlePredicateInequality(BooleanPredicate *pred, ElementSet *var, ElementConst *value) {
-       Predicate * p = pred->getPredicate();
-       PredicateOperator * pop = (PredicateOperator *) p;
+       Predicate *p = pred->getPredicate();
+       PredicateOperator *pop = (PredicateOperator *) p;
        CompOp op = pop->getOp();
 
        if (pred->isFalse()) {
@@ -85,18 +85,18 @@ void ElementOpt::handlePredicateInequality(BooleanPredicate *pred, ElementSet *v
                ASSERT(0);
        }
 
-       Set * s = var->getRange();
+       Set *s = var->getRange();
        if (s->isRange)
                return;
-       
+
        uint size = s->getSize();
        uint64_t elemArray[size];
        uint count = 0;
        uint64_t cvalue = value->value;
 
-       switch(op) {
+       switch (op) {
        case SATC_LT: {
-               for(uint i=0; i<size; i++) {
+               for (uint i = 0; i < size; i++) {
                        uint64_t val = s->getElement(i);
                        if (val < cvalue)
                                elemArray[count++] = val;
@@ -104,7 +104,7 @@ void ElementOpt::handlePredicateInequality(BooleanPredicate *pred, ElementSet *v
                break;
        }
        case SATC_GT: {
-               for(uint i=0; i<size; i++) {
+               for (uint i = 0; i < size; i++) {
                        uint64_t val = s->getElement(i);
                        if (val > cvalue)
                                elemArray[count++] = val;
@@ -112,7 +112,7 @@ void ElementOpt::handlePredicateInequality(BooleanPredicate *pred, ElementSet *v
                break;
        }
        case SATC_LTE: {
-               for(uint i=0; i<size; i++) {
+               for (uint i = 0; i < size; i++) {
                        uint64_t val = s->getElement(i);
                        if (val <= cvalue)
                                elemArray[count++] = val;
@@ -120,40 +120,40 @@ void ElementOpt::handlePredicateInequality(BooleanPredicate *pred, ElementSet *v
                break;
        }
        case SATC_GTE: {
-               for(uint i=0; i<size; i++) {
+               for (uint i = 0; i < size; i++) {
                        uint64_t val = s->getElement(i);
                        if (val >= cvalue)
                                elemArray[count++] = val;
                }
                break;
        }
-               
+
        default:
                ASSERT(0);
        }
        if (size == count)
                return;
-       
+
        Set *newset = solver->createSet(s->type, elemArray, count);
        solver->elemMap.remove(var);
        var->set = newset;
        solver->elemMap.put(var, var);
 
        if (count == 1) {
-               ElementConst * elemconst = (ElementConst *) solver->getElementConst(s->type, elemArray[0]);
+               ElementConst *elemconst = (ElementConst *) solver->getElementConst(s->type, elemArray[0]);
                replaceVarWithConst(pred, var, elemconst);
        }
 }
 
 void ElementOpt::constrainVarWithConst(BooleanPredicate *pred, ElementSet *var, ElementConst *value) {
-       Set * s = var->getRange();
+       Set *s = var->getRange();
        if (s->isRange)
                return;
        uint size = s->getSize();
        uint64_t elemArray[size];
        uint count = 0;
        uint64_t cvalue = value->value;
-       for(uint i=0; i<size; i++) {
+       for (uint i = 0; i < size; i++) {
                uint64_t val = s->getElement(i);
                if (val != cvalue)
                        elemArray[count++] = val;
@@ -167,19 +167,19 @@ void ElementOpt::constrainVarWithConst(BooleanPredicate *pred, ElementSet *var,
        solver->elemMap.put(var, var);
 
        if (count == 1) {
-               ElementConst * elemconst = (ElementConst *) solver->getElementConst(s->type, elemArray[0]);
+               ElementConst *elemconst = (ElementConst *) solver->getElementConst(s->type, elemArray[0]);
                replaceVarWithConst(pred, var, elemconst);
        }
 }
 
-void ElementOpt::replaceVarWithConst(BooleanPredicate * pred, ElementSet *var, ElementConst * value) {
+void ElementOpt::replaceVarWithConst(BooleanPredicate *pred, ElementSet *var, ElementConst *value) {
        uint size = var->parents.getSize();
-       for(uint i=0; i < size; i++) {
-               ASTNode * parent = var->parents.get(i);
+       for (uint i = 0; i < size; i++) {
+               ASTNode *parent = var->parents.get(i);
                if (parent->type == PREDICATEOP && pred != parent) {
-                       BooleanPredicate * newpred = (BooleanPredicate *) parent;
-                       for(uint j=0; j < newpred->inputs.getSize(); j++) {
-                               Element * e = newpred->inputs.get(j);
+                       BooleanPredicate *newpred = (BooleanPredicate *) parent;
+                       for (uint j = 0; j < newpred->inputs.getSize(); j++) {
+                               Element *e = newpred->inputs.get(j);
                                if (e == var) {
                                        solver->boolMap.remove(newpred);
                                        newpred->inputs.set(j, value);
old mode 100755 (executable)
new mode 100644 (file)
index a1f6005..c1b7390
@@ -14,7 +14,7 @@ private:
        void processPredicate(BooleanPredicate *);
        void handlePredicateEquals(BooleanPredicate *pred, ElementSet *left, ElementConst *right);
        void handlePredicateInequality(BooleanPredicate *pred, ElementSet *left, ElementConst *right);
-       void replaceVarWithConst(BooleanPredicate * pred, ElementSet *var, ElementConst * value);
+       void replaceVarWithConst(BooleanPredicate *pred, ElementSet *var, ElementConst *value);
        void constrainVarWithConst(BooleanPredicate *pred, ElementSet *var, ElementConst *value);
 
        Vector<BooleanPredicate *> workList;
index 37a3db4..3022060 100644 (file)
@@ -69,11 +69,11 @@ Node *allocResizeNode(uint capacity) {
 Edge cloneEdge(Edge e) {
        if (edgeIsVarConst(e))
                return e;
-       Node * node = getNodePtrFromEdge(e);
+       Node *node = getNodePtrFromEdge(e);
        bool isneg = isNegEdge(e);
        uint numEdges = node->numEdges;
-       Node * clone = allocBaseNode(node->type, numEdges);
-       for(uint i=0; i < numEdges; i++) {
+       Node *clone = allocBaseNode(node->type, numEdges);
+       for (uint i = 0; i < numEdges; i++) {
                clone->edges[i] = cloneEdge(node->edges[i]);
        }
        return isneg ? constraintNegate((Edge) {clone}) : (Edge) {clone};
@@ -82,9 +82,9 @@ Edge cloneEdge(Edge e) {
 void freeEdgeRec(Edge e) {
        if (edgeIsVarConst(e))
                return;
-       Node * node = getNodePtrFromEdge(e);
+       Node *node = getNodePtrFromEdge(e);
        uint numEdges = node->numEdges;
-       for(uint i=0; i < numEdges; i++) {
+       for (uint i = 0; i < numEdges; i++) {
                freeEdgeRec(node->edges[i]);
        }
        ourfree(node);
@@ -93,21 +93,21 @@ void freeEdgeRec(Edge e) {
 void freeEdge(Edge e) {
        if (edgeIsVarConst(e))
                return;
-       Node * node = getNodePtrFromEdge(e);
+       Node *node = getNodePtrFromEdge(e);
        ourfree(node);
 }
 
-void freeEdgesRec(uint numEdges, Edge * earray) {
-       for(uint i=0; i < numEdges; i++) {
+void freeEdgesRec(uint numEdges, Edge *earray) {
+       for (uint i = 0; i < numEdges; i++) {
                Edge e = earray[i];
                freeEdgeRec(e);
        }
 }
 
 void freeEdgeCNF(Edge e) {
-       Node * node = getNodePtrFromEdge(e);
+       Node *node = getNodePtrFromEdge(e);
        uint numEdges = node->numEdges;
-       for(uint i=0; i < numEdges; i++) {
+       for (uint i = 0; i < numEdges; i++) {
                Edge ec = node->edges[i];
                if (!edgeIsVarConst(ec)) {
                        ourfree(ec.node_ptr);
@@ -116,7 +116,7 @@ void freeEdgeCNF(Edge e) {
        ourfree(node);
 }
 
-void addEdgeToResizeNode(Node ** node, Edge e) {
+void addEdgeToResizeNode(Node **node, Edge e) {
        Node *currnode = *node;
        if (currnode->capacity == currnode->numEdges) {
                Node *newnode = allocResizeNode( currnode->capacity << 1);
@@ -124,17 +124,17 @@ void addEdgeToResizeNode(Node ** node, Edge e) {
                newnode->numEdges = currnode->numEdges;
                memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
                ourfree(currnode);
-               *node=newnode;
+               *node = newnode;
                currnode = newnode;
        }
        currnode->edges[currnode->numEdges++] = e;
 }
 
-void mergeFreeNodeToResizeNode(Node **node, Node * innode) {
-       Node * currnode = *node;
+void mergeFreeNodeToResizeNode(Node **node, Node *innode) {
+       Node *currnode = *node;
        uint currEdges = currnode->numEdges;
        uint inEdges = innode->numEdges;
-       
+
        uint newsize = currEdges + inEdges;
        if (newsize >= currnode->capacity) {
                if (newsize < innode->capacity) {
@@ -149,7 +149,7 @@ void mergeFreeNodeToResizeNode(Node **node, Node * innode) {
                        newnode->numEdges = currnode->numEdges;
                        memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
                        ourfree(currnode);
-                       *node=newnode;
+                       *node = newnode;
                        currnode = newnode;
                }
        } else {
@@ -166,8 +166,8 @@ void mergeFreeNodeToResizeNode(Node **node, Node * innode) {
        ourfree(innode);
 }
 
-void mergeNodeToResizeNode(Node **node, Node * innode) {
-       Node * currnode = *node;
+void mergeNodeToResizeNode(Node **node, Node *innode) {
+       Node *currnode = *node;
        uint currEdges = currnode->numEdges;
        uint inEdges = innode->numEdges;
        uint newsize = currEdges + inEdges;
@@ -177,7 +177,7 @@ void mergeNodeToResizeNode(Node **node, Node * innode) {
                newnode->numEdges = currnode->numEdges;
                memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
                ourfree(currnode);
-               *node=newnode;
+               *node = newnode;
                currnode = newnode;
        }
        memcpy(&currnode->edges[currnode->numEdges], innode->edges, inEdges * sizeof(Edge));
@@ -245,7 +245,7 @@ Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
                        ASSERT(!isNodeEdge(e1));
                        if (!sameSignEdge(e1, e2)) {
                                freeEdgesRec(lowindex + 1, edges);
-                               freeEdgesRec(numEdges-initindex, &edges[initindex]);
+                               freeEdgesRec(numEdges - initindex, &edges[initindex]);
                                return E_False;
                        }
                } else
@@ -265,22 +265,22 @@ Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
                Edge *e0edges = getEdgeArray(edges[0]);
                Edge *e1edges = getEdgeArray(edges[1]);
                if (sameNodeOppSign(e0edges[0], e1edges[0])) {
-                       Edge result=constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
+                       Edge result = constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
                        freeEdge(edges[0]);
                        freeEdge(edges[1]);
                        return result;
                } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
-                       Edge result=constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
+                       Edge result = constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
                        freeEdge(edges[0]);
                        freeEdge(edges[1]);
                        return result;
                } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
-                       Edge result=constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
+                       Edge result = constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
                        freeEdge(edges[0]);
                        freeEdge(edges[1]);
                        return result;
                } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
-                       Edge result=constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
+                       Edge result = constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
                        freeEdge(edges[0]);
                        freeEdge(edges[1]);
                        return result;
@@ -375,7 +375,7 @@ Edge disjoinLit(Edge vec, Edge lit) {
        Node *nvec = vec.node_ptr;
        uint nvecedges = nvec->numEdges;
 
-       for(uint i=0; i < nvecedges; i++) {
+       for (uint i = 0; i < nvecedges; i++) {
                Edge ce = nvec->edges[i];
                if (!edgeIsVarConst(ce)) {
                        Node *cne = ce.node_ptr;
@@ -388,18 +388,18 @@ Edge disjoinLit(Edge vec, Edge lit) {
                        nvec->edges[i] = (Edge) {clause};
                }
        }
-       nvec->numVars+=nvecedges;
+       nvec->numVars += nvecedges;
        return vec;
 }
 
-Edge disjoinAndFree(CNF * cnf, Edge newvec, Edge cnfform) {
+Edge disjoinAndFree(CNF *cnf, Edge newvec, Edge cnfform) {
        Node *nnewvec = newvec.node_ptr;
        Node *ncnfform = cnfform.node_ptr;
        uint newvecedges = nnewvec->numEdges;
        uint cnfedges = ncnfform->numEdges;
        uint newvecvars = nnewvec->numVars;
        uint cnfvars = ncnfform->numVars;
-       
+
        if (cnfedges > 3 ||
                        ((cnfedges * newvecvars + newvecedges * cnfvars) > (cnfedges + newvecedges + newvecvars + cnfvars))) {
                Edge proxyVar = constraintNewVar(cnf);
@@ -416,7 +416,7 @@ Edge disjoinAndFree(CNF * cnf, Edge newvec, Edge cnfform) {
 
 
 
-       if (newvecedges == 1 || cnfedges ==1) {
+       if (newvecedges == 1 || cnfedges == 1) {
                if (cnfedges != 1) {
                        Node *tmp = nnewvec;
                        nnewvec = ncnfform;
@@ -427,7 +427,7 @@ Edge disjoinAndFree(CNF * cnf, Edge newvec, Edge cnfform) {
                Edge e = ncnfform->edges[0];
                if (!edgeIsVarConst(e)) {
                        Node *n = e.node_ptr;
-                       for(uint i=0; i < newvecedges; i++) {
+                       for (uint i = 0; i < newvecedges; i++) {
                                Edge ce = nnewvec->edges[i];
                                if (isNodeEdge(ce)) {
                                        Node *cne = ce.node_ptr;
@@ -442,7 +442,7 @@ Edge disjoinAndFree(CNF * cnf, Edge newvec, Edge cnfform) {
                        }
                        nnewvec->numVars += newvecedges * n->numVars;
                } else {
-                       for(uint i=0; i < newvecedges; i++) {
+                       for (uint i = 0; i < newvecedges; i++) {
                                Edge ce = nnewvec->edges[i];
                                if (!edgeIsVarConst(ce)) {
                                        Node *cne = ce.node_ptr;
@@ -457,16 +457,16 @@ Edge disjoinAndFree(CNF * cnf, Edge newvec, Edge cnfform) {
                        }
                        nnewvec->numVars += newvecedges;
                }
-               freeEdgeCNF((Edge){ncnfform});
+               freeEdgeCNF((Edge) {ncnfform});
                return (Edge) {nnewvec};
        }
-       
-       Node * result = allocResizeNode(1);
 
-       for(uint i=0; i <newvecedges; i++) {
+       Node *result = allocResizeNode(1);
+
+       for (uint i = 0; i < newvecedges; i++) {
                Edge nedge = nnewvec->edges[i];
                uint nSize = isNodeEdge(nedge) ? nedge.node_ptr->numEdges : 1;
-               for(uint j=0; j < cnfedges; j++) {
+               for (uint j = 0; j < cnfedges; j++) {
                        Edge cedge = ncnfform->edges[j];
                        uint cSize = isNodeEdge(cedge) ? cedge.node_ptr->numEdges : 1;
                        if (equalsEdge(cedge, nedge)) {
@@ -484,7 +484,7 @@ Edge disjoinAndFree(CNF * cnf, Edge newvec, Edge cnfform) {
                                } else {
                                        addEdgeToResizeNode(&clause, cedge);
                                }
-                               addEdgeToResizeNode(&result, (Edge){clause});
+                               addEdgeToResizeNode(&result, (Edge) {clause});
                                result->numVars += clause->numEdges;
                        }
                        //otherwise skip
@@ -503,14 +503,14 @@ Edge simplifyCNF(CNF *cnf, Edge input) {
                return (Edge) {newvec};
        }
        bool negated = isNegEdge(input);
-       Node * node = getNodePtrFromEdge(input);
+       Node *node = getNodePtrFromEdge(input);
        NodeType type = node->type;
        if (!negated) {
                if (type == NodeType_AND) {
                        //AND case
                        Node *newvec = allocResizeNode(node->numEdges);
                        uint numEdges = node->numEdges;
-                       for(uint i = 0; i < numEdges; i++) {
+                       for (uint i = 0; i < numEdges; i++) {
                                Edge e = simplifyCNF(cnf, node->edges[i]);
                                uint enumvars = e.node_ptr->numVars;
                                mergeFreeNodeToResizeNode(&newvec, e.node_ptr);
@@ -530,10 +530,10 @@ Edge simplifyCNF(CNF *cnf, Edge input) {
                        //free temporary nodes
                        ourfree(getNodePtrFromEdge(thencons));
                        ourfree(getNodePtrFromEdge(elsecons));
-                       Node * result = thencnf.node_ptr;
-                       uint elsenumvars=elsecnf.node_ptr->numVars;
+                       Node *result = thencnf.node_ptr;
+                       uint elsenumvars = elsecnf.node_ptr->numVars;
                        mergeFreeNodeToResizeNode(&result, elsecnf.node_ptr);
-                       result->numVars+=elsenumvars;
+                       result->numVars += elsenumvars;
                        return (Edge) {result};
                }
        } else {
@@ -542,7 +542,7 @@ Edge simplifyCNF(CNF *cnf, Edge input) {
                        uint numEdges = node->numEdges;
 
                        Edge newvec = simplifyCNF(cnf, constraintNegate(node->edges[0]));
-                       for(uint i = 1; i < numEdges; i++) {
+                       for (uint i = 1; i < numEdges; i++) {
                                Edge e = node->edges[i];
                                Edge cnfform = simplifyCNF(cnf, constraintNegate(e));
                                newvec = disjoinAndFree(cnf, newvec, cnfform);
@@ -558,7 +558,7 @@ Edge simplifyCNF(CNF *cnf, Edge input) {
                        Edge thencons = createNode(NodeType_AND, 2, thenedges);
                        Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
                        Edge elsecons = createNode(NodeType_AND, 2, elseedges);
-                       
+
                        Edge combinededges[] = {constraintNegate(thencons), constraintNegate(elsecons)};
                        Edge combined = constraintNegate(createNode(NodeType_AND, 2, combinededges));
                        Edge result = simplifyCNF(cnf, combined);
@@ -572,26 +572,26 @@ Edge simplifyCNF(CNF *cnf, Edge input) {
 }
 
 void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar) {
-       Node * andNode = cnfform.node_ptr;
+       Node *andNode = cnfform.node_ptr;
        int orvar = getEdgeVar(eorvar);
        ASSERT(orvar != 0);
        uint numEdges = andNode->numEdges;
-       for(uint i=0; i < numEdges; i++) {
+       for (uint i = 0; i < numEdges; i++) {
                Edge e = andNode->edges[i];
                if (edgeIsVarConst(e)) {
                        int array[2] = {getEdgeVar(e), orvar};
                        ASSERT(array[0] != 0);
                        addArrayClauseLiteral(cnf->solver, 2, array);
                } else {
-                       Node * clause = e.node_ptr;
+                       Node *clause = e.node_ptr;
                        uint cnumEdges = clause->numEdges + 1;
                        if (cnumEdges > cnf->asize) {
                                cnf->asize = cnumEdges << 1;
                                ourfree(cnf->array);
                                cnf->array = (int *) ourmalloc(sizeof(int) * cnf->asize);
                        }
-                       int * array = cnf->array;
-                       for(uint j=0; j < (cnumEdges - 1); j++) {
+                       int *array = cnf->array;
+                       for (uint j = 0; j < (cnumEdges - 1); j++) {
                                array[j] = getEdgeVar(clause->edges[j]);
                                ASSERT(array[j] != 0);
                        }
@@ -602,24 +602,24 @@ void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar) {
 }
 
 void outputCNF(CNF *cnf, Edge cnfform) {
-       Node * andNode = cnfform.node_ptr;
+       Node *andNode = cnfform.node_ptr;
        uint numEdges = andNode->numEdges;
-       for(uint i=0; i < numEdges; i++) {
+       for (uint i = 0; i < numEdges; i++) {
                Edge e = andNode->edges[i];
                if (edgeIsVarConst(e)) {
                        int array[1] = {getEdgeVar(e)};
                        ASSERT(array[0] != 0);
                        addArrayClauseLiteral(cnf->solver, 1, array);
                } else {
-                       Node * clause = e.node_ptr;
+                       Node *clause = e.node_ptr;
                        uint cnumEdges = clause->numEdges;
                        if (cnumEdges > cnf->asize) {
                                cnf->asize = cnumEdges << 1;
                                ourfree(cnf->array);
                                cnf->array = (int *) ourmalloc(sizeof(int) * cnf->asize);
                        }
-                       int * array = cnf->array;
-                       for(uint j=0; j < cnumEdges; j++) {
+                       int *array = cnf->array;
+                       for (uint j = 0; j < cnumEdges; j++) {
                                array[j] = getEdgeVar(clause->edges[j]);
                                ASSERT(array[j] != 0);
                        }
@@ -664,7 +664,7 @@ void addConstraintCNF(CNF *cnf, Edge constraint) {
        printCNF(constraint);
        model_print("\n******************************\n");
 #endif
-       
+
        Edge cnfform = simplifyCNF(cnf, constraint);
        freeEdgeRec(constraint);
        outputCNF(cnf, cnfform);
@@ -785,7 +785,7 @@ Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
 }
 
 void generateAddConstraint(CNF *cnf, uint nSum, Edge *sum, uint nVar1, Edge *var1, uint nVar2, Edge *var2) {
-  //TO WRITE....
+       //TO WRITE....
 }
 
 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
index bfe3e25..d7d2744 100644 (file)
@@ -48,7 +48,7 @@ struct CNF {
        uint varcount;
        uint asize;
        IncrementalSolver *solver;
-       int * array;
+       int *array;
        long long solveTime;
        long long encodeTime;
        bool unsat;
@@ -173,9 +173,9 @@ void printCNF(Edge e);
 Node *allocBaseNode(NodeType type, uint numEdges);
 Node *allocResizeNode(uint capacity);
 Edge cloneEdge(Edge e);
-void addEdgeToResizeNode(Node ** node, Edge e);
-void mergeFreeNodeToResizeNode(Node **node, Node * innode);
-void mergeNodeToResizeNode(Node **node, Node * innode);
+void addEdgeToResizeNode(Node **node, Edge e);
+void mergeFreeNodeToResizeNode(Node **node, Node *innode);
+void mergeNodeToResizeNode(Node **node, Node *innode);
 void freeEdgeRec(Edge e);
 void outputCNF(CNF *cnf, Edge cnfform);
 void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar);
index 5342c4f..6062591 100644 (file)
@@ -7,7 +7,7 @@
 #include "predicate.h"
 
 
-void SATEncoder::shouldMemoize(Element *elem, uint64_t val, bool & memo) {
+void SATEncoder::shouldMemoize(Element *elem, uint64_t val, bool &memo) {
        uint numParents = elem->parents.getSize();
        uint posPolarity = 0;
        uint negPolarity = 0;
@@ -15,10 +15,10 @@ void SATEncoder::shouldMemoize(Element *elem, uint64_t val, bool & memo) {
        if (elem->type == ELEMFUNCRETURN) {
                memo = true;
        }
-       for(uint i = 0; i < numParents; i++) {
-               ASTNode * node = elem->parents.get(i);
+       for (uint i = 0; i < numParents; i++) {
+               ASTNode *node = elem->parents.get(i);
                if (node->type == PREDICATEOP) {
-                       BooleanPredicate * pred = (BooleanPredicate *) node;
+                       BooleanPredicate *pred = (BooleanPredicate *) node;
                        Polarity polarity = pred->polarity;
                        FunctionEncodingType encType = pred->encoding.type;
                        bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
@@ -27,49 +27,49 @@ void SATEncoder::shouldMemoize(Element *elem, uint64_t val, bool & memo) {
 
                                UndefinedBehavior undefStatus = ((PredicateTable *)pred->predicate)->undefinedbehavior;
 
-                               Polarity tpolarity=polarity;
+                               Polarity tpolarity = polarity;
                                if (generateNegation)
                                        tpolarity = negatePolarity(tpolarity);
-                               if (undefStatus ==SATC_FLAGFORCEUNDEFINED)
+                               if (undefStatus == SATC_FLAGFORCEUNDEFINED)
                                        tpolarity = P_BOTHTRUEFALSE;
                                if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
                                        memo = true;
                                if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
                                        memo = true;
                        } else if (pred->predicate->type == OPERATORPRED) {
-                                       if (pred->encoding.type == ENUMERATEIMPLICATIONS || pred->encoding.type == ENUMERATEIMPLICATIONSNEGATE) {
-                                               Polarity tpolarity = polarity;
-                                               if (generateNegation)
-                                                       tpolarity = negatePolarity(tpolarity);
-                                               PredicateOperator *predicate = (PredicateOperator *)pred->predicate;
-                                               uint numDomains = pred->inputs.getSize();
-                                               bool isConstant = true;
-                                               for (uint i = 0; i < numDomains; i++) {
-                                                       Element *e = pred->inputs.get(i);
-                                                       if (elem != e && e->type != ELEMCONST) {
-                                                               isConstant = false;
-                                                       }
+                               if (pred->encoding.type == ENUMERATEIMPLICATIONS || pred->encoding.type == ENUMERATEIMPLICATIONSNEGATE) {
+                                       Polarity tpolarity = polarity;
+                                       if (generateNegation)
+                                               tpolarity = negatePolarity(tpolarity);
+                                       PredicateOperator *predicate = (PredicateOperator *)pred->predicate;
+                                       uint numDomains = pred->inputs.getSize();
+                                       bool isConstant = true;
+                                       for (uint i = 0; i < numDomains; i++) {
+                                               Element *e = pred->inputs.get(i);
+                                               if (elem != e && e->type != ELEMCONST) {
+                                                       isConstant = false;
                                                }
-                                               if (predicate->getOp() == SATC_EQUALS) {
+                                       }
+                                       if (predicate->getOp() == SATC_EQUALS) {
+                                               if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
+                                                       posPolarity++;
+                                               if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
+                                                       negPolarity++;
+                                       } else {
+                                               if (isConstant) {
                                                        if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
                                                                posPolarity++;
                                                        if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
                                                                negPolarity++;
                                                } else {
-                                                       if (isConstant) {
-                                                               if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
-                                                                       posPolarity++;
-                                                               if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
-                                                                       negPolarity++;
-                                                       } else {
-                                                               if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
-                                                                       memo = true;
-                                                               if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
-                                                                       memo = true;                                                    
-                                                       }
+                                                       if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
+                                                               memo = true;
+                                                       if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
+                                                               memo = true;
                                                }
                                        }
-                               } else {
+                               }
+                       } else {
                                ASSERT(0);
                        }
                } else if (node->type == ELEMFUNCRETURN) {
@@ -130,7 +130,7 @@ Edge SATEncoder::getElementValueBinaryIndexConstraint(Element *elem, Polarity p,
                if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) {
                        if (elemEnc->numVars == 0)
                                return E_True;
-                       
+
                        if (elemEnc->encoding != EENC_NONE && elemEnc->numVars > 1) {
                                if (impliesPolarity(elemEnc->polarityArray[i], p)) {
                                        return elemEnc->edgeArray[i];
@@ -142,11 +142,11 @@ Edge SATEncoder::getElementValueBinaryIndexConstraint(Element *elem, Polarity p,
                                                generateProxy(cnf, generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i), elemEnc->edgeArray[i], P_BOTHTRUEFALSE);
                                                elemEnc->polarityArray[i] = p;
                                        } else if (!impliesPolarity(elemEnc->polarityArray[i], P_TRUE)  && impliesPolarity(p, P_TRUE)) {
-                                               generateProxy(cnf, generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i), elemEnc->edgeArray[i], P_TRUE);                      
-                                               elemEnc->polarityArray[i] = (Polarity) (((int) elemEnc->polarityArray[i])| ((int)P_TRUE));
-                                       }       else if (!impliesPolarity(elemEnc->polarityArray[i], P_FALSE)  && impliesPolarity(p, P_FALSE)) {
-                                               generateProxy(cnf, generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i), elemEnc->edgeArray[i], P_FALSE);                     
-                                               elemEnc->polarityArray[i] = (Polarity) (((int) elemEnc->polarityArray[i])| ((int)P_FALSE));
+                                               generateProxy(cnf, generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i), elemEnc->edgeArray[i], P_TRUE);
+                                               elemEnc->polarityArray[i] = (Polarity) (((int) elemEnc->polarityArray[i]) | ((int)P_TRUE));
+                                       } else if (!impliesPolarity(elemEnc->polarityArray[i], P_FALSE)  && impliesPolarity(p, P_FALSE)) {
+                                               generateProxy(cnf, generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i), elemEnc->edgeArray[i], P_FALSE);
+                                               elemEnc->polarityArray[i] = (Polarity) (((int) elemEnc->polarityArray[i]) | ((int)P_FALSE));
                                        }
                                        return elemEnc->edgeArray[i];
                                }
@@ -214,7 +214,7 @@ void SATEncoder::generateBinaryValueEncodingVars(ElementEncoding *encoding) {
        ASSERT(encoding->type == BINARYVAL);
        allocElementConstraintVariables(encoding, encoding->numBits);
        getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
-       if(encoding->anyValue)
+       if (encoding->anyValue)
                generateAnyValueBinaryValueEncoding(encoding);
 }
 
@@ -222,7 +222,7 @@ void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
        ASSERT(encoding->type == BINARYINDEX);
        allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize - 1));
        getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
-       if(encoding->anyValue)
+       if (encoding->anyValue)
                generateAnyValueBinaryIndexEncoding(encoding);
 }
 
@@ -234,7 +234,7 @@ void SATEncoder::generateOneHotEncodingVars(ElementEncoding *encoding) {
                        addConstraintCNF(cnf, constraintNegate(constraintAND2(cnf, encoding->variables[i], encoding->variables[j])));
                }
        }
-       if(encoding->anyValue)
+       if (encoding->anyValue)
                addConstraintCNF(cnf, constraintOR(cnf, encoding->numVars, encoding->variables));
 }
 
@@ -270,30 +270,30 @@ void SATEncoder::generateElementEncoding(Element *element) {
        }
 }
 
-void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding){
-       if(encoding->numVars == 0)
+void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding) {
+       if (encoding->numVars == 0)
                return;
        int index = -1;
-       for(uint i= encoding->encArraySize-1; i>=0; i--){
-               if(encoding->isinUseElement(i)){
-                       if(i+1 < encoding->encArraySize){
-                               index = i+1;
+       for (uint i = encoding->encArraySize - 1; i >= 0; i--) {
+               if (encoding->isinUseElement(i)) {
+                       if (i + 1 < encoding->encArraySize) {
+                               index = i + 1;
                        }
                        break;
                }
        }
-       if( index != -1 ){
+       if ( index != -1 ) {
                addConstraintCNF(cnf, generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, index));
        }
-       index = index == -1? encoding->encArraySize-1 : index-1;
-       for(int i= index; i>=0; i--) {
-               if (!encoding->isinUseElement(i)){
+       index = index == -1 ? encoding->encArraySize - 1 : index - 1;
+       for (int i = index; i >= 0; i--) {
+               if (!encoding->isinUseElement(i)) {
                        addConstraintCNF(cnf, constraintNegate( generateBinaryConstraint(cnf, encoding->numVars, encoding->variables, i)));
                }
        }
 }
 
-void SATEncoder::generateAnyValueBinaryValueEncoding(ElementEncoding *encoding){
+void SATEncoder::generateAnyValueBinaryValueEncoding(ElementEncoding *encoding) {
        uint64_t minvalueminusoffset = encoding->low - encoding->offset;
        uint64_t maxvalueminusoffset = encoding->high - encoding->offset;
        model_print("This is minvalueminus offset: %lu", minvalueminusoffset);
index b13541d..659c0d9 100644 (file)
@@ -16,7 +16,7 @@
 SATEncoder::SATEncoder(CSolver *_solver) :
        cnf(createCNF()),
        solver(_solver),
-  vector(allocDefVectorEdge()) {
+       vector(allocDefVectorEdge()) {
 }
 
 SATEncoder::~SATEncoder() {
index 7fb889c..0ccf31c 100644 (file)
@@ -22,7 +22,7 @@ public:
 
        CMEMALLOC;
 private:
-       void shouldMemoize(Element *elem, uint64_t val, bool & memo);
+       void shouldMemoize(Element *elem, uint64_t val, bool &memo);
        Edge getNewVarSATEncoder();
        void getArrayNewVarsSATEncoder(uint num, Edge *carray);
        Edge encodeVarSATEncoder(BooleanVar *constraint);
index 0cfce9b..ff91dc3 100644 (file)
@@ -48,7 +48,7 @@ Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constra
        }
 
        bool notfinished = true;
-        Edge carray[numDomains];
+       Edge carray[numDomains];
        while (notfinished) {
                if (predicate->evalPredicateOperator(vals) != generateNegation) {
                        //Include this in the set of terms
@@ -110,7 +110,7 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
        }
 
        bool notfinished = true;
-        Edge carray[numDomains + 1];
+       Edge carray[numDomains + 1];
        while (notfinished) {
                uint64_t result = function->applyFunctionOperator(numDomains, vals);
                bool isInRange = ((FunctionOperator *)func->getFunction())->isInRangeFunction(result);
index 9e6087e..da89550 100644 (file)
@@ -25,7 +25,7 @@ Edge SATEncoder::encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *con
        bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
        if (generateNegation)
                polarity = negatePolarity(polarity);
-       if (undefStatus ==SATC_FLAGFORCEUNDEFINED)
+       if (undefStatus == SATC_FLAGFORCEUNDEFINED)
                polarity = P_BOTHTRUEFALSE;
 
        Edge constraints[size];
@@ -51,7 +51,7 @@ Edge SATEncoder::encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *con
                case SATC_FLAGFORCEUNDEFINED: {
                        row = constraintAND(cnf, inputNum, carray);
                        uint pSize = constraint->parents.getSize();
-                       if(!edgeIsVarConst(row) && pSize > (uint)solver->getTuner()->getTunable(PROXYVARIABLE, &proxyparameter)){
+                       if (!edgeIsVarConst(row) && pSize > (uint)solver->getTuner()->getTunable(PROXYVARIABLE, &proxyparameter)) {
                                Edge proxy = constraintNewVar(cnf);
                                generateProxy(cnf, row, proxy, P_BOTHTRUEFALSE);
                                Edge undefConst = encodeConstraintSATEncoder(constraint->undefStatus);
@@ -102,8 +102,8 @@ Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint
 
        if (generateNegation)
                polarity = negatePolarity(polarity);
-       
-        ASSERT(numDomains != 0);
+
+       ASSERT(numDomains != 0);
        VectorEdge *clauses = allocDefVectorEdge();
 
        uint indices[numDomains];       //setup indices
@@ -214,20 +214,20 @@ void SATEncoder::encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *func)
                Edge output = getElementValueConstraint(func, P_TRUE, entry->output);
                switch (undefStatus ) {
                case SATC_IGNOREBEHAVIOR: {
-                        if(inputNum == 0){
-                                addConstraintCNF(cnf, output);
-                        }else{
-                                addConstraintCNF(cnf, constraintIMPLIES(cnf,constraintAND(cnf, inputNum, carray), output));
-                        }
+                       if (inputNum == 0) {
+                               addConstraintCNF(cnf, output);
+                       } else {
+                               addConstraintCNF(cnf, constraintIMPLIES(cnf,constraintAND(cnf, inputNum, carray), output));
+                       }
                        break;
                }
                case SATC_FLAGFORCEUNDEFINED: {
                        Edge undefConst = encodeConstraintSATEncoder(func->overflowstatus);
-                        if(inputNum ==0){
-                                addConstraintCNF(cnf, constraintAND2(cnf, output, constraintNegate(undefConst)));
-                        }else{
-                                addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray), constraintAND2(cnf, output, constraintNegate(undefConst))));
-                        }
+                       if (inputNum == 0) {
+                               addConstraintCNF(cnf, constraintAND2(cnf, output, constraintNegate(undefConst)));
+                       } else {
+                               addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray), constraintAND2(cnf, output, constraintNegate(undefConst))));
+                       }
                        break;
                }
                default:
@@ -243,7 +243,7 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc
        model_print("Enumeration Table functions ...\n");
 #endif
        ASSERT(elemFunc->getFunction()->type == TABLEFUNC);
-       
+
        //First encode children
        Array<Element *> *elements = &elemFunc->inputs;
        for (uint i = 0; i < elements->getSize(); i++) {
@@ -288,11 +288,11 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc
                switch (function->undefBehavior) {
                case SATC_UNDEFINEDSETSFLAG: {
                        if (isInRange) {
-                                if(numDomains == 0){
-                                        addConstraintCNF(cnf,carray[numDomains]);
-                                }else{
-                                        addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]));
-                                }
+                               if (numDomains == 0) {
+                                       addConstraintCNF(cnf,carray[numDomains]);
+                               } else {
+                                       addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]));
+                               }
                        } else {
                                Edge undefConstraint = encodeConstraintSATEncoder(elemFunc->overflowstatus);
                                addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint));
@@ -302,15 +302,15 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc
                case SATC_FLAGIFFUNDEFINED: {
                        Edge undefConstraint = encodeConstraintSATEncoder(elemFunc->overflowstatus);
                        if (isInRange) {
-                                if(numDomains == 0){
-                                        addConstraintCNF(cnf, constraintAND2(cnf,carray[numDomains], constraintNegate(undefConstraint)) );
-                                }else{
-                                        Edge freshvar = constraintNewVar(cnf);
-                                        addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), freshvar ));
-                                        addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, constraintNegate(undefConstraint) ));
-                                        addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, carray[numDomains]));
-                                }
-                               
+                               if (numDomains == 0) {
+                                       addConstraintCNF(cnf, constraintAND2(cnf,carray[numDomains], constraintNegate(undefConstraint)) );
+                               } else {
+                                       Edge freshvar = constraintNewVar(cnf);
+                                       addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), freshvar ));
+                                       addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, constraintNegate(undefConstraint) ));
+                                       addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, carray[numDomains]));
+                               }
+
                        } else {
                                addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint));
                        }
index 9d9e36b..28d2faf 100644 (file)
@@ -2,7 +2,7 @@
 #include "corestructs.h"
 #include "boolean.h"
 
-void BooleanEdge::print(){
+void BooleanEdge::print() {
        if (isNegated())
                model_print("!");
        getBoolean()->print();
index 009c047..86cbce9 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 0a50bb9..fdcb59f 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:
        /**
index d384220..f4e7ec9 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 3cf0010..6c53253 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 d153793..0740461 100644 (file)
@@ -33,7 +33,7 @@ public:
        }
        void print();
 
-        bool anyValue;
+       bool anyValue;
        ElementEncodingType type;
        Element *element;
        Edge *variables;/* List Variables Used To Encode Element */
@@ -41,8 +41,8 @@ public:
                struct {
                        uint64_t *encodingArray;        /* List the Variables in the appropriate order */
                        uint64_t *inUseArray;   /* Bitmap to track variables in use */
-                       Edge * edgeArray;
-                       Polarity * polarityArray;
+                       Edge *edgeArray;
+                       Polarity *polarityArray;
                        uint encArraySize;
                        ElemEnc encoding;
                };
index 952684a..1b101e3 100644 (file)
@@ -11,13 +11,13 @@ int main(int numargs, char **argv) {
        Element *e2 = solver->getElementVar(s2);
        solver->mustHaveValue(e1);
        solver->mustHaveValue(e2);
-       
+
        Predicate *equals = solver->createPredicateOperator(SATC_EQUALS);
        Element *inputs[] = {e1, e2};
        BooleanEdge b = solver->applyPredicate(equals, inputs, 2);
        b = solver->applyLogicalOperation(SATC_NOT, b);
        solver->addConstraint(b);
-       
+
        if (solver->solve() == 1)
                printf("e1=%" PRIu64 "e2=%" PRIu64 "\n", solver->getElementValue(e1), solver->getElementValue(e2));
        else
index 14c217a..a3b5392 100644 (file)
@@ -1,10 +1,10 @@
 #include "csolver.h"
 
 /**
- * !b1 AND 
+ * !b1 AND
  * !b2 OR b1 or (!b3 and b4) AND
  * b7 OR (!b1 AND (b5 or !b6))
- * 
+ *
  */
 int main(int numargs, char **argv) {
        CSolver *solver = new CSolver();
@@ -41,10 +41,10 @@ int main(int numargs, char **argv) {
        solver->printConstraints();
        if (solver->solve() == 1)
                printf("b1=%d\nb2=%d\nb3=%d\nb4=%d\nb5=%d\nb6=%d\nb7=%d\n",
-                                       solver->getBooleanValue(b1), solver->getBooleanValue(b2),
-                                       solver->getBooleanValue(b3), solver->getBooleanValue(b4),
-                                       solver->getBooleanValue(b5), solver->getBooleanValue(b6),
-                                       solver->getBooleanValue(b7));
+                                        solver->getBooleanValue(b1), solver->getBooleanValue(b2),
+                                        solver->getBooleanValue(b3), solver->getBooleanValue(b4),
+                                        solver->getBooleanValue(b5), solver->getBooleanValue(b6),
+                                        solver->getBooleanValue(b7));
        else
                printf("UNSAT\n");
        delete solver;
index 43954bd..067f7b8 100644 (file)
@@ -7,44 +7,44 @@ int main(int argc, char **argv) {
                printf("You should specify file names ...");
                exit(-1);
        }
-        //usleep(20000000);
+       //usleep(20000000);
        for (int i = 1; i < argc; i++) {
                CSolver *solver = CSolver::deserialize(argv[i]);
                CSolver *copy = solver->clone();
-                CSolver *copy2 = solver->clone();
-                CSolver *copy3 = solver->clone();
-                CSolver *copy4 = solver->clone();
-                int value = copy->solve();
-                if (value == 1) {
+               CSolver *copy2 = solver->clone();
+               CSolver *copy3 = solver->clone();
+               CSolver *copy4 = solver->clone();
+               int value = copy->solve();
+               if (value == 1) {
                        printf("Copy %s is SAT\n", argv[i]);
                } else {
                        printf("Copy %s is UNSAT\n", argv[i]);
                }
-                value = copy2->solve();
-                if (value == 1) {
+               value = copy2->solve();
+               if (value == 1) {
                        printf("Copy2 %s is SAT\n", argv[i]);
                } else {
                        printf("Copy2 %s is UNSAT\n", argv[i]);
                }
-                value = copy3->solve();
-                if (value == 1) {
+               value = copy3->solve();
+               if (value == 1) {
                        printf("Copy3 %s is SAT\n", argv[i]);
                } else {
                        printf("Copy3 %s is UNSAT\n", argv[i]);
                }
-                value = copy4->solve();
-                if (value == 1) {
+               value = copy4->solve();
+               if (value == 1) {
                        printf("Copy4 %s is SAT\n", argv[i]);
                } else {
                        printf("Copy4 %s is UNSAT\n", argv[i]);
                }
-                value = solver->solve();
+               value = solver->solve();
                if (value == 1) {
                        printf("Original %s is SAT\n", argv[i]);
                } else {
                        printf("Original %s is UNSAT\n", argv[i]);
                }
-                
+
                delete solver;
        }
        return 1;
index 2d7a852..bbb12e7 100644 (file)
@@ -7,7 +7,7 @@ int main(int argc, char **argv) {
                printf("You should specify file names ...");
                exit(-1);
        }
-        //usleep(20000000);
+       //usleep(20000000);
        for (int i = 1; i < argc; i++) {
                CSolver *solver = CSolver::deserialize(argv[i]);
                int value = solver->solve();
index 0dbaf8d..c01bf14 100644 (file)
@@ -25,12 +25,12 @@ DecomposeOrderResolver::~DecomposeOrderResolver() {
 
 void DecomposeOrderResolver::mustOrderEdge(uint64_t first, uint64_t second) {
        DOREdge edge(first, second, 0, first, second);
-       DOREdge *oldedge=edges.get(&edge);
+       DOREdge *oldedge = edges.get(&edge);
        if (oldedge != NULL) {
-               oldedge->mustbetrue=true;
+               oldedge->mustbetrue = true;
        } else {
                DOREdge *newedge = new DOREdge(first, second, 0, first, second);
-               newedge->mustbetrue=true;
+               newedge->mustbetrue = true;
                edges.add(newedge);
        }
 }
@@ -84,7 +84,7 @@ void DecomposeOrderResolver::buildGraph() {
                DOREdge *doredge = iterator->next();
                if (doredge->mustbetrue) {
                        graph->addEdge(doredge->origfirst, doredge->origsecond);
-                       if (doredge->newfirst != doredge->origfirst || doredge->newsecond!=doredge->origsecond) {
+                       if (doredge->newfirst != doredge->origfirst || doredge->newsecond != doredge->origsecond) {
                                graph->addEdge(doredge->newfirst, doredge->newsecond);
                        }
                } else if (doredge->orderindex != 0) {
index 8e2fcf1..f69bff7 100644 (file)
@@ -39,12 +39,12 @@ uint64_t getElementValueOneHotSATTranslator(CSolver *This, ElementEncoding *elem
        uint index = 0;
        bool overflow = true;
        for (uint i = 0; i < elemEnc->numVars; i++) {
-               if (getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] ))){
+               if (getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] ))) {
                        index = i;
                        overflow = false;
                }
        }
-       if(overflow)
+       if (overflow)
                model_print("WARNING: Element has undefined value!\n");
        ASSERT(elemEnc->encArraySize > index && elemEnc->isinUseElement(index));
        return elemEnc->encodingArray[index];
index 4a35fcd..3b5f8cc 100644 (file)
@@ -18,14 +18,14 @@ void AutoTuner::addProblem(CSolver *solver) {
 long long AutoTuner::evaluate(CSolver *problem, SearchTuner *tuner) {
        CSolver *copy = problem->clone();
        copy->setTuner(tuner);
-        model_print("**********************\n");
+       model_print("**********************\n");
        int sat = copy->solve();
-        if(result == UNSETVALUE)
-                result = sat;
-        else if(result != sat){
-                model_print("&&&&&&&&&&&&&&&&&& Result has changed &&&&&&&&&&&&&\n");
-                copy->printConstraints();
-        }
+       if (result == UNSETVALUE)
+               result = sat;
+       else if (result != sat) {
+               model_print("&&&&&&&&&&&&&&&&&& Result has changed &&&&&&&&&&&&&\n");
+               copy->printConstraints();
+       }
        //model_print("SAT %d\n", result);
        long long elapsedTime = copy->getElapsedTime();
 //     long long encodeTime = copy->getEncodeTime();
index 0346e42..fecba88 100644 (file)
@@ -16,6 +16,6 @@ private:
 
        Vector<CSolver *> solvers;
        uint budget;
-        int result;
+       int result;
 };
 #endif
index a57a601..6a74926 100644 (file)
@@ -15,29 +15,29 @@ int DefaultTuner::getVarTunable(VarType vartype1, VarType vartype2, TunableParam
        return descriptor->defaultValue;
 }
 
-const char* tunableParameterToString(Tunables tunable){
-        switch(tunable){
-                case DECOMPOSEORDER:
-                        return "DECOMPOSEORDER";
-                case MUSTREACHGLOBAL:
-                        return "MUSTREACHGLOBAL";
-                case MUSTREACHLOCAL:
-                        return "MUSTREACHLOCAL";
-                case MUSTREACHPRUNE:
-                        return "MUSTREACHPRUNE";
-                case OPTIMIZEORDERSTRUCTURE:
-                        return "OPTIMIZEORDERSTRUCTURE";
-                case ORDERINTEGERENCODING:
-                        return "ORDERINTEGERENCODING";
-                case PREPROCESS:
-                        return "PREPROCESS";
-                case NODEENCODING:
-                        return "NODEENCODING";
-                case EDGEENCODING:
-                        return "EDGEENCODING";
-                case MUSTEDGEPRUNE:
-                        return "MUSTEDGEPRUNE";
-                default:
-                        ASSERT(0);
-        }
+const char *tunableParameterToString(Tunables tunable) {
+       switch (tunable) {
+       case DECOMPOSEORDER:
+               return "DECOMPOSEORDER";
+       case MUSTREACHGLOBAL:
+               return "MUSTREACHGLOBAL";
+       case MUSTREACHLOCAL:
+               return "MUSTREACHLOCAL";
+       case MUSTREACHPRUNE:
+               return "MUSTREACHPRUNE";
+       case OPTIMIZEORDERSTRUCTURE:
+               return "OPTIMIZEORDERSTRUCTURE";
+       case ORDERINTEGERENCODING:
+               return "ORDERINTEGERENCODING";
+       case PREPROCESS:
+               return "PREPROCESS";
+       case NODEENCODING:
+               return "NODEENCODING";
+       case EDGEENCODING:
+               return "EDGEENCODING";
+       case MUSTEDGEPRUNE:
+               return "MUSTEDGEPRUNE";
+       default:
+               ASSERT(0);
+       }
 }
\ No newline at end of file
index 2d18a2d..9fd614a 100644 (file)
@@ -43,5 +43,5 @@ static TunableDesc proxyparameter(1, 5, 2);
 enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING, MUSTEDGEPRUNE, ELEMENTOPT, ELEMENTOPTSETS, PROXYVARIABLE};
 typedef enum Tunables Tunables;
 
-const chartunableParameterToString(Tunables tunable);
+const char *tunableParameterToString(Tunables tunable);
 #endif
index 1c45480..f9ebdbb 100644 (file)
 #include "csolver.h"
 #include "ccsolver.h"
 
-#define CCSOLVER(solver) ((CSolver*)solver)
+#define CCSOLVER(solver) ((CSolver *)solver)
 
-void* createCCSolver(){
-       return (void*) new CSolver();
+void *createCCSolver() {
+       return (void *) new CSolver();
 }
-void deleteCCSolver(void* solver){
+void deleteCCSolver(void *solver) {
        delete CCSOLVER(solver);
 }
 
-void *createSet(void* solver,unsigned int type, long *elements, unsigned int num){
+void *createSet(void *solver,unsigned int type, long *elements, unsigned int num) {
        return CCSOLVER(solver)->createSet((VarType) type, (uint64_t *)elements, (uint) num);
 }
 
-void *createRangeSet(void* solver,unsigned int type, long lowrange, long highrange){
+void *createRangeSet(void *solver,unsigned int type, long lowrange, long highrange) {
        return CCSOLVER(solver)->createRangeSet((VarType) type, (uint64_t) lowrange, (uint64_t) highrange);
 }
 
-void *createRangeVar(void* solver,unsigned int type, long lowrange, long highrange){
+void *createRangeVar(void *solver,unsigned int type, long lowrange, long highrange) {
        return CCSOLVER(solver)->createRangeVar((VarType) type, (uint64_t) lowrange, (uint64_t) highrange);
 }
 
-void *createMutableSet(void* solver,unsigned int type){
+void *createMutableSet(void *solver,unsigned int type) {
        return CCSOLVER(solver)->createMutableSet((VarType) type);
 }
 
-void addItem(void* solver,void *set, long element){
-       CCSOLVER(solver)->addItem((MutableSet*) set, (uint64_t) element);
+void addItem(void *solver,void *set, long element) {
+       CCSOLVER(solver)->addItem((MutableSet *) set, (uint64_t) element);
 }
 
-void finalizeMutableSet(void* solver,void *set){
-       CCSOLVER(solver)->finalizeMutableSet((MutableSet*) set);
+void finalizeMutableSet(void *solver,void *set) {
+       CCSOLVER(solver)->finalizeMutableSet((MutableSet *) set);
 }
 
-void *getElementVar(void* solver,void *set){
-       return CCSOLVER(solver)->getElementVar((Set*) set);
+void *getElementVar(void *solver,void *set) {
+       return CCSOLVER(solver)->getElementVar((Set *) set);
 }
 
-void *getElementConst(void* solver,unsigned int type, long value){
+void *getElementConst(void *solver,unsigned int type, long value) {
        return CCSOLVER(solver)->getElementConst((VarType) type, (uint64_t) value);
 }
 
-void *getElementRange (void* solver,void *element){
-       return CCSOLVER(solver)->getElementRange ((Element*) element);
+void *getElementRange (void *solver,void *element) {
+       return CCSOLVER(solver)->getElementRange ((Element *) element);
 }
 
-void* getBooleanVar(void* solver,unsigned int type){
+void *getBooleanVar(void *solver,unsigned int type) {
        return CCSOLVER(solver)->getBooleanVar((VarType) type).getRaw();
 }
 
-void *createFunctionOperator(void* solver,unsigned int op, void *range,unsigned int overflowbehavior){
+void *createFunctionOperator(void *solver,unsigned int op, void *range,unsigned int overflowbehavior) {
        return CCSOLVER(solver)->createFunctionOperator((ArithOp) op, (Set *)range, (OverFlowBehavior) overflowbehavior);
 }
 
-void *createPredicateOperator(voidsolver,unsigned int op) {
+void *createPredicateOperator(void *solver,unsigned int op) {
        return CCSOLVER(solver)->createPredicateOperator((CompOp) op);
 }
 
-void *createPredicateTable(void* solver,void *table, unsigned int behavior){
+void *createPredicateTable(void *solver,void *table, unsigned int behavior) {
        return CCSOLVER(solver)->createPredicateTable((Table *)table, (UndefinedBehavior) behavior);
 }
 
-void *createTable(void* solver, void *range){
+void *createTable(void *solver, void *range) {
        return CCSOLVER(solver)->createTable((Set *)range);
 }
 
-void *createTableForPredicate(voidsolver) {
+void *createTableForPredicate(void *solver) {
        return CCSOLVER(solver)->createTableForPredicate();
 }
 
-void addTableEntry(void* solver,void *table, void *inputs, unsigned int inputSize, long result){
+void addTableEntry(void *solver,void *table, void *inputs, unsigned int inputSize, long result) {
        CCSOLVER(solver)->addTableEntry((Table *)table, (uint64_t *)inputs, (uint) inputSize, (uint64_t) result);
 }
 
-void *completeTable(void* solver,void *table, unsigned int behavior){
+void *completeTable(void *solver,void *table, unsigned int behavior) {
        return CCSOLVER(solver)->completeTable((Table *) table, (UndefinedBehavior) behavior);
 }
 
-void *applyFunction(void* solver,void *function, void**array, unsigned int numArrays, void* overflowstatus){
-       return CCSOLVER(solver)->applyFunction((Function *)function, (Element **)array, (uint) numArrays, BooleanEdge ((Boolean*)overflowstatus));
+void *applyFunction(void *solver,void *function, void **array, unsigned int numArrays, void *overflowstatus) {
+       return CCSOLVER(solver)->applyFunction((Function *)function, (Element **)array, (uint) numArrays, BooleanEdge ((Boolean *)overflowstatus));
 }
 
-void* applyPredicateTable(void* solver,void *predicate, void **inputs, unsigned int numInputs, void* undefinedStatus){
-       return CCSOLVER(solver)->applyPredicateTable((Predicate *)predicate, (Element **)inputs, (uint) numInputs, BooleanEdge((Boolean*) undefinedStatus)).getRaw();
+void *applyPredicateTable(void *solver,void *predicate, void **inputs, unsigned int numInputs, void *undefinedStatus) {
+       return CCSOLVER(solver)->applyPredicateTable((Predicate *)predicate, (Element **)inputs, (uint) numInputs, BooleanEdge((Boolean *) undefinedStatus)).getRaw();
 }
 
-void* applyPredicate(void* solver,void *predicate, void **inputs, unsigned int numInputs){
+void *applyPredicate(void *solver,void *predicate, void **inputs, unsigned int numInputs) {
        return CCSOLVER(solver)->applyPredicate((Predicate *)predicate, (Element **)inputs, (uint) numInputs).getRaw();
 }
 
-void* applyLogicalOperation(void* solver,unsigned int op, void *array, unsigned int asize){
+void *applyLogicalOperation(void *solver,unsigned int op, void *array, unsigned int asize) {
        return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, (BooleanEdge *)array, (uint) asize).getRaw();
 }
 
-void* applyLogicalOperationTwo(void* solver,unsigned int op, void* arg1, void* arg2){
-       return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, BooleanEdge((Boolean*) arg1), BooleanEdge((Boolean*) arg2)).getRaw();
+void *applyLogicalOperationTwo(void *solver,unsigned int op, void *arg1, void *arg2) {
+       return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, BooleanEdge((Boolean *) arg1), BooleanEdge((Boolean *) arg2)).getRaw();
 }
 
-void* applyLogicalOperationOne(void* solver,unsigned int op, void* arg){
-       return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, BooleanEdge((Boolean*) arg)).getRaw();
+void *applyLogicalOperationOne(void *solver,unsigned int op, void *arg) {
+       return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, BooleanEdge((Boolean *) arg)).getRaw();
 }
 
-void addConstraint(void* solver,void* constraint){
-       CCSOLVER(solver)->addConstraint(BooleanEdge((Boolean*) constraint));
+void addConstraint(void *solver,void *constraint) {
+       CCSOLVER(solver)->addConstraint(BooleanEdge((Boolean *) constraint));
 }
 
-void *createOrder(void* solver,unsigned int type, void *set){
+void *createOrder(void *solver,unsigned int type, void *set) {
        return CCSOLVER(solver)->createOrder((OrderType) type, (Set *)set);
 }
 
-void* orderConstraint(void* solver,void *order, long first, long second){
+void *orderConstraint(void *solver,void *order, long first, long second) {
        return CCSOLVER(solver)->orderConstraint((Order *)order, (uint64_t) first, (uint64_t) second).getRaw();
 }
 
-int solve(void* solver){
+int solve(void *solver) {
        return CCSOLVER(solver)->solve();
 }
 
-long getElementValue(void* solver,void *element){
+long getElementValue(void *solver,void *element) {
        return (long) CCSOLVER(solver)->getElementValue((Element *)element);
 }
 
-int getBooleanValue(void* solver, void* boolean){
-       return CCSOLVER(solver)->getBooleanValue(BooleanEdge((Boolean*) boolean));
+int getBooleanValue(void *solver, void *boolean) {
+       return CCSOLVER(solver)->getBooleanValue(BooleanEdge((Boolean *) boolean));
 }
 
-int getOrderConstraintValue(void* solver,void *order, long first, long second){
+int getOrderConstraintValue(void *solver,void *order, long first, long second) {
        return CCSOLVER(solver)->getOrderConstraintValue((Order *)order, (uint64_t) first, (uint64_t) second);
 }
 
-void printConstraints(void* solver){
+void printConstraints(void *solver) {
        CCSOLVER(solver)->printConstraints();
 }
 
 
 
-void serialize(void* solver){
+void serialize(void *solver) {
        CCSOLVER(solver)->serialize();
 }
 
 
-void mustHaveValue(void *solver, void *element){
-       CCSOLVER(solver)->mustHaveValue( (Element*) element);
+void mustHaveValue(void *solver, void *element) {
+       CCSOLVER(solver)->mustHaveValue( (Element *) element);
 }
 
-void* clone(void * solver){
+void *clone(void *solver) {
        return CCSOLVER(solver)->clone();
 }
\ No newline at end of file
index a17bd1c..c88214e 100644 (file)
@@ -2,46 +2,46 @@
 #define __CCSOLVER_H
 
 
-typedef voidCCSolver;
+typedef void *CCSolver;
 #ifdef __cplusplus
 extern "C" {
 #endif
-voidcreateCCSolver();
-void deleteCCSolver(voidsolver);
-void *createSet(voidsolver,unsigned int type, long *elements, unsigned int num);
-void *createRangeSet(voidsolver,unsigned int type, long lowrange, long highrange);
-void *createRangeVar(voidsolver,unsigned int type, long lowrange, long highrange);
-void *createMutableSet(voidsolver,unsigned int type);
-void addItem(voidsolver,void *set, long element);
-void finalizeMutableSet(voidsolver,void *set);
-void *getElementVar(voidsolver,void *set);
-void *getElementConst(voidsolver,unsigned int type, long value);
-void *getElementRange (voidsolver,void *element);
-void* getBooleanVar(void* solver,unsigned int type);
-void *createFunctionOperator(voidsolver,unsigned int op, void *range,unsigned int overflowbehavior);
-void *createPredicateOperator(voidsolver,unsigned int op);
-void *createPredicateTable(voidsolver,void *table, unsigned int behavior);
-void *createTable(voidsolver, void *range);
-void *createTableForPredicate(voidsolver);
-void addTableEntry(voidsolver,void *table, void *inputs, unsigned int inputSize, long result);
-void *completeTable(voidsolver,void *table, unsigned int behavior);
-void *applyFunction(void* solver,void *function, void**array, unsigned int numArrays, void* overflowstatus);
-void* applyPredicateTable(void* solver,void *predicate, void **inputs, unsigned int numInputs, void* undefinedStatus);
-void* applyPredicate(void* solver,void *predicate, void **inputs, unsigned int numInputs);
-void* applyLogicalOperation(void* solver,unsigned int op, void *array, unsigned int asize);
-void* applyLogicalOperationTwo(void* solver,unsigned int op, void* arg1, void* arg2);
-void* applyLogicalOperationOne(void* solver,unsigned int op, void* arg);
-void addConstraint(void* solver,void* constraint);
-void *createOrder(voidsolver,unsigned int type, void *set);
-void* orderConstraint(void* solver,void *order, long first, long second);
-int solve(voidsolver);
-long getElementValue(voidsolver,void *element);
-int getBooleanValue(void* solver,void* boolean);
-int getOrderConstraintValue(voidsolver,void *order, long first, long second);
-void printConstraints(voidsolver);
-void serialize(voidsolver);
+void *createCCSolver();
+void deleteCCSolver(void *solver);
+void *createSet(void *solver,unsigned int type, long *elements, unsigned int num);
+void *createRangeSet(void *solver,unsigned int type, long lowrange, long highrange);
+void *createRangeVar(void *solver,unsigned int type, long lowrange, long highrange);
+void *createMutableSet(void *solver,unsigned int type);
+void addItem(void *solver,void *set, long element);
+void finalizeMutableSet(void *solver,void *set);
+void *getElementVar(void *solver,void *set);
+void *getElementConst(void *solver,unsigned int type, long value);
+void *getElementRange (void *solver,void *element);
+void *getBooleanVar(void *solver,unsigned int type);
+void *createFunctionOperator(void *solver,unsigned int op, void *range,unsigned int overflowbehavior);
+void *createPredicateOperator(void *solver,unsigned int op);
+void *createPredicateTable(void *solver,void *table, unsigned int behavior);
+void *createTable(void *solver, void *range);
+void *createTableForPredicate(void *solver);
+void addTableEntry(void *solver,void *table, void *inputs, unsigned int inputSize, long result);
+void *completeTable(void *solver,void *table, unsigned int behavior);
+void *applyFunction(void *solver,void *function, void **array, unsigned int numArrays, void *overflowstatus);
+void *applyPredicateTable(void *solver,void *predicate, void **inputs, unsigned int numInputs, void *undefinedStatus);
+void *applyPredicate(void *solver,void *predicate, void **inputs, unsigned int numInputs);
+void *applyLogicalOperation(void *solver,unsigned int op, void *array, unsigned int asize);
+void *applyLogicalOperationTwo(void *solver,unsigned int op, void *arg1, void *arg2);
+void *applyLogicalOperationOne(void *solver,unsigned int op, void *arg);
+void addConstraint(void *solver,void *constraint);
+void *createOrder(void *solver,unsigned int type, void *set);
+void *orderConstraint(void *solver,void *order, long first, long second);
+int solve(void *solver);
+long getElementValue(void *solver,void *element);
+int getBooleanValue(void *solver,void *boolean);
+int getOrderConstraintValue(void *solver,void *order, long first, long second);
+void printConstraints(void *solver);
+void serialize(void *solver);
 void mustHaveValue(void *solver, void *element);
-void* clone(void * solver);
+void *clone(void *solver);
 #ifdef __cplusplus
 }
 #endif
index 3a0eeaa..48b2a7e 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 44b29bb..07a6168 100644 (file)
@@ -184,8 +184,8 @@ Set *CSolver::createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange
        return set;
 }
 
-bool CSolver::itemExistInSet(Set *set, uint64_t item){
-        return set->exists(item);
+bool CSolver::itemExistInSet(Set *set, uint64_t item) {
+       return set->exists(item);
 }
 
 VarType CSolver::getSetVarType(Set *set) {
@@ -223,7 +223,7 @@ Element *CSolver::getElementVar(Set *set) {
        return element;
 }
 
-void CSolver::mustHaveValue(Element *element){
+void CSolver::mustHaveValue(Element *element) {
        element->getElementEncoding()->anyValue = true;
 }
 
index c916c58..19ba3e1 100644 (file)
@@ -18,17 +18,17 @@ public:
        /** This function creates a set from lowrange to highrange (inclusive). */
 
        Set *createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange);
-        
-        bool itemExistInSet(Set *set, uint64_t item);
+
+       bool itemExistInSet(Set *set, uint64_t item);
 
        VarType getSetVarType(Set *set);
 
        Element *createRangeVar(VarType type, uint64_t lowrange, uint64_t highrange);
 
        /** This function creates a mutable set.
-         * Note: You should use addItem for adding new item to Mutable sets, and
-         * at the end, you should call finalizeMutableSet!
-         */
+        * Note: You should use addItem for adding new item to Mutable sets, and
+        * at the end, you should call finalizeMutableSet!
+        */
 
        MutableSet *createMutableSet(VarType type);
 
@@ -58,7 +58,7 @@ public:
        Set *getElementRange (Element *element);
 
        void mustHaveValue(Element *element);
-        
+
        BooleanEdge getBooleanTrue();
 
        BooleanEdge getBooleanFalse();
@@ -176,8 +176,8 @@ public:
 private:
        void handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child);
        void handleANDTrue(BooleanLogic *bexpr, BooleanEdge child);
-       void handleFunction(ElementFunction * ef, BooleanEdge child);
-       
+       void handleFunction(ElementFunction *ef, BooleanEdge child);
+
        //These two functions are helpers if the client has a pointer to a
        //Boolean object that we have since replaced
        BooleanEdge rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uint asize);
index b78eb54..9708936 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 */