Fix tabbing
authorbdemsky <bdemsky@uci.edu>
Tue, 19 Mar 2019 20:19:16 +0000 (13:19 -0700)
committerbdemsky <bdemsky@uci.edu>
Tue, 19 Mar 2019 20:21:15 +0000 (13:21 -0700)
51 files changed:
src/AST/boolean.cc
src/AST/order.h
src/AST/rewriter.cc
src/ASTAnalyses/Polarity/polarityassignment.cc
src/ASTTransform/decomposeordertransform.cc
src/ASTTransform/elementopt.cc
src/ASTTransform/integerencoding.cc
src/ASTTransform/varorderingopt.cc
src/Backend/satencoder.cc
src/Collections/vector.h
src/Encoders/naiveencoder.cc
src/Interpreter/alloyinterpreter.cc
src/Interpreter/alloyinterpreter.h
src/Interpreter/alloysig.cc
src/Interpreter/alloysig.h
src/Interpreter/interpreter.cc
src/Interpreter/interpreter.h
src/Interpreter/mathsatinterpreter.cc
src/Interpreter/mathsatinterpreter.h
src/Interpreter/signature.cc
src/Interpreter/signature.h
src/Interpreter/signatureenc.cc
src/Interpreter/signatureenc.h
src/Interpreter/smtinterpreter.cc
src/Interpreter/smtinterpreter.h
src/Interpreter/smtratinterpreter.cc
src/Interpreter/smtratinterpreter.h
src/Interpreter/smtsig.cc
src/Interpreter/smtsig.h
src/Serialize/deserializer.cc
src/Test/deserializealloytest.cc
src/Test/printtuner.cc
src/Test/runmultituner.cc
src/Tuner/basictuner.cc
src/Tuner/basictuner.h
src/Tuner/comptuner.cc
src/Tuner/comptuner.h
src/Tuner/kmeanstuner.cc
src/Tuner/kmeanstuner.h
src/Tuner/randomtuner.cc
src/Tuner/randomtuner.h
src/Tuner/satuner.cc
src/Tuner/satuner.h
src/Tuner/searchtuner.cc
src/Tuner/searchtuner.h
src/Tuner/tunabledependent.cc
src/Tuner/tunabledependent.h
src/ccsolver.cc
src/csolver.cc
src/csolver.h
src/satune_SatuneJavaAPI.h

index e63549e..04898aa 100644 (file)
@@ -33,7 +33,7 @@ BooleanOrder::BooleanOrder(Order *_order, uint64_t _first, uint64_t _second) :
 }
 
 void BooleanOrder::updateParents() {
-       order->constraints.push(this);
+       order->addOrderConstraint(this);
 }
 
 BooleanPredicate::BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, BooleanEdge _undefinedStatus) :
index 866b1ab..cbbe846 100644 (file)
@@ -20,6 +20,7 @@ public:
        void print();
        Vector<BooleanOrder *> constraints;
        OrderEncoding encoding;
+
        void setOrderResolver(OrderResolver *_resolver) { ASSERT(encoding.resolver == NULL); encoding.resolver = _resolver;};
        void initializeOrderElementsHashtable();
        void addOrderConstraint(BooleanOrder *constraint);
