From: Hamed <hamed.gorjiara@gmail.com>
Date: Wed, 12 Jul 2017 20:14:23 +0000 (-0700)
Subject: Binary value encoding ...
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=46fde40340f7bf53c4ebc433c5bd853a2e6c31f5;p=satune.git

Binary value encoding ...
---

diff --git a/src/Backend/satelemencoder.c b/src/Backend/satelemencoder.c
index 9f3b6ab..facb374 100644
--- a/src/Backend/satelemencoder.c
+++ b/src/Backend/satelemencoder.c
@@ -16,7 +16,7 @@ Edge getElementValueConstraint(SATEncoder* This, Element* elem, uint64_t value)
 			ASSERT(0);
 			break;
 		case BINARYVAL:
-			ASSERT(0);
+			return getElementValueBinaryValueConstraint(This, elem, value);
 			break;
 		default:
 			ASSERT(0);
@@ -64,11 +64,31 @@ Edge getElementValueUnaryConstraint(SATEncoder * This, Element* elem, uint64_t v
 	return E_BOGUS;
 }
 
+Edge getElementValueBinaryValueConstraint(SATEncoder * This, Element* element, uint64_t value){
+	ASTNodeType type = GETELEMENTTYPE(element);
+	ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
+	ElementEncoding* elemEnc = getElementEncoding(element);
+	for(uint i=0; i<elemEnc->encArraySize; i++){
+		if(isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value) {
+			return generateBinaryConstraint(This->cnf, elemEnc->numVars, elemEnc->variables, value);
+			// This constraint can be generated right away without iterating over encodingArray
+			// but we need to make sure that element with that value is in use ...
+		}
+	}
+	return E_BOGUS;
+}
+
 void allocElementConstraintVariables(ElementEncoding* This, uint numVars) {
 	This->numVars = numVars;
 	This->variables = ourmalloc(sizeof(Edge) * numVars);
 }
 
+void generateBinaryValueEncodingVars(SATEncoder* This, ElementEncoding* encoding){
+	ASSERT(encoding->type==BINARYVAL);
+	allocElementConstraintVariables(encoding, getMaximumBitsBinaryValueEncodingVars(encoding));
+	getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
+}
+
 void generateBinaryIndexEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
 	ASSERT(encoding->type==BINARYINDEX);
 	allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize-1));
@@ -110,6 +130,11 @@ void generateElementEncoding(SATEncoder* This, Element * element) {
 	case UNARY:
 		generateUnaryEncodingVars(This, encoding);
 		return;
+	case ONEHOTBINARY:
+		return;
+	case BINARYVAL:
+		generateBinaryValueEncodingVars(This, encoding);
+		return;
 	default:
 		ASSERT(0);
 	}
diff --git a/src/Backend/satelemencoder.h b/src/Backend/satelemencoder.h
index ec65cf1..7ba81cd 100644
--- a/src/Backend/satelemencoder.h
+++ b/src/Backend/satelemencoder.h
@@ -4,10 +4,12 @@
 Edge getElementValueOneHotConstraint(SATEncoder * This, Element* elem, uint64_t value);
 Edge getElementValueUnaryConstraint(SATEncoder * This, Element* elem, uint64_t value);
 Edge getElementValueBinaryIndexConstraint(SATEncoder * This, Element* element, uint64_t value);
+Edge getElementValueBinaryValueConstraint(SATEncoder * This, Element* element, uint64_t value);
 Edge getElementValueConstraint(SATEncoder* encoder, Element* This, uint64_t value);
 void allocElementConstraintVariables(ElementEncoding* This, uint numVars);
 void generateOneHotEncodingVars(SATEncoder *This, ElementEncoding *encoding);
 void generateUnaryEncodingVars(SATEncoder *This, ElementEncoding *encoding);
 void generateBinaryIndexEncodingVars(SATEncoder* This, ElementEncoding* encoding);
+void generateBinaryValueEncodingVars(SATEncoder* This, ElementEncoding* encoding);
 void generateElementEncoding(SATEncoder* This, Element* element);
 #endif
diff --git a/src/Encoders/elementencoding.c b/src/Encoders/elementencoding.c
index 2d0b600..8d01cc7 100644
--- a/src/Encoders/elementencoding.c
+++ b/src/Encoders/elementencoding.c
@@ -37,3 +37,12 @@ void setElementEncodingType(ElementEncoding* This, ElementEncodingType type){
 	This->type = type;
 }
 
+uint getMaximumBitsBinaryValueEncodingVars(ElementEncoding *encoding) {
+	uint64_t max = 0;
+	for(uint i=0; i< encoding->encArraySize; i++){
+		if(encoding->encodingArray[i]>max)
+			max = encoding->encodingArray[i];
+	}
+	return NUMBITS(max-1);
+}
+
diff --git a/src/Encoders/elementencoding.h b/src/Encoders/elementencoding.h
index d52549d..49a890f 100644
--- a/src/Encoders/elementencoding.h
+++ b/src/Encoders/elementencoding.h
@@ -36,4 +36,6 @@ static inline void setInUseElement(ElementEncoding *This, uint offset) {
 	This->inUseArray[(offset>>6)] |= 1 << (offset & 63);
 }
 
+uint getMaximumBitsBinaryValueEncodingVars(ElementEncoding *encoding);
+
 #endif