Merge scratch with master branch

diff --cc src/ASTAnalyses/Encoding/encodinggraph.cc
index 8ec4ac84eafe0b1d3cea3139964f94358768e0b4,2ac69c1de22ddbedb684e04eb44cc51cc76e61f4..957fea33ba4818cd67e98a88e66f839c8293a98e
--- 1/src/ASTAnalyses/Encoding/encodinggraph.cc
--- 2/src/ASTAnalyses/Encoding/encodinggraph.cc
+++ b/src/ASTAnalyses/Encoding/encodinggraph.cc
@@@ -342,30 -348,43 +342,27 @@@ void EncodingGraph::decideEdges() 
                        newSize = convertSize(left->s->getUnionSize(right->s));
                        newSize = (leftSize > newSize) ? leftSize : newSize;
                        newSize = (rightSize > newSize) ? rightSize : newSize;
-                       max = rightSize > leftSize? rightSize : leftSize;
- //                    model_print("Merge=%s\tsimilarity=%f\n", max==newSize?"TRUE":"FALSE", left->measureSimilarity(right));
-                       merge = left->measureSimilarity(right) > 1.5 || max == newSize;
 -                      totalCost = (newSize - leftSize) * left->elements.getSize() +
 -                                                                      (newSize - rightSize) * right->elements.getSize();
 -                      //model_print("leftSize=%u\trighSize=%u\tnewSize=%u\n", leftSize, rightSize, newSize);
 -                      max = rightSize > leftSize ? rightSize : leftSize;
 -                      if (newSize == max) {
 -                              merge = true;
 -                      }
                } else if (leftGraph != NULL && rightGraph == NULL) {
                        leftSize = convertSize(leftGraph->encodingSize);
                        rightSize = convertSize(right->getSize());
                        newSize = convertSize(leftGraph->estimateNewSize(right));
                        newSize = (leftSize > newSize) ? leftSize : newSize;
                        newSize = (rightSize > newSize) ? rightSize : newSize;
 -                      totalCost = (newSize - leftSize) * leftGraph->numElements +
 -                                                                      (newSize - rightSize) * right->elements.getSize();
 -                      //model_print("leftSize=%u\trighSize=%u\tnewSize=%u\n", leftSize, rightSize, newSize);
 -                      max = rightSize > leftSize ? rightSize : leftSize;
 -                      if (newSize == max) {
 -                              merge = true;
 -                      }
 +                      max = rightSize > leftSize? rightSize : leftSize;
- //                    model_print("Merge=%s\tsimilarity=%f\n", max==newSize?"TRUE":"FALSE", leftGraph->measureSimilarity(right));
-                       merge = leftGraph->measureSimilarity(right) > 1.5 || max == newSize;
++//                    model_print("Merge=%s\tsimilarity=%f\n", max==newSize?"TRUE":"FALSE", left->measureSimilarity(right));
++                      merge = left->measureSimilarity(right) > 1.5 || max == newSize;
                } else {
                        //Neither are null
                        leftSize = convertSize(leftGraph->encodingSize);
                        rightSize = convertSize(rightGraph->encodingSize);
                        newSize = convertSize(leftGraph->estimateNewSize(rightGraph));
 +//                    model_print("MergingSubGraphs: left=%u\tright=%u\tnewSize=%u\n", leftSize, rightSize, newSize);
                        newSize = (leftSize > newSize) ? leftSize : newSize;
                        newSize = (rightSize > newSize) ? rightSize : newSize;
- //                    model_print("Merge=%s\tsimilarity=%f\n", max==newSize?"TRUE":"FALSE", leftGraph->measureSimilarity(rightGraph));
 -                      totalCost = (newSize - leftSize) * leftGraph->numElements +
 -                                                                      (newSize - rightSize) * rightGraph->numElements;
 -//                    model_print("LeftGraph size=%u\n", leftGraph->encodingSize);
 -//                    model_print("RightGraph size=%u\n", rightGraph->encodingSize);
 -//                    model_print("UnionGraph size = %u\n", leftGraph->estimateNewSize(rightGraph));
 -                      if (rightSize < 64 && leftSize < 64) {
 -                              merge = true;
 -                      }
 +                      max = rightSize > leftSize? rightSize : leftSize;
++//                    model_print("Merge=%s\tsimilarity=%f\n", max==newSize?"TRUE":"FALSE", leftGraph->measureSimilarity(right));
 +                      merge = leftGraph->measureSimilarity(right) > 1.5 || max == newSize;
                }
 -//            model_print("******************************\n");
                if (merge) {
                        //add the edge
                        mergeNodes(left, right);

diff --cc src/ASTAnalyses/Encoding/encodinggraph.h
Simple merge

diff --cc src/Backend/constraint.cc
Simple merge

diff --cc src/Backend/satelemencoder.cc
index 84880fff21574f387accacf7afcf2138defcb1f1,ad0722b2d262bf4a89a792fa220c2d1b8a554013..d2c04f62ac2a1aeeb7c9cddb4207c7fa07d61459
--- 1/src/Backend/satelemencoder.cc
--- 2/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@@ -223,16 -222,8 +223,16 @@@ void SATEncoder::generateBinaryIndexEnc
        ASSERT(encoding->type == BINARYINDEX);
        allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize - 1));
        getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
 -      if (encoding->element->anyValue)
 -              generateAnyValueBinaryIndexEncoding(encoding);
 +      if (encoding->element->anyValue){
 +              uint setSize = encoding->element->getRange()->getSize();
 +              uint encArraySize = encoding->encArraySize;
 +              model_print("setSize=%u\tencArraySize=%u\n", setSize, encArraySize);
 +              if(setSize < encArraySize * (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex)/10){
 +                      generateAnyValueBinaryIndexEncodingPositive(encoding);
 +              } else {
-               generateAnyValueBinaryIndexEncoding(encoding);
++                      generateAnyValueBinaryIndexEncoding(encoding);
 +              }
 +      }
  }
  
  void SATEncoder::generateOneHotEncodingVars(ElementEncoding *encoding) {

diff --cc src/Backend/satencoder.h
Simple merge

diff --cc src/Encoders/naiveencoder.cc
index 17b9914c80bfe9ccbfe1e004d9089689300dd331,0de7043b2d51472cc58089b1e5fa9bbe44015bfe..3f9e44eeaad1df92acc6654a93d5089b43e36ff2
--- 1/src/Encoders/naiveencoder.cc
--- 2/src/Encoders/naiveencoder.cc
+++ b/src/Encoders/naiveencoder.cc
@@@ -63,13 -62,13 +63,13 @@@ void naiveEncodingPredicate(CSolver *cs
        }
  }
  
 -void naiveEncodingElement(Element *This) {
 +void naiveEncodingElement(CSolver *csolver, Element *This) {
        ElementEncoding *encoding = This->getElementEncoding();
        if (encoding->getElementEncodingType() == ELEM_UNASSIGNED) {
-               if(This->type != ELEMCONST){
+               if (This->type != ELEMCONST) {
                        model_print("INFO: naive encoder is making the decision about element %p....\n", This);
                }
 -              encoding->setElementEncodingType(UNARY);
 +              encoding->setElementEncodingType((ElementEncodingType)csolver->getTuner()->getVarTunable(This->getRange()->getType(), NAIVEENCODER, &NaiveEncodingDesc));
                encoding->encodingArrayInitialization();
        }
  

diff --cc src/Tuner/searchtuner.cc
Simple merge

diff --cc src/csolver.cc
index 2c15b62fd87e6322fb92d60f0fad6ca7d5e19047,e72b3631de5385a23442b6f663d4f1731725198e..f1bd9b64870f4dd45ed570a2d2608d2772825f8c
--- 1/src/csolver.cc
--- 2/src/csolver.cc
+++ b/src/csolver.cc
@@@ -628,11 -628,11 +628,11 @@@ int CSolver::solve() 
        satEncoder->encodeAllSATEncoder(this);
        time1 = getTimeNano();
  
-       model_print("Elapse Encode time: %f\n", (time1- startTime) / NANOSEC);
-       
+       model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
+ 
        model_print("Is problem UNSAT after encoding: %d\n", unsat);
 -      int result = unsat ? IS_UNSAT : satEncoder->solve();
 -      model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT ? "SAT" : " UNSAT");
 +      int 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");
        time2 = getTimeNano();
        elapsedTime = time2 - startTime;
        model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);