From: Hamed <hamed.gorjiara@gmail.com>
Date: Mon, 17 Jul 2017 23:04:18 +0000 (-0700)
Subject: Translating back the set with one item (iff and ite are also tested)
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=1e8c0203c0c0eb772dda4a7c927ba8834b121345;p=satune.git

Translating back the set with one item (iff and ite are also tested)
---

diff --git a/src/Backend/satelemencoder.c b/src/Backend/satelemencoder.c
index 5a47435..80e1489 100644
--- a/src/Backend/satelemencoder.c
+++ b/src/Backend/satelemencoder.c
@@ -4,7 +4,7 @@
 #include "ops.h"
 #include "element.h"
 
-Edge getElementValueConstraint(SATEncoder* This, Element* elem, uint64_t value) {
+Edge getElementValueConstraint(SATEncoder* This, Element* elem, uint64_t value) { 
 	switch(getElementEncoding(elem)->type){
 		case ONEHOT:
 			return getElementValueOneHotConstraint(This, elem, value);
diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c
index bbf0924..01cb65a 100644
--- a/src/Backend/sattranslator.c
+++ b/src/Backend/sattranslator.c
@@ -2,6 +2,7 @@
 #include "element.h"
 #include "csolver.h"
 #include "satencoder.h"
+#include "set.h"
 
 uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding* elemEnc){
 	uint index=0;
@@ -47,6 +48,9 @@ uint64_t getElementValueUnarySATTranslator(CSolver* This, ElementEncoding* elemE
 }
 
 uint64_t getElementValueSATTranslator(CSolver* This, Element* element){
+	Set* set = getElementSet(element);
+	if(getSetSize( set ) ==1)	//case when the set has only one item
+		return getSetElement(set, 0);
 	ElementEncoding* elemEnc = getElementEncoding(element);
 	switch(elemEnc->type){
 		case ONEHOT: