From: Hamed <hamed.gorjiara@gmail.com>
Date: Tue, 25 Jul 2017 02:00:02 +0000 (-0700)
Subject: Fixing bugs for Unary encoding ...
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=51f276cbbc3b8abbdce44ca9e0ed8925e6daffa6;p=satune.git

Fixing bugs for Unary encoding ...
---

diff --git a/src/Backend/satelemencoder.c b/src/Backend/satelemencoder.c
index ab597a6..ca71c6e 100644
--- a/src/Backend/satelemencoder.c
+++ b/src/Backend/satelemencoder.c
@@ -52,10 +52,12 @@ Edge getElementValueOneHotConstraint(SATEncoder * This, Element* elem, uint64_t
 
 Edge getElementValueUnaryConstraint(SATEncoder * This, Element* elem, uint64_t value) {
 	ASTNodeType type = GETELEMENTTYPE(elem);
-	ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
+	ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
 	ElementEncoding* elemEnc = getElementEncoding(elem);
 	for(uint i=0; i<elemEnc->encArraySize; i++){
 		if (isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value) {
+			if(elemEnc->numVars == 0)
+				return E_True;
 			if (i==0)
 				return constraintNegate(elemEnc->variables[0]);
 			else if ((i+1)==elemEnc->encArraySize)
@@ -64,7 +66,7 @@ Edge getElementValueUnaryConstraint(SATEncoder * This, Element* elem, uint64_t v
 				return constraintAND2(This->cnf, elemEnc->variables[i-1], constraintNegate(elemEnc->variables[i]));
 		}
 	}
-	return E_BOGUS;
+	return E_False;
 }
 
 Edge getElementValueBinaryValueConstraint(SATEncoder * This, Element* element, uint64_t value){
@@ -101,8 +103,8 @@ void generateBinaryIndexEncodingVars(SATEncoder *This, ElementEncoding *encoding
 	getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
 }
 
-void generateOneHotEncodingVars(SATEncoder *This, ElementEncoding *encoding) { 
-	allocElementConstraintVariables(encoding, getSetSize( getElementSet(encoding->element)));
+void generateOneHotEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
+	allocElementConstraintVariables(encoding, encoding->encArraySize);
 	getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);	
 	for(uint i=0;i<encoding->numVars;i++) {
 		for(uint j=i+1;j<encoding->numVars;j++) {
diff --git a/src/Encoders/naiveencoder.c b/src/Encoders/naiveencoder.c
index d5b88d7..6fe0ac8 100644
--- a/src/Encoders/naiveencoder.c
+++ b/src/Encoders/naiveencoder.c
@@ -61,7 +61,7 @@ void naiveEncodingPredicate(BooleanPredicate * This) {
 void naiveEncodingElement(Element * This) {
 	ElementEncoding * encoding = getElementEncoding(This);
 	if (getElementEncodingType(encoding) == ELEM_UNASSIGNED) {
-		setElementEncodingType(encoding, ONEHOT);
+		setElementEncodingType(encoding, UNARY);
 		encodingArrayInitialization(encoding);
 	}
 	
@@ -77,12 +77,25 @@ void naiveEncodingElement(Element * This) {
 	}
 }
 
+uint getSizeEncodingArray(ElementEncoding *This, uint setSize){
+	switch(This->type){
+		case BINARYINDEX:
+			return NEXTPOW2(setSize);
+		case ONEHOT:
+		case UNARY:
+			return setSize;
+		default:
+			ASSERT(0);
+	}
+	return -1;
+}
+
 void encodingArrayInitialization(ElementEncoding *This) {
 	Element * element=This->element;
 	Set * set= getElementSet(element);
 	ASSERT(set->isRange==false);
 	uint size=getSizeVectorInt(set->members);
-	uint encSize=NEXTPOW2(size);
+	uint encSize=getSizeEncodingArray(This, size);
 	allocEncodingArrayElement(This, encSize);
 	allocInUseArrayElement(This, encSize);
 	for(uint i=0;i<size;i++) {
diff --git a/src/Encoders/naiveencoder.h b/src/Encoders/naiveencoder.h
index 20f2943..a4b9ec1 100644
--- a/src/Encoders/naiveencoder.h
+++ b/src/Encoders/naiveencoder.h
@@ -15,5 +15,6 @@ void naiveEncodingLogicOp(BooleanLogic * This);
 void naiveEncodingPredicate(BooleanPredicate * This);
 void naiveEncodingElement(Element * This);
 void encodingArrayInitialization(ElementEncoding *This);
+uint getSizeEncodingArray(ElementEncoding *, uint setSize);
 
 #endif