index fef4dcb..a53180e 100644 (file)
@@ -23,7 +23,7 @@ void CSolver::replaceBooleanWithFalseNoRemove(BooleanEdge bexpr) {
 void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
        updateMustValue(bexpr.getBoolean(), bexpr.isNegated() ? BV_MUSTBEFALSE : BV_MUSTBETRUE);
 
-       ASSERT((bexpr->boolVal != BV_UNSAT ) || unsat);
+       ASSERT((bexpr->boolVal != BV_UNSAT) || unsat);
 
        uint size = bexpr->parents.getSize();
        for (uint i = 0; i < size; i++) {
index b8b01d0..8a94f0a 100644 (file)
@@ -2,7 +2,7 @@
 #include "csolver.h"
 
 void computePolarities(CSolver *This) {
-       if(This->isUnSAT()){
+       if (This->isUnSAT()) {
                return;
        }
        SetIteratorBooleanEdge *iterator = This->getConstraints();
index 4b3fc4a..e63cb74 100644 (file)
@@ -28,7 +28,7 @@ DecomposeOrderTransform::~DecomposeOrderTransform() {
 }
 
 void DecomposeOrderTransform::doTransform() {
-       if(solver->isUnSAT())
+       if (solver->isUnSAT())
                return;
        HashsetOrder *orders = solver->getActiveOrders()->copy();
        SetIteratorOrder *orderit = orders->iterator();
@@ -331,11 +331,11 @@ void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, Ord
                BooleanEdge benew = solver->orderConstraint(graph->getOrder(), source->getID(), node->getID());
                updateEdgePolarity(benew, be);
                if (solver->isTrue(benew))
-                 solver->replaceBooleanWithTrue(be);
+                       solver->replaceBooleanWithTrue(be);
                else if (solver->isFalse(benew))
-                 solver->replaceBooleanWithFalse(be);
+                       solver->replaceBooleanWithFalse(be);
                else
-                 solver->replaceBooleanWithBoolean(be, benew);
+                       solver->replaceBooleanWithBoolean(be, benew);
        }
        dstnode->inEdges.reset();
        delete inedgeit;
@@ -366,11 +366,11 @@ void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, Ord
                BooleanEdge benew = solver->orderConstraint(graph->getOrder(), node->getID(), sink->getID());
                updateEdgePolarity(benew, be);
                if (solver->isTrue(benew))
-                 solver->replaceBooleanWithTrue(be);
+                       solver->replaceBooleanWithTrue(be);
                else if (solver->isFalse(benew))
-                 solver->replaceBooleanWithFalse(be);
+                       solver->replaceBooleanWithFalse(be);
                else
-                 solver->replaceBooleanWithBoolean(be, benew);
+                       solver->replaceBooleanWithBoolean(be, benew);
        }
        dstnode->outEdges.reset();
        delete outedgeit;
index 899f659..22a6dbe 100644 (file)
@@ -9,7 +9,7 @@
 
 ElementOpt::ElementOpt(CSolver *_solver)
        : Transform(_solver),
-         updateSets(false)
+       updateSets(false)
 {
 }
 
@@ -22,7 +22,7 @@ void ElementOpt::doTransform() {
 
        //Set once we know we are going to use it.
        updateSets = solver->getTuner()->getTunable(ELEMENTOPTSETS, &onoff) == 1;
-       
+
        SetIteratorBooleanEdge *iterator = solver->getConstraints();
        while (iterator->hasNext()) {
                BooleanEdge constraint = iterator->next();
index 2a7b901..d5d769d 100644 (file)
@@ -17,7 +17,7 @@ IntegerEncodingTransform::~IntegerEncodingTransform() {
 }
 
 void IntegerEncodingTransform::doTransform() {
-       if(solver->isUnSAT()){
+       if (solver->isUnSAT()) {
                return;
        }
        HashsetOrder *orders = solver->getActiveOrders()->copy();
index 9fd8c60..c78252c 100644 (file)
@@ -26,7 +26,7 @@ VarOrderingOpt::~VarOrderingOpt() {
 }
 
 void VarOrderingOpt::doTransform() {
-       if(solver->isUnSAT()){
+       if (solver->isUnSAT()) {
                return;
        }
        BooleanVarOrdering direction = (BooleanVarOrdering)solver->getTuner()->getTunable(VARIABLEORDER, &boolVarOrderingDesc);
index 618b8c1..00219ef 100644 (file)
@@ -35,7 +35,7 @@ int SATEncoder::solve(long timeout) {
 }
 
 void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
-       if(csolver->isUnSAT()){
+       if (csolver->isUnSAT()) {
                return;
        }
        SetIteratorBooleanEdge *iterator = csolver->getConstraints();
index 6c53253..2dd5e69 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 ac20be5..e3d1305 100644 (file)
@@ -15,7 +15,7 @@
 #include <strings.h>
 
 void naiveEncodingDecision(CSolver *This) {
-       if(This->isUnSAT()){
+       if (This->isUnSAT()) {
                return;
        }
        SetIteratorBooleanEdge *iterator = This->getConstraints();
index 021b087..d802529 100644 (file)
@@ -19,37 +19,37 @@ using namespace std;
 #define ALLOYFILENAME "satune.als"
 #define ALLOYSOLUTIONFILE "solution.sol"
 
-AlloyInterpreter::AlloyInterpreter(CSolver *_solver)
-       Interpreter(_solver) 
+AlloyInterpreter::AlloyInterpreter(CSolver *_solver) :
+       Interpreter(_solver)
 {
        output.open(ALLOYFILENAME);
-       if(!output.is_open()){
+       if (!output.is_open()) {
                model_print("AlloyEnc:Error in opening the dump file satune.als\n");
                exit(-1);
        }
 }
 
-AlloyInterpreter::~AlloyInterpreter(){
-       if(output.is_open()){
+AlloyInterpreter::~AlloyInterpreter() {
+       if (output.is_open()) {
                output.close();
        }
 }
 
-ValuedSignature *AlloyInterpreter::getBooleanSignature(uint id){
+ValuedSignature *AlloyInterpreter::getBooleanSignature(uint id) {
        return new AlloyBoolSig(id);
 }
 
-ValuedSignature *AlloyInterpreter::getElementSignature(uint id, Signature *ssig){
+ValuedSignature *AlloyInterpreter::getElementSignature(uint id, Signature *ssig) {
        return new AlloyElementSig(id, ssig);
 }
 
-Signature *AlloyInterpreter::getSetSignature(uint id, Set *set){
+Signature *AlloyInterpreter::getSetSignature(uint id, Set *set) {
        return new AlloySetSig(id, set);
 }
 
-void AlloyInterpreter::dumpAllConstraints(Vector<char *> &facts){
+void AlloyInterpreter::dumpAllConstraints(Vector<char *> &facts) {
        output << "fact {" << endl;
-       for(uint i=0; i< facts.getSize(); i++){
+       for (uint i = 0; i < facts.getSize(); i++) {
                char *cstr = facts.get(i);
                writeToFile(cstr);
        }
@@ -57,24 +57,24 @@ void AlloyInterpreter::dumpAllConstraints(Vector<char *> &facts){
 }
 
 
-int AlloyInterpreter::getResult(){
+int AlloyInterpreter::getResult() {
        ifstream input(ALLOYSOLUTIONFILE, ios::in);
        string line;
-       while(getline(input, line)){
-               if(line.find("Unsatisfiable.")== 0){
+       while (getline(input, line)) {
+               if (line.find("Unsatisfiable.") == 0) {
                        return IS_UNSAT;
                }
-               if(line.find("univ") == 0){
+               if (line.find("univ") == 0) {
                        continue;
                }
-               if(line.find("this/AbsBool<:value") == 0 || line.find("this/AbsElement<:value=") == 0){
+               if (line.find("this/AbsBool<:value") == 0 || line.find("this/AbsElement<:value=") == 0) {
                        const char delim [2] = ",";
-                       char cline [line.size()+1];
+                       char cline [line.size() + 1];
                        strcpy ( cline, line.c_str() );
                        char *token = strtok(cline, delim);
-                       while( token != NULL ) {
+                       while ( token != NULL ) {
                                uint i1, i2, i3;
-                               if (3 == sscanf(token,"%*[^0123456789]%u%*[^0123456789]%d%*[^0123456789]%u", &i1, &i2, &i3)){
+                               if (3 == sscanf(token,"%*[^0123456789]%u%*[^0123456789]%d%*[^0123456789]%u", &i1, &i2, &i3)) {
                                        model_print("Signature%u = %u\n", i1, i3);
                                        sigEnc.setValue(i1, i3);
                                }
@@ -86,86 +86,86 @@ int AlloyInterpreter::getResult(){
 }
 
 
-int AlloyInterpreter::getAlloyIntScope(){
+int AlloyInterpreter::getAlloyIntScope() {
        double mylog = log2(sigEnc.getMaxValue() + 1);
-       return floor(mylog) == mylog ? (int)mylog + 1: (int)mylog + 2;
+       return floor(mylog) == mylog ? (int)mylog + 1 : (int)mylog + 2;
 }
 
-void AlloyInterpreter::dumpFooter(){
+void AlloyInterpreter::dumpFooter() {
        output << "pred show {}" << endl;
        output << "run show for " << getAlloyIntScope() << " int" << endl;
 }
 
-void AlloyInterpreter::dumpHeader(){
+void AlloyInterpreter::dumpHeader() {
        output << "open util/integer" << endl;
 }
 
-void AlloyInterpreter::compileRunCommand(char * command, size_t size){
+void AlloyInterpreter::compileRunCommand(char *command, size_t size) {
        model_print("Calling Alloy...\n");
        snprintf(command, size, "./run.sh timeout %u java -Xmx10000m edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", getTimeout(), ALLOYFILENAME, ALLOYSOLUTIONFILE);
 }
 
-string AlloyInterpreter::negateConstraint(string constr){
+string AlloyInterpreter::negateConstraint(string constr) {
        return "not ( " + constr + " )";
 }
 
-string AlloyInterpreter::encodeBooleanLogic( BooleanLogic *bl){
+string AlloyInterpreter::encodeBooleanLogic( BooleanLogic *bl) {
        uint size = bl->inputs.getSize();
        string array[size];
        for (uint i = 0; i < size; i++)
                array[i] = encodeConstraint(bl->inputs.get(i));
        string op;
-       switch (bl->op){
-               case SATC_OR:
-                       op = " or ";
-                       break;
-               case SATC_AND:
-                       op = " and ";
-                       break;
-               case SATC_NOT:
-                       op = " not ";
-                       break;
-               case SATC_IFF:
-                       op = " iff ";
-                       break;
-               case SATC_IMPLIES:
-                       op = " implies ";
-                       break;
-               case SATC_XOR:
-               default:
-                       ASSERT(0);
+       switch (bl->op) {
+       case SATC_OR:
+               op = " or ";
+               break;
+       case SATC_AND:
+               op = " and ";
+               break;
+       case SATC_NOT:
+               op = " not ";
+               break;
+       case SATC_IFF:
+               op = " iff ";
+               break;
+       case SATC_IMPLIES:
+               op = " implies ";
+               break;
+       case SATC_XOR:
+       default:
+               ASSERT(0);
        }
        switch (bl->op) {
-               case SATC_OR:
-               case SATC_AND:{
-                       ASSERT(size >= 2);
-                       string res = "( ";
-                       res += array[0];
-                       for( uint i=1; i< size; i++){
-                               res += op + array[i];
-                       }
-                       res += " )";
-                       return res;
-               }
-               case SATC_NOT:{
-                       return "not ( " + array[0] + " )";
+       case SATC_OR:
+       case SATC_AND: {
+               ASSERT(size >= 2);
+               string res = "( ";
+               res += array[0];
+               for ( uint i = 1; i < size; i++) {
+                       res += op + array[i];
                }
-               case SATC_IMPLIES:
-               case SATC_IFF:
-                       return "( " + array[0] + op + array[1] + " )";
-               case SATC_XOR:
-               default:
-                       ASSERT(0);
+               res += " )";
+               return res;
+       }
+       case SATC_NOT: {
+               return "not ( " + array[0] + " )";
+       }
+       case SATC_IMPLIES:
+       case SATC_IFF:
+               return "( " + array[0] + op + array[1] + " )";
+       case SATC_XOR:
+       default:
+               ASSERT(0);
 
        }
 }
 
-string AlloyInterpreter::encodeBooleanVar( BooleanVar *bv){
-       ValuedSignature * boolSig = sigEnc.getBooleanSignature(bv);
+string AlloyInterpreter::encodeBooleanVar( BooleanVar *bv) {
+       ValuedSignature *boolSig = sigEnc.getBooleanSignature(bv);
        return *boolSig + " = 1";
 }
 
-string AlloyInterpreter::processElementFunction(ElementFunction* elemFunc, ValuedSignature *signature){
+string AlloyInterpreter::processElementFunction(ElementFunction *elemFunc, ValuedSignature *signature) {
        FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
        uint numDomains = elemFunc->inputs.getSize();
        ASSERT(numDomains > 1);
@@ -174,39 +174,39 @@ string AlloyInterpreter::processElementFunction(ElementFunction* elemFunc, Value
        for (uint i = 0; i < numDomains; i++) {
                Element *elem = elemFunc->inputs.get(i);
                inputs[i] = sigEnc.getElementSignature(elem);
-               if(elem->type == ELEMFUNCRETURN){
+               if (elem->type == ELEMFUNCRETURN) {
                        result += processElementFunction((ElementFunction *) elem, inputs[i]);
                }
        }
        string op;
-       switch(function->op){
-               case SATC_ADD:
-                       op = ".add";
-                       break;
-               case SATC_SUB:
-                       op = ".sub";
-                       break;
-               default:
-                       ASSERT(0);
+       switch (function->op) {
+       case SATC_ADD:
+               op = ".add";
+               break;
+       case SATC_SUB:
+               op = ".sub";
+               break;
+       default:
+               ASSERT(0);
        }
        result += *signature + " = " + *inputs[0];
        for (uint i = 1; i < numDomains; i++) {
-               result += op + "["+ *inputs[i] +"]";
+               result += op + "[" + *inputs[i] + "]";
        }
        result += "\n";
        return result;
 }
 
-string AlloyInterpreter::operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2){
+string AlloyInterpreter::operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2) {
        switch (op) {
-               case SATC_EQUALS:
-                       return *elemSig1 + " = " + *elemSig2;
-               case SATC_LT:
-                       return *elemSig1 + " < " + *elemSig2;
-               case SATC_GT:
-                       return *elemSig1 + " > " + *elemSig2;
-               default:
-                       ASSERT(0);
+       case SATC_EQUALS:
+               return *elemSig1 + " = " + *elemSig2;
+       case SATC_LT:
+               return *elemSig1 + " < " + *elemSig2;
+       case SATC_GT:
+               return *elemSig1 + " > " + *elemSig2;
+       default:
+               ASSERT(0);
        }
 }
 
index e4a1e3b..310f3d9 100644 (file)
@@ -7,7 +7,7 @@
 #include <iostream>
 #include <fstream>
 
-class AlloyInterpreter: public Interpreter{
+class AlloyInterpreter : public Interpreter {
 public:
        AlloyInterpreter(CSolver *solver);
        virtual ValuedSignature *getBooleanSignature(uint id);
@@ -18,7 +18,7 @@ protected:
        virtual void dumpFooter();
        virtual void dumpHeader();
        int getAlloyIntScope();
-       virtual void compileRunCommand(char * command , size_t size);
+       virtual void compileRunCommand(char *command, size_t size);
        virtual int getResult();
        virtual void dumpAllConstraints(Vector<char *> &facts);
        virtual string negateConstraint(string constr);
index 1b98cd8..b7eeb86 100644 (file)
@@ -5,18 +5,18 @@ bool AlloyBoolSig::encodeAbs = true;
 bool AlloySetSig::encodeAbs = true;
 bool AlloyElementSig::encodeAbs = true;
 
-AlloyBoolSig::AlloyBoolSig(uint id):
+AlloyBoolSig::AlloyBoolSig(uint id) :
        ValuedSignature(id)
 {
 }
 
-string AlloyBoolSig::toString() const{
+string AlloyBoolSig::toString() const {
        return "Boolean" + to_string(id) + ".value";
 }
 
-string AlloyBoolSig::getSignature() const{
+string AlloyBoolSig::getSignature() const {
        string str;
-       if(encodeAbs){
+       if (encodeAbs) {
                encodeAbs = false;
                str += getAbsSignature();
        }
@@ -24,15 +24,15 @@ string AlloyBoolSig::getSignature() const{
        return str;
 }
 
-string AlloyBoolSig::getAbsSignature() const{
+string AlloyBoolSig::getAbsSignature() const {
        string str;
-       if(AlloySetSig::encodeAbs){
+       if (AlloySetSig::encodeAbs) {
                AlloySetSig::encodeAbs = false;
                str += "abstract sig AbsSet {\
                domain: set Int\
                }\n";
        }
-       str +="one sig BooleanSet extends AbsSet {}{\n\
+       str += "one sig BooleanSet extends AbsSet {}{\n\
        domain = 0 + 1 \n\
        }\n\
        abstract sig AbsBool {\
@@ -43,19 +43,19 @@ string AlloyBoolSig::getAbsSignature() const{
        return str;
 }
 
-AlloyElementSig::AlloyElementSig(uint id, Signature *_ssig)
+AlloyElementSig::AlloyElementSig(uint id, Signature *_ssig) :
        ValuedSignature(id),
        ssig(_ssig)
 {
 }
 
-string AlloyElementSig::toString() const{
+string AlloyElementSig::toString() const {
        return "Element" + to_string(id) + ".value";
 }
 
-string AlloyElementSig::getSignature() const{
+string AlloyElementSig::getSignature() const {
        string str;
-       if(encodeAbs){
+       if (encodeAbs) {
                encodeAbs = false;
                str += getAbsSignature();
        }
@@ -65,28 +65,28 @@ string AlloyElementSig::getSignature() const{
        return str;
 }
 
-string AlloyElementSig::getAbsSignature() const{
+string AlloyElementSig::getAbsSignature() const {
        return "abstract sig AbsElement {\n\
                value: Int\n\
                }\n";
-       
+
 }
 
-AlloySetSig::AlloySetSig(uint id, Set *set): Signature(id){
+AlloySetSig::AlloySetSig(uint id, Set *set) : Signature(id) {
        ASSERT(set->getSize() > 0);
        domain = to_string(set->getElement(0));
-       for(uint i=1; i< set->getSize(); i++){
+       for (uint i = 1; i < set->getSize(); i++) {
                domain += " + " + to_string(set->getElement(i));
        }
 }
 
-string AlloySetSig::toString() const{
+string AlloySetSig::toString() const {
        return "Set" + to_string(id) + ".domain";
 }
 
-string AlloySetSig::getSignature() const{
+string AlloySetSig::getSignature() const {
        string str;
-       if(encodeAbs){
+       if (encodeAbs) {
                encodeAbs = false;
                str += getAbsSignature();
        }
@@ -96,9 +96,9 @@ string AlloySetSig::getSignature() const{
        return str;
 }
 
-string AlloySetSig::getAbsSignature() const{
+string AlloySetSig::getAbsSignature() const {
        return "abstract sig AbsSet {\n\
                domain: set Int\n\
                }\n";
-       
+
 }
index 3fb2d10..7bffadf 100644 (file)
@@ -6,10 +6,10 @@
 #include "classlist.h"
 using namespace std;
 
-class AlloyBoolSig: public ValuedSignature{
+class AlloyBoolSig : public ValuedSignature {
 public:
        AlloyBoolSig(uint id);
-       virtual ~AlloyBoolSig(){}
+       virtual ~AlloyBoolSig() {}
        virtual string toString() const;
        virtual string getAbsSignature() const;
        virtual string getSignature() const;
@@ -17,10 +17,10 @@ private:
        static bool encodeAbs;
 };
 
-class AlloySetSig: public Signature{
+class AlloySetSig : public Signature {
 public:
        AlloySetSig(uint id, Set *set);
-       virtual ~AlloySetSig(){}
+       virtual ~AlloySetSig() {}
        virtual string toString() const;
        virtual string getAbsSignature() const;
        virtual string getSignature() const;
@@ -29,10 +29,10 @@ private:
        string domain;
 };
 
-class AlloyElementSig: public ValuedSignature{
+class AlloyElementSig : public ValuedSignature {
 public:
        AlloyElementSig(uint id, Signature *ssig);
-       virtual ~AlloyElementSig(){}
+       virtual ~AlloyElementSig() {}
        virtual string toString() const;
        virtual string getAbsSignature() const;
        virtual string getSignature() const;
index a5927f7..c4c7f8a 100644 (file)
 
 using namespace std;
 
-Interpreter::Interpreter(CSolver *_solver)
+Interpreter::Interpreter(CSolver *_solver) :
        csolver(_solver),
        sigEnc(this)
 {
 }
 
-Interpreter::~Interpreter(){
+Interpreter::~Interpreter() {
 }
 
-void Interpreter::encode(){
+void Interpreter::encode() {
        dumpHeader();
        SetIteratorBooleanEdge *iterator = csolver->getConstraints();
        Vector<char *> facts;
-       while(iterator->hasNext()){
+       while (iterator->hasNext()) {
                BooleanEdge constraint = iterator->next();
                string constr = encodeConstraint(constraint);
-               char *cstr = new char [constr.length()+1];
+               char *cstr = new char [constr.length() + 1];
                strcpy (cstr, constr.c_str());
                facts.push(cstr);
        }
        dumpAllConstraints(facts);
-       for(uint i=0; i< facts.getSize(); i++){
+       for (uint i = 0; i < facts.getSize(); i++) {
                char *cstr = facts.get(i);
                delete[] cstr;
        }
        delete iterator;
 }
 
-uint Interpreter::getTimeout(){
-       uint timeout =csolver->getSatSolverTimeout(); 
-       return timeout == (uint)NOTIMEOUT? 1000: timeout;
+uint Interpreter::getTimeout() {
+       uint timeout = csolver->getSatSolverTimeout();
+       return timeout == (uint)NOTIMEOUT ? 1000 : timeout;
 }
 
-int Interpreter::solve(){
+int Interpreter::solve() {
        dumpFooter();
        int result = IS_INDETER;
        char buffer [512];
-       if( output.is_open()){
+       if ( output.is_open()) {
                output.close();
        }
        compileRunCommand(buffer, sizeof(buffer));
        int status = system(buffer);
-       if (status == 0 || status == 512 ) { //For some unknown reason, SMTSat returns 512 when the problem successfully gets solved
+       if (status == 0 || status == 512 ) {//For some unknown reason, SMTSat returns 512 when the problem successfully gets solved
                //Read data in from results file
                result = getResult();
        } else {
@@ -66,73 +66,73 @@ int Interpreter::solve(){
        return result;
 }
 
-string Interpreter::encodeConstraint(BooleanEdge c){
+string Interpreter::encodeConstraint(BooleanEdge c) {
        Boolean *constraint = c.getBoolean();
        string res;
-       switch(constraint->type){
-               case LOGICOP:{
-                       res = encodeBooleanLogic((BooleanLogic *) constraint);
-                       break;
-               }
-               case PREDICATEOP:{
-                       res = encodePredicate((BooleanPredicate *) constraint);
-                       break;
-               }
-               case BOOLEANVAR:{
-                       res = encodeBooleanVar( (BooleanVar *) constraint);
-                       break;
-               }
-               default:
-                       ASSERT(0);
+       switch (constraint->type) {
+       case LOGICOP: {
+               res = encodeBooleanLogic((BooleanLogic *) constraint);
+               break;
        }
-       if(c.isNegated()){
+       case PREDICATEOP: {
+               res = encodePredicate((BooleanPredicate *) constraint);
+               break;
+       }
+       case BOOLEANVAR: {
+               res = encodeBooleanVar( (BooleanVar *) constraint);
+               break;
+       }
+       default:
+               ASSERT(0);
+       }
+       if (c.isNegated()) {
                return negateConstraint(res);
        }
        return res;
 }
 
-string Interpreter::encodePredicate( BooleanPredicate *bp){
+string Interpreter::encodePredicate( BooleanPredicate *bp) {
        switch (bp->predicate->type) {
-               case TABLEPRED:
-                       ASSERT(0);
-               case OPERATORPRED:
-                       return encodeOperatorPredicate(bp);
-               default:
-                       ASSERT(0);
+       case TABLEPRED:
+               ASSERT(0);
+       case OPERATORPRED:
+               return encodeOperatorPredicate(bp);
+       default:
+               ASSERT(0);
        }
 }
 
-string Interpreter::encodeOperatorPredicate(BooleanPredicate *constraint){
+string Interpreter::encodeOperatorPredicate(BooleanPredicate *constraint) {
        PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
        ASSERT(constraint->inputs.getSize() == 2);
        string str;
        Element *elem0 = constraint->inputs.get(0);
        ASSERT(elem0->type == ELEMSET || elem0->type == ELEMFUNCRETURN || elem0->type == ELEMCONST);
        ValuedSignature *elemSig1 = sigEnc.getElementSignature(elem0);
-       if(elem0->type == ELEMFUNCRETURN){
+       if (elem0->type == ELEMFUNCRETURN) {
                str += processElementFunction((ElementFunction *) elem0, elemSig1);
        }
        Element *elem1 = constraint->inputs.get(1);
        ASSERT(elem1->type == ELEMSET || elem1->type == ELEMFUNCRETURN || elem1->type == ELEMCONST);
        ValuedSignature *elemSig2 = sigEnc.getElementSignature(elem1);
-       if(elem1->type == ELEMFUNCRETURN){
+       if (elem1->type == ELEMFUNCRETURN) {
                str += processElementFunction((ElementFunction *) elem1, elemSig2);
        }
        str += operatorPredicateConstraint(predicate->getOp(), elemSig1, elemSig2);
        return str;
 }
 
-void Interpreter::writeToFile(string str){
-       if(!str.empty()){
+void Interpreter::writeToFile(string str) {
+       if (!str.empty()) {
                output << str << endl;
        }
 }
 
-bool Interpreter::getBooleanValue(Boolean *b){
+bool Interpreter::getBooleanValue(Boolean *b) {
        return (bool)sigEnc.getValue(b);
 }
 
-uint64_t Interpreter::getValue(Element * element){
+uint64_t Interpreter::getValue(Element *element) {
        return (uint64_t)sigEnc.getValue(element);
 }
 
index 32eed4a..dc61c18 100644 (file)
@@ -8,7 +8,7 @@
 #include <fstream>
 using namespace std;
 
-class Interpreter{
+class Interpreter {
 public:
        Interpreter(CSolver *solver);
        void encode();
@@ -24,7 +24,7 @@ protected:
        virtual void dumpFooter() = 0;
        virtual void dumpHeader() = 0;
        uint getTimeout();
-       virtual void compileRunCommand(char * command, size_t size) = 0;
+       virtual void compileRunCommand(char *command, size_t size) = 0;
        string encodeConstraint(BooleanEdge constraint);
        virtual int getResult() = 0;
        virtual string negateConstraint(string constr) = 0;
index 5123efe..8fb5f09 100644 (file)
@@ -4,48 +4,48 @@
  * and open the template in the editor.
  */
 
-/* 
+/*
  * File:   smtsolvers.cc
  * Author: hamed
- * 
+ *
  * Created on February 21, 2019, 12:26 PM
  */
 
 #include "mathsatinterpreter.h"
 #include "solver_interface.h"
 
-MathSATInterpreter::MathSATInterpreter(CSolver *solver):
+MathSATInterpreter::MathSATInterpreter(CSolver *solver) :
        SMTInterpreter(solver)
-{      
+{
 }
 
-void MathSATInterpreter::compileRunCommand(char * command , size_t size){
+void MathSATInterpreter::compileRunCommand(char *command, size_t size) {
        model_print("Calling MathSAT...\n");
        snprintf(command, size, "./run.sh timeout %u mathsat -model %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
 }
 
-MathSATInterpreter::~MathSATInterpreter(){
+MathSATInterpreter::~MathSATInterpreter() {
 }
 
-int MathSATInterpreter::getResult(){
+int MathSATInterpreter::getResult() {
        ifstream input(SMTSOLUTIONFILE, ios::in);
        string line;
-       while(getline(input, line)){
-               if(line.find("unsat")!= line.npos){
+       while (getline(input, line)) {
+               if (line.find("unsat") != line.npos) {
                        return IS_UNSAT;
                }
-               if(line.find("(") != line.npos){
-                       char cline [line.size()+1];
+               if (line.find("(") != line.npos) {
+                       char cline [line.size() + 1];
                        strcpy ( cline, line.c_str() );
                        char valuestr [512];
                        uint id;
-                       if (2 == sscanf(cline,"%*[^0123456789]%u %s", &id, valuestr)){
+                       if (2 == sscanf(cline,"%*[^0123456789]%u %s", &id, valuestr)) {
                                uint value;
-                               if (strcmp (valuestr, "true)") == 0 ){
-                                       value =1;
-                               }else if (strcmp(valuestr, "false)") == 0){
+                               if (strcmp (valuestr, "true)") == 0 ) {
+                                       value = 1;
+                               } else if (strcmp(valuestr, "false)") == 0) {
                                        value = 0;
-                               }else {
+                               } else {
                                        ASSERT(2 == sscanf(cline, "%*[^0123456789]%u%*[^0123456789]%u", &id, &value));
                                }
 
index ef2ec9f..2110f59 100644 (file)
@@ -4,7 +4,7 @@
  * and open the template in the editor.
  */
 
-/* 
+/*
  * File:   mathsatinterpreter.h
  * Author: hamed
  *
 #include "smtinterpreter.h"
 
 
-class MathSATInterpreter: public SMTInterpreter{
+class MathSATInterpreter : public SMTInterpreter {
 public:
        MathSATInterpreter(CSolver *solver);
        virtual ~MathSATInterpreter();
 protected:
-       virtual void compileRunCommand(char * command , size_t size);
+       virtual void compileRunCommand(char *command, size_t size);
        virtual int getResult();
 };
 
 
-#endif /* SMTSOLVERS_H */
+#endif/* SMTSOLVERS_H */
 
index 94efbb2..d9724c9 100644 (file)
@@ -1,21 +1,21 @@
 #include "signature.h"
 #include "set.h"
 
-ValuedSignature::ValuedSignature(uint id)
-       Signature(id), 
-       value(-1) 
+ValuedSignature::ValuedSignature(uint id) :
+       Signature(id),
+       value(-1)
 {
 }
 
-int ValuedSignature::getValue(){
+int ValuedSignature::getValue() {
        ASSERT(value != -1);
        return value;
 }
 
-string Signature::operator+(const string& str){
+string Signature::operator+(const string &str) {
        return toString() + str;
 }
 
-string operator+(const string& str, const Signature& sig){
-        return str + sig.toString();
+string operator+(const string &str, const Signature &sig) {
+       return str + sig.toString();
 }
index e8c9e1c..3121051 100644 (file)
@@ -5,27 +5,27 @@
 #include "classlist.h"
 using namespace std;
 
-class Signature{
+class Signature {
 public:
-       Signature(uint _id):id(_id){}
-       string operator+(const strings);
+       Signature(uint _id) : id(_id) {}
+       string operator+(const string &s);
        virtual string toString() const = 0;
-       virtual string getAbsSignature() const =0;
-       virtual string getSignature() const =0;
-       virtual ~Signature(){}
+       virtual string getAbsSignature() const = 0;
+       virtual string getSignature() const = 0;
+       virtual ~Signature() {}
 protected:
        uint id;
 };
 
-class ValuedSignature: public Signature{
+class ValuedSignature : public Signature {
 public:
        ValuedSignature(uint id);
        int getValue();
-       void setValue(int v){value = v;}
+       void setValue(int v) {value = v;}
 protected:
        int value;
 };
 
-string operator+(const string& str, const Signature& sig);
+string operator+(const string &str, const Signature &sig);
 
 #endif
index cdc8aa1..1672c7a 100644 (file)
@@ -4,30 +4,30 @@
 #include "signature.h"
 #include "interpreter.h"
 
-SignatureEnc::SignatureEnc(Interpreter *inter)
+SignatureEnc::SignatureEnc(Interpreter *inter) :
        interpreter(inter),
        maxValue(0)
 {
 }
 
-SignatureEnc::~SignatureEnc(){
-       for(uint i=0; i<signatures.getSize(); i++){
+SignatureEnc::~SignatureEnc() {
+       for (uint i = 0; i < signatures.getSize(); i++) {
                Signature *s = signatures.get(i);
                delete s;
        }
 }
 
-void SignatureEnc::updateMaxValue(Set *set){
-       for(uint i=0; i< set->getSize(); i++){
-               if(set->getElement(i) > maxValue){
+void SignatureEnc::updateMaxValue(Set *set) {
+       for (uint i = 0; i < set->getSize(); i++) {
+               if (set->getElement(i) > maxValue) {
                        maxValue = set->getElement(i);
                }
        }
 }
 
-ValuedSignature *SignatureEnc::getBooleanSignature(Boolean *bvar){
+ValuedSignature *SignatureEnc::getBooleanSignature(Boolean *bvar) {
        ValuedSignature *bsig = (ValuedSignature *)encoded.get((void *)bvar);
-       if(bsig == NULL){
+       if (bsig == NULL) {
                bsig = interpreter->getBooleanSignature(getUniqueSigID());
                encoded.put(bvar, bsig);
                signatures.push(bsig);
@@ -36,12 +36,12 @@ ValuedSignature *SignatureEnc::getBooleanSignature(Boolean *bvar){
        return bsig;
 }
 
-ValuedSignature *SignatureEnc::getElementSignature(Element *element){
+ValuedSignature *SignatureEnc::getElementSignature(Element *element) {
        ValuedSignature *esig = (ValuedSignature *)encoded.get((void *)element);
-       if(esig == NULL){
+       if (esig == NULL) {
                Set *set = element->getRange();
                Signature *ssig = (Signature *)encoded.get((void *)set);
-               if(ssig == NULL){
+               if (ssig == NULL) {
                        ssig = interpreter->getSetSignature(getUniqueSigID(), set);
                        encoded.put(set, ssig);
                        signatures.push(ssig);
@@ -57,13 +57,13 @@ ValuedSignature *SignatureEnc::getElementSignature(Element *element){
        return esig;
 }
 
-void SignatureEnc::setValue(uint id, uint value){
+void SignatureEnc::setValue(uint id, uint value) {
        ValuedSignature *sig = getValuedSignature(id);
        ASSERT(sig != NULL);
        sig->setValue(value);
 }
 
-int SignatureEnc::getValue(void *astnode){
+int SignatureEnc::getValue(void *astnode) {
        ValuedSignature *sig = (ValuedSignature *)encoded.get(astnode);
        ASSERT(sig != NULL);
        return sig->getValue();
index 988ac71..b11d9c5 100644 (file)
@@ -13,13 +13,13 @@ public:
        ValuedSignature *getElementSignature(Element *element);
        ValuedSignature *getBooleanSignature(Boolean *bvar);
        int getValue(void *astnode);
-       uint64_t getMaxValue(){ return maxValue;}
+       uint64_t getMaxValue() { return maxValue;}
 private:
-       ValuedSignature *getValuedSignature(uint uniqueID){return (ValuedSignature*)signatures.get(uniqueID-1);}
-       uint getUniqueSigID(){return signatures.getSize() +1;}
+       ValuedSignature *getValuedSignature(uint uniqueID) {return (ValuedSignature *)signatures.get(uniqueID - 1);}
+       uint getUniqueSigID() {return signatures.getSize() + 1;}
        void updateMaxValue(Set *set);
        CloneMap encoded;
-       Vector<Signature*> signatures;
+       Vector<Signature *> signatures;
        Interpreter *interpreter;
        uint64_t maxValue;
 };
index 7780931..1b5e028 100644 (file)
 
 using namespace std;
 
-SMTInterpreter::SMTInterpreter(CSolver *_solver)
-       Interpreter(_solver) 
+SMTInterpreter::SMTInterpreter(CSolver *_solver) :
+       Interpreter(_solver)
 {
        output.open(SMTFILENAME);
-       if(!output.is_open()){
+       if (!output.is_open()) {
                model_print("AlloyEnc:Error in opening the dump file satune.smt\n");
                exit(-1);
        }
 }
 
-SMTInterpreter::~SMTInterpreter(){
-       if(output.is_open()){
+SMTInterpreter::~SMTInterpreter() {
+       if (output.is_open()) {
                output.close();
        }
 }
 
 
-ValuedSignature *SMTInterpreter::getBooleanSignature(uint id){
+ValuedSignature *SMTInterpreter::getBooleanSignature(uint id) {
        return new SMTBoolSig(id);
 }
 
-ValuedSignature *SMTInterpreter::getElementSignature(uint id, Signature *ssig){
+ValuedSignature *SMTInterpreter::getElementSignature(uint id, Signature *ssig) {
        return new SMTElementSig(id, (SMTSetSig *)ssig);
 }
 
-Signature *SMTInterpreter::getSetSignature(uint id, Set *set){
+Signature *SMTInterpreter::getSetSignature(uint id, Set *set) {
        return new SMTSetSig(id, set);
 }
 
-void SMTInterpreter::dumpAllConstraints(Vector<char *> &facts){
-       for(uint i=0; i< facts.getSize(); i++){
+void SMTInterpreter::dumpAllConstraints(Vector<char *> &facts) {
+       for (uint i = 0; i < facts.getSize(); i++) {
                char *cstr = facts.get(i);
                writeToFile("(assert " + string(cstr) + ")");
        }
 }
 
-void SMTInterpreter::extractValue(char *idline, char *valueline){
+void SMTInterpreter::extractValue(char *idline, char *valueline) {
        uint id;
-       if (1 == sscanf(idline,"%*[^0123456789]%u", &id)){
+       if (1 == sscanf(idline,"%*[^0123456789]%u", &id)) {
                char valuestr [512];
                ASSERT(1 == sscanf(valueline,"%s)", valuestr));
                uint value;
-               if (strcmp (valuestr, "true)") == 0 ){
-                       value =1;
-               }else if (strcmp(valuestr, "false)") == 0){
+               if (strcmp (valuestr, "true)") == 0 ) {
+                       value = 1;
+               } else if (strcmp(valuestr, "false)") == 0) {
                        value = 0;
-               }else {
+               } else {
                        ASSERT(1 == sscanf(valueline, "%*[^0123456789]%u", &value));
                }
 
@@ -72,19 +72,19 @@ void SMTInterpreter::extractValue(char *idline, char *valueline){
        }
 }
 
-int SMTInterpreter::getResult(){
+int SMTInterpreter::getResult() {
        ifstream input(SMTSOLUTIONFILE, ios::in);
        string line;
-       while(getline(input, line)){
-               if(line.find("unsat")!= line.npos){
+       while (getline(input, line)) {
+               if (line.find("unsat") != line.npos) {
                        return IS_UNSAT;
                }
-               if(line.find("(define-fun") != line.npos || line.find("( (") != line.npos){
+               if (line.find("(define-fun") != line.npos || line.find("( (") != line.npos) {
                        string valueline;
                        ASSERT(getline(input, valueline));
-                       char cline [line.size()+1];
+                       char cline [line.size() + 1];
                        strcpy ( cline, line.c_str() );
-                       char vline [valueline.size()+1];
+                       char vline [valueline.size() + 1];
                        strcpy ( vline, valueline.c_str() );
                        extractValue(cline, vline);
                }
@@ -92,75 +92,75 @@ int SMTInterpreter::getResult(){
        return IS_SAT;
 }
 
-void SMTInterpreter::dumpFooter(){
+void SMTInterpreter::dumpFooter() {
        output << "(check-sat)" << endl;
        output << "(get-model)" << endl;
 }
 
-void SMTInterpreter::dumpHeader(){
+void SMTInterpreter::dumpHeader() {
 }
 
-void SMTInterpreter::compileRunCommand(char * command, size_t size){
+void SMTInterpreter::compileRunCommand(char *command, size_t size) {
        model_print("Calling Z3...\n");
        snprintf(command, size, "./run.sh z3 -T:%u -in < %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
 }
 
-string SMTInterpreter::negateConstraint(string constr){
+string SMTInterpreter::negateConstraint(string constr) {
        return "( not " + constr + " )";
 }
 
-string SMTInterpreter::encodeBooleanLogic( BooleanLogic *bl){
+string SMTInterpreter::encodeBooleanLogic( BooleanLogic *bl) {
        uint size = bl->inputs.getSize();
        string array[size];
        for (uint i = 0; i < size; i++)
                array[i] = encodeConstraint(bl->inputs.get(i));
        string op;
-       switch (bl->op){
-               case SATC_OR:
-                       op = "or";
-                       break;
-               case SATC_AND:
-                       op = "and";
-                       break;
-               case SATC_NOT:
-                       op = "not";
-                       break;
-               case SATC_IMPLIES:
-                       op = "=>";
-                       break;
-               case SATC_XOR:
-               default:
-                       ASSERT(0);
+       switch (bl->op) {
+       case SATC_OR:
+               op = "or";
+               break;
+       case SATC_AND:
+               op = "and";
+               break;
+       case SATC_NOT:
+               op = "not";
+               break;
+       case SATC_IMPLIES:
+               op = "=>";
+               break;
+       case SATC_XOR:
+       default:
+               ASSERT(0);
        }
        switch (bl->op) {
-               case SATC_XOR:
-               case SATC_OR:
-               case SATC_AND:{
-                       ASSERT(size >= 2);
-                       string res = array[0];
-                       for( uint i=1; i< size; i++){
-                               res = "( " + op + " " + res + " " +  array[i] + " )";
-                       }
-                       return res;
+       case SATC_XOR:
+       case SATC_OR:
+       case SATC_AND: {
+               ASSERT(size >= 2);
+               string res = array[0];
+               for ( uint i = 1; i < size; i++) {
+                       res = "( " + op + " " + res + " " +  array[i] + " )";
                }
-               case SATC_NOT:{
-                       return "( not " + array[0] + " )";
-               }
-               case SATC_IMPLIES:
-                       return "( " + op + " " + array[0] + " " + array[1] + " )";
-               case SATC_IFF:
-               default:
-                       ASSERT(0);
+               return res;
+       }
+       case SATC_NOT: {
+               return "( not " + array[0] + " )";
+       }
+       case SATC_IMPLIES:
+               return "( " + op + " " + array[0] + " " + array[1] + " )";
+       case SATC_IFF:
+       default:
+               ASSERT(0);
 
        }
 }
 
-string SMTInterpreter::encodeBooleanVar( BooleanVar *bv){
-       ValuedSignature * boolSig = sigEnc.getBooleanSignature(bv);
+string SMTInterpreter::encodeBooleanVar( BooleanVar *bv) {
+       ValuedSignature *boolSig = sigEnc.getBooleanSignature(bv);
        return *boolSig + "";
 }
 
-string SMTInterpreter::processElementFunction(ElementFunction* elemFunc, ValuedSignature *signature){
+string SMTInterpreter::processElementFunction(ElementFunction *elemFunc, ValuedSignature *signature) {
        FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
        uint numDomains = elemFunc->inputs.getSize();
        ASSERT(numDomains > 1);
@@ -169,22 +169,22 @@ string SMTInterpreter::processElementFunction(ElementFunction* elemFunc, ValuedS
        for (uint i = 0; i < numDomains; i++) {
                Element *elem = elemFunc->inputs.get(i);
                inputs[i] = sigEnc.getElementSignature(elem);
-               if(elem->type == ELEMFUNCRETURN){
+               if (elem->type == ELEMFUNCRETURN) {
                        result += processElementFunction((ElementFunction *) elem, inputs[i]);
                }
        }
        string op;
-       switch(function->op){
-               case SATC_ADD:
-                       op = "+";
-                       break;
-               case SATC_SUB:
-                       op = "-";
-                       break;
-               default:
-                       ASSERT(0);
+       switch (function->op) {
+       case SATC_ADD:
+               op = "+";
+               break;
+       case SATC_SUB:
+               op = "-";
+               break;
+       default:
+               ASSERT(0);
        }
-       result += "( = " + *signature; 
+       result += "( = " + *signature;
        string tmp = "" + *inputs[0];
        for (uint i = 1; i < numDomains; i++) {
                tmp = "( " + op + " " + tmp + " " + *inputs[i] + " )";
@@ -193,16 +193,16 @@ string SMTInterpreter::processElementFunction(ElementFunction* elemFunc, ValuedS
        return result;
 }
 
-string SMTInterpreter::operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2){
+string SMTInterpreter::operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2) {
        switch (op) {
-               case SATC_EQUALS:
-                       return "( = " + *elemSig1 + " " + *elemSig2 +" )";
-               case SATC_LT:
-                       return "( < " + *elemSig1 + " " + *elemSig2 + " )";
-               case SATC_GT:
-                       return "(> " + *elemSig1 + " " + *elemSig2 + " )";
-               default:
-                       ASSERT(0);
+       case SATC_EQUALS:
+               return "( = " + *elemSig1 + " " + *elemSig2 + " )";
+       case SATC_LT:
+               return "( < " + *elemSig1 + " " + *elemSig2 + " )";
+       case SATC_GT:
+               return "(> " + *elemSig1 + " " + *elemSig2 + " )";
+       default:
+               ASSERT(0);
        }
 }
 
index 035e76b..37dae88 100644 (file)
@@ -10,7 +10,7 @@
 #define SMTFILENAME "satune.smt"
 #define SMTSOLUTIONFILE "solution.sol"
 
-class SMTInterpreter: public Interpreter{
+class SMTInterpreter : public Interpreter {
 public:
        SMTInterpreter(CSolver *solver);
        virtual ValuedSignature *getBooleanSignature(uint id);
@@ -20,7 +20,7 @@ public:
 protected:
        virtual void dumpFooter();
        virtual void dumpHeader();
-       virtual void compileRunCommand(char * command , size_t size);
+       virtual void compileRunCommand(char *command, size_t size);
        virtual int getResult();
        virtual void dumpAllConstraints(Vector<char *> &facts);
        virtual string negateConstraint(string constr);
index 9742bda..2a59cc5 100644 (file)
@@ -4,24 +4,24 @@
  * and open the template in the editor.
  */
 
-/* 
+/*
  * File:   smtratinterpreter.cc
  * Author: hamed
- * 
+ *
  * Created on February 21, 2019, 2:33 PM
  */
 
 #include "smtratinterpreter.h"
 
-SMTRatInterpreter::SMTRatInterpreter(CSolver *solver)
+SMTRatInterpreter::SMTRatInterpreter(CSolver *solver) :
        SMTInterpreter(solver)
-{      
+{
 }
 
-void SMTRatInterpreter::compileRunCommand(char * command , size_t size){
+void SMTRatInterpreter::compileRunCommand(char *command, size_t size) {
        model_print("Calling SMTRat...\n");
        snprintf(command, size, "./run.sh timeout %u smtrat %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
 }
 
-SMTRatInterpreter::~SMTRatInterpreter(){
+SMTRatInterpreter::~SMTRatInterpreter() {
 }
index f2afb49..f6eea03 100644 (file)
@@ -4,7 +4,7 @@
  * and open the template in the editor.
  */
 
-/* 
+/*
  * File:   smtratinterpreter.h
  * Author: hamed
  *
 #define SMTRATINTERPRETER_H
 #include "smtinterpreter.h"
 
-class SMTRatInterpreter: public SMTInterpreter{
+class SMTRatInterpreter : public SMTInterpreter {
 public:
        SMTRatInterpreter(CSolver *solver);
        virtual ~SMTRatInterpreter();
 protected:
-       void compileRunCommand(char * command , size_t size);
+       void compileRunCommand(char *command, size_t size);
 };
 
-#endif /* SMTRATINTERPRETER_H */
+#endif/* SMTRATINTERPRETER_H */
 
index 4c77493..6ccbd22 100644 (file)
@@ -1,39 +1,39 @@
 #include "smtsig.h"
 #include "set.h"
 
-SMTBoolSig::SMTBoolSig(uint id):
+SMTBoolSig::SMTBoolSig(uint id) :
        ValuedSignature(id)
 {
 }
 
-string SMTBoolSig::toString() const{
+string SMTBoolSig::toString() const {
        return "b" + to_string(id);
 }
 
-string SMTBoolSig::getSignature() const{
+string SMTBoolSig::getSignature() const {
        return "(declare-const b" + to_string(id) + " Bool)";
 }
 
-string SMTBoolSig::getAbsSignature() const{
+string SMTBoolSig::getAbsSignature() const {
        return "";
 }
 
-SMTElementSig::SMTElementSig(uint id, SMTSetSig *_ssig)
+SMTElementSig::SMTElementSig(uint id, SMTSetSig *_ssig) :
        ValuedSignature(id),
        ssig(_ssig)
 {
 }
 
-string SMTElementSig::toString() const{
+string SMTElementSig::toString() const {
        return "e" + to_string(id);
 }
 
-string SMTElementSig::getSignature() const{
+string SMTElementSig::getSignature() const {
        string str = "(declare-const e" + to_string(id) + " Int)\n";
        string constraint = ssig->getAbsSignature();
        size_t start_pos;
        string placeholder = "$";
-       while((start_pos = constraint.find(placeholder)) != string::npos){
+       while ((start_pos = constraint.find(placeholder)) != string::npos) {
                constraint.replace(start_pos, placeholder.size(), to_string(id));
        }
        //constraint.replace(constraint.begin(), constraint.end(), "$", );
@@ -41,41 +41,41 @@ string SMTElementSig::getSignature() const{
        return str;
 }
 
-string SMTElementSig::getAbsSignature() const{
+string SMTElementSig::getAbsSignature() const {
        return "";
-       
+
 }
 
-SMTSetSig::SMTSetSig(uint id, Set *set): Signature(id){
+SMTSetSig::SMTSetSig(uint id, Set *set) : Signature(id) {
        ASSERT(set->getSize() > 0);
-       int min = set->getElement(0), max = set->getElement(set->getSize()-1);
+       int min = set->getElement(0), max = set->getElement(set->getSize() - 1);
        Vector<int> holes;
        int prev = set->getElement(0);
-       for(uint i=1; i< set->getSize(); i++){
+       for (uint i = 1; i < set->getSize(); i++) {
                int curr = set->getElement(i);
-               if(prev != curr -1){
-                       for(int j=prev+1; j< curr; j++){
+               if (prev != curr - 1) {
+                       for (int j = prev + 1; j < curr; j++) {
                                holes.push(j);
                        }
                }
                prev = curr;
        }
-       constraint = "(assert (<= e$ " + to_string(max) +"))\n";
-       constraint += "(assert (>= e$ " + to_string(min) +"))\n";
-       for(uint i=0; i< holes.getSize(); i++){
-               constraint += "(assert (not (= e$ " + to_string(holes.get(i)) +")))\n";
+       constraint = "(assert (<= e$ " + to_string(max) + "))\n";
+       constraint += "(assert (>= e$ " + to_string(min) + "))\n";
+       for (uint i = 0; i < holes.getSize(); i++) {
+               constraint += "(assert (not (= e$ " + to_string(holes.get(i)) + ")))\n";
        }
 }
 
-string SMTSetSig::toString() const{
+string SMTSetSig::toString() const {
        return "";
 }
 
-string SMTSetSig::getSignature() const{
+string SMTSetSig::getSignature() const {
        return "";
 }
 
-string SMTSetSig::getAbsSignature() const{
+string SMTSetSig::getAbsSignature() const {
        return constraint;
-       
+
 }
index 7804176..21271e2 100644 (file)
@@ -6,19 +6,19 @@
 #include "classlist.h"
 using namespace std;
 
-class SMTBoolSig: public ValuedSignature{
+class SMTBoolSig : public ValuedSignature {
 public:
        SMTBoolSig(uint id);
-       virtual ~SMTBoolSig(){}
+       virtual ~SMTBoolSig() {}
        virtual string toString() const;
        virtual string getAbsSignature() const;
        virtual string getSignature() const;
 };
 
-class SMTSetSig: public Signature{
+class SMTSetSig : public Signature {
 public:
        SMTSetSig(uint id, Set *set);
-       virtual ~SMTSetSig(){}
+       virtual ~SMTSetSig() {}
        virtual string toString() const;
        virtual string getAbsSignature() const;
        virtual string getSignature() const;
@@ -26,10 +26,10 @@ private:
        string constraint;
 };
 
-class SMTElementSig: public ValuedSignature{
+class SMTElementSig : public ValuedSignature {
 public:
        SMTElementSig(uint id, SMTSetSig *ssig);
-       virtual ~SMTElementSig(){}
+       virtual ~SMTElementSig() {}
        virtual string toString() const;
        virtual string getAbsSignature() const;
        virtual string getSignature() const;
index eac11e9..d0cfb6c 100644 (file)
@@ -29,7 +29,7 @@ Deserializer::Deserializer(const char *file, InterpreterType itype) :
        if (filedesc < 0) {
                exit(-1);
        }
-       if(itype != SATUNE){
+       if (itype != SATUNE) {
                solver->setInterpreter(itype);
        }
 }
index 8677bf3..69c29fb 100644 (file)
@@ -1,14 +1,14 @@
 #include "csolver.h"
 
 
-InterpreterType getInterpreterType(char * itype){
-       if(strcmp (itype,"--alloy") == 0){
+InterpreterType getInterpreterType(char *itype) {
+       if (strcmp (itype,"--alloy") == 0) {
                return ALLOY;
-       } else if(strcmp (itype,"--z3") == 0){
+       } else if (strcmp (itype,"--z3") == 0) {
                return Z3;
-       } else if(strcmp (itype,"--smtrat") == 0){
+       } else if (strcmp (itype,"--smtrat") == 0) {
                return SMTRAT;
-       } else if(strcmp (itype,"--mathsat") == 0){
+       } else if (strcmp (itype,"--mathsat") == 0) {
                return MATHSAT;
        } else {
                printf("Unknown interpreter type: %s\n", itype);
@@ -24,10 +24,10 @@ int main(int argc, char **argv) {
                printf("./run.sh deserializer test.dump [--alloy/--z3/--smtrat/--mathsat] [timeout]\n");
                exit(-1);
        }
-       CSolver *solver; 
-       if(argc >= 3){
+       CSolver *solver;
+       if (argc >= 3) {
                solver = CSolver::deserialize(argv[1], getInterpreterType(argv[2]));
-               if(argc == 4){
+               if (argc == 4) {
                        solver->setSatSolverTimeout(atol(argv[3]));
                }
        } else {
index 8a3ccbd..8a3395a 100644 (file)
@@ -7,7 +7,7 @@ int main(int argc, char **argv) {
                printf("You should specify a tuner: %s <best.tuner>\n", argv[0]);
                exit(-1);
        }
-       
+
        SearchTuner *tuner = new SearchTuner(argv[1]);
        tuner->print();
        delete tuner;
index e2ecbd8..8ba717e 100644 (file)
@@ -5,20 +5,20 @@
 #include "comptuner.h"
 #include "randomtuner.h"
 
-void printKnownTunerTypes(){
+void printKnownTunerTypes() {
        printf("Known Tuner Types:\nRandom Tuner=1\nComp Tuner=2\nKmeans Tuner=3\nSimulated Annealing Tuner=4\n");
 }
 
-BasicTuner *createTuner(uint tunertype, uint budget, uint rounds, uint timeout){
-       switch(tunertype){
-               case 1: return new RandomTuner(budget, timeout);
-               case 2: return new CompTuner(budget, timeout);
-               case 3: return new KMeansTuner(budget, rounds, timeout);
-               case 4: return new SATuner(budget, timeout);
-               default:
-                       printf("Tuner type %u is unknown\n", tunertype);
-                       printKnownTunerTypes();
-                       exit(-1);
+BasicTuner *createTuner(uint tunertype, uint budget, uint rounds, uint timeout) {
+       switch (tunertype) {
+       case 1: return new RandomTuner(budget, timeout);
+       case 2: return new CompTuner(budget, timeout);
+       case 3: return new KMeansTuner(budget, rounds, timeout);
+       case 4: return new SATuner(budget, timeout);
+       default:
+               printf("Tuner type %u is unknown\n", tunertype);
+               printKnownTunerTypes();
+               exit(-1);
        }
 
 }
@@ -47,7 +47,7 @@ int main(int argc, char **argv) {
                        else
                                multituner->addProblem(argv[i]);
                } else
-                       multituner->addTuner(new SearchTuner(argv[i], true )); //add settings to usedsettigs
+                       multituner->addTuner(new SearchTuner(argv[i], true ));//add settings to usedsettigs
        }
 
        if (!tunerfiles) {
index 889b543..31b4375 100644 (file)
@@ -4,10 +4,10 @@
  * and open the template in the editor.
  */
 
-/* 
+/*
  * File:   basictuner.cc
  * Author: hamed
- * 
+ *
  * Created on December 17, 2018, 2:02 PM
  */
 
@@ -38,7 +38,7 @@ void TunerRecord::setTime(Problem *problem, long long time) {
        timetaken.put(problem, time);
 }
 
-void TunerRecord::print(){
+void TunerRecord::print() {
        model_print("*************TUNER NUMBER=%d***********\n", tunernumber);
        tuner->print();
        model_print("&&&&&&&&&&&&&USED SETTINGS &&&&&&&&&&&&\n");
@@ -46,7 +46,7 @@ void TunerRecord::print(){
        model_print("\n");
 }
 
-void TunerRecord::printProblemsInfo(){
+void TunerRecord::printProblemsInfo() {
        for (uint j = 0; j < problems.getSize(); j++) {
                Problem *problem = problems.get(j);
                model_print("Problem %s\n", problem->getProblem());
@@ -70,7 +70,7 @@ TunerRecord *TunerRecord::changeTuner(SearchTuner *_newtuner) {
 
 
 BasicTuner::BasicTuner(uint _budget, uint _timeout) :
-       budget(_budget), timeout(_timeout), execnum(0){
+       budget(_budget), timeout(_timeout), execnum(0) {
 }
 
 BasicTuner::~BasicTuner() {
@@ -102,10 +102,10 @@ void BasicTuner::printData() {
        }
 }
 
-bool BasicTuner::tunerExists(TunerRecord *tunerec){
+bool BasicTuner::tunerExists(TunerRecord *tunerec) {
        SearchTuner *tuner = tunerec->getTuner();
-       for(uint i=0; i< explored.getSize(); i++){
-               if(explored.get(i)->getTuner()->equalUsed(tuner)){
+       for (uint i = 0; i < explored.getSize(); i++) {
+               if (explored.get(i)->getTuner()->equalUsed(tuner)) {
                        model_print("************Tuner <%d> is replicate of Tuner <%d>\n", tunerec->getTunerNumber(), explored.get(i)->getTunerNumber());
                        return true;
                }
@@ -209,10 +209,10 @@ SearchTuner *BasicTuner::mutateTuner(SearchTuner *oldTuner, uint k) {
        return newTuner;
 }
 
-int BasicTuner::subTunerIndex(SearchTuner *newTuner){
-       for (uint i=0; i< explored.getSize(); i++){
+int BasicTuner::subTunerIndex(SearchTuner *newTuner) {
+       for (uint i = 0; i < explored.getSize(); i++) {
                SearchTuner *tuner = explored.get(i)->getTuner();
-               if(tuner->isSubTunerof(newTuner)){
+               if (tuner->isSubTunerof(newTuner)) {
                        return i;
                }
        }
index 14ab7d8..0df9a65 100644 (file)
@@ -4,7 +4,7 @@
  * and open the template in the editor.
  */
 
-/* 
+/*
  * File:   basictuner.h
  * Author: hamed
  *
@@ -25,11 +25,11 @@ class Problem {
 public:
        Problem(const char *problem);
        char *getProblem() {return problem;}
-       inline int getResult(){return result;}
-       inline int getProblemNumber(){return problemnumber;}
-       inline void setResult(int res){result = res;}
-       inline void setProblemNumber(int probNum){problemnumber = probNum;}
-       inline long long getBestTime() {return besttime ;} 
+       inline int getResult() {return result;}
+       inline int getProblemNumber() {return problemnumber;}
+       inline void setResult(int res) {result = res;}
+       inline void setProblemNumber(int probNum) {problemnumber = probNum;}
+       inline long long getBestTime() {return besttime ;}
        inline void setBestTime(long long time) {besttime = time;}
        ~Problem();
        CMEMALLOC;
@@ -45,18 +45,18 @@ public:
        TunerRecord(SearchTuner *_tuner) : tuner(_tuner), tunernumber(-1), isduplicate(false) {}
        TunerRecord(SearchTuner *_tuner, int _tunernumber) : tuner(_tuner), tunernumber(_tunernumber), isduplicate(false) {}
        SearchTuner *getTuner() {return tuner;}
-       void inline addProblem(Problem * problem){problems.push(problem);}
+       void inline addProblem(Problem *problem) {problems.push(problem);}
        TunerRecord *changeTuner(SearchTuner *_newtuner);
        void updateTuner(SearchTuner *_newtuner) {tuner = _newtuner;}
        long long getTime(Problem *problem);
        void setTime(Problem *problem, long long time);
-       inline void setTunerNumber(int numb){tunernumber = numb;}
-       inline int getTunerNumber(){return tunernumber;}
+       inline void setTunerNumber(int numb) {tunernumber = numb;}
+       inline int getTunerNumber() {return tunernumber;}
        inline uint problemsSize() {return problems.getSize();}
        inline void setDuplicate(bool _duplicate) { isduplicate = _duplicate;}
        inline bool isDuplicate() {return isduplicate;}
-       inline Problem *getProblem(uint index){return problems.get(index);}
-        void print();
+       inline Problem *getProblem(uint index) {return problems.get(index);}
+       void print();
        void printProblemsInfo();
        CMEMALLOC;
 private:
@@ -80,12 +80,12 @@ public:
 protected:
        long long evaluate(Problem *problem, TunerRecord *tuner);
        /**
-         * returns the index of the tuner which is subtune of
-         * the newTuner 
-         * @param newTuner
-         * @return 
-         */
-        int subTunerIndex(SearchTuner *newTuner);
+        * returns the index of the tuner which is subtune of
+        * the newTuner
+        * @param newTuner
+        * @return
+        */
+       int subTunerIndex(SearchTuner *newTuner);
        bool tunerExists(TunerRecord *tunerRec);
        SearchTuner *mutateTuner(SearchTuner *oldTuner, uint k);
        void updateTimeout(Problem *problem, long long metric);
@@ -98,5 +98,5 @@ protected:
        int execnum;
 };
 
-#endif /* BASICTUNER_H */
+#endif/* BASICTUNER_H */
 
index 895e06b..8069915 100644 (file)
@@ -11,8 +11,8 @@ CompTuner::CompTuner(uint _budget, uint _timeout) :
 {
 }
 
-CompTuner::~CompTuner(){
-       
+CompTuner::~CompTuner() {
+
 }
 
 void CompTuner::findBestThreeTuners() {
@@ -127,12 +127,12 @@ void CompTuner::tune() {
                model_print("Round %u of %u\n", b, budget);
                Hashtable<TunerRecord *, int, uint64_t> scores;
                Vector<Vector<TunerRecord *> *> allplaces;
-               for(uint ii=0; ii< problems.getSize(); ii++){
+               for (uint ii = 0; ii < problems.getSize(); ii++) {
                        allplaces.push(new Vector<TunerRecord *>());
                }
                for (uint j = 0; j < tunerV->getSize(); j++) {
                        TunerRecord *tuner = tunerV->get(j);
-                       
+
                        for (uint i = 0; i < problems.getSize(); i++) {
                                Vector<TunerRecord *> *places = allplaces.get(i);
                                Problem *problem = problems.get(i);
@@ -148,8 +148,8 @@ void CompTuner::tune() {
                                                tuner->setTime(problem, metric);
                                        else
                                                tuner->setTime(problem, -2);
-                                       
-                                       if(tunerExists(tuner)){
+
+                                       if (tunerExists(tuner)) {
                                                //Solving the problem and noticing the tuner
                                                //already exists
                                                tuner->setDuplicate(true);
@@ -167,13 +167,13 @@ void CompTuner::tune() {
                                }
                        }
                }
-               for(uint ii=0; ii < problems.getSize(); ii++){
+               for (uint ii = 0; ii < problems.getSize(); ii++) {
                        Problem *problem = problems.get(ii);
                        Vector<TunerRecord *> *places = allplaces.get(ii);
                        int points = 9;
                        for (uint k = 0; k < places->getSize() && points; k++) {
                                TunerRecord *tuner = places->get(k);
-                               if(tuner->isDuplicate()){
+                               if (tuner->isDuplicate()) {
                                        continue;
                                }
                                int currScore = 0;
@@ -186,7 +186,7 @@ void CompTuner::tune() {
                                points = points / 3;
                        }
                }
-               for(uint ii=0; ii< problems.getSize(); ii++){
+               for (uint ii = 0; ii < problems.getSize(); ii++) {
                        delete allplaces.get(ii);
                }
                Vector<TunerRecord *> ranking;
@@ -220,7 +220,7 @@ void CompTuner::tune() {
                uint tSize = tunerV->getSize();
                for (uint i = 0; i < tSize; i++) {
                        SearchTuner *tmpTuner = mutateTuner(tunerV->get(i)->getTuner(), b);
-                       while(subTunerIndex(tmpTuner) != -1){
+                       while (subTunerIndex(tmpTuner) != -1) {
                                model_print("******** New Tuner already explored...\n");
                                delete tmpTuner;
                                tmpTuner = mutateTuner(tunerV->get(i)->getTuner(), b);
index dd28105..39e7946 100644 (file)
@@ -13,7 +13,7 @@ public:
        void tune();
        void findBestThreeTuners();
 protected:
-       
+
 };
 
 inline long long min(long long num1, long long num2, long long num3) {
index 333d9d9..a4c1cdc 100644 (file)
@@ -4,10 +4,10 @@
  * and open the template in the editor.
  */
 
-/* 
+/*
  * File:   kmeanstuner.cc
  * Author: hamed
- * 
+ *
  * Created on December 19, 2018, 4:16 PM
  */
 
@@ -16,7 +16,7 @@
 #include "searchtuner.h"
 #include "math.h"
 
-KMeansTuner::KMeansTuner(uint budget, uint _rounds, uint timeout) : 
+KMeansTuner::KMeansTuner(uint budget, uint _rounds, uint timeout) :
        BasicTuner(budget, timeout),
        rounds(_rounds) {
 }
index a6025a3..1e8adb3 100644 (file)
@@ -4,7 +4,7 @@
  * and open the template in the editor.
  */
 
-/* 
+/*
  * File:   kmeanstuner.h
  * Author: hamed
  *
@@ -30,5 +30,5 @@ private:
        uint rounds;
 };
 
-#endif /* KMEANSTUNER_H */
+#endif/* KMEANSTUNER_H */
 
index 6fefc46..04b5e7c 100644 (file)
@@ -8,24 +8,24 @@
 
 #define UNSETVALUE -1
 
-RandomTuner::RandomTuner(uint _budget, uint _timeout) : 
+RandomTuner::RandomTuner(uint _budget, uint _timeout) :
        BasicTuner(_budget, _timeout) {
 }
 
-RandomTuner::~RandomTuner(){
-       
+RandomTuner::~RandomTuner() {
+
 }
 
 void RandomTuner::tune() {
        for (uint r = 0; r < budget; r++) {
                model_print("Round %u of %u\n", r, budget);
-               for (uint i = 0; i < tuners.getSize(); i++){
+               for (uint i = 0; i < tuners.getSize(); i++) {
                        TunerRecord *tuner = tuners.get(i);
                        bool isNew = true;
-                       for (uint j = 0; j < problems.getSize(); j++){
+                       for (uint j = 0; j < problems.getSize(); j++) {
                                Problem *problem = problems.get(j);
                                long long metric = tuner->getTime(problem);
-                               if(metric == -1){
+                               if (metric == -1) {
                                        metric = evaluate(problem, tuner);
                                        ASSERT(tuner->getTime(problem) == -1);
                                        tuner->addProblem(problem);
@@ -34,7 +34,7 @@ void RandomTuner::tune() {
                                                tuner->setTime(problem, metric);
                                        else
                                                tuner->setTime(problem, -2);
-                                       if(tunerExists(tuner)){
+                                       if (tunerExists(tuner)) {
                                                //Solving the problem and noticing the tuner
                                                //already exists
                                                isNew = false;
@@ -42,15 +42,15 @@ void RandomTuner::tune() {
                                        }
                                }
                        }
-                       if(isNew){
+                       if (isNew) {
                                explored.push(tuner);
                        }
-                       
+
                }
                uint tSize = tuners.getSize();
                for (uint i = 0; i < tSize; i++) {
                        SearchTuner *tmpTuner = mutateTuner(tuners.get(i)->getTuner(), budget);
-                       while(subTunerIndex(tmpTuner) != -1){
+                       while (subTunerIndex(tmpTuner) != -1) {
                                tmpTuner->randomMutate();
                        }
                        TunerRecord *tmp = new TunerRecord(tmpTuner);
@@ -61,5 +61,5 @@ void RandomTuner::tune() {
                }
        }
        printData();
-       
+
 }
index 75b8800..47612da 100644 (file)
@@ -6,7 +6,7 @@
 #include "basictuner.h"
 
 /**
- * This is a Tuner which is being used for 
+ * This is a Tuner which is being used for
  */
 class RandomTuner : public BasicTuner {
 public:
@@ -14,7 +14,7 @@ public:
        virtual ~RandomTuner();
        void tune();
 protected:
-        bool randomMutation(SearchTuner *tuner);        
+       bool randomMutation(SearchTuner *tuner);
        TunerRecord *tune(SearchTuner *tuner);
 };
 
index 61c9c35..4844ce3 100644 (file)
@@ -12,28 +12,28 @@ SATuner::SATuner(uint _budget, uint _timeout) :
 {
 }
 
-SATuner::~SATuner(){
+SATuner::~SATuner() {
 
 }
 
-void SATuner::rankTunerForProblem(Vector<TunerRecord *> *places, TunerRecord *tuner, Problem *problem, long long metric){
+void SATuner::rankTunerForProblem(Vector<TunerRecord *> *places, TunerRecord *tuner, Problem *problem, long long metric) {
        uint k = 0;
        for (; k < places->getSize(); k++) {
                if (metric < places->get(k)->getTime(problem))
                        break;
        }
        model_print("Problem<%s>:place[%u]=Tuner<%p,%d>\n", problem->getProblem(), k, tuner, tuner->getTunerNumber());
-       places->insertAt(k, tuner);             
+       places->insertAt(k, tuner);
 }
 
-void SATuner::removeTunerIndex(Vector<TunerRecord *> *tunerV, int index,  Vector<Vector<TunerRecord *> *> &allplaces){
+void SATuner::removeTunerIndex(Vector<TunerRecord *> *tunerV, int index,  Vector<Vector<TunerRecord *> *> &allplaces) {
        TunerRecord *tuner = tunerV->get(index);
        model_print("Removing Tuner %d\n", tuner->getTunerNumber());
        tunerV->set(index, NULL);
-       for(uint i=0; i < allplaces.getSize(); i++){
+       for (uint i = 0; i < allplaces.getSize(); i++) {
                Vector<TunerRecord *> *places = allplaces.get(i);
-               for(uint j=0; j < places->getSize(); j++){
-                       if(tuner == places->get(j)){
+               for (uint j = 0; j < places->getSize(); j++) {
+                       if (tuner == places->get(j)) {
                                places->removeAt(j);
                                break;
                        }
@@ -42,32 +42,32 @@ void SATuner::removeTunerIndex(Vector<TunerRecord *> *tunerV, int index,  Vector
 
 }
 
-void SATuner::removeNullsFromTunerVector( Vector<TunerRecord *> *tunerV){
-       for (int i= tunerV->getSize() -1; i >= 0; i--){
-               if(tunerV->get(i) == NULL){
+void SATuner::removeNullsFromTunerVector( Vector<TunerRecord *> *tunerV) {
+       for (int i = tunerV->getSize() - 1; i >= 0; i--) {
+               if (tunerV->get(i) == NULL) {
                        tunerV->removeAt(i);
                }
        }
        model_print("TunerV size after removing nulls = %u\n", tunerV->getSize());
 }
 
-void SATuner::initialize(Vector<TunerRecord *> *tunerV, Vector<Vector<TunerRecord *> *> &allplaces){
-       for(uint ii=0; ii< problems.getSize(); ii++){
+void SATuner::initialize(Vector<TunerRecord *> *tunerV, Vector<Vector<TunerRecord *> *> &allplaces) {
+       for (uint ii = 0; ii < problems.getSize(); ii++) {
                allplaces.push(new Vector<TunerRecord *>());
        }
-       for (uint j = 0; j< tunerV->getSize(); j++){
+       for (uint j = 0; j < tunerV->getSize(); j++) {
                TunerRecord *tuner = tunerV->get(j);
-               for (uint i=0; i < problems.getSize(); i++){
+               for (uint i = 0; i < problems.getSize(); i++) {
                        Problem *problem = problems.get(i);
                        long long metric = evaluate(problem, tuner);
                        ASSERT(tuner->getTime(problem) == -1);
                        tuner->addProblem(problem);
-                       if(metric != -1){
-                               tuner->setTime(problem , metric);
-                       }else{
-                               tuner->setTime(problem , -2);
+                       if (metric != -1) {
+                               tuner->setTime(problem, metric);
+                       } else {
+                               tuner->setTime(problem, -2);
                        }
-                       if(metric >=0){
+                       if (metric >= 0) {
                                Vector<TunerRecord *> *places = allplaces.get(i);
                                rankTunerForProblem(places, tuner, problem, metric);
                        }
@@ -77,27 +77,27 @@ void SATuner::initialize(Vector<TunerRecord *> *tunerV, Vector<Vector<TunerRecor
 }
 
 void SATuner::tune() {
-       Vector<TunerRecord *> *tunerV = new Vector<TunerRecord *>(&tuners);     
+       Vector<TunerRecord *> *tunerV = new Vector<TunerRecord *>(&tuners);
        Vector<Vector<TunerRecord *> *> allplaces;
        uint tunerNumber = tuners.getSize();
        //Initialization
        initialize(tunerV, allplaces);
        //Starting the body of algorithm
-       for (uint t = budget; t >0; t--) {
+       for (uint t = budget; t > 0; t--) {
                model_print("Current Temperature = %u\n", t);
                Hashtable<TunerRecord *, int, uint64_t> scores;
                for (uint i = 0; i < tunerNumber; i++) {
-                       SearchTuner *tmpTuner = mutateTuner(tunerV->get(i)->getTuner(), budget-t);
+                       SearchTuner *tmpTuner = mutateTuner(tunerV->get(i)->getTuner(), budget - t);
                        int tunerIndex = subTunerIndex(tmpTuner);
                        TunerRecord *tmp = NULL;
-                       if(tunerIndex == -1){
+                       if (tunerIndex == -1) {
                                tmp = new TunerRecord(tmpTuner);
                                tmp->setTunerNumber(allTuners.getSize());
                                model_print("Mutated tuner %u to generate tuner %u\n", tunerV->get(i)->getTunerNumber(), tmp->getTunerNumber());
-                               allTuners.push(tmp);    
-                       }else{
+                               allTuners.push(tmp);
+                       } else {
                                //Previous tuners might get explored with new combination of tuners.
-                               tmp = explored.get(tunerIndex); 
+                               tmp = explored.get(tunerIndex);
                                model_print("Using exploread tuner <%u>\n", tmp->getTunerNumber());
                        }
                        tunerV->push(tmp);
@@ -129,11 +129,11 @@ void SATuner::tune() {
                                }
                        }
                }
-               for(uint ii=0; ii < problems.getSize(); ii++){
+               for (uint ii = 0; ii < problems.getSize(); ii++) {
                        Problem *problem = problems.get(ii);
                        ASSERT(ii < allplaces.getSize());
                        Vector<TunerRecord *> *places = allplaces.get(ii);
-                       int points = pow(tunerNumber*1.0, 2*tunerNumber - 1);
+                       int points = pow(tunerNumber * 1.0, 2 * tunerNumber - 1);
                        for (uint k = 0; k < places->getSize() && points; k++) {
                                TunerRecord *tuner = places->get(k);
                                int currScore = 0;
@@ -147,7 +147,7 @@ void SATuner::tune() {
                        }
                }
 
-               for(uint i= 0; i < tunerNumber; i++){
+               for (uint i = 0; i < tunerNumber; i++) {
                        ASSERT(i < tunerV->getSize());
                        TunerRecord *tuner1 = tunerV->get(i);
                        TunerRecord *tuner2 = tunerV->get(tunerNumber + i);
@@ -157,28 +157,28 @@ void SATuner::tune() {
                        ASSERT(scores.contains(tuner2));
                        int score1 = scores.get(tuner1);
                        int score2 = scores.get(tuner2);
-                       if( score2 > score1 ){
+                       if ( score2 > score1 ) {
                                removeTunerIndex(tunerV, i, allplaces);
-                       } else if( score2 < score1){
-                               model_print("score1=%d\tscore2=%d\tt=%u\texp=%f\n", score1, score2, t, exp((score1-score2)*1.0/t));
-                               double prob = 1/(exp((score1-score2)*1.0/t) );
+                       } else if ( score2 < score1) {
+                               model_print("score1=%d\tscore2=%d\tt=%u\texp=%f\n", score1, score2, t, exp((score1 - score2) * 1.0 / t));
+                               double prob = 1 / (exp((score1 - score2) * 1.0 / t) );
                                double random = ((double) rand() / (RAND_MAX));
                                model_print("prob=%f\trandom=%f\n", prob, random);
-                               if(prob > random){
+                               if (prob > random) {
                                        removeTunerIndex(tunerV, i, allplaces);
-                               }else{
+                               } else {
                                        removeTunerIndex(tunerV, tunerNumber + i, allplaces);
                                }
-                       } else{
+                       } else {
                                double random = ((double) rand() / (RAND_MAX));
-                               int index = random > 0.5? i : tunerNumber + i;
+                               int index = random > 0.5 ? i : tunerNumber + i;
                                removeTunerIndex(tunerV, index, allplaces);
                        }
                }
                removeNullsFromTunerVector(tunerV);
-               
+
        }
-       for(uint ii=0; ii< allplaces.getSize(); ii++){
+       for (uint ii = 0; ii < allplaces.getSize(); ii++) {
                delete allplaces.get(ii);
        }
        printData();
index fd05423..34ed7ae 100644 (file)
@@ -5,9 +5,9 @@
 #include "basictuner.h"
 
 /**
-*This tuner has the simulated annealing in its core
-*
-*/
+ * This tuner has the simulated annealing in its core
+ *
+ */
 class SATuner : public BasicTuner {
 public:
        SATuner(uint budget, uint timeout);
index a600580..9ab6d45 100644 (file)
@@ -86,7 +86,7 @@ SearchTuner::SearchTuner(const char *filename, bool addused) {
                        }
                        setting->setDecision(lowValue, highValue, defaultValue, selectedValue);
                        settings.add(setting);
-                       if(addused){
+                       if (addused) {
                                usedSettings.add(setting);
                        }
                }
@@ -96,20 +96,20 @@ SearchTuner::SearchTuner(const char *filename, bool addused) {
        }
 }
 
-bool SearchTuner::equalUsed(SearchTuner* tuner){
-       if(tuner->usedSettings.getSize() != usedSettings.getSize()){
+bool SearchTuner::equalUsed(SearchTuner *tuner) {
+       if (tuner->usedSettings.getSize() != usedSettings.getSize()) {
                return false;
        }
        bool result = true;
        SetIteratorTunableSetting *iterator = usedSettings.iterator();
-       while(iterator->hasNext()){
+       while (iterator->hasNext()) {
                TunableSetting *setting = iterator->next();
-               if(!tuner->usedSettings.contains(setting)){
+               if (!tuner->usedSettings.contains(setting)) {
                        result = false;
                        break;
-               }else{
+               } else {
                        TunableSetting *tunerSetting = tuner->usedSettings.get(setting);
-                       if(tunerSetting->selectedValue != setting->selectedValue){
+                       if (tunerSetting->selectedValue != setting->selectedValue) {
                                result = false;
                                break;
                        }
@@ -156,15 +156,15 @@ void SearchTuner::addUsed(const char *filename) {
        }
 }
 
-bool SearchTuner::isSubTunerof(SearchTuner *newTuner){
+bool SearchTuner::isSubTunerof(SearchTuner *newTuner) {
        SetIteratorTunableSetting *iterator = usedSettings.iterator();
        while (iterator->hasNext()) {
                TunableSetting *setting = iterator->next();
-               if(!newTuner->settings.contains(setting)){
+               if (!newTuner->settings.contains(setting)) {
                        return false;
-               } else{
+               } else {
                        TunableSetting *newSetting = newTuner->settings.get(setting);
-                       if(newSetting->selectedValue != setting->selectedValue){
+                       if (newSetting->selectedValue != setting->selectedValue) {
                                return false;
                        }
                }
index 935f527..9d5913b 100644 (file)
@@ -43,7 +43,7 @@ public:
        void setVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor, uint value);
        void setVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor, uint value);
        SearchTuner *copyUsed();
-        bool isSubTunerof(SearchTuner *newTuner);
+       bool isSubTunerof(SearchTuner *newTuner);
        void randomMutate();
        uint getSize() { return usedSettings.getSize();}
        void print();
@@ -51,7 +51,7 @@ public:
        void serialize(const char *file);
        void serializeUsed(const char *file);
        void addUsed(const char *file);
-        bool equalUsed(SearchTuner *tuner);
+       bool equalUsed(SearchTuner *tuner);
        CMEMALLOC;
 protected:
        /** Used Settings keeps track of settings that were actually used by
index e1b0dba..7c5d49a 100644 (file)
@@ -4,16 +4,16 @@
  * and open the template in the editor.
  */
 
-/* 
+/*
  * File:   TunableDependent.cc
  * Author: hamed
- * 
+ *
  * Created on October 5, 2018, 11:26 AM
  */
 
 #include "tunabledependent.h"
 
-TunableDependent::TunableDependent(Tunables dependent, Tunables parent):
+TunableDependent::TunableDependent(Tunables dependent, Tunables parent) :
        dependent(dependent),
        parent(parent)
 {
index 241b9eb..0874316 100644 (file)
@@ -4,7 +4,7 @@
  * and open the template in the editor.
  */
 
-/* 
+/*
  * File:   TunableDependent.h
  * Author: hamed
  *
 
 class TunableDependent {
 public:
-        TunableDependent(Tunables dependent, Tunables parent = (Tunables) -1);
-        TunableDependent(TunableDependent &setting);
-        virtual ~TunableDependent();
-        Tunables dependent;
-        Tunables parent;
+       TunableDependent(Tunables dependent, Tunables parent = (Tunables) - 1);
+       TunableDependent(TunableDependent &setting);
+       virtual ~TunableDependent();
+       Tunables dependent;
+       Tunables parent;
 };
 
-#endif /* TUNABLEDEPENDENT_H */
+#endif/* TUNABLEDEPENDENT_H */
 
index 05f66a3..d773522 100644 (file)
@@ -54,11 +54,11 @@ void *getBooleanVar(void *solver,unsigned int type) {
        return CCSOLVER(solver)->getBooleanVar((VarType) type).getRaw();
 }
 
-void *getBooleanTrue(void *solver){
+void *getBooleanTrue(void *solver) {
        return CCSOLVER(solver)->getBooleanTrue().getRaw();
 }
 
-void *getBooleanFalse(void *solver){
+void *getBooleanFalse(void *solver) {
        return CCSOLVER(solver)->getBooleanFalse().getRaw();
 }
 
@@ -160,7 +160,7 @@ void mustHaveValue(void *solver, void *element) {
        CCSOLVER(solver)->mustHaveValue( (Element *) element);
 }
 
-void setInterpreter(void *solver, unsigned int type){
+void setInterpreter(void *solver, unsigned int type) {
        CCSOLVER(solver)->setInterpreter((InterpreterType)type);
 }
 
index cd2ec55..1dfe9eb 100644 (file)
@@ -85,8 +85,8 @@ CSolver::~CSolver() {
        for (uint i = 0; i < size; i++) {
                delete allFunctions.get(i);
        }
-       
-       if(interpreter != NULL){
+
+       if (interpreter != NULL) {
                delete interpreter;
        }
 
@@ -319,7 +319,7 @@ Function *CSolver::completeTable(Table *table, UndefinedBehavior behavior) {
 BooleanEdge CSolver::getBooleanVar(VarType type) {
        Boolean *boolean = new BooleanVar(type);
        allBooleans.push(boolean);
-       if(!booleanVarUsed)
+       if (!booleanVarUsed)
                booleanVarUsed = true;
        return BooleanEdge(boolean);
 }
@@ -397,7 +397,7 @@ BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uin
 }
 
 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
-       if(!useInterpreter()){
+       if (!useInterpreter()) {
                BooleanEdge newarray[asize];
                switch (op) {
                case SATC_NOT: {
@@ -460,7 +460,7 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
                        return applyLogicalOperation(SATC_OR, applyLogicalOperation(SATC_NOT, array[0]), array[1]);
                }
                }
-       
+
                ASSERT(asize != 0);
                Boolean *boolean = new BooleanLogic(this, op, array, asize);
                Boolean *b = boolMap.get(boolean);
@@ -478,7 +478,7 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
                Boolean *boolean = new BooleanLogic(this, op, array, asize);
                allBooleans.push(boolean);
                return BooleanEdge(boolean);
-       
+
        }
 }
 
@@ -497,7 +497,7 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
                }
        }
        Boolean *constraint = new BooleanOrder(order, first, second);
-       if (!useInterpreter() )
+       if (!useInterpreter() ) {
                Boolean *b = boolMap.get(constraint);
 
                if (b == NULL) {
@@ -534,7 +534,7 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
 }
 
 void CSolver::addConstraint(BooleanEdge constraint) {
-       if(!useInterpreter()){
+       if (!useInterpreter()) {
                if (isTrue(constraint))
                        return;
                else if (isFalse(constraint)) {
@@ -572,7 +572,7 @@ void CSolver::addConstraint(BooleanEdge constraint) {
                        replaceBooleanWithTrueNoRemove(constraint);
                        constraint->parents.clear();
                }
-       } else{
+       } else {
                constraints.add(constraint);
                constraint->parents.clear();
        }
@@ -605,7 +605,7 @@ void CSolver::inferFixedOrders() {
 }
 
 int CSolver::solve() {
-       if(isUnSAT()){
+       if (isUnSAT()) {
                return IS_UNSAT;
        }
        long long startTime = getTimeNano();
@@ -615,12 +615,12 @@ int CSolver::solve() {
                deleteTuner = true;
        }
        int result = IS_INDETER;
-       if(useInterpreter()){
+       if (useInterpreter()) {
                interpreter->encode();
                model_print("Problem encoded in Interpreter\n");
                result = interpreter->solve();
                model_print("Problem solved by Interpreter\n");
-       } else{
+       } else {
 
                {
                        SetIteratorOrder *orderit = activeOrders.iterator();
@@ -656,21 +656,21 @@ int CSolver::solve() {
                eg.encode();
 
                naiveEncodingDecision(this);
-       //      eg.validate();
+               //      eg.validate();
 
                VarOrderingOpt bor(this, satEncoder);
                bor.doTransform();
 
                time2 = getTimeNano();
                model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
-               
+
                satEncoder->encodeAllSATEncoder(this);
                time1 = getTimeNano();
 
                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");
@@ -685,28 +685,28 @@ int CSolver::solve() {
        return result;
 }
 
-void CSolver::setInterpreter(InterpreterType type){
-       if(interpreter == NULL){
-               switch(type){
-                       case SATUNE:
-                               break;
-                       case ALLOY:{
-                               interpreter = new AlloyInterpreter(this);
-                               break;
-                       }case Z3:{
-                               interpreter = new SMTInterpreter(this);
-                               break;
-                       }
-                       case MATHSAT:{
-                               interpreter = new MathSATInterpreter(this);
-                               break;
-                       }
-                       case SMTRAT:{
-                               interpreter = new SMTRatInterpreter(this);
-                               break;
-                       }
-                       default:
-                               ASSERT(0);
+void CSolver::setInterpreter(InterpreterType type) {
+       if (interpreter == NULL) {
+               switch (type) {
+               case SATUNE:
+                       break;
+               case ALLOY: {
+                       interpreter = new AlloyInterpreter(this);
+                       break;
+               } case Z3: {
+                       interpreter = new SMTInterpreter(this);
+                       break;
+               }
+               case MATHSAT: {
+                       interpreter = new MathSATInterpreter(this);
+                       break;
+               }
+               case SMTRAT: {
+                       interpreter = new SMTRatInterpreter(this);
+                       break;
+               }
+               default:
+                       ASSERT(0);
                }
        }
 }
@@ -729,8 +729,8 @@ uint64_t CSolver::getElementValue(Element *element) {
        case ELEMSET:
        case ELEMCONST:
        case ELEMFUNCRETURN:
-               return useInterpreter()? interpreter->getValue(element):
-                       getElementValueSATTranslator(this, element);
+               return useInterpreter() ? interpreter->getValue(element) :
+                                        getElementValueSATTranslator(this, element);
        default:
                ASSERT(0);
        }
@@ -741,8 +741,8 @@ bool CSolver::getBooleanValue(BooleanEdge bedge) {
        Boolean *boolean = bedge.getBoolean();
        switch (boolean->type) {
        case BOOLEANVAR:
-               return useInterpreter()? interpreter->getBooleanValue(boolean):
-                       getBooleanVariableValueSATTranslator(this, boolean);
+               return useInterpreter() ? interpreter->getBooleanValue(boolean) :
+                                        getBooleanVariableValueSATTranslator(this, boolean);
        default:
                ASSERT(0);
        }
index 54012de..b99cf80 100644 (file)
@@ -126,7 +126,7 @@ public:
 
        /** When everything is done, the client calls this function and then csolver starts to encode*/
        int solve();
-       
+
        /** After getting the solution from the SAT solver, client can get the value of an element via this function*/
        uint64_t getElementValue(Element *element);
 
@@ -141,7 +141,7 @@ public:
        void setUnSAT() { model_print("Setting UNSAT %%%%%%\n"); unsat = true; }
        void setSatSolverTimeout(long seconds) { satsolverTimeout = seconds;}
        bool isUnSAT() { return unsat; }
-        bool isBooleanVarUsed(){return booleanVarUsed;}
+       bool isBooleanVarUsed() {return booleanVarUsed;}
        void printConstraint(BooleanEdge boolean);
        void printConstraints();
 
@@ -219,8 +219,8 @@ private:
 
        SATEncoder *satEncoder;
        bool unsat;
-        bool booleanVarUsed;
-        Tuner *tuner;
+       bool booleanVarUsed;
+       Tuner *tuner;
        long long elapsedTime;
        long satsolverTimeout;
        Interpreter *interpreter;
index bde12a6..db22513 100644 (file)
@@ -13,7 +13,7 @@ extern "C" {
  * Signature: ()J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createCCSolver
-  (JNIEnv *, jobject);
+       (JNIEnv *, jobject);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -21,7 +21,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createCCSolver
  * Signature: (J)V
  */
 JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_deleteCCSolver
-  (JNIEnv *, jobject, jlong);
+       (JNIEnv *, jobject, jlong);
 
 
 /*
@@ -30,7 +30,7 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_deleteCCSolver
  * Signature: (J)V
  */
 JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_resetCCSolver
-  (JNIEnv *, jobject, jlong);
+       (JNIEnv *, jobject, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -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, jlong, jint);
+       (JNIEnv *, jobject, jlong, jint, jlong, jint);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -46,7 +46,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createSet
  * Signature: (JIJJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createRangeSet
-  (JNIEnv *, jobject, jlong, jint, jlong, jlong);
+       (JNIEnv *, jobject, jlong, jint, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -54,7 +54,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createRangeSet
  * Signature: (JIJJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createRangeVar
-  (JNIEnv *, jobject, jlong, jint, jlong, jlong);
+       (JNIEnv *, jobject, jlong, jint, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -62,7 +62,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createRangeVar
  * Signature: (JI)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createMutableSet
-  (JNIEnv *, jobject, jlong, jint);
+       (JNIEnv *, jobject, jlong, jint);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -70,7 +70,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createMutableSet
  * Signature: (JJJ)V
  */
 JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_addItem
-  (JNIEnv *, jobject, jlong, jlong, jlong);
+       (JNIEnv *, jobject, jlong, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -78,7 +78,7 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_addItem
  * Signature: (JJ)V
  */
 JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_finalizeMutableSet
-  (JNIEnv *, jobject, jlong, jlong);
+       (JNIEnv *, jobject, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -86,7 +86,7 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_finalizeMutableSet
  * Signature: (JJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementVar
-  (JNIEnv *, jobject, jlong, jlong);
+       (JNIEnv *, jobject, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -94,7 +94,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementVar
  * Signature: (JIJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementConst
-  (JNIEnv *, jobject, jlong, jint, jlong);
+       (JNIEnv *, jobject, jlong, jint, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -102,7 +102,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementConst
  * Signature: (JJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementRange
-  (JNIEnv *, jobject, jlong, jlong);
+       (JNIEnv *, jobject, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -110,7 +110,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementRange
  * Signature: (JI)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanVar
-  (JNIEnv *, jobject, jlong, jint);
+       (JNIEnv *, jobject, jlong, jint);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -118,7 +118,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanVar
  * Signature: (J)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanTrue
-  (JNIEnv *, jobject, jlong);
+       (JNIEnv *, jobject, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -126,7 +126,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanTrue
  * Signature: (J)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanFalse
-  (JNIEnv *, jobject, jlong);
+       (JNIEnv *, jobject, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -134,7 +134,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanFalse
  * Signature: (JIJI)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createFunctionOperator
-  (JNIEnv *, jobject, jlong, jint, jlong, jint);
+       (JNIEnv *, jobject, jlong, jint, jlong, jint);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -142,7 +142,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createFunctionOperator
  * Signature: (JI)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createPredicateOperator
-  (JNIEnv *, jobject, jlong, jint);
+       (JNIEnv *, jobject, jlong, jint);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -150,7 +150,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createPredicateOperator
  * Signature: (JJI)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createPredicateTable
-  (JNIEnv *, jobject, jlong, jlong, jint);
+       (JNIEnv *, jobject, jlong, jlong, jint);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -158,7 +158,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createPredicateTable
  * Signature: (JJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createTable
-  (JNIEnv *, jobject, jlong, jlong);
+       (JNIEnv *, jobject, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -166,7 +166,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createTable
  * Signature: (J)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createTableForPredicate
-  (JNIEnv *, jobject, jlong);
+       (JNIEnv *, jobject, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -174,7 +174,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createTableForPredicate
  * Signature: (JJJIJ)V
  */
 JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_addTableEntry
-  (JNIEnv *, jobject, jlong, jlong, jlong, jint, jlong);
+       (JNIEnv *, jobject, jlong, jlong, jlong, jint, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -182,7 +182,7 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_addTableEntry
  * Signature: (JJI)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_completeTable
-  (JNIEnv *, jobject, jlong, jlong, jint);
+       (JNIEnv *, jobject, jlong, jlong, jint);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -190,7 +190,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_completeTable
  * Signature: (JJJIJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyFunction
-  (JNIEnv *, jobject, jlong, jlong, jlong, jint, jlong);
+       (JNIEnv *, jobject, jlong, jlong, jlong, jint, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -198,7 +198,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyFunction
  * Signature: (JJJIJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyPredicateTable
-  (JNIEnv *, jobject, jlong, jlong, jlong, jint, jlong);
+       (JNIEnv *, jobject, jlong, jlong, jlong, jint, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -206,7 +206,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyPredicateTable
  * Signature: (JJJI)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyPredicate
-  (JNIEnv *, jobject, jlong, jlong, jlong, jint);
+       (JNIEnv *, jobject, jlong, jlong, jlong, jint);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -214,7 +214,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyPredicate
  * Signature: (JIJI)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyLogicalOperation
-  (JNIEnv *, jobject, jlong, jint, jlong, jint);
+       (JNIEnv *, jobject, jlong, jint, jlong, jint);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -222,7 +222,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyLogicalOperation
  * Signature: (JIJJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyLogicalOperationTwo
-  (JNIEnv *, jobject, jlong, jint, jlong, jlong);
+       (JNIEnv *, jobject, jlong, jint, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -230,7 +230,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyLogicalOperationTwo
  * Signature: (JIJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyLogicalOperationOne
-  (JNIEnv *, jobject, jlong, jint, jlong);
+       (JNIEnv *, jobject, jlong, jint, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -238,7 +238,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyLogicalOperationOne
  * Signature: (JJ)V
  */
 JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_addConstraint
-  (JNIEnv *, jobject, jlong, jlong);
+       (JNIEnv *, jobject, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -246,7 +246,7 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_addConstraint
  * Signature: (JJ)V
  */
 JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_printConstraint
-  (JNIEnv *, jobject, jlong, jlong);
+       (JNIEnv *, jobject, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -254,7 +254,7 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_printConstraint
  * Signature: (JIJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createOrder
-  (JNIEnv *, jobject, jlong, jint, jlong);
+       (JNIEnv *, jobject, jlong, jint, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -262,7 +262,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createOrder
  * Signature: (JJJJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_orderConstraint
-  (JNIEnv *, jobject, jlong, jlong, jlong, jlong);
+       (JNIEnv *, jobject, jlong, jlong, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -270,7 +270,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_orderConstraint
  * Signature: (J)I
  */
 JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_solve
-  (JNIEnv *, jobject, jlong);
+       (JNIEnv *, jobject, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -278,7 +278,7 @@ JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_solve
  * Signature: (JJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementValue
-  (JNIEnv *, jobject, jlong, jlong);
+       (JNIEnv *, jobject, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -286,7 +286,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementValue
  * Signature: (JJ)I
  */
 JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_getBooleanValue
-  (JNIEnv *, jobject, jlong, jlong);
+       (JNIEnv *, jobject, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -294,7 +294,7 @@ JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_getBooleanValue
  * Signature: (JJJJ)I
  */
 JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_getOrderConstraintValue
-  (JNIEnv *, jobject, jlong, jlong, jlong, jlong);
+       (JNIEnv *, jobject, jlong, jlong, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -302,7 +302,7 @@ JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_getOrderConstraintValue
  * Signature: (J)V
  */
 JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_printConstraints
-  (JNIEnv *, jobject, jlong);
+       (JNIEnv *, jobject, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -310,7 +310,7 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_printConstraints
  * Signature: (J)V
  */
 JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_serialize
-  (JNIEnv *, jobject, jlong);
+       (JNIEnv *, jobject, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -318,7 +318,7 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_serialize
  * Signature: (JJ)V
  */
 JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_mustHaveValue
-  (JNIEnv *, jobject, jlong, jlong);
+       (JNIEnv *, jobject, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -326,7 +326,7 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_mustHaveValue
  * Signature: (JI)V
  */
 JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_setInterpreter
-  (JNIEnv *, jobject, jlong, jint);
+       (JNIEnv *, jobject, jlong, jint);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -334,7 +334,7 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_setInterpreter
  * Signature: (J)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_clone
-  (JNIEnv *, jobject, jlong);
+       (JNIEnv *, jobject, jlong);
 
 #ifdef __cplusplus
 }