Fix tabbing
authorbdemsky <bdemsky@uci.edu>
Wed, 18 Oct 2017 23:54:43 +0000 (16:54 -0700)
committerbdemsky <bdemsky@uci.edu>
Wed, 18 Oct 2017 23:54:43 +0000 (16:54 -0700)
56 files changed:
src/AST/astops.h
src/AST/boolean.cc
src/AST/boolean.h
src/AST/element.cc
src/AST/element.h
src/AST/function.cc
src/AST/function.h
src/AST/iterator.cc
src/AST/iterator.h
src/AST/mutableset.cc
src/AST/order.cc
src/AST/order.h
src/AST/predicate.cc
src/AST/predicate.h
src/AST/rewriter.cc
src/AST/set.cc
src/AST/set.h
src/AST/table.cc
src/AST/table.h
src/ASTAnalyses/Encoding/encodinggraph.cc
src/ASTAnalyses/Encoding/encodinggraph.h
src/ASTAnalyses/Encoding/subgraph.cc
src/ASTAnalyses/Encoding/subgraph.h
src/ASTAnalyses/Order/orderanalysis.cc
src/ASTAnalyses/Order/ordergraph.cc
src/ASTAnalyses/Order/ordergraph.h
src/ASTAnalyses/Polarity/polarityassignment.cc
src/ASTTransform/decomposeordertransform.cc
src/ASTTransform/integerencoding.cc
src/ASTTransform/preprocess.cc
src/ASTTransform/preprocess.h
src/Backend/orderpair.cc
src/Backend/orderpair.h
src/Backend/satencoder.cc
src/Backend/satorderencoder.cc
src/Collections/corestructs.h
src/Collections/qsort.cc
src/Collections/vector.h
src/Encoders/naiveencoder.cc
src/Encoders/orderencoding.cc
src/Serialize/deserializer.cc
src/Serialize/deserializer.h
src/Serialize/serializer.cc
src/Serialize/serializer.h
src/Test/bug1.cc
src/Test/bug_minimal.cc
src/Test/ordertest.cc
src/Translator/decomposeorderresolver.cc
src/Translator/decomposeorderresolver.h
src/Translator/orderpairresolver.cc
src/Translator/orderpairresolver.h
src/Tuner/searchtuner.cc
src/common.h
src/csolver.cc
src/csolver.h
src/mymemory.h

index ebe9fc0..d4e185d 100644 (file)
@@ -8,7 +8,7 @@ enum PredicateType {TABLEPRED, OPERATORPRED};
 typedef enum PredicateType PredicateType;
 
 enum ASTNodeType {ORDERCONST, BOOLEANVAR, LOGICOP, PREDICATEOP, BOOLCONST, ELEMSET, ELEMFUNCRETURN, ELEMCONST,
-       BOOLEANEDGE, ORDERTYPE, SETTYPE, PREDTABLETYPE, PREDOPERTYPE, TABLETYPE, FUNCTABLETYPE, FUNCOPTYPE};
+                                                                       BOOLEANEDGE, ORDERTYPE, SETTYPE, PREDTABLETYPE, PREDOPERTYPE, TABLETYPE, FUNCTABLETYPE, FUNCOPTYPE};
 typedef enum ASTNodeType ASTNodeType;
 
 enum Polarity {P_UNDEFINED=0, P_TRUE=1, P_FALSE=2, P_BOTHTRUEFALSE=3};
index fff3658..f7d3e88 100644 (file)
@@ -47,9 +47,9 @@ BooleanLogic::BooleanLogic(CSolver *solver, LogicOp _op, BooleanEdge *array, uin
 }
 
 BooleanEdge cloneEdge(CSolver *solver, CloneMap *map, BooleanEdge e) {
-       bool isnegated=e.isNegated();
-       Boolean *b=e->clone(solver, map);
-       BooleanEdge be=BooleanEdge(b);
+       bool isnegated = e.isNegated();
+       Boolean *b = e->clone(solver, map);
+       BooleanEdge be = BooleanEdge(b);
        return isnegated ? be.negate() : be;
 }
 
@@ -62,7 +62,7 @@ Boolean *BooleanVar::clone(CSolver *solver, CloneMap *map) {
        if (b != NULL)
                return b;
        BooleanEdge bvar = solver->getBooleanVar(type);
-       Boolean * base=bvar.getRaw();
+       Boolean *base = bvar.getRaw();
        map->put(this, base);
        return base;
 }
@@ -92,117 +92,117 @@ Boolean *BooleanPredicate::clone(CSolver *solver, CloneMap *map) {
 }
 
 void BooleanPredicate::updateParents() {
-       for(uint i=0;i < inputs.getSize(); i++) inputs.get(i)->parents.push(this);
+       for (uint i = 0; i < inputs.getSize(); i++) inputs.get(i)->parents.push(this);
 }
 
 void BooleanLogic::updateParents() {
-       for(uint i=0;i < inputs.getSize(); i++) inputs.get(i)->parents.push(this);
+       for (uint i = 0; i < inputs.getSize(); i++) inputs.get(i)->parents.push(this);
 }
 
-void BooleanVar::serialize(Serializer* serializer){
-       if(serializer->isSerialized(this))
+void BooleanVar::serialize(Serializer *serializer) {
+       if (serializer->isSerialized(this))
                return;
        serializer->addObject(this);
        serializer->mywrite(&type, sizeof(ASTNodeType));
-       BooleanVarThis = this;
-       serializer->mywrite(&This, sizeof(BooleanVar*));
+       BooleanVar *This = this;
+       serializer->mywrite(&This, sizeof(BooleanVar *));
        serializer->mywrite(&vtype, sizeof(VarType));
 }
 
-void BooleanVar::print(){
+void BooleanVar::print() {
        model_print("BooleanVar:%lu\n", (uintptr_t)this);
 }
 
-void BooleanConst::print(){
-       model_print("BooleanConst:%s\n", istrue?"TRUE" :"FALSE");
+void BooleanConst::print() {
+       model_print("BooleanConst:%s\n", istrue ? "TRUE" : "FALSE");
 }
 
-void BooleanOrder::serialize(Serializer* serializer){
-       if(serializer->isSerialized(this))
+void BooleanOrder::serialize(Serializer *serializer) {
+       if (serializer->isSerialized(this))
                return;
        serializer->addObject(this);
        order->serialize(serializer);
-       
+
        serializer->mywrite(&type, sizeof(ASTNodeType));
-       BooleanOrderThis = this;
-       serializer->mywrite(&This, sizeof(BooleanOrder*));
-       serializer->mywrite(&order, sizeof(Order*));
+       BooleanOrder *This = this;
+       serializer->mywrite(&This, sizeof(BooleanOrder *));
+       serializer->mywrite(&order, sizeof(Order *));
        serializer->mywrite(&first, sizeof(uint64_t));
        serializer->mywrite(&second, sizeof(uint64_t));
 }
 
-void BooleanOrder::print(){
+void BooleanOrder::print() {
        model_print("{BooleanOrder: First= %lu, Second = %lu on Order:\n", first, second);
        order->print();
        model_print("}\n");
 }
 
-void BooleanPredicate::serialize(Serializer* serializer){
-       if(serializer->isSerialized(this))
+void BooleanPredicate::serialize(Serializer *serializer) {
+       if (serializer->isSerialized(this))
                return;
        serializer->addObject(this);
-       
+
        predicate->serialize(serializer);
        uint size = inputs.getSize();
-       for(uint i=0; i<size; i++){
-               Elementinput = inputs.get(i);
+       for (uint i = 0; i < size; i++) {
+               Element *input = inputs.get(i);
                input->serialize(serializer);
        }
        serializeBooleanEdge(serializer, undefStatus);
-       
+
        serializer->mywrite(&type, sizeof(ASTNodeType));
-       BooleanPredicateThis = this;
-       serializer->mywrite(&This, sizeof(BooleanPredicate*));
+       BooleanPredicate *This = this;
+       serializer->mywrite(&This, sizeof(BooleanPredicate *));
        serializer->mywrite(&predicate, sizeof(Predicate *));
        serializer->mywrite(&size, sizeof(uint));
-       for(uint i=0; i<size; i++){
+       for (uint i = 0; i < size; i++) {
                Element *input = inputs.get(i);
                serializer->mywrite(&input, sizeof(Element *));
        }
-       Boolean* undefStat = undefStatus!= BooleanEdge(NULL)?undefStatus.getRaw() : NULL;
-       serializer->mywrite(&undefStat, sizeof(Boolean*));
+       Boolean *undefStat = undefStatus != BooleanEdge(NULL) ? undefStatus.getRaw() : NULL;
+       serializer->mywrite(&undefStat, sizeof(Boolean *));
 }
 
-void BooleanPredicate::print(){
+void BooleanPredicate::print() {
        model_print("{BooleanPredicate:\n");
        predicate->print();
        model_print("elements:\n");
        uint size = inputs.getSize();
-       for(uint i=0; i<size; i++){
+       for (uint i = 0; i < size; i++) {
                Element *input = inputs.get(i);
                input->print();
        }
        model_print("}\n");
 }
 
-void BooleanLogic::serialize(Serializer* serializer){
-       if(serializer->isSerialized(this))
+void BooleanLogic::serialize(Serializer *serializer) {
+       if (serializer->isSerialized(this))
                return;
        serializer->addObject(this);
        uint size = inputs.getSize();
-       for(uint i=0; i<size; i++){
+       for (uint i = 0; i < size; i++) {
                BooleanEdge input = inputs.get(i);
                serializeBooleanEdge(serializer, input);
        }
        serializer->mywrite(&type, sizeof(ASTNodeType));
-       BooleanLogicThis = this;
-       serializer->mywrite(&This, sizeof(BooleanLogic*));
+       BooleanLogic *This = this;
+       serializer->mywrite(&This, sizeof(BooleanLogic *));
        serializer->mywrite(&op, sizeof(LogicOp));
        serializer->mywrite(&size, sizeof(uint));
-       for(uint i=0; i<size; i++){
-               Booleaninput = inputs.get(i).getRaw();
-               serializer->mywrite(&input, sizeof(Boolean*));
+       for (uint i = 0; i < size; i++) {
+               Boolean *input = inputs.get(i).getRaw();
+               serializer->mywrite(&input, sizeof(Boolean *));
        }
 }
 
-void BooleanLogic::print(){
-       model_print("{BooleanLogic: %s\n", 
-                                                       op ==SATC_AND? "AND": op == SATC_OR? "OR": op==SATC_NOT? "NOT":
-                                                       op == SATC_XOR? "XOR" : op==SATC_IFF? "IFF" : "IMPLIES");
+void BooleanLogic::print() {
+       model_print("{BooleanLogic: %s\n",
+                                                       op == SATC_AND ? "AND" : op == SATC_OR ? "OR" : op == SATC_NOT ? "NOT" :
+                                                       op == SATC_XOR ? "XOR" : op == SATC_IFF ? "IFF" : "IMPLIES");
        uint size = inputs.getSize();
-       for(uint i=0; i<size; i++){
+       for (uint i = 0; i < size; i++) {
                BooleanEdge input = inputs.get(i);
-               if(input.isNegated())
+               if (input.isNegated())
                        model_print("!");
                input.getBoolean()->print();
        }
index 3674d9f..9864d9b 100644 (file)
@@ -15,15 +15,15 @@ public:
        Boolean(ASTNodeType _type);
        virtual ~Boolean() {}
        virtual Boolean *clone(CSolver *solver, CloneMap *map) = 0;
-       virtual void serialize(Serializer* ) = 0;
-        virtual void print() =0;
+       virtual void serialize(Serializer * ) = 0;
+       virtual void print() = 0;
        virtual bool isTrue() {return boolVal == BV_MUSTBETRUE;}
        virtual bool isFalse() {return boolVal == BV_MUSTBEFALSE;}
        Polarity polarity;
        BooleanValue boolVal;
        Vector<Boolean *> parents;
        virtual void updateParents() {}
-       
+
        CMEMALLOC;
 };
 
@@ -33,8 +33,8 @@ public:
        Boolean *clone(CSolver *solver, CloneMap *map);
        bool isTrue() {return istrue;}
        bool isFalse() {return !istrue;}
-       void serialize(Serializer *serializer ){};
-        virtual void print();
+       void serialize(Serializer *serializer ) {};
+       virtual void print();
        bool istrue;
        CMEMALLOC;
 };
@@ -44,7 +44,7 @@ public:
        BooleanVar(VarType t);
        Boolean *clone(CSolver *solver, CloneMap *map);
        void serialize(Serializer *serializer );
-        virtual void print();
+       virtual void print();
        VarType vtype;
        Edge var;
        CMEMALLOC;
@@ -55,7 +55,7 @@ public:
        BooleanOrder(Order *_order, uint64_t _first, uint64_t _second);
        Boolean *clone(CSolver *solver, CloneMap *map);
        void serialize(Serializer *serializer );
-        virtual void print();
+       virtual void print();
 
        Order *order;
        uint64_t first;
@@ -71,7 +71,7 @@ public:
        FunctionEncoding *getFunctionEncoding() {return &encoding;}
        void updateParents();
        void serialize(Serializer *serializer );
-        virtual void print();
+       virtual void print();
        CMEMALLOC;
 
        Predicate *predicate;
@@ -85,12 +85,12 @@ public:
        BooleanLogic(CSolver *solver, LogicOp _op, BooleanEdge *array, uint asize);
        Boolean *clone(CSolver *solver, CloneMap *map);
        void serialize(Serializer *serializer );
-        virtual void print();
+       virtual void print();
        LogicOp op;
        bool replaced;
        Array<BooleanEdge> inputs;
        void updateParents();
-       
+
        CMEMALLOC;
 };
 BooleanEdge cloneEdge(CSolver *solver, CloneMap *map, BooleanEdge e);
index 205d31f..87c0ef8 100644 (file)
@@ -57,83 +57,83 @@ Element *ElementFunction::clone(CSolver *solver, CloneMap *map) {
 }
 
 void ElementFunction::updateParents() {
-       for(uint i=0;i < inputs.getSize(); i++) inputs.get(i)->parents.push(this);
+       for (uint i = 0; i < inputs.getSize(); i++) inputs.get(i)->parents.push(this);
 }
 
-Set * ElementFunction::getRange() {
+Set *ElementFunction::getRange() {
        return function->getRange();
 }
 
-void ElementSet::serialize(Serializer* serializer){
-       if(serializer->isSerialized(this))
+void ElementSet::serialize(Serializer *serializer) {
+       if (serializer->isSerialized(this))
                return;
        serializer->addObject(this);
-       
+
        set->serialize(serializer);
-       
+
        serializer->mywrite(&type, sizeof(ASTNodeType));
        ElementSet *This = this;
-       serializer->mywrite(&This, sizeof(ElementSet*));
-       serializer->mywrite(&set, sizeof(Set*));
+       serializer->mywrite(&This, sizeof(ElementSet *));
+       serializer->mywrite(&set, sizeof(Set *));
 }
 
-void ElementSet::print(){
+void ElementSet::print() {
        model_print("{ElementSet:\n");
        set->print();
        model_print("}\n");
 }
 
-void ElementConst::serialize(Serializer* serializer){
-       if(serializer->isSerialized(this))
+void ElementConst::serialize(Serializer *serializer) {
+       if (serializer->isSerialized(this))
                return;
        serializer->addObject(this);
-       
+
        set->serialize(serializer);
-       
+
        serializer->mywrite(&type, sizeof(ASTNodeType));
        ElementSet *This = this;
-       serializer->mywrite(&This, sizeof(ElementSet*));
+       serializer->mywrite(&This, sizeof(ElementSet *));
        VarType type = set->getType();
        serializer->mywrite(&type, sizeof(VarType));
        serializer->mywrite(&value, sizeof(uint64_t));
 }
 
-void ElementConst::print(){
-       model_print("{ElementConst: %lu}\n", value);    
+void ElementConst::print() {
+       model_print("{ElementConst: %lu}\n", value);
 }
 
-void ElementFunction::serialize(Serializer* serializer){
-       if(serializer->isSerialized(this))
+void ElementFunction::serialize(Serializer *serializer) {
+       if (serializer->isSerialized(this))
                return;
        serializer->addObject(this);
 
        function->serialize(serializer);
        uint size = inputs.getSize();
-       for(uint i=0; i<size; i++){
+       for (uint i = 0; i < size; i++) {
                Element *input = inputs.get(i);
                input->serialize(serializer);
        }
        serializeBooleanEdge(serializer, overflowstatus);
-       
+
        serializer->mywrite(&type, sizeof(ASTNodeType));
        ElementFunction *This = this;
        serializer->mywrite(&This, sizeof(ElementFunction *));
        serializer->mywrite(&function, sizeof(Function *));
        serializer->mywrite(&size, sizeof(uint));
-       for(uint i=0; i<size; i++){
-               Elementinput = inputs.get(i);
-               serializer->mywrite(&input, sizeof(Element*));
+       for (uint i = 0; i < size; i++) {
+               Element *input = inputs.get(i);
+               serializer->mywrite(&input, sizeof(Element *));
        }
-       Booleanoverflowstat = overflowstatus.getRaw();
-       serializer->mywrite(&overflowstat, sizeof(Boolean*));
+       Boolean *overflowstat = overflowstatus.getRaw();
+       serializer->mywrite(&overflowstat, sizeof(Boolean *));
 }
 
-void ElementFunction::print(){
+void ElementFunction::print() {
        model_print("{ElementFunction:\n");
        function->print();
        model_print("Elements:\n");
        uint size = inputs.getSize();
-       for(uint i=0; i<size; i++){
+       for (uint i = 0; i < size; i++) {
                Element *input = inputs.get(i);
                input->print();
        }
index c643603..b74e582 100644 (file)
@@ -14,12 +14,12 @@ public:
        virtual ~Element() {}
        Vector<ASTNode *> parents;
        ElementEncoding encoding;
-       inline ElementEncoding *getElementEncoding(){ return &encoding; }
+       inline ElementEncoding *getElementEncoding() { return &encoding; }
        virtual Element *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;};
-       virtual void serialize(Serializer* serializer) =0;
-        virtual void print() = 0;
+       virtual void serialize(Serializer *serializer) = 0;
+       virtual void print() = 0;
        virtual void updateParents() {}
-       virtual Set * getRange() = 0;
+       virtual Set *getRange() = 0;
        CMEMALLOC;
 };
 
@@ -28,11 +28,11 @@ public:
        ElementSet(ASTNodeType type, Set *s);
        ElementSet(Set *s);
        virtual Element *clone(CSolver *solver, CloneMap *map);
-       virtual void serialize(Serializerserializer);
-        virtual void print();
+       virtual void serialize(Serializer *serializer);
+       virtual void print();
        CMEMALLOC;
        Set *getRange() {return set;}
- protected:
+protected:
        Set *set;
 
 };
@@ -41,8 +41,8 @@ class ElementConst : public ElementSet {
 public:
        ElementConst(uint64_t value, Set *_set);
        uint64_t value;
-       virtual void serialize(Serializerserializer);
-        virtual void print();
+       virtual void serialize(Serializer *serializer);
+       virtual void print();
        Element *clone(CSolver *solver, CloneMap *map);
        CMEMALLOC;
 };
@@ -54,14 +54,14 @@ public:
        BooleanEdge overflowstatus;
        FunctionEncoding functionencoding;
        Element *clone(CSolver *solver, CloneMap *map);
-       virtual void serialize(Serializerserializer);
-        virtual void print();
-       Set * getRange();
+       virtual void serialize(Serializer *serializer);
+       virtual void print();
+       Set *getRange();
        void updateParents();
-       Function * getFunction() {return function;}
+       Function *getFunction() {return function;}
        inline FunctionEncoding *getElementFunctionEncoding() {return &functionencoding;}
        CMEMALLOC;
- private:
+private:
        Function *function;
 };
 
index f17fb62..c385512 100644 (file)
@@ -62,51 +62,51 @@ Function *FunctionTable::clone(CSolver *solver, CloneMap *map) {
        return f;
 }
 
-Set * FunctionTable::getRange() {
+Set *FunctionTable::getRange() {
        return table->getRange();
 }
 
-void FunctionTable::serialize(Serializer* serializer){
-       if(serializer->isSerialized(this))
+void FunctionTable::serialize(Serializer *serializer) {
+       if (serializer->isSerialized(this))
                return;
        serializer->addObject(this);
-       
+
        table->serialize(serializer);
-       
-       ASTNodeType type = FUNCTABLETYPE;       
+
+       ASTNodeType type = FUNCTABLETYPE;
        serializer->mywrite(&type, sizeof(ASTNodeType));
-       FunctionTableThis = this;
-       serializer->mywrite(&This, sizeof(FunctionTable*));
+       FunctionTable *This = this;
+       serializer->mywrite(&This, sizeof(FunctionTable *));
        serializer->mywrite(&table, sizeof(Table *));
        serializer->mywrite(&undefBehavior, sizeof(UndefinedBehavior));
-       
+
 }
 
-void FunctionTable::print(){
+void FunctionTable::print() {
        model_print("{FunctionTable:\n");
        table->print();
        model_print("}\n");
 }
 
-void FunctionOperator::serialize(Serializer* serializer){
-       if(serializer->isSerialized(this))
+void FunctionOperator::serialize(Serializer *serializer) {
+       if (serializer->isSerialized(this))
                return;
        serializer->addObject(this);
-       
+
        uint size = domains.getSize();
-       for(uint i=0; i<size; i++){
-               Setdomain = domains.get(i);
+       for (uint i = 0; i < size; i++) {
+               Set *domain = domains.get(i);
                domain->serialize(serializer);
        }
        range->serialize(serializer);
-       
-       ASTNodeType nodeType = FUNCOPTYPE; 
+
+       ASTNodeType nodeType = FUNCOPTYPE;
        serializer->mywrite(&nodeType, sizeof(ASTNodeType));
-       FunctionOperatorThis = this;
-       serializer->mywrite(&This, sizeof(FunctionOperator*));
+       FunctionOperator *This = this;
+       serializer->mywrite(&This, sizeof(FunctionOperator *));
        serializer->mywrite(&op, sizeof(ArithOp));
        serializer->mywrite(&size, sizeof(uint));
-       for(uint i=0; i<size; i++){
+       for (uint i = 0; i < size; i++) {
                Set *domain = domains.get(i);
                serializer->mywrite(&domain, sizeof(Set *));
        }
@@ -115,5 +115,5 @@ void FunctionOperator::serialize(Serializer* serializer){
 }
 
 void FunctionOperator::print() {
-       model_print("{FunctionOperator: %s}\n", op == SATC_ADD? "ADD": "SUB" );
+       model_print("{FunctionOperator: %s}\n", op == SATC_ADD ? "ADD" : "SUB" );
 }
index b8d0c78..5cfbb7d 100644 (file)
@@ -12,9 +12,9 @@ public:
        FunctionType type;
        virtual ~Function() {}
        virtual Function *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;}
-       virtual void serialize(Serializer* serialiezr) =0;
-        virtual void print() = 0;
-       virtual Set * getRange() = 0;
+       virtual void serialize(Serializer *serialiezr) = 0;
+       virtual void print() = 0;
+       virtual Set *getRange() = 0;
        CMEMALLOC;
 };
 
@@ -28,9 +28,9 @@ public:
        uint64_t applyFunctionOperator(uint numVals, uint64_t *values);
        bool isInRangeFunction(uint64_t val);
        Function *clone(CSolver *solver, CloneMap *map);
-       virtual void serialize(Serializerserialiezr);
-        virtual void print();
-       Set * getRange() {return range;}
+       virtual void serialize(Serializer *serialiezr);
+       virtual void print();
+       Set *getRange() {return range;}
        CMEMALLOC;
 };
 
@@ -40,9 +40,9 @@ public:
        UndefinedBehavior undefBehavior;
        FunctionTable (Table *table, UndefinedBehavior behavior);
        Function *clone(CSolver *solver, CloneMap *map);
-       virtual void serialize(Serializerserialiezr);
-        virtual void print();
-       Set * getRange();
+       virtual void serialize(Serializer *serialiezr);
+       virtual void print();
+       Set *getRange();
        CMEMALLOC;
 };
 
index 2b0dea4..03b368f 100644 (file)
@@ -3,7 +3,7 @@
 #include "element.h"
 #include "csolver.h"
 
-BooleanIterator::BooleanIterator(CSolver * _solver) :
+BooleanIterator::BooleanIterator(CSolver *_solver) :
        solverit(_solver->getConstraints()) {
        updateNext();
 }
@@ -21,11 +21,11 @@ void BooleanIterator::updateNext() {
                boolean.pop();
                index.pop();
        }
-       
-       while(true) {
+
+       while (true) {
                if (boolean.getSize() == 0) {
                        if (solverit->hasNext()) {
-                               Boolean *b=solverit->next().getBoolean();
+                               Boolean *b = solverit->next().getBoolean();
                                if (discovered.add(b)) {
                                        boolean.push(b);
                                        index.push(0);
@@ -34,22 +34,22 @@ void BooleanIterator::updateNext() {
                        } else
                                return;
                }
-               Boolean *topboolean=boolean.last();
-               uint topindex=index.last();
-               switch(topboolean->type) {
+               Boolean *topboolean = boolean.last();
+               uint topindex = index.last();
+               switch (topboolean->type) {
                case ORDERCONST:
                case BOOLEANVAR:
                case PREDICATEOP:
                case BOOLCONST:
                        return;
                case LOGICOP: {
-                       BooleanLogic * logicop=(BooleanLogic*) topboolean;
-                       uint size=logicop->inputs.getSize();
+                       BooleanLogic *logicop = (BooleanLogic *) topboolean;
+                       uint size = logicop->inputs.getSize();
                        if (topindex == size)
                                return;
                        index.pop();
-                       index.push(topindex+1);
-                       Boolean *newchild=logicop->inputs.get(topindex).getBoolean();
+                       index.push(topindex + 1);
+                       Boolean *newchild = logicop->inputs.get(topindex).getBoolean();
                        if (discovered.add(newchild)) {
                                boolean.push(newchild);
                                index.push(0);
@@ -62,8 +62,8 @@ void BooleanIterator::updateNext() {
        }
 }
 
-Boolean * BooleanIterator::next() {
-       Boolean * b = boolean.last();
+Boolean *BooleanIterator::next() {
+       Boolean *b = boolean.last();
        updateNext();
        return b;
 }
@@ -87,15 +87,15 @@ void ElementIterator::updateNext() {
                element.pop();
                index.pop();
        }
-       
-       while(true) {
+
+       while (true) {
                if (element.getSize() == 0) {
                        if (base != NULL) {
                                if (baseindex == base->inputs.getSize()) {
                                        base = NULL;
                                        continue;
                                } else {
-                                       Element * e = base->inputs.get(baseindex);
+                                       Element *e = base->inputs.get(baseindex);
                                        baseindex++;
                                        if (discovered.add(e)) {
                                                element.push(e);
@@ -105,30 +105,30 @@ void ElementIterator::updateNext() {
                                }
                        } else {
                                if (bit.hasNext()) {
-                                       Boolean *b=bit.next();
+                                       Boolean *b = bit.next();
                                        if (b->type == PREDICATEOP) {
                                                base = (BooleanPredicate *)b;
-                                               baseindex=0;
+                                               baseindex = 0;
                                        }
                                        continue;
                                } else
                                        return;
                        }
                }
-               Element *topelement=element.last();
-               uint topindex=index.last();
-               switch(topelement->type) {
+               Element *topelement = element.last();
+               uint topindex = index.last();
+               switch (topelement->type) {
                case ELEMSET:
                case ELEMCONST:
                        return;
                case ELEMFUNCRETURN: {
-                       ElementFunction * func=(ElementFunction*) topelement;
-                       uint size=func->inputs.getSize();
+                       ElementFunction *func = (ElementFunction *) topelement;
+                       uint size = func->inputs.getSize();
                        if (topindex == size)
                                return;
                        index.pop();
-                       index.push(topindex+1);
-                       Element *newchild=func->inputs.get(topindex);
+                       index.push(topindex + 1);
+                       Element *newchild = func->inputs.get(topindex);
                        if (discovered.add(newchild)) {
                                element.push(newchild);
                                index.push(0);
@@ -141,8 +141,8 @@ void ElementIterator::updateNext() {
        }
 }
 
-Element * ElementIterator::next() {
-       Element * e = element.last();
+Element *ElementIterator::next() {
+       Element *e = element.last();
        updateNext();
        return e;
 }
index 0e7303f..5309934 100644 (file)
@@ -4,15 +4,15 @@
 #include "structs.h"
 
 class BooleanIterator {
- public:
-       BooleanIterator(CSolver * _solver);
+public:
+       BooleanIterator(CSolver *_solver);
        ~BooleanIterator();
        bool hasNext();
-       Boolean * next();
+       Boolean *next();
        CMEMALLOC;
 
- private:
-       SetIteratorBooleanEdge * solverit;
+private:
+       SetIteratorBooleanEdge *solverit;
        HashsetBoolean discovered;
        Vector<Boolean *> boolean;
        Vector<uint> index;
@@ -20,14 +20,14 @@ class BooleanIterator {
 };
 
 class ElementIterator {
- public:
+public:
        ElementIterator(CSolver *_solver);
        ~ElementIterator();
        bool hasNext();
-       Element * next();
+       Element *next();
        CMEMALLOC;
 
- private:
+private:
        BooleanIterator bit;
        BooleanPredicate *base;
        uint baseindex;
index 3d9db49..31ce431 100644 (file)
@@ -16,13 +16,13 @@ Set *MutableSet::clone(CSolver *solver, CloneMap *map) {
        s = solver->createMutableSet(type);
        for (uint i = 0; i < members->getSize(); i++) {
                ((MutableSet *)s)->addElementMSet(members->get(i));
-                               solver->addItem((MutableSet *) s, members->get(i));
+               solver->addItem((MutableSet *) s, members->get(i));
        }
-       ((MutableSet*)s)->finalize();
+       ((MutableSet *)s)->finalize();
        map->put(this, s);
        return s;
 }
 
-void MutableSet::finalize(){
+void MutableSet::finalize() {
        bsdqsort(members->expose(), members->getSize(), sizeof(uint64_t), intcompare);
 }
\ No newline at end of file
index a28d6c0..f3ccde4 100644 (file)
@@ -31,9 +31,9 @@ Order *Order::clone(CSolver *solver, CloneMap *map) {
        return o;
 }
 
-HashtableOrderPair* Order::getOrderPairTable(){
+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);
@@ -46,20 +46,20 @@ Order::~Order() {
        }
 }
 
-void Order::serialize(Serializer* serializer){
-       if(serializer->isSerialized(this))
+void Order::serialize(Serializer *serializer) {
+       if (serializer->isSerialized(this))
                return;
        serializer->addObject(this);
        set->serialize(serializer);
        ASTNodeType asttype = ORDERTYPE;
        serializer->mywrite(&asttype, sizeof(ASTNodeType));
-       OrderThis = this;
-       serializer->mywrite(&This, sizeof(Order*));
+       Order *This = this;
+       serializer->mywrite(&This, sizeof(Order *));
        serializer->mywrite(&type, sizeof(OrderType));
        serializer->mywrite(&set, sizeof(Set *));
 }
 
-void Order::print(){
+void Order::print() {
        model_print("{Order on Set:\n");
        set->print();
        model_print("}\n");
index e2e0b43..866b1ab 100644 (file)
@@ -8,7 +8,7 @@
 #include "boolean.h"
 #include "orderpair.h"
 
-class Order{
+class Order {
 public:
        Order(OrderType type, Set *set);
        virtual ~Order();
@@ -24,7 +24,7 @@ public:
        void initializeOrderElementsHashtable();
        void addOrderConstraint(BooleanOrder *constraint);
        void setOrderEncodingType(OrderEncodingType type);
-       HashtableOrderPairgetOrderPairTable();
+       HashtableOrderPair *getOrderPairTable();
        CMEMALLOC;
 };
 
index 1e0bb21..ac3b617 100644 (file)
@@ -51,52 +51,52 @@ Predicate *PredicateTable::clone(CSolver *solver, CloneMap *map) {
        return p;
 }
 
-void PredicateTable::serialize(Serializer* serializer){        
-       if(serializer->isSerialized(this))
+void PredicateTable::serialize(Serializer *serializer) {
+       if (serializer->isSerialized(this))
                return;
        serializer->addObject(this);
-       
+
        table->serialize(serializer);
-       
-       ASTNodeType type = PREDTABLETYPE;       
+
+       ASTNodeType type = PREDTABLETYPE;
        serializer->mywrite(&type, sizeof(ASTNodeType));
-       PredicateTableThis = this;
-       serializer->mywrite(&This, sizeof(PredicateTable*));
+       PredicateTable *This = this;
+       serializer->mywrite(&This, sizeof(PredicateTable *));
        serializer->mywrite(&table, sizeof(Table *));
        serializer->mywrite(&undefinedbehavior, sizeof(UndefinedBehavior));
 }
 
-void PredicateTable::print(){  
+void PredicateTable::print() {
        model_print("{PredicateTable:\n");
        table->print();
        model_print("}\n");
 }
 
-void PredicateOperator::serialize(Serializer* serializer){     
-       if(serializer->isSerialized(this))
+void PredicateOperator::serialize(Serializer *serializer) {
+       if (serializer->isSerialized(this))
                return;
        serializer->addObject(this);
-       
+
        uint size = domains.getSize();
-       for(uint i=0; i<size; i++){
-               Setdomain = domains.get(i);
+       for (uint i = 0; i < size; i++) {
+               Set *domain = domains.get(i);
                domain->serialize(serializer);
        }
-               
-       ASTNodeType type = PREDOPERTYPE;        
+
+       ASTNodeType type = PREDOPERTYPE;
        serializer->mywrite(&type, sizeof(ASTNodeType));
-       PredicateOperatorThis = this;
-       serializer->mywrite(&This, sizeof(PredicateOperator*));
+       PredicateOperator *This = this;
+       serializer->mywrite(&This, sizeof(PredicateOperator *));
        serializer->mywrite(&op, sizeof(CompOp));
        serializer->mywrite(&size, sizeof(uint));
-       for(uint i=0; i<size; i++){
-               Setdomain = domains.get(i);
-               serializer->mywrite(&domain, sizeof(Set*));
+       for (uint i = 0; i < size; i++) {
+               Set *domain = domains.get(i);
+               serializer->mywrite(&domain, sizeof(Set *));
        }
 }
 
-void PredicateOperator::print(){       
-       model_print("{PredicateOperator: %s }\n", op ==SATC_EQUALS? "EQUAL": "NOT-EQUAL");
+void PredicateOperator::print() {
+       model_print("{PredicateOperator: %s }\n", op == SATC_EQUALS ? "EQUAL" : "NOT-EQUAL");
 }
 
 
index 94a7e2e..812d4bd 100644 (file)
@@ -12,8 +12,8 @@ public:
        Predicate(PredicateType _type) : type(_type) {}
        virtual ~Predicate() {}
        virtual Predicate *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;}
-       virtual void serialize(Serializerserializer) = 0;
-        virtual void print() =0;
+       virtual void serialize(Serializer *serializer) = 0;
+       virtual void print() = 0;
        PredicateType type;
        CMEMALLOC;
 };
@@ -23,12 +23,12 @@ public:
        PredicateOperator(CompOp op, Set **domain, uint numDomain);
        bool evalPredicateOperator(uint64_t *inputs);
        Predicate *clone(CSolver *solver, CloneMap *map);
-       virtual void serialize(Serializerserializer);
-        virtual void print();
+       virtual void serialize(Serializer *serializer);
+       virtual void print();
        Array<Set *> domains;
        CompOp getOp() {return op;}
        CMEMALLOC;
- private:
+private:
        CompOp op;
 };
 
@@ -36,8 +36,8 @@ class PredicateTable : public Predicate {
 public:
        PredicateTable(Table *table, UndefinedBehavior undefBehavior);
        Predicate *clone(CSolver *solver, CloneMap *map);
-       virtual void serialize(Serializerserializer);
-        virtual void print();
+       virtual void serialize(Serializer *serializer);
+       virtual void print();
        Table *table;
        UndefinedBehavior undefinedbehavior;
        CMEMALLOC;
index b6908e1..2c946d5 100644 (file)
@@ -7,19 +7,19 @@ void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
        if (constraints.contains(bexpr.negate())) {
                constraints.remove(bexpr.negate());
                setUnSAT();
-       }       
+       }
        if (constraints.contains(bexpr)) {
                constraints.remove(bexpr);
        }
 
        replaceBooleanWithTrueNoRemove(bexpr);
 }
-       
+
 void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
        updateMustValue(bexpr.getBoolean(), bexpr.isNegated() ? BV_MUSTBEFALSE : BV_MUSTBETRUE);
 
        ASSERT(bexpr->boolVal != BV_UNSAT);
-       
+
        uint size = bexpr->parents.getSize();
        for (uint i = 0; i < size; i++) {
                Boolean *parent = bexpr->parents.get(i);
@@ -44,8 +44,8 @@ void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
 void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) {
        //Canonicalize
        if (oldb.isNegated()) {
-               oldb=oldb.negate();
-               newb=newb.negate();
+               oldb = oldb.negate();
+               newb = newb.negate();
 
        }
        if (constraints.contains(oldb)) {
@@ -72,8 +72,8 @@ void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) {
        for (uint i = 0; i < size; i++) {
                Boolean *parent = oldb->parents.get(i);
                BooleanLogic *logicop = (BooleanLogic *) parent;
-               boolMap.remove(parent); //could change parent's hash
-               
+               boolMap.remove(parent); //could change parent's hash
+
                uint parentsize = logicop->inputs.getSize();
                for (uint j = 0; j < parentsize; j++) {
                        BooleanEdge b = logicop->inputs.get(j);
@@ -108,13 +108,13 @@ void CSolver::handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child) {
 }
 
 void CSolver::handleANDTrue(BooleanLogic *bexpr, BooleanEdge child) {
-       BooleanEdge childNegate=child.negate();
-       
+       BooleanEdge childNegate = child.negate();
+
        boolMap.remove(bexpr);
-       
+
        for (uint i = 0; i < bexpr->inputs.getSize(); i++) {
                BooleanEdge b = bexpr->inputs.get(i);
-               
+
                if (b == child) {
                        bexpr->inputs.remove(i);
                        i--;
@@ -124,7 +124,7 @@ void CSolver::handleANDTrue(BooleanLogic *bexpr, BooleanEdge child) {
                }
        }
 
-       uint size=bexpr->inputs.getSize();
+       uint size = bexpr->inputs.getSize();
        if (size == 0) {
                bexpr->replaced = true;
                replaceBooleanWithTrue(bexpr);
@@ -142,8 +142,8 @@ void CSolver::replaceBooleanWithFalse(BooleanEdge bexpr) {
 }
 
 BooleanEdge CSolver::doRewrite(BooleanEdge bexpr) {
-       bool isNegated=bexpr.isNegated();
-       BooleanLogic * b = (BooleanLogic *) bexpr.getBoolean();
+       bool isNegated = bexpr.isNegated();
+       BooleanLogic *b = (BooleanLogic *) bexpr.getBoolean();
        BooleanEdge result;
        if (b->op == SATC_IFF) {
                if (isTrue(b->inputs.get(0))) {
@@ -155,7 +155,7 @@ BooleanEdge CSolver::doRewrite(BooleanEdge bexpr) {
                } else if (isFalse(b->inputs.get(1))) {
                        result = b->inputs.get(0).negate();
                } else ASSERT(0);
-       } else if (b->op==SATC_AND) {
+       } else if (b->op == SATC_AND) {
                uint size = b->inputs.getSize();
                if (size == 0)
                        result = boolTrue;
index 8fa9eda..ac4d088 100644 (file)
@@ -5,11 +5,11 @@
 #include "qsort.h"
 
 int intcompare(const void *p1, const void *p2) {
-       uint64_t a=*(uint64_t const *) p1;
-       uint64_t b=*(uint64_t const *) p2;
+       uint64_t a = *(uint64_t const *) p1;
+       uint64_t b = *(uint64_t const *) p2;
        if (a < b)
                return -1;
-       else if (a==b)
+       else if (a == b)
                return 0;
        else
                return 1;
@@ -34,18 +34,18 @@ bool Set::exists(uint64_t element) {
                return element >= low && element <= high;
        } else {
                //Use Binary Search
-               uint low=0;
-               uint high=members->getSize()-1;
-               while(true) {
-                       uint middle=(low+high)/2;
-                       uint64_t val=members->get(middle);
+               uint low = 0;
+               uint high = members->getSize() - 1;
+               while (true) {
+                       uint middle = (low + high) / 2;
+                       uint64_t val = members->get(middle);
                        if (element < val) {
-                               high=middle-1;
-                               if (middle<=low)
+                               high = middle - 1;
+                               if (middle <= low)
                                        return false;
                        } else if (element > val) {
-                               low=middle+1;
-                               if (middle>=high)
+                               low = middle + 1;
+                               if (middle >= high)
                                        return false;
                        } else {
                                return true;
@@ -103,7 +103,7 @@ uint Set::getUnionSize(Set *s) {
        uint sum = 0;
        uint64_t sValue = s->getElement(sIndex);
        uint64_t thisValue = getElement(thisIndex);
-       while(thisIndex < thisSize && sIndex < sSize) {
+       while (thisIndex < thisSize && sIndex < sSize) {
                if (sValue < thisValue) {
                        sValue = s->getElement(++sIndex);
                        sum++;
@@ -117,18 +117,18 @@ uint Set::getUnionSize(Set *s) {
                }
        }
        sum += (thisSize - thisIndex) + (sSize - sIndex);
-       
+
        return sum;
 }
 
-void Set::serialize(Serializer* serializer){
-       if(serializer->isSerialized(this))
+void Set::serialize(Serializer *serializer) {
+       if (serializer->isSerialized(this))
                return;
        serializer->addObject(this);
        ASTNodeType asttype = SETTYPE;
        serializer->mywrite(&asttype, sizeof(ASTNodeType));
-       SetThis = this;
-       serializer->mywrite(&This, sizeof(Set*));
+       Set *This = this;
+       serializer->mywrite(&This, sizeof(Set *));
        serializer->mywrite(&type, sizeof(VarType));
        serializer->mywrite(&isRange, sizeof(bool));
        serializer->mywrite(&low, sizeof(uint64_t));
@@ -137,20 +137,20 @@ void Set::serialize(Serializer* serializer){
        serializer->mywrite(&isMutable, sizeof(bool));
        uint size = members->getSize();
        serializer->mywrite(&size, sizeof(uint));
-       for(uint i=0; i<size; i++){
+       for (uint i = 0; i < size; i++) {
                uint64_t mem = members->get(i);
                serializer->mywrite(&mem, sizeof(uint64_t));
        }
 }
 
-void Set::print(){
+void Set::print() {
        model_print("{Set:");
-       if(isRange){
+       if (isRange) {
                model_print("Range: low=%lu, high=%lu}\n\n", low, high);
        } else {
                uint size = members->getSize();
                model_print("Members: ");
-               for(uint i=0; i<size; i++){
+               for (uint i = 0; i < size; i++) {
                        uint64_t mem = members->get(i);
                        model_print("%lu, ", mem);
                }
index a0bd449..c647af5 100644 (file)
@@ -27,7 +27,7 @@ public:
        uint getUnionSize(Set *s);
        virtual bool isMutableSet() {return false;}
        virtual Set *clone(CSolver *solver, CloneMap *map);
-       virtual void serialize(Serializerserializer);
+       virtual void serialize(Serializer *serializer);
        virtual void print();
        CMEMALLOC;
 protected:
index 3778767..5786b17 100644 (file)
@@ -61,34 +61,34 @@ Table::~Table() {
 
 
 
-void Table::serialize(Serializer* serializer){
-       if(serializer->isSerialized(this))
+void Table::serialize(Serializer *serializer) {
+       if (serializer->isSerialized(this))
                return;
        serializer->addObject(this);
-       
+
        uint size = domains.getSize();
-       for(uint i=0; i<size; i++){
-               Setdomain = domains.get(i);
+       for (uint i = 0; i < size; i++) {
+               Set *domain = domains.get(i);
                domain->serialize(serializer);
        }
-       if(range!= NULL)
+       if (range != NULL)
                range->serialize(serializer);
-       
-       ASTNodeType type = TABLETYPE;   
+
+       ASTNodeType type = TABLETYPE;
        serializer->mywrite(&type, sizeof(ASTNodeType));
-       TableThis = this;
-       serializer->mywrite(&This, sizeof(Table*));
+       Table *This = this;
+       serializer->mywrite(&This, sizeof(Table *));
        serializer->mywrite(&size, sizeof(uint));
-       for(uint i=0; i<size; i++){
-               Setdomain = domains.get(i);
-               serializer->mywrite(&domain, sizeof(Set*));
+       for (uint i = 0; i < size; i++) {
+               Set *domain = domains.get(i);
+               serializer->mywrite(&domain, sizeof(Set *));
        }
-       serializer->mywrite(&range, sizeof(Set*));
+       serializer->mywrite(&range, sizeof(Set *));
        size = entries->getSize();
        serializer->mywrite(&size, sizeof(uint));
-       SetIteratorTableEntryiterator = getEntries();
-       while(iterator->hasNext()){
-               TableEntryentry = iterator->next();
+       SetIteratorTableEntry *iterator = getEntries();
+       while (iterator->hasNext()) {
+               TableEntry *entry = iterator->next();
                serializer->mywrite(&entry->output, sizeof(uint64_t));
                serializer->mywrite(&entry->inputSize, sizeof(uint));
                serializer->mywrite(entry->inputs, sizeof(uint64_t) * entry->inputSize);
@@ -97,13 +97,13 @@ void Table::serialize(Serializer* serializer){
 }
 
 
-void Table::print(){
+void Table::print() {
        model_print("{Table:\n");
-       SetIteratorTableEntryiterator = getEntries();
-       while(iterator->hasNext()){
-               TableEntryentry = iterator->next();
+       SetIteratorTableEntry *iterator = getEntries();
+       while (iterator->hasNext()) {
+               TableEntry *entry = iterator->next();
                model_print("<");
-               for(uint i=0; i<entry->inputSize; i++){
+               for (uint i = 0; i < entry->inputSize; i++) {
                        model_print("%lu, ", entry->inputs[i]);
                }
                model_print(" == %lu>", entry->output);
index d8c7829..c196d3c 100644 (file)
@@ -11,19 +11,19 @@ public:
        TableEntry *getTableEntry(uint64_t *inputs, uint inputSize);
        Table *clone(CSolver *solver, CloneMap *map);
        void serialize(Serializer *serializer);
-        void print();
+       void print();
        ~Table();
-       Set * getRange() {return range;}
-       
-       Set * getDomain(uint i) {return domains.get(i);}
+       Set *getRange() {return range;}
+
+       Set *getDomain(uint i) {return domains.get(i);}
        uint numDomains() {return domains.getSize();}
-       SetIteratorTableEntry * getEntries() {return entries->iterator();}
+
+       SetIteratorTableEntry *getEntries() {return entries->iterator();}
        uint getSize() {return entries->getSize();}
 
        CMEMALLOC;
-       
- private:
+
+private:
        Array<Set *> domains;
        Set *range;
        HashsetTableEntry *entries;
index ebe6d7a..abbaf29 100644 (file)
 #include "subgraph.h"
 #include "elementencoding.h"
 
-EncodingGraph::EncodingGraph(CSolver * _solver) :
+EncodingGraph::EncodingGraph(CSolver *_solver) :
        solver(_solver) {
 }
 
-int sortEncodingEdge(const void * p1, const void *p2) {
-       const EncodingEdge * e1 = * (const EncodingEdge **) p1;
-       const EncodingEdge * e2 = * (const EncodingEdge **) p2;
+int sortEncodingEdge(const void *p1, const void *p2) {
+       const EncodingEdge *e1 = *(const EncodingEdge **) p1;
+       const EncodingEdge *e2 = *(const EncodingEdge **) p2;
        uint64_t v1 = e1->getValue();
        uint64_t v2 = e2->getValue();
        if (v1 < v2)
@@ -29,9 +29,9 @@ int sortEncodingEdge(const void * p1, const void *p2) {
 
 void EncodingGraph::buildGraph() {
        ElementIterator it(solver);
-       while(it.hasNext()) {
-               Element * e = it.next();
-               switch(e->type) {
+       while (it.hasNext()) {
+               Element *e = it.next();
+               switch (e->type) {
                case ELEMSET:
                case ELEMFUNCRETURN:
                        processElement(e);
@@ -47,40 +47,40 @@ void EncodingGraph::buildGraph() {
 }
 
 void EncodingGraph::encode() {
-       SetIteratorEncodingSubGraph * itesg=subgraphs.iterator();
-       while(itesg->hasNext()) {
-               EncodingSubGraph *sg=itesg->next();
+       SetIteratorEncodingSubGraph *itesg = subgraphs.iterator();
+       while (itesg->hasNext()) {
+               EncodingSubGraph *sg = itesg->next();
                sg->encode();
        }
        delete itesg;
 
        ElementIterator it(solver);
-       while(it.hasNext()) {
-               Element * e = it.next();
-               switch(e->type) {
+       while (it.hasNext()) {
+               Element *e = it.next();
+               switch (e->type) {
                case ELEMSET:
                case ELEMFUNCRETURN: {
-                       ElementEncoding *encoding=e->getElementEncoding();
+                       ElementEncoding *encoding = e->getElementEncoding();
                        if (encoding->getElementEncodingType() == ELEM_UNASSIGNED) {
                                EncodingNode *n = getNode(e);
                                if (n == NULL)
                                        continue;
-                               ElementEncodingType encodetype=n->getEncoding();
+                               ElementEncodingType encodetype = n->getEncoding();
                                encoding->setElementEncodingType(encodetype);
                                if (encodetype == UNARY || encodetype == ONEHOT) {
                                        encoding->encodingArrayInitialization();
                                } else if (encodetype == BINARYINDEX) {
-                                       EncodingSubGraph * subgraph = graphMap.get(n);
+                                       EncodingSubGraph *subgraph = graphMap.get(n);
                                        if (subgraph == NULL)
                                                continue;
                                        uint encodingSize = subgraph->getEncodingSize(n);
                                        uint paddedSize = encoding->getSizeEncodingArray(encodingSize);
                                        encoding->allocInUseArrayElement(paddedSize);
                                        encoding->allocEncodingArrayElement(paddedSize);
-                                       Set * s=e->getRange();
-                                       for(uint i=0;i<s->getSize();i++) {
-                                               uint64_t value=s->getElement(i);
-                                               uint encodingIndex=subgraph->getEncoding(n, value);
+                                       Set *s = e->getRange();
+                                       for (uint i = 0; i < s->getSize(); i++) {
+                                               uint64_t value = s->getElement(i);
+                                               uint encodingIndex = subgraph->getEncoding(n, value);
                                                encoding->setInUseElement(encodingIndex);
                                                encoding->encodingArray[encodingIndex] = value;
                                        }
@@ -96,23 +96,23 @@ void EncodingGraph::encode() {
 }
 
 void EncodingGraph::encodeParent(Element *e) {
-       uint size=e->parents.getSize();
-       for(uint i=0;i<size;i++) {
-               ASTNode * n = e->parents.get(i);
-               if (n->type==PREDICATEOP) {
-                       BooleanPredicate *b=(BooleanPredicate *)n;
-                       FunctionEncoding *fenc=b->getFunctionEncoding();
+       uint size = e->parents.getSize();
+       for (uint i = 0; i < size; i++) {
+               ASTNode *n = e->parents.get(i);
+               if (n->type == PREDICATEOP) {
+                       BooleanPredicate *b = (BooleanPredicate *)n;
+                       FunctionEncoding *fenc = b->getFunctionEncoding();
                        if (fenc->getFunctionEncodingType() != FUNC_UNASSIGNED)
                                continue;
-                       Predicate *p=b->getPredicate();
-                       if (p->type==OPERATORPRED) {
-                               PredicateOperator *po=(PredicateOperator *)p;
-                               ASSERT(b->inputs.getSize()==2);
-                               EncodingNode *left=createNode(b->inputs.get(0));
-                               EncodingNode *right=createNode(b->inputs.get(1));
+                       Predicate *p = b->getPredicate();
+                       if (p->type == OPERATORPRED) {
+                               PredicateOperator *po = (PredicateOperator *)p;
+                               ASSERT(b->inputs.getSize() == 2);
+                               EncodingNode *left = createNode(b->inputs.get(0));
+                               EncodingNode *right = createNode(b->inputs.get(1));
                                if (left == NULL || right == NULL)
                                        return;
-                               EncodingEdge *edge=getEdge(left, right, NULL);
+                               EncodingEdge *edge = getEdge(left, right, NULL);
                                if (edge != NULL && edge->getEncoding() == EDGE_MATCH) {
                                        fenc->setFunctionEncodingType(CIRCUIT);
                                }
@@ -122,8 +122,8 @@ void EncodingGraph::encodeParent(Element *e) {
 }
 
 void EncodingGraph::mergeNodes(EncodingNode *first, EncodingNode *second) {
-       EncodingSubGraph *graph1=graphMap.get(first);
-       EncodingSubGraph *graph2=graphMap.get(second);
+       EncodingSubGraph *graph1 = graphMap.get(first);
+       EncodingSubGraph *graph2 = graphMap.get(second);
        if (graph1 == NULL)
                first->setEncoding(BINARYINDEX);
        if (graph2 == NULL)
@@ -143,9 +143,9 @@ void EncodingGraph::mergeNodes(EncodingNode *first, EncodingNode *second) {
                first = tmp;
        }
        if (graph1 != NULL && graph2 != NULL) {
-               SetIteratorEncodingNode * nodeit=graph2->nodeIterator();
-               while(nodeit->hasNext()) {
-                       EncodingNode *node=nodeit->next();
+               SetIteratorEncodingNode *nodeit = graph2->nodeIterator();
+               while (nodeit->hasNext()) {
+                       EncodingNode *node = nodeit->next();
                        graph1->addNode(node);
                        graphMap.put(node, graph1);
                }
@@ -160,10 +160,10 @@ void EncodingGraph::mergeNodes(EncodingNode *first, EncodingNode *second) {
 }
 
 void EncodingGraph::processElement(Element *e) {
-       uint size=e->parents.getSize();
-       for(uint i=0;i<size;i++) {
-               ASTNode * n = e->parents.get(i);
-               switch(n->type) {
+       uint size = e->parents.getSize();
+       for (uint i = 0; i < size; i++) {
+               ASTNode *n = e->parents.get(i);
+               switch (n->type) {
                case PREDICATEOP:
                        processPredicate((BooleanPredicate *)n);
                        break;
@@ -177,32 +177,32 @@ void EncodingGraph::processElement(Element *e) {
 }
 
 void EncodingGraph::processFunction(ElementFunction *ef) {
-       Function *f=ef->getFunction();
-       if (f->type==OPERATORFUNC) {
-               FunctionOperator *fo=(FunctionOperator*)f;
+       Function *f = ef->getFunction();
+       if (f->type == OPERATORFUNC) {
+               FunctionOperator *fo = (FunctionOperator *)f;
                ASSERT(ef->inputs.getSize() == 2);
-               EncodingNode *left=createNode(ef->inputs.get(0));
-               EncodingNode *right=createNode(ef->inputs.get(1));
+               EncodingNode *left = createNode(ef->inputs.get(0));
+               EncodingNode *right = createNode(ef->inputs.get(1));
                if (left == NULL && right == NULL)
                        return;
-               EncodingNode *dst=createNode(ef);
-               EncodingEdge *edge=createEdge(left, right, dst);
+               EncodingNode *dst = createNode(ef);
+               EncodingEdge *edge = createEdge(left, right, dst);
                edge->numArithOps++;
        }
 }
 
 void EncodingGraph::processPredicate(BooleanPredicate *b) {
-       Predicate *p=b->getPredicate();
-       if (p->type==OPERATORPRED) {
-               PredicateOperator *po=(PredicateOperator *)p;
-               ASSERT(b->inputs.getSize()==2);
-               EncodingNode *left=createNode(b->inputs.get(0));
-               EncodingNode *right=createNode(b->inputs.get(1));
+       Predicate *p = b->getPredicate();
+       if (p->type == OPERATORPRED) {
+               PredicateOperator *po = (PredicateOperator *)p;
+               ASSERT(b->inputs.getSize() == 2);
+               EncodingNode *left = createNode(b->inputs.get(0));
+               EncodingNode *right = createNode(b->inputs.get(1));
                if (left == NULL || right == NULL)
                        return;
-               EncodingEdge *edge=createEdge(left, right, NULL);
-               CompOp op=po->getOp();
-               switch(op) {
+               EncodingEdge *edge = createEdge(left, right, NULL);
+               CompOp op = po->getOp();
+               switch (op) {
                case SATC_EQUALS:
                        edge->numEquals++;
                        break;
@@ -219,60 +219,60 @@ void EncodingGraph::processPredicate(BooleanPredicate *b) {
 }
 
 uint convertSize(uint cost) {
-       cost = 1.2 * cost; // fudge factor
+       cost = 1.2 * cost;// fudge factor
        return NEXTPOW2(cost);
 }
 
 void EncodingGraph::decideEdges() {
-       uint size=edgeVector.getSize();
-       for(uint i=0; i<size; i++) {
+       uint size = edgeVector.getSize();
+       for (uint i = 0; i < size; i++) {
                EncodingEdge *ee = edgeVector.get(i);
                EncodingNode *left = ee->left;
                EncodingNode *right = ee->right;
-               
+
                if (ee->encoding != EDGE_UNASSIGNED ||
                                !left->couldBeBinaryIndex() ||
                                !right->couldBeBinaryIndex())
                        continue;
-               
+
                uint64_t eeValue = ee->getValue();
                if (eeValue == 0)
                        return;
 
                EncodingSubGraph *leftGraph = graphMap.get(left);
                EncodingSubGraph *rightGraph = graphMap.get(right);
-               if (leftGraph == NULL && rightGraph !=NULL) {
-                       EncodingNode *tmp = left; left=right; right=tmp;
+               if (leftGraph == NULL && rightGraph != NULL) {
+                       EncodingNode *tmp = left; left = right; right = tmp;
                        EncodingSubGraph *tmpsg = leftGraph; leftGraph = rightGraph; rightGraph = tmpsg;
                }
 
-               uint leftSize=0, rightSize=0, newSize=0;
-               uint64_t totalCost=0;
+               uint leftSize = 0, rightSize = 0, newSize = 0;
+               uint64_t totalCost = 0;
                if (leftGraph == NULL && rightGraph == NULL) {
-                       leftSize=convertSize(left->getSize());
-                       rightSize=convertSize(right->getSize());
-                       newSize=convertSize(left->s->getUnionSize(right->s));
-                       newSize=(leftSize > newSize) ? leftSize: newSize;
-                       newSize=(rightSize > newSize) ? rightSize: newSize;
+                       leftSize = convertSize(left->getSize());
+                       rightSize = convertSize(right->getSize());
+                       newSize = convertSize(left->s->getUnionSize(right->s));
+                       newSize = (leftSize > newSize) ? leftSize : newSize;
+                       newSize = (rightSize > newSize) ? rightSize : newSize;
                        totalCost = (newSize - leftSize) * left->elements.getSize() +
-                               (newSize - rightSize) * right->elements.getSize();
+                                                                       (newSize - rightSize) * right->elements.getSize();
                } else if (leftGraph != NULL && rightGraph == NULL) {
-                       leftSize=convertSize(leftGraph->encodingSize);
-                       rightSize=convertSize(right->getSize());
-                       newSize=convertSize(leftGraph->estimateNewSize(right));
-                       newSize=(leftSize > newSize) ? leftSize: newSize;
-                       newSize=(rightSize > newSize) ? rightSize: newSize;
+                       leftSize = convertSize(leftGraph->encodingSize);
+                       rightSize = convertSize(right->getSize());
+                       newSize = convertSize(leftGraph->estimateNewSize(right));
+                       newSize = (leftSize > newSize) ? leftSize : newSize;
+                       newSize = (rightSize > newSize) ? rightSize : newSize;
                        totalCost = (newSize - leftSize) * leftGraph->numElements +
-                               (newSize - rightSize) * right->elements.getSize();
+                                                                       (newSize - rightSize) * right->elements.getSize();
                } else {
                        //Neither are null
-                       leftSize=convertSize(leftGraph->encodingSize);
-                       rightSize=convertSize(rightGraph->encodingSize);
-                       newSize=convertSize(leftGraph->estimateNewSize(rightGraph));
-                       newSize=(leftSize > newSize) ? leftSize: newSize;
-                       newSize=(rightSize > newSize) ? rightSize: newSize;
+                       leftSize = convertSize(leftGraph->encodingSize);
+                       rightSize = convertSize(rightGraph->encodingSize);
+                       newSize = convertSize(leftGraph->estimateNewSize(rightGraph));
+                       newSize = (leftSize > newSize) ? leftSize : newSize;
+                       newSize = (rightSize > newSize) ? rightSize : newSize;
                        totalCost = (newSize - leftSize) * leftGraph->numElements +
-                               (newSize - rightSize) * rightGraph->numElements;
+                                                                       (newSize - rightSize) * rightGraph->numElements;
                }
                double conversionfactor = 0.5;
                if ((totalCost * conversionfactor) < eeValue) {
@@ -284,28 +284,28 @@ void EncodingGraph::decideEdges() {
 
 static TunableDesc EdgeEncodingDesc(EDGE_UNASSIGNED, EDGE_MATCH, EDGE_UNASSIGNED);
 
-EncodingEdge * EncodingGraph::getEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst) {
+EncodingEdge *EncodingGraph::getEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst) {
        EncodingEdge e(left, right, dst);
        EncodingEdge *result = edgeMap.get(&e);
        return result;
 }
 
-EncodingEdge * EncodingGraph::createEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst) {
+EncodingEdge *EncodingGraph::createEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst) {
        EncodingEdge e(left, right, dst);
        EncodingEdge *result = edgeMap.get(&e);
        if (result == NULL) {
-               result=new EncodingEdge(left, right, dst);
-               VarType v1=left->getType();
-               VarType v2=right->getType();
+               result = new EncodingEdge(left, right, dst);
+               VarType v1 = left->getType();
+               VarType v2 = right->getType();
                if (v1 > v2) {
-                       VarType tmp=v2;
-                       v2=v1;
-                       v1=tmp;
+                       VarType tmp = v2;
+                       v2 = v1;
+                       v1 = tmp;
                }
 
                if ((left != NULL && left->couldBeBinaryIndex()) &&
                                (right != NULL) && right->couldBeBinaryIndex()) {
-                       EdgeEncodingType type=(EdgeEncodingType)solver->getTuner()->getVarTunable(v1, v2, EDGEENCODING, &EdgeEncodingDesc);
+                       EdgeEncodingType type = (EdgeEncodingType)solver->getTuner()->getVarTunable(v1, v2, EDGEENCODING, &EdgeEncodingDesc);
                        result->setEncoding(type);
                        if (type == EDGE_MATCH) {
                                mergeNodes(left, right);
@@ -337,7 +337,7 @@ VarType EncodingNode::getType() const {
 
 static TunableDesc NodeEncodingDesc(ELEM_UNASSIGNED, BINARYINDEX, ELEM_UNASSIGNED);
 
-EncodingNode * EncodingGraph::createNode(Element *e) {
+EncodingNode *EncodingGraph::createNode(Element *e) {
        if (e->type == ELEMCONST)
                return NULL;
        Set *s = e->getRange();
@@ -345,14 +345,14 @@ EncodingNode * EncodingGraph::createNode(Element *e) {
        if (n == NULL) {
                n = new EncodingNode(s);
                n->setEncoding((ElementEncodingType)solver->getTuner()->getVarTunable(n->getType(), NODEENCODING, &NodeEncodingDesc));
-               
+
                encodingMap.put(s, n);
        }
        n->addElement(e);
        return n;
 }
 
-EncodingNode * EncodingGraph::getNode(Element *e) {
+EncodingNode *EncodingGraph::getNode(Element *e) {
        if (e->type == ELEMCONST)
                return NULL;
        Set *s = e->getRange();
@@ -387,7 +387,7 @@ EncodingEdge::EncodingEdge(EncodingNode *_left, EncodingNode *_right, EncodingNo
 }
 
 uint hashEncodingEdge(EncodingEdge *edge) {
-       uintptr_t hash=(((uintptr_t) edge->left) >> 2) ^ (((uintptr_t)edge->right) >> 4) ^ (((uintptr_t)edge->dst) >> 6);
+       uintptr_t hash = (((uintptr_t) edge->left) >> 2) ^ (((uintptr_t)edge->right) >> 4) ^ (((uintptr_t)edge->dst) >> 6);
        return (uint) hash;
 }
 
index 301a74a..0c27e0a 100644 (file)
@@ -5,44 +5,44 @@
 #include "graphstructs.h"
 
 class EncodingGraph {
- public:
-       EncodingGraph(CSolver * solver);
+public:
+       EncodingGraph(CSolver *solver);
        void buildGraph();
        void encode();
-       
+
        CMEMALLOC;
- private:
-       CSolver * solver;
+private:
+       CSolver *solver;
        HashtableEncoding encodingMap;
        HashtableEdge edgeMap;
        Vector<EncodingEdge *> edgeVector;
        HashsetElement discovered;
        HashtableNodeToSubGraph graphMap;
        HashsetEncodingSubGraph subgraphs;
-       
+
        void encodeParent(Element *e);
        void decideEdges();
        void mergeNodes(EncodingNode *first, EncodingNode *second);
        void processElement(Element *e);
        void processFunction(ElementFunction *f);
        void processPredicate(BooleanPredicate *b);
-       EncodingNode * createNode(Element *e);
-       EncodingNode * getNode(Element *e);
-       EncodingEdge * getEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst);
-       EncodingEdge * createEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst);
+       EncodingNode *createNode(Element *e);
+       EncodingNode *getNode(Element *e);
+       EncodingEdge *getEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst);
+       EncodingEdge *createEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst);
 };
 
 class EncodingNode {
- public:
+public:
        EncodingNode(Set *_s);
        void addElement(Element *e);
        uint getSize() const;
        VarType getType() const;
-       void setEncoding(ElementEncodingType e) {encoding=e;}
+       void setEncoding(ElementEncodingType e) {encoding = e;}
        ElementEncodingType getEncoding() {return encoding;}
        bool couldBeBinaryIndex() {return encoding == BINARYINDEX || encoding == ELEM_UNASSIGNED;}
        CMEMALLOC;
- private:
+private:
        Set *s;
        HashsetElement elements;
        HashsetEncodingEdge edges;
@@ -55,16 +55,16 @@ enum EdgeEncodingType { EDGE_UNASSIGNED, EDGE_BREAK, EDGE_MATCH};
 typedef enum EdgeEncodingType EdgeEncodingType;
 
 class EncodingEdge {
- public:
+public:
        EncodingEdge(EncodingNode *_l, EncodingNode *_r);
        EncodingEdge(EncodingNode *_l, EncodingNode *_r, EncodingNode *_d);
-       void setEncoding(EdgeEncodingType e) {encoding=e;}
+       void setEncoding(EdgeEncodingType e) {encoding = e;}
        uint64_t getValue() const;
        EdgeEncodingType getEncoding() {return encoding;}
 
        CMEMALLOC;
-       
- private:
+
+private:
        EncodingNode *left;
        EncodingNode *right;
        EncodingNode *dst;
index afddea1..f2c0de2 100644 (file)
@@ -18,10 +18,10 @@ bool equalsNodeValuePair(NodeValuePair *nvp1, NodeValuePair *nvp2) {
 }
 
 int sortEncodingValue(const void *p1, const void *p2) {
-       const EncodingValue * e1 = * (const EncodingValue **) p1;
-       const EncodingValue * e2 = * (const EncodingValue **) p2;
-       uint se1=e1->notequals.getSize();
-       uint se2=e2->notequals.getSize();
+       const EncodingValue *e1 = *(const EncodingValue **) p1;
+       const EncodingValue *e2 = *(const EncodingValue **) p2;
+       uint se1 = e1->notequals.getSize();
+       uint se2 = e2->notequals.getSize();
        if (se1 > se2)
                return -1;
        else if (se2 == se1)
@@ -39,9 +39,9 @@ uint EncodingSubGraph::getEncoding(EncodingNode *n, uint64_t val) {
 void EncodingSubGraph::solveEquals() {
        Vector<EncodingValue *> toEncode;
        Vector<bool> encodingArray;
-       SetIteratorEncodingValue *valIt=values.iterator();
-       while(valIt->hasNext()) {
-               EncodingValue *ev=valIt->next();
+       SetIteratorEncodingValue *valIt = values.iterator();
+       while (valIt->hasNext()) {
+               EncodingValue *ev = valIt->next();
                if (!ev->inComparison)
                        toEncode.push(ev);
                else
@@ -49,20 +49,20 @@ void EncodingSubGraph::solveEquals() {
        }
        delete valIt;
        bsdqsort(toEncode.expose(), toEncode.getSize(), sizeof(EncodingValue *), sortEncodingValue);
-       uint toEncodeSize=toEncode.getSize();
-       for(uint i=0; i<toEncodeSize; i++) {
-               EncodingValue * ev=toEncode.get(i);
+       uint toEncodeSize = toEncode.getSize();
+       for (uint i = 0; i < toEncodeSize; i++) {
+               EncodingValue *ev = toEncode.get(i);
                encodingArray.clear();
-               SetIteratorEncodingValue *conflictIt=ev->notequals.iterator();
-               while(conflictIt->hasNext()) {
-                       EncodingValue * conflict=conflictIt->next();
+               SetIteratorEncodingValue *conflictIt = ev->notequals.iterator();
+               while (conflictIt->hasNext()) {
+                       EncodingValue *conflict = conflictIt->next();
                        if (conflict->assigned) {
                                encodingArray.setExpand(conflict->encoding, true);
                        }
                }
                delete conflictIt;
-               uint encoding=0;
-               for(;encoding<encodingArray.getSize();encoding++) {
+               uint encoding = 0;
+               for (; encoding < encodingArray.getSize(); encoding++) {
                        //See if this is unassigned
                        if (!encodingArray.get(encoding))
                                break;
@@ -77,17 +77,17 @@ void EncodingSubGraph::solveEquals() {
 void EncodingSubGraph::solveComparisons() {
        HashsetEncodingValue discovered;
        Vector<EncodingValue *> tovisit;
-       SetIteratorEncodingValue *valIt=values.iterator();
-       while(valIt->hasNext()) {
-               EncodingValue *ev=valIt->next();
+       SetIteratorEncodingValue *valIt = values.iterator();
+       while (valIt->hasNext()) {
+               EncodingValue *ev = valIt->next();
                if (discovered.add(ev)) {
                        tovisit.push(ev);
-                       while(tovisit.getSize()!=0) {
-                               EncodingValue * val=tovisit.last(); tovisit.pop();
-                               SetIteratorEncodingValue *nextIt=val->larger.iterator();
+                       while (tovisit.getSize() != 0) {
+                               EncodingValue *val = tovisit.last(); tovisit.pop();
+                               SetIteratorEncodingValue *nextIt = val->larger.iterator();
                                uint minVal = val->encoding + 1;
-                               while(nextIt->hasNext()) {
-                                       EncodingValue *nextVal=nextIt->next();
+                               while (nextIt->hasNext()) {
+                                       EncodingValue *nextVal = nextIt->next();
                                        if (nextVal->encoding < minVal) {
                                                if (minVal > maxEncodingVal)
                                                        maxEncodingVal = minVal;
@@ -104,11 +104,11 @@ void EncodingSubGraph::solveComparisons() {
 }
 
 uint EncodingSubGraph::estimateNewSize(EncodingSubGraph *sg) {
-       uint newSize=0;
-       SetIteratorEncodingNode * nit = sg->nodes.iterator();
-       while(nit->hasNext()) {
+       uint newSize = 0;
+       SetIteratorEncodingNode *nit = sg->nodes.iterator();
+       while (nit->hasNext()) {
                EncodingNode *en = nit->next();
-               uint size=estimateNewSize(en);
+               uint size = estimateNewSize(en);
                if (size > newSize)
                        newSize = size;
        }
@@ -117,10 +117,10 @@ uint EncodingSubGraph::estimateNewSize(EncodingSubGraph *sg) {
 }
 
 uint EncodingSubGraph::estimateNewSize(EncodingNode *n) {
-       SetIteratorEncodingEdge * eeit = n->edges.iterator();
-       uint newsize=n->getSize();
-       while(eeit->hasNext()) {
-               EncodingEdge * ee = eeit->next();
+       SetIteratorEncodingEdge *eeit = n->edges.iterator();
+       uint newsize = n->getSize();
+       while (eeit->hasNext()) {
+               EncodingEdge *ee = eeit->next();
                if (ee->left != NULL && ee->left != n && nodes.contains(ee->left)) {
                        uint intersectSize = n->s->getUnionSize(ee->left->s);
                        if (intersectSize > newsize)
@@ -143,13 +143,13 @@ uint EncodingSubGraph::estimateNewSize(EncodingNode *n) {
 
 void EncodingSubGraph::addNode(EncodingNode *n) {
        nodes.add(n);
-       uint newSize=estimateNewSize(n);
+       uint newSize = estimateNewSize(n);
        numElements += n->elements.getSize();
        if (newSize > encodingSize)
-               encodingSize=newSize;
+               encodingSize = newSize;
 }
 
-SetIteratorEncodingNode * EncodingSubGraph::nodeIterator() {
+SetIteratorEncodingNode *EncodingSubGraph::nodeIterator() {
        return nodes.iterator();
 }
 
@@ -162,14 +162,14 @@ void EncodingSubGraph::encode() {
 }
 
 void EncodingSubGraph::computeEqualities() {
-       SetIteratorEncodingNode *nodeit=nodes.iterator();
-       while(nodeit->hasNext()) {
-               EncodingNode *node=nodeit->next();
+       SetIteratorEncodingNode *nodeit = nodes.iterator();
+       while (nodeit->hasNext()) {
+               EncodingNode *node = nodeit->next();
                generateEquals(node, node);
-               
-               SetIteratorEncodingEdge *edgeit=node->edges.iterator();
-               while(edgeit->hasNext()) {
-                       EncodingEdge *edge=edgeit->next();
+
+               SetIteratorEncodingEdge *edgeit = node->edges.iterator();
+               while (edgeit->hasNext()) {
+                       EncodingEdge *edge = edgeit->next();
                        //skip over comparisons as we have already handled them
                        if (edge->numComparisons != 0)
                                continue;
@@ -194,12 +194,12 @@ void EncodingSubGraph::computeEqualities() {
 }
 
 void EncodingSubGraph::computeComparisons() {
-       SetIteratorEncodingNode *nodeit=nodes.iterator();
-       while(nodeit->hasNext()) {
-               EncodingNode *node=nodeit->next();
-               SetIteratorEncodingEdge *edgeit=node->edges.iterator();
-               while(edgeit->hasNext()) {
-                       EncodingEdge *edge=edgeit->next();
+       SetIteratorEncodingNode *nodeit = nodes.iterator();
+       while (nodeit->hasNext()) {
+               EncodingNode *node = nodeit->next();
+               SetIteratorEncodingEdge *edgeit = node->edges.iterator();
+               while (edgeit->hasNext()) {
+                       EncodingEdge *edge = edgeit->next();
                        if (edge->numComparisons == 0)
                                continue;
                        if (edge->left == NULL || !nodes.contains(edge->left))
@@ -222,15 +222,15 @@ void EncodingSubGraph::orderEV(EncodingValue *earlier, EncodingValue *later) {
 }
 
 void EncodingSubGraph::generateEquals(EncodingNode *left, EncodingNode *right) {
-       Set *lset=left->s;
-       Set *rset=right->s;
-       uint lSize=lset->getSize(), rSize=rset->getSize();
-       for(uint lindex=0; lindex < lSize; lindex++) {
-               for(uint rindex=0; rindex < rSize; rindex++) {
-                       uint64_t lVal=lset->getElement(lindex);
+       Set *lset = left->s;
+       Set *rset = right->s;
+       uint lSize = lset->getSize(), rSize = rset->getSize();
+       for (uint lindex = 0; lindex < lSize; lindex++) {
+               for (uint rindex = 0; rindex < rSize; rindex++) {
+                       uint64_t lVal = lset->getElement(lindex);
                        NodeValuePair nvp1(left, lVal);
                        EncodingValue *lev = map.get(&nvp1);
-                       uint64_t rVal=rset->getElement(rindex);
+                       uint64_t rVal = rset->getElement(rindex);
                        NodeValuePair nvp2(right, rVal);
                        EncodingValue *rev = map.get(&nvp2);
                        if (lev != rev) {
@@ -252,21 +252,21 @@ void EncodingSubGraph::generateEquals(EncodingNode *left, EncodingNode *right) {
 }
 
 void EncodingSubGraph::generateComparison(EncodingNode *left, EncodingNode *right) {
-       Set *lset=left->s;
-       Set *rset=right->s;
-       uint lindex=0, rindex=0;
-       uint lSize=lset->getSize(), rSize=rset->getSize();
-       uint64_t lVal=lset->getElement(lindex);
+       Set *lset = left->s;
+       Set *rset = right->s;
+       uint lindex = 0, rindex = 0;
+       uint lSize = lset->getSize(), rSize = rset->getSize();
+       uint64_t lVal = lset->getElement(lindex);
        NodeValuePair nvp1(left, lVal);
        EncodingValue *lev = map.get(&nvp1);
        lev->inComparison = true;
-       uint64_t rVal=rset->getElement(rindex);
+       uint64_t rVal = rset->getElement(rindex);
        NodeValuePair nvp2(right, rVal);
        EncodingValue *rev = map.get(&nvp2);
        rev->inComparison = true;
        EncodingValue *last = NULL;
 
-       while(lindex < lSize || rindex < rSize) {
+       while (lindex < lSize || rindex < rSize) {
                if (last != NULL) {
                        if (lev != NULL)
                                orderEV(last, lev);
@@ -280,7 +280,7 @@ void EncodingSubGraph::generateComparison(EncodingNode *left, EncodingNode *righ
                                        orderEV(lev, rev);
                                last = lev;
                                if (++lindex < lSize) {
-                                       lVal=lset->getElement(lindex);
+                                       lVal = lset->getElement(lindex);
                                        NodeValuePair nvpl(left, lVal);
                                        lev = map.get(&nvpl);
                                        lev->inComparison = true;
@@ -291,7 +291,7 @@ void EncodingSubGraph::generateComparison(EncodingNode *left, EncodingNode *righ
                                        orderEV(rev, lev);
                                last = rev;
                                if (++rindex < rSize) {
-                                       rVal=rset->getElement(rindex);
+                                       rVal = rset->getElement(rindex);
                                        NodeValuePair nvpr(right, rVal);
                                        rev = map.get(&nvpr);
                                        rev->inComparison = true;
@@ -301,7 +301,7 @@ void EncodingSubGraph::generateComparison(EncodingNode *left, EncodingNode *righ
                } else {
                        last = lev;
                        if (++lindex < lSize) {
-                               lVal=lset->getElement(lindex);
+                               lVal = lset->getElement(lindex);
                                NodeValuePair nvpl(left, lVal);
                                lev = map.get(&nvpl);
                                lev->inComparison = true;
@@ -309,7 +309,7 @@ void EncodingSubGraph::generateComparison(EncodingNode *left, EncodingNode *righ
                                lev = NULL;
 
                        if (++rindex < rSize) {
-                               rVal=rset->getElement(rindex);
+                               rVal = rset->getElement(rindex);
                                NodeValuePair nvpr(right, rVal);
                                rev = map.get(&nvpr);
                                rev->inComparison = true;
@@ -320,12 +320,12 @@ void EncodingSubGraph::generateComparison(EncodingNode *left, EncodingNode *righ
 }
 
 void EncodingSubGraph::computeEncodingValue() {
-       SetIteratorEncodingNode *nodeit=nodes.iterator();
-       while(nodeit->hasNext()) {
-               EncodingNode *node=nodeit->next();
-               Set * set = node->s;
+       SetIteratorEncodingNode *nodeit = nodes.iterator();
+       while (nodeit->hasNext()) {
+               EncodingNode *node = nodeit->next();
+               Set *set = node->s;
                uint setSize = set->getSize();
-               for(uint i=0; i<setSize; i++) {
+               for (uint i = 0; i < setSize; i++) {
                        uint64_t val = set->getElement(i);
                        NodeValuePair nvp(node, val);
                        if (!map.contains(&nvp)) {
@@ -337,21 +337,21 @@ void EncodingSubGraph::computeEncodingValue() {
 }
 
 void EncodingSubGraph::traverseValue(EncodingNode *node, uint64_t value) {
-       EncodingValue *ecv=new EncodingValue(value);
+       EncodingValue *ecv = new EncodingValue(value);
        values.add(ecv);
        HashsetEncodingNode discovered;
        Vector<EncodingNode *> tovisit;
        tovisit.push(node);
        discovered.add(node);
-       while(tovisit.getSize()!=0) {
-               EncodingNode *n=tovisit.last();tovisit.pop();
+       while (tovisit.getSize() != 0) {
+               EncodingNode *n = tovisit.last();tovisit.pop();
                //Add encoding node to structures
                ecv->nodes.add(n);
-               NodeValuePair *nvp=new NodeValuePair(n, value);
+               NodeValuePair *nvp = new NodeValuePair(n, value);
                map.put(nvp, ecv);
-               SetIteratorEncodingEdge *edgeit=node->edges.iterator();
-               while(edgeit->hasNext()) {
-                       EncodingEdge *ee=edgeit->next();
+               SetIteratorEncodingEdge *edgeit = node->edges.iterator();
+               while (edgeit->hasNext()) {
+                       EncodingEdge *ee = edgeit->next();
                        if (!discovered.contains(ee->left) && nodes.contains(ee->left) && ee->left->s->exists(value)) {
                                tovisit.push(ee->left);
                                discovered.add(ee->left);
index 1f90e91..36f1902 100644 (file)
@@ -5,8 +5,8 @@
 #include "graphstructs.h"
 
 class NodeValuePair {
- public:
- NodeValuePair(EncodingNode *n, uint64_t val) : node(n), value(val) {}
+public:
      NodeValuePair(EncodingNode *n, uint64_t val) : node(n), value(val) {}
        EncodingNode *node;
        uint64_t value;
 };
@@ -17,8 +17,8 @@ typedef Hashset<EncodingValue *, uintptr_t, PTRSHIFT> HashsetEncodingValue;
 typedef SetIterator<EncodingValue *, uintptr_t, PTRSHIFT> SetIteratorEncodingValue;
 
 class EncodingValue {
- public:
- EncodingValue(uint64_t _val) : value(_val), encoding(0), inComparison(false), assigned(false) {}
+public:
      EncodingValue(uint64_t _val) : value(_val), encoding(0), inComparison(false), assigned(false) {}
        void merge(EncodingValue *value);
        uint64_t value;
        uint encoding;
@@ -35,16 +35,16 @@ bool equalsNodeValuePair(NodeValuePair *nvp1, NodeValuePair *nvp2);
 typedef Hashtable<NodeValuePair *, EncodingValue *, uintptr_t, 0, hashNodeValuePair, equalsNodeValuePair> NVPMap;
 
 class EncodingSubGraph {
- public:
+public:
        EncodingSubGraph();
        void addNode(EncodingNode *n);
-       SetIteratorEncodingNode * nodeIterator();
+       SetIteratorEncodingNode *nodeIterator();
        void encode();
        uint getEncoding(EncodingNode *n, uint64_t val);
        uint getEncodingSize(EncodingNode *n) { return maxEncodingVal;}
-       
+
        CMEMALLOC;
- private:
+private:
        uint estimateNewSize(EncodingNode *n);
        uint estimateNewSize(EncodingSubGraph *sg);
        void traverseValue(EncodingNode *node, uint64_t value);
@@ -63,7 +63,7 @@ class EncodingSubGraph {
        uint encodingSize;
        uint numElements;
        uint maxEncodingVal;
-       
+
        friend class EncodingGraph;
 };
 
index ae3c752..701efde 100644 (file)
@@ -115,7 +115,7 @@ void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node) {
                        OrderNode *sinkNode = outEdge->sink;
                        sinkNode->inEdges.remove(outEdge);
                        //Adding new edge to new sink and src nodes ...
-                       if(srcNode == sinkNode) {
+                       if (srcNode == sinkNode) {
                                This->setUnSAT();
                                delete iterout;
                                delete iterin;
@@ -297,7 +297,7 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode
                                if (!edge->mustNeg && sources->contains(child)) {
                                        edge->mustNeg = true;
                                        edge->polNeg = true;
-                                       if (edge->mustPos){
+                                       if (edge->mustPos) {
                                                solver->setUnSAT();
                                        }
                                }
index 822af1f..07d7f7f 100644 (file)
@@ -12,7 +12,7 @@ OrderGraph::OrderGraph(Order *_order) :
 }
 
 OrderGraph *buildOrderGraph(Order *order) {
-        ASSERT(order->graph == NULL);
+       ASSERT(order->graph == NULL);
        OrderGraph *orderGraph = new OrderGraph(order);
        order->graph = orderGraph;
        uint constrSize = order->constraints.getSize();
@@ -24,7 +24,7 @@ OrderGraph *buildOrderGraph(Order *order) {
 
 //Builds only the subgraph for the must order graph.
 OrderGraph *buildMustOrderGraph(Order *order) {
-        ASSERT(order->graph == NULL);
+       ASSERT(order->graph == NULL);
        OrderGraph *orderGraph = new OrderGraph(order);
        uint constrSize = order->constraints.getSize();
        for (uint j = 0; j < constrSize; j++) {
@@ -180,23 +180,23 @@ OrderGraph::~OrderGraph() {
        delete edges;
 }
 
-bool OrderGraph::isTherePath(OrderNode *source, OrderNode *destination){
+bool OrderGraph::isTherePath(OrderNode *source, OrderNode *destination) {
        HashsetOrderNode visited;
        visited.add(source);
        SetIteratorOrderEdge *iterator = source->outEdges.iterator();
        bool found = false;
-       while(iterator->hasNext()){
-               OrderEdgeedge = iterator->next();
-               if(edge->polPos){
-                       OrderNodenode = edge->sink;
-                       if(!visited.contains(node)){
-                               if( node == destination ){
+       while (iterator->hasNext()) {
+               OrderEdge *edge = iterator->next();
+               if (edge->polPos) {
+                       OrderNode *node = edge->sink;
+                       if (!visited.contains(node)) {
+                               if ( node == destination ) {
                                        found = true;
                                        break;
                                }
                                visited.add(node);
-                               found =isTherePathVisit(visited, node, destination);
-                               if(found){
+                               found = isTherePathVisit(visited, node, destination);
+                               if (found) {
                                        break;
                                }
                        }
@@ -206,19 +206,19 @@ bool OrderGraph::isTherePath(OrderNode *source, OrderNode *destination){
        return found;
 }
 
-bool OrderGraph::isTherePathVisit(HashsetOrderNode &visited, OrderNode* current, OrderNode* destination){
+bool OrderGraph::isTherePathVisit(HashsetOrderNode &visited, OrderNode *current, OrderNode *destination) {
        SetIteratorOrderEdge *iterator = current->outEdges.iterator();
        bool found = false;
-       while(iterator->hasNext()){
-               OrderEdgeedge = iterator->next();
-               if(edge->polPos){
-                       OrderNodenode = edge->sink;
-                       if(node == destination){
+       while (iterator->hasNext()) {
+               OrderEdge *edge = iterator->next();
+               if (edge->polPos) {
+                       OrderNode *node = edge->sink;
+                       if (node == destination) {
                                found = true;
                                break;
                        }
                        visited.add(node);
-                       if(isTherePathVisit(visited, node, destination)){
+                       if (isTherePathVisit(visited, node, destination)) {
                                found = true;
                                break;
                        }
index a155c7f..2bb8812 100644 (file)
@@ -24,9 +24,9 @@ public:
        void addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
        void addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
        OrderEdge *getInverseOrderEdge(OrderEdge *edge);
-       Order *getOrder() {return order;} 
-       bool isTherePath(OrderNode* source, OrderNode* destination);
-       bool isTherePathVisit(HashsetOrderNode &visited, OrderNode* current, OrderNode* destination);
+       Order *getOrder() {return order;}
+       bool isTherePath(OrderNode *source, OrderNode *destination);
+       bool isTherePathVisit(HashsetOrderNode &visited, OrderNode *current, OrderNode *destination);
        SetIteratorOrderNode *getNodes() {return nodes->iterator();}
        SetIteratorOrderEdge *getEdges() {return edges->iterator();}
 
index 0be8066..6254832 100644 (file)
@@ -46,10 +46,10 @@ void computePredicatePolarity(BooleanPredicate *This) {
 }
 
 void computeLogicOpPolarity(BooleanLogic *This) {
-       Polarity child=computeLogicOpPolarityChildren(This);
+       Polarity child = computeLogicOpPolarityChildren(This);
        uint size = This->inputs.getSize();
        for (uint i = 0; i < size; i++) {
-               BooleanEdge b=This->inputs.get(i);
+               BooleanEdge b = This->inputs.get(i);
                computePolarity(b.getBoolean(), b.isNegated() ? negatePolarity(child) : child);
        }
 }
index 3791b10..3b8571d 100644 (file)
@@ -28,8 +28,8 @@ DecomposeOrderTransform::~DecomposeOrderTransform() {
 
 void DecomposeOrderTransform::doTransform() {
        HashsetOrder *orders = solver->getActiveOrders()->copy();
-       SetIteratorOrder * orderit=orders->iterator();
-       while(orderit->hasNext()) {
+       SetIteratorOrder *orderit = orders->iterator();
+       while (orderit->hasNext()) {
                Order *order = orderit->next();
 
                if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0) {
@@ -60,12 +60,12 @@ void DecomposeOrderTransform::doTransform() {
                        }
                }
 
-               
+
                bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
 
                if (mustReachPrune)
                        removeMustBeTrueNodes(solver, graph);
-               
+
                //This is needed for splitorder
                computeStronglyConnectedComponentGraph(graph);
                decomposeOrder(order, graph);
index 25ef990..1b34bae 100644 (file)
@@ -17,8 +17,8 @@ IntegerEncodingTransform::~IntegerEncodingTransform() {
 
 void IntegerEncodingTransform::doTransform() {
        HashsetOrder *orders = solver->getActiveOrders()->copy();
-       SetIteratorOrder * orderit=orders->iterator();
-       while(orderit->hasNext()) {
+       SetIteratorOrder *orderit = orders->iterator();
+       while (orderit->hasNext()) {
                Order *order = orderit->next();
                if (GETVARTUNABLE(solver->getTuner(), order->type, ORDERINTEGERENCODING, &onoff))
                        integerEncode(order);
index 1e04fd0..1e60c19 100644 (file)
@@ -15,10 +15,10 @@ Preprocess::~Preprocess() {
 void Preprocess::doTransform() {
        if (solver->getTuner()->getTunable(PREPROCESS, &onoff) == 0)
                return;
-       
+
        BooleanIterator bit(solver);
-       while(bit.hasNext()) {
-               Boolean *b=bit.next();
+       while (bit.hasNext()) {
+               Boolean *b = bit.next();
                if (b->type == BOOLEANVAR)
                        processBooleanVar((BooleanVar *)b);
        }
@@ -26,7 +26,7 @@ void Preprocess::doTransform() {
 }
 
 void Preprocess::resolveBooleanVars() {
-       SetIteratorBoolean * iterator = toremove.iterator();
+       SetIteratorBoolean *iterator = toremove.iterator();
        while (iterator->hasNext()) {
                BooleanVar *bv = (BooleanVar *) iterator->next();
                if (bv->polarity == P_TRUE) {
@@ -38,9 +38,9 @@ void Preprocess::resolveBooleanVars() {
        delete iterator;
 }
 
-void Preprocess::processBooleanVar(BooleanVar * b) {
-       if (b->polarity==P_TRUE ||
-                       b->polarity==P_FALSE) {
+void Preprocess::processBooleanVar(BooleanVar *b) {
+       if (b->polarity == P_TRUE ||
+                       b->polarity == P_FALSE) {
                toremove.add(b);
        }
 }
index ea9800d..2bca8bc 100644 (file)
@@ -4,15 +4,15 @@
 #include "transform.h"
 
 class Preprocess : public Transform {
- public:
+public:
        Preprocess(CSolver *_solver);
        ~Preprocess();
        void doTransform();
-       
+
        CMEMALLOC;
- private:
+private:
        HashsetBoolean toremove;
-       void processBooleanVar(BooleanVar * b);
+       void processBooleanVar(BooleanVar *b);
        void resolveBooleanVars();
 };
 
index abe29cc..e778247 100644 (file)
@@ -15,21 +15,21 @@ OrderPair::OrderPair() :
        constraint(E_NULL) {
 }
 
-OrderPair::~OrderPair(){
+OrderPair::~OrderPair() {
 }
 
-Edge OrderPair::getConstraint(){
+Edge OrderPair::getConstraint() {
        return constraint;
 }
 
-Edge OrderPair::getNegatedConstraint(){
+Edge OrderPair::getNegatedConstraint() {
        return constraintNegate(constraint);
 }
 
-bool OrderPair::getConstraintValue(CSolver* solver){
+bool OrderPair::getConstraintValue(CSolver *solver) {
        return getValueCNF(solver->getSATEncoder()->getCNF(), constraint);
 }
 
-bool OrderPair::getNegatedConstraintValue(CSolver* solver){
+bool OrderPair::getNegatedConstraintValue(CSolver *solver) {
        return getValueCNF(solver->getSATEncoder()->getCNF(), constraintNegate(constraint));
 }
index f650648..7c1cabd 100644 (file)
@@ -18,11 +18,11 @@ public:
        OrderPair();
        virtual ~OrderPair();
        virtual Edge getConstraint();
-       virtual bool getConstraintValue(CSolversolver);
+       virtual bool getConstraintValue(CSolver *solver);
        //for the cases that we swap first and second ... For total order is straight forward.
        // but for partial order it has some complexity which should be hidden ... -HG
        virtual Edge getNegatedConstraint();
-       virtual bool getNegatedConstraintValue(CSolversolver);
+       virtual bool getNegatedConstraintValue(CSolver *solver);
        uint64_t first;
        uint64_t second;
        CMEMALLOC;
index fdeee9e..2a58c06 100644 (file)
@@ -37,7 +37,7 @@ void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
 
 Edge SATEncoder::encodeConstraintSATEncoder(BooleanEdge c) {
        Edge result;
-       Boolean * constraint = c.getBoolean();
+       Boolean *constraint = c.getBoolean();
 
        if (booledgeMap.contains(constraint)) {
                Edge e = {(Node *) booledgeMap.get(constraint)};
@@ -96,7 +96,7 @@ Edge SATEncoder::encodeLogicSATEncoder(BooleanLogic *constraint) {
        case SATC_OR:
        case SATC_XOR:
        case SATC_IMPLIES:
-               //Don't handle, translate these away...
+       //Don't handle, translate these away...
        default:
                model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
                exit(-1);
index d525bda..56614fa 100644 (file)
@@ -65,7 +65,7 @@ Edge SATEncoder::getPairConstraint(Order *order, OrderPair *pair) {
                flipped.second = pair->first;
                pair = &flipped;
        }
-       OrderPairtmp;
+       OrderPair *tmp;
        if (!(table->contains(pair))) {
                tmp = new OrderPair(pair->first, pair->second, getNewVarSATEncoder());
                table->put(tmp, tmp);
@@ -81,8 +81,8 @@ Edge SATEncoder::getPartialPairConstraint(Order *order, OrderPair *pair) {
                return gvalue;
 
        HashtableOrderPair *table = order->getOrderPairTable();
-       
-       OrderPairtmp;
+
+       OrderPair *tmp;
        if (!(table->contains(pair))) {
                Edge constraint = getNewVarSATEncoder();
                tmp = new OrderPair(pair->first, pair->second, constraint);
@@ -104,7 +104,7 @@ Edge SATEncoder::encodeTotalOrderSATEncoder(BooleanOrder *boolOrder) {
                boolOrder->order->setOrderResolver(new OrderPairResolver(solver, boolOrder->order));
                bool doOptOrderStructure = GETVARTUNABLE(solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
                if (doOptOrderStructure) {
-                        ASSERT(boolOrder->order->graph == NULL);
+                       ASSERT(boolOrder->order->graph == NULL);
                        boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
                        reachMustAnalysis(solver, boolOrder->order->graph, true);
                }
@@ -153,7 +153,7 @@ Edge SATEncoder::generatePartialOrderConstraintsSATEncoder(Edge ij,Edge ji, Edge
        Edge uoIJ = constraintAND2(cnf, constraintNegate(ij), constraintNegate(ji));
        Edge uoJK = constraintAND2(cnf, constraintNegate(jk), constraintNegate(kj));
        Edge uoIK = constraintAND2(cnf, constraintNegate(ik), constraintNegate(ki));
-               
+
        Edge t1[] = {ij, jk, ik};
        Edge t2[] = {ji, jk, ik};
        Edge t3[] = {ij, kj, ki};
@@ -166,7 +166,7 @@ Edge SATEncoder::generatePartialOrderConstraintsSATEncoder(Edge ij,Edge ji, Edge
        Edge ct4 = constraintAND(cnf, 3, t4);
        Edge ct5 = constraintAND(cnf, 3, t5);
        Edge ct6 = constraintAND(cnf, 3, t6);
-       
+
        Edge p1[] = {uoIJ, jk, ik};
        Edge p2[] = {ij, kj, uoIK};
        Edge p3[] = {ji, uoJK, ki};
@@ -179,7 +179,7 @@ Edge SATEncoder::generatePartialOrderConstraintsSATEncoder(Edge ij,Edge ji, Edge
        Edge cp4 = constraintAND(cnf, 3, p4);
        Edge cp5 = constraintAND(cnf, 3, p5);
        Edge cp6 = constraintAND(cnf, 3, p6);
-       
+
        Edge o1[] = {uoIJ, uoJK, ik};
        Edge o2[] = {ij, uoJK, uoIK};
        Edge o3[] = {uoIK, jk, uoIK};
@@ -192,15 +192,15 @@ Edge SATEncoder::generatePartialOrderConstraintsSATEncoder(Edge ij,Edge ji, Edge
        Edge co4 = constraintAND(cnf, 3, o4);
        Edge co5 = constraintAND(cnf, 3, o5);
        Edge co6 = constraintAND(cnf, 3, o6);
-       
+
        Edge unorder [] = {uoIJ, uoJK, uoIK};
        Edge cunorder = constraintAND(cnf, 3, unorder);
-       
-       
+
+
        Edge res[] = {ct1,ct2,ct3,ct4,ct5,ct6,
-                       cp1,cp2,cp3,cp4,cp5,cp6,
-                       co1,co2,co3,co4,co5,co6,
-                       cunorder};
+                                                               cp1,cp2,cp3,cp4,cp5,cp6,
+                                                               co1,co2,co3,co4,co5,co6,
+                                                               cunorder};
        return constraintOR(cnf, 19, res);
 }
 
@@ -248,7 +248,7 @@ void SATEncoder::createAllPartialOrderConstraintsSATEncoder(Order *order) {
                                Edge constKI = getPartialPairConstraint(order, &pairKI);
                                Edge constKJ = getPartialPairConstraint(order, &pairKJ);
                                addConstraintCNF(cnf, generatePartialOrderConstraintsSATEncoder(constIJ, constJI,
-                                       constJK, constKJ, constIK, constKI));
+                                                                                                                                                                                                                                                                                               constJK, constKJ, constIK, constKI));
                        }
                }
        }
index 5e8a7de..7a8104d 100644 (file)
 #define PTRSHIFT 5
 
 class BooleanEdge {
- public:
- BooleanEdge() : b(NULL) {}
BooleanEdge(Boolean * _b) : b(_b) {}
+public:
      BooleanEdge() : b(NULL) {}
      BooleanEdge(Boolean *_b) : b(_b) {}
        BooleanEdge negate() {return BooleanEdge((Boolean *)(((uintptr_t) b) ^ 1));}
-       bool operator==(BooleanEdge e) { return b==e.b;}
-       bool operator!=(BooleanEdge e) { return b!=e.b;}
+       bool operator==(BooleanEdge e) { return b == e.b;}
+       bool operator!=(BooleanEdge e) { return b != e.b;}
        bool isNegated() { return ((uintptr_t) b) & 1; }
-       Boolean * getBoolean() {return (Boolean *)(((uintptr_t)b) & ~((uintptr_t) 1));}
-       Boolean * getRaw() {return b;}
-       Boolean * operator->() {return getBoolean();}
+       Boolean *getBoolean() {return (Boolean *)(((uintptr_t)b) & ~((uintptr_t) 1));}
+       Boolean *getRaw() {return b;}
+       Boolean *operator->() {return getBoolean();}
        operator bool() const {return b != NULL;}
- private:
+private:
        Boolean *b;
 };
 
 inline bool boolEdgeEquals(BooleanEdge b1, BooleanEdge b2) {
-       return b1==b2;
+       return b1 == b2;
 }
 
 inline unsigned int boolEdgeHash(BooleanEdge b) {
-       return (unsigned int) (((uintptr_t)b.getRaw())>>PTRSHIFT);
+       return (unsigned int) (((uintptr_t)b.getRaw()) >> PTRSHIFT);
 }
-                                                                       
-typedef Hashset<BooleanEdge, uintptr_t, PTRSHIFT, & boolEdgeHash, & boolEdgeEquals> HashsetBooleanEdge;
+
+typedef Hashset<BooleanEdge, uintptr_t, PTRSHIFT, &boolEdgeHash, &boolEdgeEquals> HashsetBooleanEdge;
 typedef Hashset<Order *, uintptr_t, PTRSHIFT> HashsetOrder;
-typedef SetIterator<BooleanEdge, uintptr_t, PTRSHIFT, & boolEdgeHash, & boolEdgeEquals> SetIteratorBooleanEdge;
+typedef SetIterator<BooleanEdge, uintptr_t, PTRSHIFT, &boolEdgeHash, &boolEdgeEquals> SetIteratorBooleanEdge;
 typedef SetIterator<Order *, uintptr_t, PTRSHIFT> SetIteratorOrder;
 
 #endif
index 0c415b5..f4e7ec9 100644 (file)
  * isn't worth optimizing; the SWAP's get sped up by the cache, and pointer
  * arithmetic gets lost in the time required for comparison function calls.
  */
-#define        SWAP(a, b, count, size, tmp) { \
-       count = size; \
-       do { \
-               tmp = *a; \
-               *a++ = *b; \
-               *b++ = tmp; \
-       } while (--count); \
+#define SWAP(a, b, count, size, tmp) { \
+               count = size; \
+               do { \
+                       tmp = *a; \
+                       *a++ = *b; \
+                       *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; \
-       do { \
-               *tmp1++ = *tmp2++; \
-       } while (--count); \
+               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) { \
-               child = base + child_i * size; \
-               if (child_i < nmemb && compar(child, child + size) < 0) { \
-                       child += size; \
-                       ++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) { \
+                               child += size; \
+                               ++child_i; \
+                       } \
+                       par = base + par_i * size; \
+                       if (compar(child, par) <= 0) \
+                               break; \
+                       SWAP(par, child, count, size, tmp); \
                } \
-               par = base + par_i * size; \
-               if (compar(child, par) <= 0) \
-                       break; \
-               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) { \
-       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) { \
-                       child += size; \
-                       ++child_i; \
+               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) { \
+                               child += size; \
+                               ++child_i; \
+                       } \
+                       par = base + par_i * size; \
+                       COPY(par, child, count, size, tmp1, tmp2); \
                } \
-               par = base + par_i * size; \
-               COPY(par, child, count, size, tmp1, tmp2); \
-       } \
-       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) { \
-                       COPY(child, k, count, size, tmp1, tmp2); \
-                       break; \
+               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) { \
+                               COPY(child, k, count, size, tmp1, tmp2); \
+                               break; \
+                       } \
+                       COPY(child, par, count, size, tmp1, tmp2); \
                } \
-               COPY(child, par, count, size, tmp1, tmp2); \
-       } \
 }
 
 /*
  */
 int
 bsdheapsort(void *vbase, size_t nmemb, size_t size,
-    int (*compar)(const void *, const void *))
+                                               int (*compar)(const void *, const void *))
 {
        size_t cnt, i, j, l;
        char tmp, *tmp1, *tmp2;
@@ -188,7 +188,7 @@ bsdheapsort(void *vbase, size_t nmemb, size_t size,
         */
        base = (char *)vbase - size;
 
-       for (l = nmemb / 2 + 1; --l;)
+       for (l = nmemb / 2 + 1; --l; )
                CREATE(l, nmemb, i, j, t, p, size, cnt, tmp);
 
        /*
@@ -207,10 +207,10 @@ bsdheapsort(void *vbase, size_t nmemb, size_t size,
 }
 
 
-static __inline char   *med3(char *, char *, char *, int (*)(const void *, const void *));
-static __inline void    swapfunc(char *, char *, size_t, int);
+static __inline char  *med3(char *, char *, char *, int (*)(const void *, const void *));
+static __inline void swapfunc(char *, char *, size_t, int);
 
-#define min(a, b)      (a) < (b) ? a : b
+#define min(a, b) (a) < (b) ? a : b
 
 /*
  * Qsort routine from Bentley & McIlroy's "Engineering a Sort Function".
@@ -230,24 +230,24 @@ static __inline void       swapfunc(char *, char *, size_t, int);
  *   4. Tail recursion is eliminated when sorting the larger of two
  *     subpartitions to save stack space.
  */
-#define SWAPTYPE_BYTEV 1
-#define SWAPTYPE_INTV  2
-#define SWAPTYPE_LONGV 3
-#define SWAPTYPE_INT   4
-#define SWAPTYPE_LONG  5
+#define SWAPTYPE_BYTEV  1
+#define SWAPTYPE_INTV 2
+#define SWAPTYPE_LONGV  3
+#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,47 +268,47 @@ 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)
+#define vecswap(a, b, n)  if ((n) > 0) swapfunc(a, b, n, swaptype)
 
 static __inline char *
 med3(char *a, char *b, char *c, int (*cmp)(const void *, const void *))
 {
        return cmp(a, b) < 0 ?
-              (cmp(b, c) < 0 ? b : (cmp(a, c) < 0 ? c : a ))
-              :(cmp(b, c) > 0 ? b : (cmp(a, c) < 0 ? a : c ));
+                                (cmp(b, c) < 0 ? b : (cmp(a, c) < 0 ? c : a))
+                                : (cmp(b, c) > 0 ? b : (cmp(a, c) < 0 ? a : c));
 }
 
 static void
 introsort(char *a, size_t n, size_t es, size_t maxdepth, int swaptype,
-    int (*cmp)(const void *, const void *))
+                                       int (*cmp)(const void *, const void *))
 {
        char *pa, *pb, *pc, *pd, *pl, *pm, *pn;
        int cmp_result;
        size_t r, s;
 
-loop:  if (n < 7) {
+loop: if (n < 7) {
                for (pm = a + es; pm < a + n * es; pm += es)
                        for (pl = pm; pl > a && cmp(pl - es, pl) > 0;
-                            pl -= es)
+                                        pl -= es)
                                swap(pl, pl - es);
                return;
        }
@@ -332,7 +332,7 @@ loop:       if (n < 7) {
        swap(a, pm);
        pa = pb = a + es;
        pc = pd = a + (n - 1) * es;
-       for (;;) {
+       for (;; ) {
                while (pb <= pc && (cmp_result = cmp(pb, a)) <= 0) {
                        if (cmp_result == 0) {
                                swap(pa, pb);
@@ -370,7 +370,7 @@ loop:       if (n < 7) {
                if (s > es) {
                        if (r > es) {
                                introsort(a, r / es, es, maxdepth,
-                                   swaptype, cmp);
+                                                                       swaptype, cmp);
                        }
                        a = pn - s;
                        n = s / es;
@@ -381,7 +381,7 @@ loop:       if (n < 7) {
                if (r > es) {
                        if (s > es) {
                                introsort(pn - s, s / es, es, maxdepth,
-                                   swaptype, cmp);
+                                                                       swaptype, cmp);
                        }
                        n = r / es;
                        goto loop;
index 80ec918..6c53253 100644 (file)
@@ -81,7 +81,7 @@
        void setVector ## name(Vector ## name * vector, uint index, type item) { \
                vector->array[index] = item;                                          \
        }                                                                     \
-       uint getSizeVector ## name(const Vector ## name * vector) {                                             \
+       uint getSizeVector ## name(const Vector ## name * vector) {           \
                return vector->size;                                                \
        }                                                                     \
        void deleteVector ## name(Vector ## name * vector) {                     \
index ace0313..e42f398 100644 (file)
@@ -28,7 +28,7 @@ void naiveEncodingConstraint(Boolean *This) {
                return;
        }
        case ORDERCONST: {
-               if(((BooleanOrder *) This)->order->encoding.type == ORDER_UNASSIGNED)
+               if (((BooleanOrder *) This)->order->encoding.type == ORDER_UNASSIGNED)
                        ((BooleanOrder *) This)->order->setOrderEncodingType(PAIRWISE);
                return;
        }
index 556554e..e3c150a 100644 (file)
@@ -8,8 +8,8 @@ OrderEncoding::OrderEncoding(Order *_order) :
 {
 }
 
-OrderEncoding::~OrderEncoding(){
-       if(resolver!= NULL){
+OrderEncoding::~OrderEncoding() {
+       if (resolver != NULL) {
                delete resolver;
        }
 }
index fc4cd7b..cd1e1a2 100644 (file)
@@ -1,8 +1,8 @@
 
-/* 
+/*
  * File:   deserializer.cc
  * Author: hamed
- * 
+ *
  * Created on September 7, 2017, 6:08 PM
  */
 
 #include "element.h"
 #include "mutableset.h"
 
-Deserializer::Deserializer(const char* file):
+Deserializer::Deserializer(const char *file) :
        solver(new CSolver())
 {
        filedesc = open(file, O_RDONLY);
+
        if (filedesc < 0) {
                exit(-1);
        }
@@ -27,98 +27,98 @@ Deserializer::Deserializer(const char* file):
 
 Deserializer::~Deserializer() {
        delete solver;
-       
-       if (-1 == close(filedesc)){
+
+       if (-1 == close(filedesc)) {
                exit(-1);
        }
 }
 
-ssize_t Deserializer::myread(void* __buf, size_t __nbytes){
+ssize_t Deserializer::myread(void *__buf, size_t __nbytes) {
        return read (filedesc, __buf, __nbytes);
 }
 
-CSolver * Deserializer::deserialize(){
+CSolver *Deserializer::deserialize() {
        ASTNodeType nodeType;
-       while(myread(&nodeType, sizeof(ASTNodeType) ) >0){
-               switch(nodeType){
-                       case BOOLEANEDGE:
-                               deserializeBooleanEdge();
-                               break;
-                       case BOOLEANVAR:
-                               deserializeBooleanVar();
-                               break;
-                       case ORDERCONST:
-                               deserializeBooleanOrder();
-                               break;
-                       case ORDERTYPE:
-                               deserializeOrder();
-                               break;
-                       case SETTYPE:
-                               deserializeSet();
-                               break;
-                       case LOGICOP:
-                               deserializeBooleanLogic();
-                               break;
-                       case PREDICATEOP:
-                               deserializeBooleanPredicate();
-                               break;
-                       case PREDTABLETYPE:
-                               deserializePredicateTable();
-                               break;
-                       case PREDOPERTYPE:
-                               deserializePredicateOperator();
-                               break;
-                       case TABLETYPE:
-                               deserializeTable();
-                               break;
-                       case ELEMSET:
-                               deserializeElementSet();
-                               break;
-                       case ELEMCONST:
-                               deserializeElementConst();
-                               break;
-                       case ELEMFUNCRETURN:
-                               deserializeElementFunction();
-                               break;
-                       case FUNCOPTYPE:
-                               deserializeFunctionOperator();
-                               break;
-                       case FUNCTABLETYPE:
-                               deserializeFunctionTable();
-                               break;
-                       default:
-                               ASSERT(0);
+       while (myread(&nodeType, sizeof(ASTNodeType) ) > 0) {
+               switch (nodeType) {
+               case BOOLEANEDGE:
+                       deserializeBooleanEdge();
+                       break;
+               case BOOLEANVAR:
+                       deserializeBooleanVar();
+                       break;
+               case ORDERCONST:
+                       deserializeBooleanOrder();
+                       break;
+               case ORDERTYPE:
+                       deserializeOrder();
+                       break;
+               case SETTYPE:
+                       deserializeSet();
+                       break;
+               case LOGICOP:
+                       deserializeBooleanLogic();
+                       break;
+               case PREDICATEOP:
+                       deserializeBooleanPredicate();
+                       break;
+               case PREDTABLETYPE:
+                       deserializePredicateTable();
+                       break;
+               case PREDOPERTYPE:
+                       deserializePredicateOperator();
+                       break;
+               case TABLETYPE:
+                       deserializeTable();
+                       break;
+               case ELEMSET:
+                       deserializeElementSet();
+                       break;
+               case ELEMCONST:
+                       deserializeElementConst();
+                       break;
+               case ELEMFUNCRETURN:
+                       deserializeElementFunction();
+                       break;
+               case FUNCOPTYPE:
+                       deserializeFunctionOperator();
+                       break;
+               case FUNCTABLETYPE:
+                       deserializeFunctionTable();
+                       break;
+               default:
+                       ASSERT(0);
                }
        }
        return solver;
 }
 
-void Deserializer::deserializeBooleanEdge(){
+void Deserializer::deserializeBooleanEdge() {
        Boolean *b;
-       myread(&b, sizeof(Boolean*));
+       myread(&b, sizeof(Boolean *));
        BooleanEdge tmp(b);
        bool isNegated = tmp.isNegated();
        ASSERT(map.contains(tmp.getBoolean()));
-       b = (Boolean*) map.get(tmp.getBoolean());
+       b = (Boolean *) map.get(tmp.getBoolean());
        BooleanEdge res(b);
-       solver->addConstraint(isNegated?res.negate():res);
+       solver->addConstraint(isNegated ? res.negate() : res);
 }
 
-void Deserializer::deserializeBooleanVar(){
+void Deserializer::deserializeBooleanVar() {
        BooleanVar *b;
-       myread(&b, sizeof(BooleanVar*));
+       myread(&b, sizeof(BooleanVar *));
        VarType vtype;
        myread(&vtype, sizeof(VarType));
        map.put(b, solver->getBooleanVar(vtype).getBoolean());
 }
 
-void Deserializer::deserializeBooleanOrder(){
-       BooleanOrderbo_ptr;
-       myread(&bo_ptr, sizeof(BooleanOrder*));
-       Orderorder;
-       myread(&order, sizeof(Order*));
+void Deserializer::deserializeBooleanOrder() {
+       BooleanOrder *bo_ptr;
+       myread(&bo_ptr, sizeof(BooleanOrder *));
+       Order *order;
+       myread(&order, sizeof(Order *));
        ASSERT(map.contains(order));
-       order  = (Order*) map.get(order);
+       order  = (Order *) map.get(order);
        uint64_t first;
        myread(&first, sizeof(uint64_t));
        uint64_t second;
@@ -126,21 +126,21 @@ void Deserializer::deserializeBooleanOrder(){
        map.put(bo_ptr, solver->orderConstraint(order, first, second).getBoolean());
 }
 
-void Deserializer::deserializeOrder(){
-       Ordero_ptr;
-       myread(&o_ptr, sizeof(Order*));
+void Deserializer::deserializeOrder() {
+       Order *o_ptr;
+       myread(&o_ptr, sizeof(Order *));
        OrderType type;
        myread(&type, sizeof(OrderType));
-       Set * set_ptr;
+       Set *set_ptr;
        myread(&set_ptr, sizeof(Set *));
        ASSERT(map.contains(set_ptr));
-       Set* set  = (Set*) map.get(set_ptr);
+       Set *set  = (Set *) map.get(set_ptr);
        map.put(o_ptr, solver->createOrder(type, set));
 }
 
-void Deserializer::deserializeSet(){
+void Deserializer::deserializeSet() {
        Set *s_ptr;
-       myread(&s_ptr, sizeof(Set*));
+       myread(&s_ptr, sizeof(Set *));
        VarType type;
        myread(&type, sizeof(VarType));
        bool isRange;
@@ -152,29 +152,29 @@ void Deserializer::deserializeSet(){
        bool isMutable;
        myread(&isMutable, sizeof(bool));
        Set *set;
-       if(isMutable){
+       if (isMutable) {
                set = new MutableSet(type);
        }
        uint size;
        myread(&size, sizeof(uint));
        Vector<uint64_t> members;
-       for(uint i=0; i<size; i++){
+       for (uint i = 0; i < size; i++) {
                uint64_t mem;
                myread(&mem, sizeof(uint64_t));
-               if(isMutable) {
-                       ((MutableSet*) set)->addElementMSet(mem);
-               }else {
+               if (isMutable) {
+                       ((MutableSet *) set)->addElementMSet(mem);
+               } else {
                        members.push(mem);
                }
        }
-       if(!isMutable){
-               set = isRange? solver->createRangeSet(type, low, high):
-                       solver->createSet(type, members.expose(), size);
+       if (!isMutable) {
+               set = isRange ? solver->createRangeSet(type, low, high) :
+                                       solver->createSet(type, members.expose(), size);
        }
        map.put(s_ptr, set);
 }
 
-void Deserializer::deserializeBooleanLogic(){
+void Deserializer::deserializeBooleanLogic() {
        BooleanLogic *bl_ptr;
        myread(&bl_ptr, sizeof(BooleanLogic *));
        LogicOp op;
@@ -182,134 +182,134 @@ void Deserializer::deserializeBooleanLogic(){
        uint size;
        myread(&size, sizeof(uint));
        Vector<BooleanEdge> members;
-       for(uint i=0; i<size; i++){
-               Booleanmember;
+       for (uint i = 0; i < size; i++) {
+               Boolean *member;
                myread(&member, sizeof(Boolean *));
                BooleanEdge tmp(member);
                bool isNegated = tmp.isNegated();
                ASSERT(map.contains(tmp.getBoolean()));
-               member = (Boolean*) map.get(tmp.getBoolean());
+               member = (Boolean *) map.get(tmp.getBoolean());
                BooleanEdge res(member);
-               members.push( isNegated?res.negate():res );
+               members.push( isNegated ? res.negate() : res );
        }
        map.put(bl_ptr, solver->applyLogicalOperation(op, members.expose(), size).getBoolean());
 }
 
-void Deserializer::deserializeBooleanPredicate(){
+void Deserializer::deserializeBooleanPredicate() {
        BooleanPredicate *bp_ptr;
        myread(&bp_ptr, sizeof(BooleanPredicate *));
-       Predicatepredicate;
-       myread(&predicate, sizeof(Predicate*));
+       Predicate *predicate;
+       myread(&predicate, sizeof(Predicate *));
        ASSERT(map.contains(predicate));
-       predicate = (Predicate*) map.get(predicate);
+       predicate = (Predicate *) map.get(predicate);
        uint size;
        myread(&size, sizeof(uint));
-       Vector<Element*> members;
-       for(uint i=0; i<size; i++){
-               Elementinput;
+       Vector<Element *> members;
+       for (uint i = 0; i < size; i++) {
+               Element *input;
                myread(&input, sizeof(Element *));
                ASSERT(map.contains(input));
-               input = (Element*) map.get(input);
+               input = (Element *) map.get(input);
                members.push(input);
        }
-       
-       Booleanstat_ptr;
+
+       Boolean *stat_ptr;
        myread(&stat_ptr, sizeof(Boolean *));
        BooleanEdge undefStatus;
-       if(stat_ptr != NULL){
+       if (stat_ptr != NULL) {
                BooleanEdge tmp(stat_ptr);
                bool isNegated = tmp.isNegated();
                ASSERT(map.contains(tmp.getBoolean()));
-               stat_ptr = (Boolean*) map.get(tmp.getBoolean());
+               stat_ptr = (Boolean *) map.get(tmp.getBoolean());
                BooleanEdge res(stat_ptr);
-               undefStatus = isNegated?res.negate():res;
+               undefStatus = isNegated ? res.negate() : res;
        } else {
                undefStatus = NULL;
        }
        map.put(bp_ptr, solver->applyPredicateTable(predicate, members.expose(), size, undefStatus).getBoolean());
 }
 
-void Deserializer::deserializePredicateTable(){
+void Deserializer::deserializePredicateTable() {
        PredicateTable *pt_ptr;
        myread(&pt_ptr, sizeof(PredicateTable *));
-       Tabletable;
-       myread(&table, sizeof(Table*));
+       Table *table;
+       myread(&table, sizeof(Table *));
        ASSERT(map.contains(table));
-       table = (Table*) map.get(table);
+       table = (Table *) map.get(table);
        UndefinedBehavior undefinedbehavior;
        myread(&undefinedbehavior, sizeof(UndefinedBehavior));
-       
+
        map.put(pt_ptr, solver->createPredicateTable(table, undefinedbehavior));
 }
 
-void Deserializer::deserializePredicateOperator(){
+void Deserializer::deserializePredicateOperator() {
        PredicateOperator *po_ptr;
        myread(&po_ptr, sizeof(PredicateOperator *));
        CompOp op;
        myread(&op, sizeof(CompOp));
        uint size;
        myread(&size, sizeof(uint));
-       Vector<Set*> domains;
-       for(uint i=0; i<size; i++){
-               Setdomain;
-               myread(&domain, sizeof(Set*));
+       Vector<Set *> domains;
+       for (uint i = 0; i < size; i++) {
+               Set *domain;
+               myread(&domain, sizeof(Set *));
                ASSERT(map.contains(domain));
-               domain = (Set*) map.get(domain);
+               domain = (Set *) map.get(domain);
                domains.push(domain);
        }
 
        map.put(po_ptr, solver->createPredicateOperator(op, domains.expose(), size));
 }
 
-void Deserializer::deserializeTable(){
+void Deserializer::deserializeTable() {
        Table *t_ptr;
        myread(&t_ptr, sizeof(Table *));
        uint size;
        myread(&size, sizeof(uint));
-       Vector<Set*> domains;
-       for(uint i=0; i<size; i++){
-               Setdomain;
-               myread(&domain, sizeof(Set*));
+       Vector<Set *> domains;
+       for (uint i = 0; i < size; i++) {
+               Set *domain;
+               myread(&domain, sizeof(Set *));
                ASSERT(map.contains(domain));
-               domain = (Set*) map.get(domain);
+               domain = (Set *) map.get(domain);
                domains.push(domain);
        }
-       Setrange;
-       myread(&range, sizeof(Set*));
-       if(range != NULL){
+       Set *range;
+       myread(&range, sizeof(Set *));
+       if (range != NULL) {
                ASSERT(map.contains(range));
-               range = (Set*) map.get(range);
+               range = (Set *) map.get(range);
        }
-       Tabletable = solver->createTable(domains.expose(), size, range);
+       Table *table = solver->createTable(domains.expose(), size, range);
        myread(&size, sizeof(uint));
-       for(uint i=0; i<size; i++){
+       for (uint i = 0; i < size; i++) {
                uint64_t output;
                myread(&output, sizeof(uint64_t));
                uint inputSize;
                myread(&inputSize, sizeof(uint));
                Vector<uint64_t> inputs;
                inputs.setSize(inputSize);
-               myread(inputs.expose(), sizeof(uint64_t)*inputSize);
+               myread(inputs.expose(), sizeof(uint64_t) * inputSize);
                table->addNewTableEntry(inputs.expose(), inputSize, output);
        }
-       
+
        map.put(t_ptr, table);
 }
 
 
-void Deserializer::deserializeElementSet(){
-       ElementSetes_ptr;
-       myread(&es_ptr, sizeof(ElementSet*));
-       Set * set;
+void Deserializer::deserializeElementSet() {
+       ElementSet *es_ptr;
+       myread(&es_ptr, sizeof(ElementSet *));
+       Set *set;
        myread(&set, sizeof(Set *));
        ASSERT(map.contains(set));
-       set  = (Set*) map.get(set);
+       set  = (Set *) map.get(set);
        map.put(es_ptr, solver->getElementVar(set));
 }
 
-void Deserializer::deserializeElementConst(){
-       ElementSetes_ptr;
-       myread(&es_ptr, sizeof(ElementSet*));
+void Deserializer::deserializeElementConst() {
+       ElementSet *es_ptr;
+       myread(&es_ptr, sizeof(ElementSet *));
        VarType type;
        myread(&type, sizeof(VarType));
        uint64_t value;
@@ -317,70 +317,70 @@ void Deserializer::deserializeElementConst(){
        map.put(es_ptr, solver->getElementConst(type, value));
 }
 
-void Deserializer::deserializeElementFunction(){
+void Deserializer::deserializeElementFunction() {
        ElementFunction *ef_ptr;
        myread(&ef_ptr, sizeof(ElementFunction *));
        Function *function;
-       myread(&function, sizeof(Function*));
+       myread(&function, sizeof(Function *));
        ASSERT(map.contains(function));
-       function = (Function*) map.get(function);
+       function = (Function *) map.get(function);
        uint size;
        myread(&size, sizeof(uint));
-       Vector<Element*> members;
-       for(uint i=0; i<size; i++){
-               Elementinput;
+       Vector<Element *> members;
+       for (uint i = 0; i < size; i++) {
+               Element *input;
                myread(&input, sizeof(Element *));
                ASSERT(map.contains(input));
-               input = (Element*) map.get(input);
+               input = (Element *) map.get(input);
                members.push(input);
        }
-       
-       Booleanoverflowstatus;
+
+       Boolean *overflowstatus;
        myread(&overflowstatus, sizeof(Boolean *));
        BooleanEdge tmp(overflowstatus);
        bool isNegated = tmp.isNegated();
        ASSERT(map.contains(tmp.getBoolean()));
-       overflowstatus = (Boolean*) map.get(tmp.getBoolean());
+       overflowstatus = (Boolean *) map.get(tmp.getBoolean());
        BooleanEdge res(overflowstatus);
-       BooleanEdge undefStatus = isNegated?res.negate():res;
-       
+       BooleanEdge undefStatus = isNegated ? res.negate() : res;
+
        map.put(ef_ptr, solver->applyFunction(function, members.expose(), size, undefStatus));
 }
 
 
-void Deserializer::deserializeFunctionOperator(){
+void Deserializer::deserializeFunctionOperator() {
        FunctionOperator *fo_ptr;
        myread(&fo_ptr, sizeof(FunctionOperator *));
        ArithOp op;
        myread(&op, sizeof(ArithOp));
        uint size;
        myread(&size, sizeof(uint));
-       Vector<Set*> domains;
-       for(uint i=0; i<size; i++){
-               Setdomain;
-               myread(&domain, sizeof(Set*));
+       Vector<Set *> domains;
+       for (uint i = 0; i < size; i++) {
+               Set *domain;
+               myread(&domain, sizeof(Set *));
                ASSERT(map.contains(domain));
-               domain = (Set*) map.get(domain);
+               domain = (Set *) map.get(domain);
                domains.push(domain);
        }
-       Setrange;
-       myread(&range, sizeof(Set*));
+       Set *range;
+       myread(&range, sizeof(Set *));
        ASSERT(map.contains(range));
-       range = (Set*) map.get(range);
+       range = (Set *) map.get(range);
        OverFlowBehavior overflowbehavior;
        myread(&overflowbehavior, sizeof(OverFlowBehavior));
        map.put(fo_ptr, solver->createFunctionOperator(op, domains.expose(), size, range, overflowbehavior));
 }
 
-void Deserializer::deserializeFunctionTable(){
+void Deserializer::deserializeFunctionTable() {
        FunctionTable *ft_ptr;
        myread(&ft_ptr, sizeof(FunctionTable *));
-       Tabletable;
-       myread(&table, sizeof(Table*));
+       Table *table;
+       myread(&table, sizeof(Table *));
        ASSERT(map.contains(table));
-       table = (Table*) map.get(table);
+       table = (Table *) map.get(table);
        UndefinedBehavior undefinedbehavior;
        myread(&undefinedbehavior, sizeof(UndefinedBehavior));
-       
+
        map.put(ft_ptr, solver->completeTable(table, undefinedbehavior));
 }
\ No newline at end of file
index 057346d..6335c89 100644 (file)
@@ -1,5 +1,5 @@
 
-/* 
+/*
  * File:   deserializer.h
  * Author: hamed
  *
 /**
  * Style of serialized file:
  * ASTNodeType#Pointer#ObjectDATA
- * 
+ *
  * @param file
  */
 class Deserializer {
 public:
-       Deserializer(const charfile);
+       Deserializer(const char *file);
        CSolver *deserialize();
        virtual ~Deserializer();
 private:
@@ -44,5 +44,5 @@ private:
        CloneMap map;
 };
 
-#endif /* DESERIALIZER_H */
+#endif/* DESERIALIZER_H */
 
index b49b98b..810ece8 100644 (file)
@@ -1,8 +1,8 @@
 
-/* 
+/*
  * File:   serializer.cc
  * Author: hamed
- * 
+ *
  * Created on September 7, 2017, 3:38 PM
  */
 
 
 Serializer::Serializer(const char *file) {
        filedesc = open(file, O_WRONLY | O_CREAT | O_TRUNC, 0666);
+
        if (filedesc < 0) {
                exit(-1);
        }
 }
 
 Serializer::~Serializer() {
-       if (-1 == close(filedesc)){
+       if (-1 == close(filedesc)) {
                exit(-1);
        }
 }
 
-void Serializer::mywrite(const void *__buf, size_t __n){
+void Serializer::mywrite(const void *__buf, size_t __n) {
        write (filedesc, __buf, __n);
 }
 
 
-void serializeBooleanEdge(Serializer* serializer, BooleanEdge be){
-       if(be == BooleanEdge(NULL))
+void serializeBooleanEdge(Serializer *serializer, BooleanEdge be) {
+       if (be == BooleanEdge(NULL))
                return;
        be.getBoolean()->serialize(serializer);
        ASTNodeType type = BOOLEANEDGE;
        serializer->mywrite(&type, sizeof(ASTNodeType));
-       Booleanboolean = be.getRaw();
-       serializer->mywrite(&boolean, sizeof(Boolean*));
+       Boolean *boolean = be.getRaw();
+       serializer->mywrite(&boolean, sizeof(Boolean *));
 }
\ No newline at end of file
index e6d2b50..f147773 100644 (file)
@@ -1,5 +1,5 @@
 
-/* 
+/*
  * File:   serializer.h
  * Author: hamed
  *
@@ -26,14 +26,14 @@ private:
        CloneMap map;
 };
 
-inline bool Serializer::isSerialized(void* obj){
+inline bool Serializer::isSerialized(void *obj) {
        return map.contains(obj);
 }
 
 
 
 
-void serializeBooleanEdge(Serializerserializer, BooleanEdge be);
+void serializeBooleanEdge(Serializer *serializer, BooleanEdge be);
 
-#endif /* SERIALIZER_H */
+#endif/* SERIALIZER_H */
 
index 52707c5..208d9a9 100644 (file)
@@ -13,8 +13,8 @@
  * 8=>9
  * 9=>2
  * 6=>2
- * 
- * 
+ *
+ *
  */
 int main(int numargs, char **argv) {
        CSolver *solver = new CSolver();
@@ -22,110 +22,110 @@ int main(int numargs, char **argv) {
        Set *s = solver->createSet(0, set1, 10);
        Order *order = solver->createOrder(SATC_TOTAL, s);
        BooleanEdge b01 =  solver->orderConstraint(order, 0, 1);
-        solver->addConstraint(b01);
+       solver->addConstraint(b01);
        BooleanEdge b12 =  solver->orderConstraint(order, 1, 2);
-        solver->addConstraint(b12);
+       solver->addConstraint(b12);
        BooleanEdge b23 =  solver->orderConstraint(order, 2, 3);
-        solver->addConstraint(b23);
+       solver->addConstraint(b23);
        BooleanEdge b14 =  solver->orderConstraint(order, 1, 4);
-        solver->addConstraint(b14);
+       solver->addConstraint(b14);
        BooleanEdge b45 =  solver->orderConstraint(order, 4, 5);
-        solver->addConstraint(b45);
+       solver->addConstraint(b45);
        BooleanEdge b56 =  solver->orderConstraint(order, 5, 6);
-        solver->addConstraint(b56);
+       solver->addConstraint(b56);
        BooleanEdge b17 =  solver->orderConstraint(order, 1, 7);
-        solver->addConstraint(b17);
+       solver->addConstraint(b17);
        BooleanEdge b78 =  solver->orderConstraint(order, 7, 8);
-        solver->addConstraint(b78);
+       solver->addConstraint(b78);
        BooleanEdge b89 =  solver->orderConstraint(order, 8, 9);
-        solver->addConstraint(b89);
+       solver->addConstraint(b89);
        BooleanEdge b92 =  solver->orderConstraint(order, 9, 2);
-        solver->addConstraint(b92);
+       solver->addConstraint(b92);
        BooleanEdge b62 =  solver->orderConstraint(order, 6, 2);
-        solver->addConstraint(b62);
+       solver->addConstraint(b62);
 
-        BooleanEdge v1 = solver->getBooleanVar(0);
-        solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v1));
-        BooleanEdge v2 = solver->getBooleanVar(0);
-        solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v2));
-        BooleanEdge v3 = solver->getBooleanVar(0);
-        BooleanEdge v4 = solver->getBooleanVar(0);
-        BooleanEdge v5 = solver->getBooleanVar(0);
-        solver->addConstraint(
-                solver->applyLogicalOperation(SATC_OR, 
-                solver->applyLogicalOperation(SATC_IFF, v3, v4),
-                v5));
-        solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v5));
-        BooleanEdge v6 = solver->getBooleanVar(0);
-        BooleanEdge v7 = solver->getBooleanVar(0);
-        BooleanEdge v8 = solver->getBooleanVar(0);
-        solver->addConstraint(
-                solver->applyLogicalOperation(SATC_OR, 
-                solver->applyLogicalOperation(SATC_IFF, v7, v8),
-                v6));
+       BooleanEdge v1 = solver->getBooleanVar(0);
+       solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v1));
+       BooleanEdge v2 = solver->getBooleanVar(0);
+       solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v2));
+       BooleanEdge v3 = solver->getBooleanVar(0);
+       BooleanEdge v4 = solver->getBooleanVar(0);
+       BooleanEdge v5 = solver->getBooleanVar(0);
+       solver->addConstraint(
+               solver->applyLogicalOperation(SATC_OR,
+                                                                                                                                       solver->applyLogicalOperation(SATC_IFF, v3, v4),
+                                                                                                                                       v5));
+       solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v5));
+       BooleanEdge v6 = solver->getBooleanVar(0);
+       BooleanEdge v7 = solver->getBooleanVar(0);
+       BooleanEdge v8 = solver->getBooleanVar(0);
+       solver->addConstraint(
+               solver->applyLogicalOperation(SATC_OR,
+                                                                                                                                       solver->applyLogicalOperation(SATC_IFF, v7, v8),
+                                                                                                                                       v6));
        solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v6));
-        BooleanEdge v9 = solver->getBooleanVar(0);
+       BooleanEdge v9 = solver->getBooleanVar(0);
        solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v9, v3));
-        BooleanEdge v10 = solver->getBooleanVar(0);
-        BooleanEdge v11 = solver->getBooleanVar(0);
-        BooleanEdge v12 = solver->getBooleanVar(0);
-        solver->addConstraint(
-                solver->applyLogicalOperation(SATC_OR, 
-                solver->applyLogicalOperation(SATC_OR, v10, v11),
-                solver->applyLogicalOperation(SATC_IFF, v1, v12)));
-        BooleanEdge b48 =  solver->orderConstraint(order, 4, 8);
-        solver->addConstraint(
-                solver->applyLogicalOperation(SATC_OR, 
-                solver->applyLogicalOperation(SATC_OR, v10, v11),
-                b48));
-        BooleanEdge v13 = solver->getBooleanVar(0);
-        BooleanEdge v14 = solver->getBooleanVar(0);
-        solver->addConstraint(
-                solver->applyLogicalOperation(SATC_OR, 
-                solver->applyLogicalOperation(SATC_IMPLIES, v10, v11),
-                solver->applyLogicalOperation(SATC_AND,
-                        solver->applyLogicalOperation(SATC_IFF, v12, v13),
-                        solver->applyLogicalOperation(SATC_NOT,b48))
-        ));
-        solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v11));
-        solver->addConstraint(v14);
-        solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v8, v12));
-        solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v12, v8));
-        BooleanEdge v15 = solver->getBooleanVar(0);
-        BooleanEdge v16 = solver->getBooleanVar(0);
-        BooleanEdge v17 = solver->getBooleanVar(0);
-        BooleanEdge v18 = solver->getBooleanVar(0);
-        solver->addConstraint(
-                solver->applyLogicalOperation(SATC_OR, 
-                solver->applyLogicalOperation(SATC_OR, v15, v16),
-                solver->applyLogicalOperation(SATC_IFF, v17, v2)
-        ));
-        BooleanEdge b57 =  solver->orderConstraint(order, 5, 7);
-        solver->addConstraint(
-                solver->applyLogicalOperation(SATC_IMPLIES, 
-                b57,
-                solver->applyLogicalOperation(SATC_OR, v15, v16)
-        ));
-        solver->addConstraint(
-                solver->applyLogicalOperation(SATC_IMPLIES, 
-                solver->applyLogicalOperation(SATC_AND, v15, solver->applyLogicalOperation(SATC_NOT,v16)),
-                solver->applyLogicalOperation(SATC_AND, b57, solver->applyLogicalOperation(SATC_IFF, v17, v14))
-        ));
-        solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v16));
-        solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v13, v17));
-        solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v17, v13));
-        solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v4, v17));
-        solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v17, v4));
-        solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v18, v9));
-        solver->addConstraint(v18);
-        
-        if (solver->solve() == 1){
+       BooleanEdge v10 = solver->getBooleanVar(0);
+       BooleanEdge v11 = solver->getBooleanVar(0);
+       BooleanEdge v12 = solver->getBooleanVar(0);
+       solver->addConstraint(
+               solver->applyLogicalOperation(SATC_OR,
+                                                                                                                                       solver->applyLogicalOperation(SATC_OR, v10, v11),
+                                                                                                                                       solver->applyLogicalOperation(SATC_IFF, v1, v12)));
+       BooleanEdge b48 =  solver->orderConstraint(order, 4, 8);
+       solver->addConstraint(
+               solver->applyLogicalOperation(SATC_OR,
+                                                                                                                                       solver->applyLogicalOperation(SATC_OR, v10, v11),
+                                                                                                                                       b48));
+       BooleanEdge v13 = solver->getBooleanVar(0);
+       BooleanEdge v14 = solver->getBooleanVar(0);
+       solver->addConstraint(
+               solver->applyLogicalOperation(SATC_OR,
+                                                                                                                                       solver->applyLogicalOperation(SATC_IMPLIES, v10, v11),
+                                                                                                                                       solver->applyLogicalOperation(SATC_AND,
+                                                                                                                                                                                                                                                               solver->applyLogicalOperation(SATC_IFF, v12, v13),
+                                                                                                                                                                                                                                                               solver->applyLogicalOperation(SATC_NOT,b48))
+                                                                                                                                       ));
+       solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v11));
+       solver->addConstraint(v14);
+       solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v8, v12));
+       solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v12, v8));
+       BooleanEdge v15 = solver->getBooleanVar(0);
+       BooleanEdge v16 = solver->getBooleanVar(0);
+       BooleanEdge v17 = solver->getBooleanVar(0);
+       BooleanEdge v18 = solver->getBooleanVar(0);
+       solver->addConstraint(
+               solver->applyLogicalOperation(SATC_OR,
+                                                                                                                                       solver->applyLogicalOperation(SATC_OR, v15, v16),
+                                                                                                                                       solver->applyLogicalOperation(SATC_IFF, v17, v2)
+                                                                                                                                       ));
+       BooleanEdge b57 =  solver->orderConstraint(order, 5, 7);
+       solver->addConstraint(
+               solver->applyLogicalOperation(SATC_IMPLIES,
+                                                                                                                                       b57,
+                                                                                                                                       solver->applyLogicalOperation(SATC_OR, v15, v16)
+                                                                                                                                       ));
+       solver->addConstraint(
+               solver->applyLogicalOperation(SATC_IMPLIES,
+                                                                                                                                       solver->applyLogicalOperation(SATC_AND, v15, solver->applyLogicalOperation(SATC_NOT,v16)),
+                                                                                                                                       solver->applyLogicalOperation(SATC_AND, b57, solver->applyLogicalOperation(SATC_IFF, v17, v14))
+                                                                                                                                       ));
+       solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v16));
+       solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v13, v17));
+       solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v17, v13));
+       solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v4, v17));
+       solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v17, v4));
+       solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v18, v9));
+       solver->addConstraint(v18);
+
+       if (solver->solve() == 1) {
                printf("SAT\n");
-               printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n", 
-                       solver->getOrderConstraintValue(order, 5, 1), 
-                       solver->getOrderConstraintValue(order, 1, 4),
-                       solver->getOrderConstraintValue(order, 5, 4),
-                       solver->getOrderConstraintValue(order, 1, 5));
+               printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n",
+                                        solver->getOrderConstraintValue(order, 5, 1),
+                                        solver->getOrderConstraintValue(order, 1, 4),
+                                        solver->getOrderConstraintValue(order, 5, 4),
+                                        solver->getOrderConstraintValue(order, 1, 5));
        } else {
                printf("UNSAT\n");
        }
index 8780b27..1d1124c 100644 (file)
@@ -13,8 +13,8 @@
  * 8=>9
  * 9=>2
  * 6=>2
- * 
- * 
+ *
+ *
  */
 int main(int numargs, char **argv) {
        CSolver *solver = new CSolver();
@@ -53,11 +53,11 @@ int main(int numargs, char **argv) {
        BooleanEdge b57 =  solver->orderConstraint(order, 5, 7);
        solver->addConstraint(b57);
 
-       
-       if (solver->solve() == 1){
+
+       if (solver->solve() == 1) {
                printf("SAT\n");
-               printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n", 
-                                        solver->getOrderConstraintValue(order, 5, 1), 
+               printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n",
+                                        solver->getOrderConstraintValue(order, 5, 1),
                                         solver->getOrderConstraintValue(order, 1, 4),
                                         solver->getOrderConstraintValue(order, 5, 4),
                                         solver->getOrderConstraintValue(order, 1, 5));
index e2c46e0..148235a 100644 (file)
@@ -17,13 +17,13 @@ int main(int numargs, char **argv) {
        solver->addConstraint(solver->applyLogicalOperation(SATC_OR, b1, solver->applyLogicalOperation(SATC_NOT, b2)));
        solver->addConstraint(solver->applyLogicalOperation(SATC_OR, b2, solver->applyLogicalOperation(SATC_NOT, b1)));
        solver->serialize();
-       if (solver->solve() == 1){
+       if (solver->solve() == 1) {
                printf("SAT\n");
-               printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n", 
-                       solver->getOrderConstraintValue(order, 5, 1), 
-                       solver->getOrderConstraintValue(order, 1, 4),
-                       solver->getOrderConstraintValue(order, 5, 4),
-                       solver->getOrderConstraintValue(order, 1, 5));
+               printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n",
+                                        solver->getOrderConstraintValue(order, 5, 1),
+                                        solver->getOrderConstraintValue(order, 1, 4),
+                                        solver->getOrderConstraintValue(order, 5, 4),
+                                        solver->getOrderConstraintValue(order, 1, 5));
        } else {
                printf("UNSAT\n");
        }
index 8a177fa..64ebc34 100644 (file)
@@ -51,12 +51,12 @@ bool DecomposeOrderResolver::resolveOrder(uint64_t first, uint64_t second) {
        }
 }
 
-bool DecomposeOrderResolver::resolvePartialOrder(OrderNode* first, OrderNode* second){
-       if(first->sccNum > second->sccNum){
+bool DecomposeOrderResolver::resolvePartialOrder(OrderNode *first, OrderNode *second) {
+       if (first->sccNum > second->sccNum) {
                return false;
        } else {
                return graph->isTherePath(first, second);
        }
-               
+
 }
 
index f1d06c6..1f3b266 100644 (file)
@@ -17,7 +17,7 @@ class DecomposeOrderResolver : public OrderResolver {
 public:
        DecomposeOrderResolver(OrderGraph *graph, Vector<Order *> &orders);
        bool resolveOrder(uint64_t first, uint64_t second);
-       bool resolvePartialOrder(OrderNode* first, OrderNode* second);
+       bool resolvePartialOrder(OrderNode *first, OrderNode *second);
        virtual ~DecomposeOrderResolver();
 private:
        OrderGraph *graph;
index e32a757..6044e06 100644 (file)
@@ -38,7 +38,7 @@ bool OrderPairResolver::resolveOrder(uint64_t first, uint64_t second) {
                ASSERT(to != NULL);
 
                OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to);
-               
+
                if (edge != NULL && edge->mustPos) {
                        return true;
                } else if ( edge != NULL && edge->mustNeg) {
index dde7378..79212ae 100644 (file)
@@ -15,13 +15,13 @@ class OrderPairResolver : public OrderResolver {
 public:
        OrderPairResolver(CSolver *_solver, Order *_order);
        bool resolveOrder(uint64_t first, uint64_t second);
-       HashtableOrderPairgetOrderPairTable() { return orderPairTable;}
+       HashtableOrderPair *getOrderPairTable() { return orderPairTable;}
        virtual ~OrderPairResolver();
 private:
        CSolver *solver;
        Order *order;
        HashtableOrderPair *orderPairTable;
-       
+
        bool getOrderConstraintValue(uint64_t first, uint64_t second);
 };
 
index 3e95860..c119597 100644 (file)
@@ -54,9 +54,9 @@ unsigned int tunableSettingHash(TunableSetting *setting) {
 
 bool tunableSettingEquals(TunableSetting *setting1, TunableSetting *setting2) {
        return setting1->hasVar == setting2->hasVar &&
-               setting1->type1 == setting2->type1 &&
-               setting1->type2 == setting2->type2 &&
-               setting1->param == setting2->param;
+                                setting1->type1 == setting2->type1 &&
+                                setting1->type2 == setting2->type2 &&
+                                setting1->param == setting2->param;
 }
 
 SearchTuner::SearchTuner() {
@@ -110,7 +110,7 @@ int SearchTuner::getVarTunable(VarType vartype1, VarType vartype2, TunableParam
                result = settings.get(&setting);
                if ( result == NULL) {
                        result = new
-                               TunableSetting(vartype1, vartype2, param);
+                                                        TunableSetting(vartype1, vartype2, param);
                        uint value = descriptor->lowValue + (random() % (1 + descriptor->highValue - descriptor->lowValue));
                        result->setDecision(descriptor->lowValue, descriptor->highValue, descriptor->defaultValue, value);
                        settings.add(result);
index a15f7df..52c0b5f 100644 (file)
 #include "time.h"
 
 /*
-       extern int model_out;
-       extern int model_err;
-       extern int switch_alloc;
-       
      #define model_dprintf(fd, fmt, ...) do { switch_alloc = 1; dprintf(fd, fmt, ## __VA_ARGS__); switch_alloc = 0; } while (0)
      #define model_print(fmt, ...) do { printf(fmt, ## __VA_ARGS__); } while (0)
      #define model_println(fmt, ...) do { model_print(fmt, ## __VA_ARGS__); model_print("\n");} while(0)
      #define model_print(fmt, ...) do { model_dprintf(model_out, fmt, ## __VA_ARGS__); } while (0)
      #define model_print_err(fmt, ...) do { model_dprintf(model_err, fmt, ## __VA_ARGS__); } while (0)
+   extern int model_out;
+   extern int model_err;
+   extern int switch_alloc;
+
+ #define model_dprintf(fd, fmt, ...) do { switch_alloc = 1; dprintf(fd, fmt, ## __VA_ARGS__); switch_alloc = 0; } while (0)
+ #define model_print(fmt, ...) do { printf(fmt, ## __VA_ARGS__); } while (0)
+ #define model_println(fmt, ...) do { model_print(fmt, ## __VA_ARGS__); model_print("\n");} while(0)
+
+ #define model_print(fmt, ...) do { model_dprintf(model_out, fmt, ## __VA_ARGS__); } while (0)
+
+ #define model_print_err(fmt, ...) do { model_dprintf(model_err, fmt, ## __VA_ARGS__); } while (0)
  */
 
 #define model_print printf
index 592d1d5..0988a57 100644 (file)
@@ -103,7 +103,7 @@ void CSolver::serialize() {
                Deserializer deserializer("dump");
                deserializer.deserialize();
        }
-       
+
 }
 
 Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) {
@@ -118,7 +118,7 @@ Set *CSolver::createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange
        return set;
 }
 
-VarType CSolver::getSetVarType(Set *set){
+VarType CSolver::getSetVarType(Set *set) {
        return set->getType();
 }
 
@@ -143,7 +143,7 @@ uint64_t CSolver::createUniqueItem(MutableSet *set) {
        return element;
 }
 
-void CSolver::finalizeMutableSet(MutableSet* set){
+void CSolver::finalizeMutableSet(MutableSet *set) {
        set->finalize();
 }
 
@@ -153,7 +153,7 @@ Element *CSolver::getElementVar(Set *set) {
        return element;
 }
 
-Set* CSolver::getElementRange (Element* element){
+Set *CSolver::getElementRange (Element *element) {
        return element->getRange();
 }
 
@@ -260,11 +260,11 @@ BooleanEdge CSolver::applyPredicateTable(Predicate *predicate, Element **inputs,
 }
 
 bool CSolver::isTrue(BooleanEdge b) {
-        return b.isNegated()?b->isFalse():b->isTrue();
+       return b.isNegated() ? b->isFalse() : b->isTrue();
 }
 
 bool CSolver::isFalse(BooleanEdge b) {
-        return b.isNegated()?b->isTrue():b->isFalse();
+       return b.isNegated() ? b->isTrue() : b->isFalse();
 }
 
 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg1, BooleanEdge arg2) {
@@ -279,7 +279,7 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg) {
 
 static int ptrcompares(const void *p1, const void *p2) {
        uintptr_t b1 = *(uintptr_t const *) p1;
-  uintptr_t b2 = *(uintptr_t const *) p2;
+       uintptr_t b2 = *(uintptr_t const *) p2;
        if (b1 < b2)
                return -1;
        else if (b1 == b2)
@@ -288,11 +288,11 @@ static int ptrcompares(const void *p1, const void *p2) {
                return 1;
 }
 
-BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge * array, uint asize) {
+BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
        BooleanEdge newarray[asize];
        memcpy(newarray, array, asize * sizeof(BooleanEdge));
-       for(uint i=0; i < asize; i++) {
-               BooleanEdge b=newarray[i];
+       for (uint i = 0; i < asize; i++) {
+               BooleanEdge b = newarray[i];
                if (b->type == LOGICOP) {
                        if (((BooleanLogic *) b.getBoolean())->replaced) {
                                newarray[i] = doRewrite(newarray[i]);
@@ -312,14 +312,14 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
        case SATC_IFF: {
                for (uint i = 0; i < 2; i++) {
                        if (array[i]->type == BOOLCONST) {
-                               if (isTrue(array[i])) { // It can be undefined
+                               if (isTrue(array[i])) { // It can be undefined
                                        return array[1 - i];
-                               } else if(isFalse(array[i])) {
+                               } else if (isFalse(array[i])) {
                                        newarray[0] = array[1 - i];
                                        return applyLogicalOperation(SATC_NOT, newarray, 1);
                                }
                        } else if (array[i]->type == LOGICOP) {
-                               BooleanLogic *b =(BooleanLogic *)array[i].getBoolean();
+                               BooleanLogic *b = (BooleanLogic *)array[i].getBoolean();
                                if (b->replaced) {
                                        return rewriteLogicalOperation(op, array, asize);
                                }
@@ -328,7 +328,7 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
                break;
        }
        case SATC_OR: {
-               for (uint i =0; i <asize; i++) {
+               for (uint i = 0; i < asize; i++) {
                        newarray[i] = applyLogicalOperation(SATC_NOT, array[i]);
                }
                return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_AND, newarray, asize));
@@ -344,9 +344,9 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
                        if (b->type == BOOLCONST) {
                                if (isTrue(b))
                                        continue;
-                               else{
+                               else {
                                        return boolFalse;
-                                }
+                               }
                        } else
                                newarray[newindex++] = b;
                }
@@ -393,21 +393,21 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
 }
 
 void CSolver::addConstraint(BooleanEdge constraint) {
-       if(constraint.isNegated())
+       if (constraint.isNegated())
                model_print("!");
        constraint.getBoolean()->print();
        if (isTrue(constraint))
                return;
        else if (isFalse(constraint)) {
-               int t=0;
+               int t = 0;
                setUnSAT();
        }
        else {
                if (constraint->type == LOGICOP) {
-                       BooleanLogic *b=(BooleanLogic *) constraint.getBoolean();
+                       BooleanLogic *b = (BooleanLogic *) constraint.getBoolean();
                        if (!constraint.isNegated()) {
-                               if (b->op==SATC_AND) {
-                                       for(uint i=0;i<b->inputs.getSize();i++) {
+                               if (b->op == SATC_AND) {
+                                       for (uint i = 0; i < b->inputs.getSize(); i++) {
                                                addConstraint(b->inputs.get(i));
                                        }
                                        return;
@@ -419,12 +419,12 @@ void CSolver::addConstraint(BooleanEdge constraint) {
                        }
                }
                constraints.add(constraint);
-               Boolean *ptr=constraint.getBoolean();
-               
+               Boolean *ptr = constraint.getBoolean();
+
                if (ptr->boolVal == BV_UNSAT) {
                        setUnSAT();
                }
-               
+
                replaceBooleanWithTrueNoRemove(constraint);
                constraint->parents.clear();
        }
@@ -449,7 +449,7 @@ int CSolver::solve() {
 
        Preprocess pp(this);
        pp.doTransform();
-       
+
        DecomposeOrderTransform dot(this);
        dot.doTransform();
 
@@ -459,12 +459,12 @@ int CSolver::solve() {
        EncodingGraph eg(this);
        eg.buildGraph();
        eg.encode();
-       
+
        naiveEncodingDecision(this);
        satEncoder->encodeAllSATEncoder(this);
-        model_print("Is problem UNSAT after encoding: %d\n", unsat);
+       model_print("Is problem UNSAT after encoding: %d\n", unsat);
        int result = unsat ? IS_UNSAT : satEncoder->solve();
-        model_print("Result Computed in CSolver: %d\n", result);
+       model_print("Result Computed in CSolver: %d\n", result);
        long long finishTime = getTimeNano();
        elapsedTime = finishTime - startTime;
        if (deleteTuner) {
@@ -487,7 +487,7 @@ uint64_t CSolver::getElementValue(Element *element) {
 }
 
 bool CSolver::getBooleanValue(BooleanEdge bedge) {
-       Boolean *boolean=bedge.getBoolean();
+       Boolean *boolean = bedge.getBoolean();
        switch (boolean->type) {
        case BOOLEANVAR:
                return getBooleanVariableValueSATTranslator(this, boolean);
index 41c4627..71ee874 100644 (file)
@@ -20,7 +20,7 @@ public:
        Set *createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange);
 
        VarType getSetVarType(Set *set);
-       
+
        Element *createRangeVar(VarType type, uint64_t lowrange, uint64_t highrange);
 
        /** This function creates a mutable set. */
@@ -37,11 +37,11 @@ public:
            items to the set. */
 
        uint64_t createUniqueItem(MutableSet *set);
-       
+
        /**
         * Freeze and finalize the mutableSet ...
         */
-       void finalizeMutableSet(MutableSetset);
+       void finalizeMutableSet(MutableSet *set);
 
        /** This function creates an element variable over a set. */
 
@@ -49,8 +49,8 @@ public:
 
        /** This function creates an element constrant. */
        Element *getElementConst(VarType type, uint64_t value);
-       
-       Set* getElementRange (Element* element);
+
+       Set *getElementRange (Element *element);
 
        BooleanEdge getBooleanTrue();
 
@@ -136,11 +136,11 @@ public:
        bool isUnSAT() { return unsat; }
 
        Vector<Order *> *getOrders() { return &allOrders;}
-       HashsetOrder * getActiveOrders() { return &activeOrders;}
+       HashsetOrder *getActiveOrders() { return &activeOrders;}
 
        Tuner *getTuner() { return tuner; }
 
-       SetIteratorBooleanEdge * getConstraints() { return constraints.iterator(); }
+       SetIteratorBooleanEdge *getConstraints() { return constraints.iterator(); }
 
        SATEncoder *getSATEncoder() {return satEncoder;}
 
@@ -189,7 +189,7 @@ private:
        Vector<Order *> allOrders;
 
        HashsetOrder activeOrders;
-       
+
        /** This is a vector of all function structs that we have allocated. */
        Vector<Function *> allFunctions;
 
index 7c63aa1..9708936 100644 (file)
    void ourfree(void *ptr);
    void * ourcalloc(size_t count, size_t size);
    void * ourrealloc(void *ptr, size_t size);
-*/
+ */
 
 #if 0
-void * model_malloc(size_t size);
+void *model_malloc(size_t size);
 void model_free(void *ptr);
-void * model_calloc(size_t count, size_t size);
-void * model_realloc(void *ptr, size_t size);
+void *model_calloc(size_t count, size_t size);
+void *model_realloc(void *ptr, size_t size);
 
 
 #define ourmalloc model_malloc