Remove unimplemented enum

[satune.git] / src / Translator / sattranslator.cc

diff --git a/src/Translator/sattranslator.cc b/src/Translator/sattranslator.cc
index 7c48be6324430b094e51477ac696b8f0075e9ebd..792d58b38bc62f7370b253b68e65007bb7cd2e64 100644 (file)
--- a/src/Translator/sattranslator.cc
+++ b/src/Translator/sattranslator.cc
@@ -59,7 +59,7 @@ uint64_t getElementValueUnarySATTranslator(CSolver *This, ElementEncoding *elemE
 uint64_t getElementValueSATTranslator(CSolver *This, Element *element) {
        ElementEncoding *elemEnc = getElementEncoding(element);
        if (elemEnc->numVars == 0)//case when the set has only one item
-               return getElementSet(element)->getElement(0);
+               return element->getRange()->getElement(0);
        switch (elemEnc->type) {
        case ONEHOT:
                return getElementValueOneHotSATTranslator(This, elemEnc);
@@ -67,8 +67,6 @@ uint64_t getElementValueSATTranslator(CSolver *This, Element *element) {
                return getElementValueUnarySATTranslator(This, elemEnc);
        case BINARYINDEX:
                return getElementValueBinaryIndexSATTranslator(This, elemEnc);
-       case ONEHOTBINARY:
-               ASSERT(0);
                break;
        case BINARYVAL:
                ASSERT(0);
@@ -81,8 +79,14 @@ uint64_t getElementValueSATTranslator(CSolver *This, Element *element) {
 }
 
 bool getBooleanVariableValueSATTranslator( CSolver *This, Boolean *boolean) {
-       int index = getEdgeVar( ((BooleanVar *) boolean)->var );
-       return getValueSolver(This->getSATEncoder()->getCNF()->solver, index);
+       if (boolean->boolVal == BV_MUSTBETRUE)
+               return true;
+       else if (boolean->boolVal == BV_MUSTBEFALSE)
+               return false;
+       else {
+               int index = getEdgeVar( ((BooleanVar *) boolean)->var );
+               return getValueSolver(This->getSATEncoder()->getCNF()->solver, index);
+       }
 }