From da55e8568d6c9a2d5bd0995bae4dc317e7f4db5f Mon Sep 17 00:00:00 2001
From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Thu, 27 Aug 2020 00:37:05 -0700
Subject: [PATCH] Edits

---
 src/Backend/satelemencoder.cc | 27 +++++++--------------------
 src/Backend/satencoder.h      |  5 ++---
 src/Tuner/tunable.h           |  2 +-
 3 files changed, 10 insertions(+), 24 deletions(-)

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index 9a698e0..d70bd9a 100644
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -266,15 +266,13 @@ void SATEncoder::generateOneHotAtMostOne(ElementEncoding *encoding) {
 	switch (enc)
 	{
 	case ONEHOT_BINOMIAL:
-		model_print("Encode using bionomial encoding\n");
-		model_print("size = %u\n", encoding->numVars);
 		generateOneHotBinomialAtMostOne(encoding->variables, encoding->numVars);
 		break;
 	case ONEHOT_COMMANDER:
-		generateOneHotCommanderEncodingVars(encoding);
+		generateOneHotCommanderAtMostOne(encoding->variables, encoding->numVars);
 		break;
 	case ONEHOT_SEQ_COUNTER:
-		generateOneHotSequentialAtMostOne(encoding);
+		generateOneHotSequentialAtMostOne(encoding->variables, encoding->numVars);
 		break;
 	default:
 		ASSERT(0);
@@ -290,7 +288,8 @@ void SATEncoder::generateOneHotBinomialAtMostOne(Edge *array, uint size, uint of
 	}
 }
 
-void SATEncoder::generateOneHotCommanderAtMostOneRecursive(Edge *array, uint size) {
+void SATEncoder::generateOneHotCommanderAtMostOne(Edge *array, uint size) {
+	//For more detail look at paper "Efficient CNF Encoding for Selecting 1 from N Objects"
 	ASSERT(size > 1);
 	if (size <= SEQ_COUNTER_GROUP_SIZE) {
 		//Using binomial encoding
@@ -329,18 +328,14 @@ void SATEncoder::generateOneHotCommanderAtMostOneRecursive(Edge *array, uint siz
 		}
 		ASSERT(commanderSize <= (size/SEQ_COUNTER_GROUP_SIZE + 1));
 		if(commanderSize > 1) {
-			generateOneHotCommanderAtMostOneRecursive(commanders, commanderSize);
+			generateOneHotCommanderAtMostOne(commanders, commanderSize);
 		}
 	}
 }
 
-void SATEncoder::generateOneHotSequentialAtMostOne(ElementEncoding *encoding) {
-	model_print("At-Most-One constraint using sequential counter\n");
-	model_print("size = %u\n", encoding->numVars);
+void SATEncoder::generateOneHotSequentialAtMostOne(Edge *array, uint size) {
 	// for more information, look at "Towards an Optimal CNF Encoding of Boolean Cardinality Constraints" paper
-	ASSERT(encoding->numVars > 1);
-	Edge *array = encoding->variables;
-	uint size = encoding->numVars;
+	ASSERT(size > 1);
 	Edge s [size -1 ];
 	getArrayNewVarsSATEncoder(size-1, s);
 	addConstraintCNF(cnf, constraintOR2(cnf, constraintNegate(array[0]), s[0]));
@@ -352,14 +347,6 @@ void SATEncoder::generateOneHotSequentialAtMostOne(ElementEncoding *encoding) {
 	}
 }
 
-void SATEncoder::generateOneHotCommanderEncodingVars(ElementEncoding *encoding) {
-	//For more detail look at paper "Efficient CNF Encoding for Selecting 1 from N Objects"
-	model_print("At-Most-One constraint using commander\n");
-	model_print("size = %u\n", encoding->numVars);
-	ASSERT(encoding->numVars > 1);
-	generateOneHotCommanderAtMostOneRecursive(encoding->variables, encoding->numVars);
-}
-
 void SATEncoder::generateOneHotEncodingVars(ElementEncoding *encoding) {
 	allocElementConstraintVariables(encoding, encoding->encArraySize);
 	getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 20683c5..5b8af05 100644
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -40,9 +40,8 @@ private:
 	Edge getElementValueConstraint(Element *element, Polarity p, uint64_t value);
 	void generateOneHotAtMostOne(ElementEncoding *encoding);
 	void generateOneHotBinomialAtMostOne(Edge *array, uint size, uint offset = 0);
-	void generateOneHotCommanderAtMostOneRecursive(Edge *array, uint size);
-	void generateOneHotSequentialAtMostOne(ElementEncoding *encoding);
-	void generateOneHotCommanderEncodingVars(ElementEncoding *encoding);
+	void generateOneHotCommanderAtMostOne(Edge *array, uint size);
+	void generateOneHotSequentialAtMostOne(Edge *array, uint size);
 	void generateOneHotEncodingVars(ElementEncoding *encoding);
 	void generateUnaryEncodingVars(ElementEncoding *encoding);
 	void generateBinaryIndexEncodingVars(ElementEncoding *encoding);
diff --git a/src/Tuner/tunable.h b/src/Tuner/tunable.h
index fc7ef8a..46a1412 100644
--- a/src/Tuner/tunable.h
+++ b/src/Tuner/tunable.h
@@ -44,7 +44,7 @@ static TunableDesc mustValueBinaryIndex(0, 6, 3);
 static TunableDesc NodeEncodingDesc(ELEM_UNASSIGNED, BINARYINDEX, ELEM_UNASSIGNED);
 static TunableDesc NaiveEncodingDesc(ONEHOT, BINARYINDEX, ONEHOT);
 static TunableDesc boolVarOrderingDesc(CONSTRAINTORDERING, REVERSEORDERING, REVERSEORDERING);
-static TunableDesc OneHotAtMostOneDesc(ONEHOT_BINOMIAL, ONEHOT_SEQ_COUNTER, ONEHOT_SEQ_COUNTER);
+static TunableDesc OneHotAtMostOneDesc(ONEHOT_BINOMIAL, ONEHOT_SEQ_COUNTER, ONEHOT_COMMANDER);
 
 enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING, MUSTEDGEPRUNE, ELEMENTOPT,
 							 ENCODINGGRAPHOPT, ELEMENTOPTSETS, PROXYVARIABLE, MUSTVALUE, NAIVEENCODER, VARIABLEORDER, ONEHOTATMOSTONE};
-- 
2.34.1