From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Tue, 2 Oct 2018 19:12:24 +0000 (-0700)
Subject: Merge scratch with master branch
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=a79d8bc322e551f909de6757484480bcf6cbc55d

Merge scratch with master branch
---

a79d8bc322e551f909de6757484480bcf6cbc55d
diff --cc src/ASTAnalyses/Encoding/encodinggraph.cc
index 8ec4ac8,2ac69c1..957fea3
--- a/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/Backend/satelemencoder.cc
index 84880ff,ad0722b..d2c04f6
--- a/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/Encoders/naiveencoder.cc
index 17b9914,0de7043..3f9e44e
--- a/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/csolver.cc
index 2c15b62,e72b363..f1bd9b6
--- a/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);