Merging + fixing memory bugs
authorHamed Gorjiara <hgorjiar@uci.edu>
Thu, 5 Sep 2019 23:01:44 +0000 (16:01 -0700)
committerHamed Gorjiara <hgorjiar@uci.edu>
Thu, 5 Sep 2019 23:01:44 +0000 (16:01 -0700)
16 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/dirkreader.cc [new file with mode: 0644]
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 34bcd74..25c5ec8 100644 (file)
@@ -24,7 +24,9 @@ void IntegerEncodingTransform::doTransform() {
        SetIteratorOrder *orderit = orders->iterator();
        while (orderit->hasNext()) {
                Order *order = orderit->next();
-               if (GETVARTUNABLE(solver->getTuner(), order->type, ORDERINTEGERENCODING, &offon))
+               if (order->type == SATC_PARTIAL)
+                       continue;
+               if (GETVARTUNABLE(solver->getTuner(), order->set->type, ORDERINTEGERENCODING, &offon))
                        integerEncode(order);
        }
        delete orders;
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 d924e6a..7687f35 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;                                                         \
diff --git a/src/Test/dirkreader.cc b/src/Test/dirkreader.cc
new file mode 100644 (file)
index 0000000..56393fb
--- /dev/null
@@ -0,0 +1,372 @@
+#include <iostream>
+#include <fstream>
+#include "csolver.h"
+#include "hashset.h"
+#include "cppvector.h"
+
+const char * assertstart = "ASSERTSTART";
+const char * assertend = "ASSERTEND";
+const char * satstart = "SATSTART";
+const char * satend = "SATEND";
+
+int skipahead(const char * token1, const char * token2);
+char * readuntilend(const char * token);
+BooleanEdge parseConstraint(CSolver * solver, char * constraint, int & offset);
+void processEquality(char * constraint, int &offset);
+
+std::ifstream * file;
+Order * order;
+MutableSet * set;
+class intwrapper {
+public:
+  intwrapper(int _val) : value(_val) {
+  }
+  int32_t value;
+};
+
+unsigned int iw_hash_function(intwrapper *i) {
+  return i->value;
+}
+
+bool iw_equals(intwrapper *key1, intwrapper *key2) {
+  return (key1->value == key2->value);
+}
+
+typedef Hashset<intwrapper *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashsetIW;
+
+class OrderRec {
+public:
+  OrderRec() : set (NULL), value(-1), alloced(false) {
+  }
+  ~OrderRec() {
+    if (set != NULL) {
+      set->resetAndDelete();
+      delete set;
+    }
+  }
+  HashsetIW * set;
+  int32_t value;
+  bool alloced;
+};
+
+typedef Hashtable<intwrapper *, OrderRec *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashtableIW;
+typedef Hashtable<intwrapper *, Boolean *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashtableBV;
+Vector<OrderRec*> * orderRecVector = NULL;
+HashtableIW * ordertable = NULL;
+HashtableBV * vartable = new HashtableBV();
+
+void cleanAndFreeOrderRecVector(){
+       for(uint i=0; i< orderRecVector->getSize(); i++){
+               delete orderRecVector->get(i);
+       }
+       orderRecVector->clear();
+}
+
+int main(int numargs, char ** argv) {
+  file = new std::ifstream(argv[1]);
+  char * assert = NULL;
+  char * sat = NULL;
+  Vector<OrderRec*> orderRecs;
+  orderRecVector = &orderRecs;
+  while(true) {
+    int retval = skipahead(assertstart, satstart);
+    printf("%d\n", retval);
+    if (retval == 0){
+      break;
+    }
+    if (retval == 1) {
+      if (assert != NULL){
+       free(assert);
+       assert = NULL;
+      }
+      assert = readuntilend(assertend);
+      printf("[%s]\n", assert);
+    } else if (retval == 2) {
+      if (sat != NULL) {
+       free(sat);
+       sat = NULL;
+       vartable->resetAndDeleteKeys();
+       ordertable->reset();
+       cleanAndFreeOrderRecVector();
+      } else {
+       ordertable = new HashtableIW();
+      }
+      sat = readuntilend(satend);
+      CSolver *solver = new CSolver();
+      solver->turnoffOptimizations();
+      set = solver->createMutableSet(1);
+      order = solver->createOrder(SATC_TOTAL, (Set *) set);
+      int offset = 0;
+      processEquality(sat, offset);
+      offset = 0;
+      processEquality(assert, offset);
+      offset = 0;
+      solver->addConstraint(parseConstraint(solver, sat, offset));
+      offset = 0;
+      solver->addConstraint(parseConstraint(solver, assert, offset));
+      printf("[%s]\n", sat);
+      solver->finalizeMutableSet(set);
+      solver->serialize();
+      solver->printConstraints();
+      delete solver;
+    }
+  }
+
+  cleanAndFreeOrderRecVector();
+  if(ordertable != NULL){
+       delete ordertable;
+  }
+  if(assert != NULL){
+       free(assert);
+  }
+  if(sat != NULL){
+       free(sat);
+  }
+  vartable->resetAndDeleteKeys();
+  delete vartable;
+  file->close();
+  delete file;
+}
+
+void skipwhitespace(char * constraint, int & offset) {
+  //skip whitespace
+  while (constraint[offset] == ' ' || constraint[offset] == '\n')
+    offset++;
+}
+
+void doExit() {
+  printf("PARSE ERROR\n");
+  exit(-1);
+}
+
+int32_t getOrderVar(char *constraint, int & offset) {
+  if (constraint[offset++] != 'O' || constraint[offset++] != '!' ) {
+    doExit();
+  }
+  int32_t num = 0;
+  while(true) {
+    char next = constraint[offset];
+    if (next >= '0' && next <= '9') {
+      num = (num * 10) + (next - '0');
+      offset++;
+    } else
+      return num;
+  }
+}
+
+int32_t getBooleanVar(char *constraint, int & offset) {
+  if (constraint[offset++] != 'S' || constraint[offset++] != '!' ) {
+    doExit();
+  }
+  int32_t num = 0;
+  while(true) {
+    char next = constraint[offset];
+    if (next >= '0' && next <= '9') {
+      num = (num * 10) + (next - '0');
+      offset++;
+    } else
+      return num;
+  }
+}
+
+BooleanEdge checkBooleanVar(CSolver *solver, int32_t value) {
+  intwrapper v(value);
+  if (vartable->contains(&v)) {
+    return BooleanEdge(vartable->get(&v));
+  } else {
+    Boolean* ve = solver->getBooleanVar(2).getBoolean();
+    vartable->put(new intwrapper(value), ve);
+    return BooleanEdge(ve);
+  }
+}
+
+void mergeVars(int32_t value1, int32_t value2) {
+  intwrapper v1(value1);
+  intwrapper v2(value2);
+  OrderRec *r1 = ordertable->get(&v1);
+  OrderRec *r2 = ordertable->get(&v2);
+  if (r1 == r2) {
+    if (r1 == NULL) {
+      OrderRec * r = new OrderRec();
+      orderRecVector->push(r);
+      r->value = value1;
+      r->set = new HashsetIW();
+      intwrapper * k1 = new intwrapper(v1);
+      intwrapper * k2 = new intwrapper(v2);
+      r->set->add(k1);
+      r->set->add(k2);
+      ordertable->put(k1, r);
+      ordertable->put(k2, r);
+    }
+  } else if (r1 == NULL) {
+    intwrapper * k = new intwrapper(v1);
+    ordertable->put(k, r2);
+    r2->set->add(k);
+  } else if (r2 == NULL) {
+    intwrapper * k = new intwrapper(v2);
+    ordertable->put(k, r1);
+    r1->set->add(k);
+  } else {
+    SetIterator<intwrapper *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> * it1 = r1->set->iterator();
+    while (it1->hasNext()) {
+      intwrapper * k = it1->next();
+      ordertable->put(k, r2);
+      r2->set->add(k);
+    }
+    delete r2->set;
+    r2->set = NULL;
+    delete r2;
+    delete it1;
+  }
+}
+
+int32_t checkordervar(CSolver * solver, int32_t value) {
+  intwrapper v(value);
+  OrderRec * rec = ordertable->get(&v);
+  if (rec == NULL) {
+    intwrapper * k = new intwrapper(value);
+    rec = new OrderRec();
+    orderRecVector->push(rec);
+    rec->value = value;
+    rec->set = new HashsetIW();
+    rec->set->add(k);
+    ordertable->put(k, rec);
+  }
+  if (!rec->alloced) {
+    solver->addItem(set, rec->value);
+    rec->alloced = true;
+  }
+  return rec->value;
+}
+
+void processEquality(char * constraint, int &offset) {
+  skipwhitespace(constraint, offset);
+  if (strncmp(&constraint[offset], "(and",4) == 0) {
+    offset +=4;
+    Vector<BooleanEdge> vec;
+    while(true) {
+      skipwhitespace(constraint, offset);
+      if (constraint[offset] == ')') {
+       offset++;
+       return;
+      }
+      processEquality(constraint, offset);
+    }
+  } else if (strncmp(&constraint[offset], "(<", 2) == 0) {
+    offset+=2;
+    skipwhitespace(constraint, offset);
+    getOrderVar(constraint, offset);
+    skipwhitespace(constraint, offset);
+    getOrderVar(constraint, offset);
+    skipwhitespace(constraint, offset);
+    if (constraint[offset++] != ')')
+      doExit();
+    return;
+  } else if (strncmp(&constraint[offset], "(=", 2) == 0) {
+    offset+=2;
+    skipwhitespace(constraint, offset);
+    int v1=getOrderVar(constraint, offset);
+    skipwhitespace(constraint, offset);
+    int v2=getOrderVar(constraint, offset);
+    skipwhitespace(constraint, offset);
+    if (constraint[offset++] != ')')
+      doExit();
+    mergeVars(v1, v2);
+    return;
+  } else {
+    getBooleanVar(constraint, offset);
+    skipwhitespace(constraint, offset);
+    return;
+  }
+}
+
+BooleanEdge parseConstraint(CSolver * solver, char * constraint, int & offset) {
+  skipwhitespace(constraint, offset);
+  if (strncmp(&constraint[offset], "(and", 4) == 0) {
+    offset +=4;
+    Vector<BooleanEdge> vec;
+    while(true) {
+      skipwhitespace(constraint, offset);
+      if (constraint[offset] == ')') {
+       offset++;
+       return solver->applyLogicalOperation(SATC_AND, vec.expose(), vec.getSize());
+      }
+      vec.push(parseConstraint(solver, constraint, offset));
+    }
+  } else if (strncmp(&constraint[offset], "(<", 2) == 0) {
+    offset+=2;
+    skipwhitespace(constraint, offset);
+    int32_t v1 = getOrderVar(constraint, offset);
+    skipwhitespace(constraint, offset);
+    int32_t v2 = getOrderVar(constraint, offset);
+    skipwhitespace(constraint, offset);
+    if (constraint[offset++] != ')')
+      doExit();
+    return solver->orderConstraint(order, checkordervar(solver, v1), checkordervar(solver, v2));
+  } else if (strncmp(&constraint[offset], "(=", 2) == 0) {
+    offset+=2;
+    skipwhitespace(constraint, offset);
+    getOrderVar(constraint, offset);
+    skipwhitespace(constraint, offset);
+    getOrderVar(constraint, offset);
+    skipwhitespace(constraint, offset);
+    if (constraint[offset++] != ')')
+      doExit();
+    return solver->getBooleanTrue();
+  } else {
+    int32_t v = getBooleanVar(constraint, offset);
+    skipwhitespace(constraint, offset);
+    return checkBooleanVar(solver, v);
+  }
+}
+
+int skipahead(const char * token1, const char * token2) {
+  int index1 = 0, index2 = 0;
+  char buffer[256];
+  while(true) {
+    if (token1[index1] == 0)
+      return 1;
+    if (token2[index2] == 0)
+      return 2;
+    if (file->eof())
+      return 0;
+    file->read(buffer, 1);
+    if (buffer[0] == token1[index1])
+      index1++;
+    else
+      index1 = 0;
+    if (buffer[0] == token2[index2])
+      index2++;
+    else
+      index2 = 0;
+  }
+}
+
+char * readuntilend(const char * token) {
+  int index = 0;
+  char buffer[256];
+  int length = 256;
+  int offset = 0;
+  char * outbuffer = (char *) malloc(length);
+  while(true) {
+    if (token[index] == 0) {
+      outbuffer[offset - index] = 0;
+      return outbuffer;
+    }
+    if (file->eof()) {
+      free(outbuffer);
+      return NULL;
+    }
+      
+    file->read(buffer, 1);
+    outbuffer[offset++] = buffer[0];
+    if (offset == length) {
+      length = length * 2;
+      outbuffer = (char *) realloc(outbuffer, length);
+    }
+    if (buffer[0] == token[index])
+      index++;
+    else
+      index=0;
+  }
+}
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 7707b74..aca46a5 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 3798586..17e2378 100644 (file)
@@ -244,10 +244,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);
                }
        }
@@ -409,24 +409,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) {
@@ -641,8 +641,8 @@ int CSolver::solveIncremental() {
        if (isUnSAT()) {
                return IS_UNSAT;
        }
-       
-       
+
+
        long long startTime = getTimeNano();
        bool deleteTuner = false;
        if (tuner == NULL) {
@@ -672,7 +672,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);
@@ -698,7 +698,7 @@ int CSolver::solveIncremental() {
        time2 = getTimeNano();
        elapsedTime = time2 - startTime;
        model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);
-       
+
        if (deleteTuner) {
                delete tuner;
                tuner = NULL;
@@ -775,7 +775,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");
@@ -842,9 +842,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 49438b6..eba7b3c 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,17 +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);
-       
        void turnoffOptimizations(){optimizationsOff = true;}
-       
        /** After getting the solution from the SAT solver, client can get the value of a boolean via this function*/
        bool getBooleanValue(BooleanEdge boolean);
 
@@ -167,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);
@@ -196,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 e337590..0a7d672 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 e606b44..0a0b6e5 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