From 0b9f7bb16590ae7da2629986c236ad7c7e1a97fa Mon Sep 17 00:00:00 2001
From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Mon, 22 Oct 2018 10:16:52 -0700
Subject: [PATCH] Bug fix: Droping the log from the anyvalue heuristic...

---
 src/Backend/satelemencoder.cc | 16 ++++++++++------
 src/Backend/satencoder.h      |  1 +
 2 files changed, 11 insertions(+), 6 deletions(-)

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index 3cd2c1c..6f421ee 100644
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -226,9 +226,8 @@ void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
 	getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
 	if (encoding->element->anyValue) {
 		uint setSize = encoding->element->getRange()->getSize();
-		uint encArraySize = encoding->encArraySize;
-		double metric = encArraySize == setSize?setSize:setSize/(encArraySize-setSize);
-		if ( log(metric) <  pow(1.9, (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex) - 4)) {
+		int maxIndex = getMaximumUsedIndex(encoding);
+		if (maxIndex !=-1 && (maxIndex - setSize) != 0 && (setSize/(maxIndex-setSize)) <  pow(1.9, (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex) - 4)) {
 			generateAnyValueBinaryIndexEncodingPositive(encoding);
 		} else {
 			generateAnyValueBinaryIndexEncoding(encoding);
@@ -280,9 +279,7 @@ void SATEncoder::generateElementEncoding(Element *element) {
 	}
 }
 
-void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding) {
-	if (encoding->numVars == 0)
-		return;
+int SATEncoder::getMaximumUsedIndex(ElementEncoding *encoding){
 	int index = -1;
 	for (uint i = encoding->encArraySize - 1; i >= 0; i--) {
 		if (encoding->isinUseElement(i)) {
@@ -292,6 +289,13 @@ void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding)
 			break;
 		}
 	}
+	return index;
+}
+
+void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding) {
+	if (encoding->numVars == 0)
+		return;
+	int index = getMaximumUsedIndex(encoding);
 	if ( index != -1 ) {
 		addConstraintCNF(cnf, generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, index));
 	}
diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 0bb29f5..a89ab1b 100644
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -63,6 +63,7 @@ private:
 	void encodeEnumTableElemFunctionSATEncoder(ElementFunction *This);
 	void encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *This);
 	void generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding);
+	int getMaximumUsedIndex(ElementEncoding *encoding);
 	void generateAnyValueBinaryIndexEncodingPositive(ElementEncoding *encoding);
 	void generateAnyValueBinaryValueEncoding(ElementEncoding *encoding);
 	CNF *cnf;
-- 
2.34.1