From 3fe1ee3bd7a1e31ec099c9c2d5c597c4bc0f9e49 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Tue, 23 Oct 2018 16:08:21 -0700
Subject: [PATCH] bug fix

---
 src/ASTAnalyses/Encoding/encodinggraph.cc |  2 +-
 src/Backend/satelemencoder.cc             | 30 +++++++++--------------
 src/Backend/satencoder.h                  |  2 +-
 3 files changed, 14 insertions(+), 20 deletions(-)

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index b7d4c8d..66d8606 100644
--- a/src/ASTAnalyses/Encoding/encodinggraph.cc
+++ b/src/ASTAnalyses/Encoding/encodinggraph.cc
@@ -113,7 +113,7 @@ void EncodingGraph::validate() {
 
 
 void EncodingGraph::encode() {
-	if (solver->getTuner()->getTunable(ENCODINGGRAPHOPT, &onoff) == 0)
+	if (solver->getTuner()->getTunable(ENCODINGGRAPHOPT, &offon) == 0)
 		return;
 	buildGraph();
 	SetIteratorEncodingSubGraph *itesg = subgraphs.iterator();
diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index 61db2fd..3aa0927 100644
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -226,12 +226,11 @@ void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
 	getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
 	if (encoding->element->anyValue) {
 		uint setSize = encoding->element->getRange()->getSize();
-		int maxIndex = getMaximumUsedIndex(encoding);
-		maxIndex = maxIndex == -1? (int)encoding->encArraySize : maxIndex;
-		if(setSize == encoding->encArraySize && maxIndex == (int)setSize){
+		int maxIndex = getMaximumUsedSize(encoding);
+		if (setSize == encoding->encArraySize && maxIndex == (int)setSize) {
 			return;
 		}
-		double ratio = (setSize*(1+2*encoding->numVars))/ (encoding->numVars*(encoding->numVars + maxIndex*1.0 - setSize));
+		double ratio = (setSize * (1 + 2 * encoding->numVars)) / (encoding->numVars * (encoding->numVars + maxIndex * 1.0 - setSize));
 //		model_print("encArraySize=%u\tmaxIndex=%d\tsetSize=%u\tmetric=%f\tnumBits=%u\n", encoding->encArraySize, maxIndex, setSize, ratio, encoding->numVars);
 		if ( ratio <  pow(2, (uint)solver->getTuner()->getTunable(MUSTVALUE, &mustValueBinaryIndex) - 3)) {
 			generateAnyValueBinaryIndexEncodingPositive(encoding);
@@ -285,28 +284,23 @@ void SATEncoder::generateElementEncoding(Element *element) {
 	}
 }
 
-int SATEncoder::getMaximumUsedIndex(ElementEncoding *encoding) {
-	int index = -1;
-	for (uint i = encoding->encArraySize - 1; i >= 0; i--) {
-		if (encoding->isinUseElement(i)) {
-			if (i + 1 < encoding->encArraySize) {
-				index = i + 1;
-			}
-			break;
-		}
+int SATEncoder::getMaximumUsedSize(ElementEncoding *encoding) {
+	for (int i = encoding->encArraySize - 1; i >= 0; i--) {
+		if (encoding->isinUseElement(i))
+			return i + 1;
 	}
-	return index;
+	ASSERT(false);
+	return -1;
 }
 
 void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding) {
 	if (encoding->numVars == 0)
 		return;
-	int index = getMaximumUsedIndex(encoding);
-	if ( index != -1 ) {
+	int index = getMaximumUsedSize(encoding);
+	if ( index != encoding->encArraySize ) {
 		addConstraintCNF(cnf, generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, index));
 	}
-	index = index == -1 ? encoding->encArraySize - 1 : index - 1;
-	for (int i = index; i >= 0; i--) {
+	for (int i = index - 1; i >= 0; i--) {
 		if (!encoding->isinUseElement(i)) {
 			addConstraintCNF(cnf, constraintNegate( generateBinaryConstraint(cnf, encoding->numVars, encoding->variables, i)));
 		}
diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index a89ab1b..63b5a61 100644
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -63,7 +63,7 @@ private:
 	void encodeEnumTableElemFunctionSATEncoder(ElementFunction *This);
 	void encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *This);
 	void generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding);
-	int getMaximumUsedIndex(ElementEncoding *encoding);
+	int getMaximumUsedSize(ElementEncoding *encoding);
 	void generateAnyValueBinaryIndexEncodingPositive(ElementEncoding *encoding);
 	void generateAnyValueBinaryValueEncoding(ElementEncoding *encoding);
 	CNF *cnf;
-- 
2.34.1