From: Hamed <hamed.gorjiara@gmail.com>
Date: Wed, 12 Jul 2017 02:24:10 +0000 (-0700)
Subject: One-hot encoding sat solution translator
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=93ff173fb80070dd48c884449095d0a7bc65160f;p=satune.git

One-hot encoding sat solution translator
---

diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c
index a768a4f..f6827f5 100644
--- a/src/Backend/sattranslator.c
+++ b/src/Backend/sattranslator.c
@@ -13,6 +13,15 @@ uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding*
 	ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, index));
 	return elemEnc->encodingArray[index];
 }
+uint64_t getElementValueOneHotSATTranslator(CSolver* This, ElementEncoding* elemEnc){
+	uint index=0;
+	for(int i=elemEnc->numVars-1;i>=0;i--) {
+		if (This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ])
+			index = i;
+	}
+	ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, index));
+	return elemEnc->encodingArray[index];
+}
 uint64_t getElementValueSATTranslator(CSolver* This, Element* element){
 	switch(getElementEncoding(element)->type){
 		case ONEHOT:
diff --git a/src/Backend/sattranslator.h b/src/Backend/sattranslator.h
index 5378cdd..ea0085c 100644
--- a/src/Backend/sattranslator.h
+++ b/src/Backend/sattranslator.h
@@ -11,6 +11,7 @@
 #include "classlist.h"
 
 bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean);
+uint64_t getElementValueOneHotSATTranslator(CSolver* This, ElementEncoding* elemEnc);
 uint64_t getElementValueSATTranslator(CSolver* This, Element* element);
 
 #endif /* SATTRANSLATOR_H */