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 5a47435dcda90adf0205bd02b62eac8f8a77c13b..80e14898d843e179827367c615eed4f33ddc3cf3 100644 (file)
--- 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 bbf0924e2a59389f4c182ddaa2198d8e082965a6..01cb65a2845a4b29cbf84c015d0923847e08b133 100644 (file)
--- 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: