X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FTranslator%2Fsattranslator.cc;h=d49883e447642641fdd2f0f4073015763ebc7887;hb=37c1d6b2727508d8af302bdf85ef1f47a5e5d6da;hp=7c48be6324430b094e51477ac696b8f0075e9ebd;hpb=9979be547581fdc1b75fdc09d006fa3497a7827c;p=satune.git

diff --git a/src/Translator/sattranslator.cc b/src/Translator/sattranslator.cc
index 7c48be6..d49883e 100644
--- a/src/Translator/sattranslator.cc
+++ b/src/Translator/sattranslator.cc
@@ -57,9 +57,9 @@ uint64_t getElementValueUnarySATTranslator(CSolver *This, ElementEncoding *elemE
 }
 
 uint64_t getElementValueSATTranslator(CSolver *This, Element *element) {
-	ElementEncoding *elemEnc = getElementEncoding(element);
+	ElementEncoding *elemEnc = element->getElementEncoding();
 	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);
+	}
 }