Remove unimplemented enum

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

diff --git a/src/Translator/sattranslator.cc b/src/Translator/sattranslator.cc
index 766c5c7cf6928f78e481a49d27d98ce85c09a06b..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,16 +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);
+       }
 }
 
-HappenedBefore getOrderConstraintValueSATTranslator(CSolver *This, Order *order, uint64_t first, uint64_t second) {
-       ASSERT(order->orderPairTable != NULL);
-       OrderPair pair(first, second, E_NULL);
-       Edge var = getOrderConstraint(order->orderPairTable, &pair);
-       if (edgeIsNull(var))
-               return SATC_UNORDERED;
-       return getValueCNF(This->getSATEncoder()->getCNF(), var) ? SATC_FIRST : SATC_SECOND;
-}