fix tabbing

diff --git a/src/AST/element.cc b/src/AST/element.cc
index 8044966070f70bf13045bbdd2d52499e2ffe482d..4fc9f4b37d08a2e4290cef2b078d72290d8e79b3 100644 (file)
--- a/src/AST/element.cc
+++ b/src/AST/element.cc
@@ -10,7 +10,7 @@ Element::Element(ASTNodeType _type) :
        ASTNode(_type),
        encoding(this),
        anyValue(false),
-       frozen(false){
+       frozen(false) {
 }
 
 ElementSet::ElementSet(Set *s) :

diff --git a/src/AST/element.h b/src/AST/element.h
index 166078af6c6f08d730d59b44dc00c381dbc71450..53f6008594fcf8858a07859a49486671e39549a0 100644 (file)
--- a/src/AST/element.h
+++ b/src/AST/element.h
@@ -15,8 +15,8 @@ public:
        Vector<ASTNode *> parents;
        ElementEncoding encoding;
        inline ElementEncoding *getElementEncoding() { return &encoding; }
-       inline void freezeElement(){frozen = true;}
-       inline bool isFrozen(){return frozen;}
+       inline void freezeElement() {frozen = true;}
+       inline bool isFrozen() {return frozen;}
        virtual Element *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;};
        virtual void serialize(Serializer *serializer) = 0;
        virtual void print() = 0;

diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index 621d2a8c927ee9d10d81315c7dab1f25192d1879..25c5ec87ee2147cc46d697156684f018e54b0321 100644 (file)
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -25,7 +25,7 @@ void IntegerEncodingTransform::doTransform() {
        while (orderit->hasNext()) {
                Order *order = orderit->next();
                if (order->type == SATC_PARTIAL)
-                 continue;
+                       continue;
                if (GETVARTUNABLE(solver->getTuner(), order->set->type, ORDERINTEGERENCODING, &offon))
                        integerEncode(order);
        }

diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
index 52461012e1d4c36162651ebd06e55ce69c597b51..27de0649aea4893bd5f9c3b7dc3dcb257b9ad321 100644 (file)
--- a/src/Backend/constraint.cc
+++ b/src/Backend/constraint.cc
@@ -589,7 +589,7 @@ void addClause(CNF *cnf, uint numliterals, int *literals) {
        addArrayClauseLiteral(cnf->solver, numliterals, literals);
 }
 
-void freezeVariable(CNF *cnf, Edge e){
+void freezeVariable(CNF *cnf, Edge e) {
        int literal = getEdgeVar(e);
        freeze(cnf->solver, literal);
 }

diff --git a/src/Backend/inc_solver.cc b/src/Backend/inc_solver.cc
index 72d34083dcd4b096b32aee4b51816a361f708600..a89ed8b86de8af3d7724bd21a265249af290dbd7 100644 (file)
--- a/src/Backend/inc_solver.cc
+++ b/src/Backend/inc_solver.cc
@@ -102,7 +102,7 @@ int getSolution(IncrementalSolver *This) {
                }
                readSolver(This, &This->solution[1], numVars * sizeof(int));
                This->solutionsize = numVars;
-       } else { //Reading unsat explanation
+       } else {//Reading unsat explanation
                int numVars = readIntSolver(This);
                if (numVars > This->solutionsize) {
                        if (This->solution != NULL)

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index aa739242d002acb28330e6112a6f702ec7548b41..b380c3a78116387eb470362e2692331aa42959b0 100644 (file)
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -220,9 +220,9 @@ void SATEncoder::generateBinaryValueEncodingVars(ElementEncoding *encoding) {
                generateAnyValueBinaryValueEncoding(encoding);
 }
 
-void SATEncoder::freezeElementVariables(ElementEncoding *encoding){
+void SATEncoder::freezeElementVariables(ElementEncoding *encoding) {
        ASSERT(encoding->element->frozen);
-       for(uint i=0; i< encoding->numVars; i++){
+       for (uint i = 0; i < encoding->numVars; i++) {
                Edge e = encoding->variables[i];
                ASSERT(edgeIsVarConst(e));
                freezeVariable(cnf, e);

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
old mode 100755 (executable)
new mode 100644 (file)
index 5312b4f..2e09491
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -34,7 +34,7 @@ int SATEncoder::solve(long timeout) {
        long long startTime = getTimeNano();
        finishedClauses(cnf->solver);
        cnf->encodeTime = getTimeNano() - startTime;
-       if(solver->isIncrementalMode()){
+       if (solver->isIncrementalMode()) {
                solver->freezeElementsVariables();
        }
        return solveCNF(cnf);
@@ -47,7 +47,7 @@ void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
        SetIteratorBooleanEdge *iterator = csolver->getConstraints();
        while (iterator->hasNext()) {
                BooleanEdge constraint = iterator->next();
-               if(!csolver->isConstraintEncoded(constraint)){
+               if (!csolver->isConstraintEncoded(constraint)) {
                        Edge c = encodeConstraintSATEncoder(constraint);
                        addConstraintCNF(cnf, c);
                        csolver->addEncodedConstraint(constraint);

diff --git a/src/Collections/vector.h b/src/Collections/vector.h
index 2dd5e694e2689f72926af3758650c4f7e24587c8..6c532532c8e39a3f115c61900d7fdfa0bfc894ce 100644 (file)
--- a/src/Collections/vector.h
+++ b/src/Collections/vector.h
@@ -9,9 +9,9 @@
                type *array;                                                       \
        };                                                                    \
        typedef struct Vector ## name Vector ## name;                         \
-       Vector ## name *allocVector ## name(uint capacity);                  \
-       Vector ## name *allocDefVector ## name();                            \
-       Vector ## name *allocVectorArray ## name(uint capacity, type * array); \
+       Vector ## name * allocVector ## name(uint capacity);                  \
+       Vector ## name * allocDefVector ## name();                            \
+       Vector ## name * allocVectorArray ## name(uint capacity, type * array); \
        void pushVector ## name(Vector ## name * vector, type item);           \
        type lastVector ## name(Vector ## name * vector);                      \
        void popVector ## name(Vector ## name * vector);                       \
@@ -29,18 +29,18 @@
        void initVectorArray ## name(Vector ## name * vector, uint capacity, type * array);
 
 #define VectorImpl(name, type, defcap)                                  \
-       Vector ## name *allocDefVector ## name() {                           \
+       Vector ## name * allocDefVector ## name() {                           \
                return allocVector ## name(defcap);                                 \
        }                                                                     \
-       Vector ## name *allocVector ## name(uint capacity) {                 \
-               Vector ## name *tmp = (Vector ## name *)ourmalloc(sizeof(Vector ## name));  \
+       Vector ## name * allocVector ## name(uint capacity) {                 \
+               Vector ## name * tmp = (Vector ## name *)ourmalloc(sizeof(Vector ## name));  \
                tmp->size = 0;                                                      \
                tmp->capacity = capacity;                                           \
                tmp->array = (type *) ourmalloc(sizeof(type) * capacity);           \
                return tmp;                                                         \
        }                                                                     \
-       Vector ## name *allocVectorArray ## name(uint capacity, type * array)  { \
-               Vector ## name *tmp = allocVector ## name(capacity);               \
+       Vector ## name * allocVectorArray ## name(uint capacity, type * array)  { \
+               Vector ## name * tmp = allocVector ## name(capacity);               \
                tmp->size = capacity;                                                 \
                memcpy(tmp->array, array, capacity * sizeof(type));                 \
                return tmp;                                                         \

diff --git a/src/Test/incrementaltest.cc b/src/Test/incrementaltest.cc
index c71645db5cb2e5d313bf84c5bd18d9090f8867de..e559630415a9f5768cbfa3a28128b96121b34ee8 100644 (file)
--- a/src/Test/incrementaltest.cc
+++ b/src/Test/incrementaltest.cc
@@ -17,21 +17,21 @@ int main(int numargs, char **argv) {
        solver->addConstraint(b);
        solver->freezeElement(e1);
        solver->freezeElement(e2);
-       if (solver->solve() == 1){
+       if (solver->solve() == 1) {
                int run = 1;
-               do{
+               do {
                        printf("result %d: e1=%" PRIu64 " e2=%" PRIu64 "\n", run, solver->getElementValue(e1), solver->getElementValue(e2));
-                       for(int i=0; i< INPUTSIZE; i++){
+                       for (int i = 0; i < INPUTSIZE; i++) {
                                uint64_t val = solver->getElementValue(inputs[i]);
                                Element *econst = solver->getElementConst(0, val);
-                               Element * tmpInputs[] = {inputs[i], econst};
+                               Element *tmpInputs[] = {inputs[i], econst};
                                BooleanEdge b = solver->applyPredicate(equals, tmpInputs, INPUTSIZE);
                                solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, b));
                        }
                        run++;
-               }while(solver->solveIncremental() == 1);
+               } while (solver->solveIncremental() == 1);
                printf("After %d runs, there are no more models to find ...\n", run);
-       }else{
+       } else {
                printf("UNSAT\n");
        }
        delete solver;

diff --git a/src/Tuner/basictuner.cc b/src/Tuner/basictuner.cc
index 7d08098148c4db28c5c92b5eb495b42ab45d98eb..44cd2bc8b3eee8b0b7479e8a2062397946c4caf7 100644 (file)
--- a/src/Tuner/basictuner.cc
+++ b/src/Tuner/basictuner.cc
@@ -182,10 +182,10 @@ long long BasicTuner::evaluate(Problem *problem, TunerRecord *tuner) {
                updateTimeout(problem, metric);
                snprintf(buffer, sizeof(buffer), "tuner%uused", execnum);
                tuner->getTuner()->addUsed(buffer);
-       } else if (status == 124 << 8){ // timeout happens ...
+       } else if (status == 124 << 8) {// timeout happens ...
                tuner->getTuner()->copySettingstoUsedSettings();
        }
-       
+
        //Increment execution count
        execnum++;
 

diff --git a/src/ccsolver.cc b/src/ccsolver.cc
index fa2e3426211b50e34f786e506e865307d3aa2d04..aea2161e6da9eb5e8c62042a6c6f68ede22cb4cc 100644 (file)
--- a/src/ccsolver.cc
+++ b/src/ccsolver.cc
@@ -104,16 +104,16 @@ void *applyPredicate(void *solver,void *predicate, void **inputs, unsigned int n
 
 void *applyLogicalOperation(void *solver,unsigned int op, void **array, unsigned int asize) {
        BooleanEdge constr [asize];
-       for(uint i=0; i< asize; i++){
-               constr[i] = BooleanEdge((Boolean*)array[i]);
+       for (uint i = 0; i < asize; i++) {
+               constr[i] = BooleanEdge((Boolean *)array[i]);
        }
        return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, constr, (uint) asize).getRaw();
 }
 
 void *applyExactlyOneConstraint(void *solver, void **array, unsigned int asize) {
        BooleanEdge constr [asize];
-       for(uint i=0; i< asize; i++){
-               constr[i] = BooleanEdge((Boolean*)array[i]);
+       for (uint i = 0; i < asize; i++) {
+               constr[i] = BooleanEdge((Boolean *)array[i]);
        }
        return CCSOLVER(solver)->applyExactlyOneConstraint( constr, (uint) asize).getRaw();
 }

diff --git a/src/csolver.cc b/src/csolver.cc
index d1c6d33f202826cdb41807586c441efca6543c86..17b3dc31b565db26711b89aebba6f4b31aa420c0 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -243,10 +243,10 @@ void CSolver::mustHaveValue(Element *element) {
 }
 
 void CSolver::freezeElementsVariables() {
-       
-       for(uint i=0; i< allElements.getSize(); i++){
+
+       for (uint i = 0; i < allElements.getSize(); i++) {
                Element *e = allElements.get(i);
-               if(e->frozen){
+               if (e->frozen) {
                        satEncoder->freezeElementVariables(&e->encoding);
                }
        }
@@ -408,24 +408,24 @@ BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uin
        return applyLogicalOperation(op, newarray, asize);
 }
 
-BooleanEdge CSolver::applyExactlyOneConstraint (BooleanEdge *array, uint asize){
+BooleanEdge CSolver::applyExactlyOneConstraint (BooleanEdge *array, uint asize) {
        BooleanEdge newarray[asize + 1];
 
        newarray[asize] = applyLogicalOperation(SATC_OR, array, asize);
-       for (uint i=0; i< asize; i++){
+       for (uint i = 0; i < asize; i++) {
                BooleanEdge oprand1 = array[i];
-               BooleanEdge carray [asize -1];
+               BooleanEdge carray [asize - 1];
                uint index = 0;
-               for( uint j =0; j< asize; j++){
-                       if(i != j){
+               for ( uint j = 0; j < asize; j++) {
+                       if (i != j) {
                                BooleanEdge oprand2 = applyLogicalOperation(SATC_NOT, array[j]);
                                carray[index++] = applyLogicalOperation(SATC_IMPLIES, oprand1, oprand2);
                        }
                }
-               ASSERT(index == asize -1);
-               newarray[i] = applyLogicalOperation(SATC_AND, carray, asize-1);
+               ASSERT(index == asize - 1);
+               newarray[i] = applyLogicalOperation(SATC_AND, carray, asize - 1);
        }
-       return applyLogicalOperation(SATC_AND, newarray, asize+1);
+       return applyLogicalOperation(SATC_AND, newarray, asize + 1);
 }
 
 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
@@ -640,8 +640,8 @@ int CSolver::solveIncremental() {
        if (isUnSAT()) {
                return IS_UNSAT;
        }
-       
-       
+
+
        long long startTime = getTimeNano();
        bool deleteTuner = false;
        if (tuner == NULL) {
@@ -650,7 +650,7 @@ int CSolver::solveIncremental() {
        }
        int result = IS_INDETER;
        ASSERT (!useInterpreter());
-       
+
        computePolarities(this);
 //     long long time1 = getTimeNano();
 //     model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
@@ -670,7 +670,7 @@ int CSolver::solveIncremental() {
        //Doing element optimization on new constraints
 //     ElementOpt eop(this);
 //     eop.doTransform();
-       
+
        //Since no new element is added, we assuming adding new constraint
        //has no impact on previous encoding decisions
 //     EncodingGraph eg(this);
@@ -696,7 +696,7 @@ int CSolver::solveIncremental() {
        time2 = getTimeNano();
        elapsedTime = time2 - startTime;
        model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);
-       
+
        if (deleteTuner) {
                delete tuner;
                tuner = NULL;
@@ -770,7 +770,7 @@ int CSolver::solve() {
                model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
 
                model_print("Is problem UNSAT after encoding: %d\n", unsat);
-               
+
 
                result = unsat ? IS_UNSAT : satEncoder->solve(satsolverTimeout);
                model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT ? "SAT" : result == IS_INDETER ? "INDETERMINATE" : " UNSAT");
@@ -837,9 +837,9 @@ uint64_t CSolver::getElementValue(Element *element) {
        exit(-1);
 }
 
-void CSolver::freezeElement(Element *e){
+void CSolver::freezeElement(Element *e) {
        e->freezeElement();
-       if(!incrementalMode){
+       if (!incrementalMode) {
                incrementalMode = true;
        }
 }

diff --git a/src/csolver.h b/src/csolver.h
index 6996e4229c9376f78b5d4258ee7d2669f334b858..b27e3c00038d586908d6d17bb80f79a774b7eaed 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -58,7 +58,7 @@ public:
        Set *getElementRange (Element *element);
 
        void mustHaveValue(Element *element);
-       
+
        BooleanEdge getBooleanTrue();
 
        BooleanEdge getBooleanFalse();
@@ -103,9 +103,9 @@ public:
 
        /** This exactly one element of array can be true! (i.e. a1 + a2 + a3 + ... + an = 1)*/
        BooleanEdge applyExactlyOneConstraint (BooleanEdge *array, uint asize);
-       
+
        /** This function applies a logical operation to the Booleans in its input. */
-       
+
        BooleanEdge applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize);
 
        /** This function applies a logical operation to the Booleans in its input. */
@@ -133,15 +133,15 @@ public:
         * Incremental Solving for SATUNE.
         * It only supports incremental solving for elements!
         * No support for BooleanVar, BooleanOrder or using interpreters
-        * @return 
+        * @return
         */
        int solveIncremental();
-       
+
        /** After getting the solution from the SAT solver, client can get the value of an element via this function*/
        uint64_t getElementValue(Element *element);
 
        void freezeElement(Element *e);
-       
+
        /** After getting the solution from the SAT solver, client can get the value of a boolean via this function*/
        bool getBooleanValue(BooleanEdge boolean);
 
@@ -165,7 +165,7 @@ public:
        SetIteratorBooleanEdge *getConstraints() { return constraints.iterator(); }
        bool isConstraintEncoded(BooleanEdge be) { return encodedConstraints.contains(be);}
        void addEncodedConstraint(BooleanEdge be) {encodedConstraints.add(be);}
-       
+
        SATEncoder *getSATEncoder() {return satEncoder;}
 
        void replaceBooleanWithTrue(BooleanEdge bexpr);
@@ -194,7 +194,7 @@ private:
        void handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child);
        void handleANDTrue(BooleanLogic *bexpr, BooleanEdge child);
        void handleFunction(ElementFunction *ef, BooleanEdge child);
-       
+
        //These two functions are helpers if the client has a pointer to a
        //Boolean object that we have since replaced
        BooleanEdge rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uint asize);

diff --git a/src/satune_SatuneJavaAPI.cc b/src/satune_SatuneJavaAPI.cc
index 21cd504ff5f00029cff1c7ef6041496c97b7dcf0..37bfba46129c9db1664436af915ccd4af2ae030f 100644 (file)
--- a/src/satune_SatuneJavaAPI.cc
+++ b/src/satune_SatuneJavaAPI.cc
@@ -1,7 +1,7 @@
 /* DO NOT EDIT THIS FILE - it is machine generated */
 #include "satune_SatuneJavaAPI.h"
 #include "ccsolver.h"
-#define CCSOLVER(solver) (void*)solver
+#define CCSOLVER(solver) (void *)solver
 /* Header for class SatuneJavaAPI */
 
 /*
@@ -14,7 +14,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createCCSolver
        (JNIEnv *env, jobject obj)
 {
        return (jlong)createCCSolver();
-       
+
 }
 
 /*
@@ -158,7 +158,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanVar
  * Signature: (JI)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanTrue
-       (JNIEnv * env, jobject obj, jlong solver)
+       (JNIEnv *env, jobject obj, jlong solver)
 {
        return (jlong)getBooleanTrue((void *)solver);
 }
@@ -169,7 +169,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanTrue
  * Signature: (JI)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanFalse
-       (JNIEnv * env, jobject obj, jlong solver)
+       (JNIEnv *env, jobject obj, jlong solver)
 {
        return (jlong)getBooleanFalse((void *)solver);
 }

diff --git a/src/satune_SatuneJavaAPI.h b/src/satune_SatuneJavaAPI.h
index 68703bcbf8b55f7bb0b5239fb3ec38348e2abb71..93a386df53c7b49999410adbbbc45e53cd5e75e9 100644 (file)
--- a/src/satune_SatuneJavaAPI.h
+++ b/src/satune_SatuneJavaAPI.h
@@ -38,7 +38,7 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_resetCCSolver
  * Signature: (JIJI)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createSet
-       (JNIEnv *, jobject , jlong , jint , jlongArray arr);
+       (JNIEnv *, jobject, jlong, jint, jlongArray arr);
 
 /*
  * Class:     satune_SatuneJavaAPI