fix tabbing
authorbdemsky <bdemsky@uci.edu>
Mon, 26 Aug 2019 19:01:00 +0000 (12:01 -0700)
committerbdemsky <bdemsky@uci.edu>
Mon, 26 Aug 2019 19:01:00 +0000 (12:01 -0700)
15 files changed:
src/AST/element.cc
src/AST/element.h
src/ASTTransform/integerencoding.cc
src/Backend/constraint.cc
src/Backend/inc_solver.cc
src/Backend/satelemencoder.cc
src/Backend/satencoder.cc [changed mode: 0755->0644]
src/Collections/vector.h
src/Test/incrementaltest.cc
src/Tuner/basictuner.cc
src/ccsolver.cc
src/csolver.cc
src/csolver.h
src/satune_SatuneJavaAPI.cc
src/satune_SatuneJavaAPI.h

index 8044966..4fc9f4b 100644 (file)
@@ -10,7 +10,7 @@ Element::Element(ASTNodeType _type) :
        ASTNode(_type),
        encoding(this),
        anyValue(false),
-       frozen(false){
+       frozen(false) {
 }
 
 ElementSet::ElementSet(Set *s) :
index 166078a..53f6008 100644 (file)
@@ -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;
index 621d2a8..25c5ec8 100644 (file)
@@ -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);
        }
index 5246101..27de064 100644 (file)
@@ -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);
 }
index 72d3408..a89ed8b 100644 (file)
@@ -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)
index aa73924..b380c3a 100644 (file)
@@ -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);
old mode 100755 (executable)
new mode 100644 (file)
index 5312b4f..2e09491
@@ -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);
index 2dd5e69..6c53253 100644 (file)
@@ -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);                       \
        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;                                                         \
index c71645d..e559630 100644 (file)
@@ -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;
index 7d08098..44cd2bc 100644 (file)
@@ -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++;
 
index fa2e342..aea2161 100644 (file)
@@ -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();
 }
index d1c6d33..17b3dc3 100644 (file)
@@ -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;
        }
 }
index 6996e42..b27e3c0 100644 (file)
@@ -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);
index 21cd504..37bfba4 100644 (file)
@@ -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);
 }
index 68703bc..93a386d 100644 (file)
@@ -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