From: bdemsky <bdemsky@uci.edu>
Date: Tue, 18 Jul 2017 00:38:58 +0000 (-0700)
Subject: Include encoding for values
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=60fea51356847772c9f012a1a6b37e57e461dff8;p=satune.git

Include encoding for values
---

diff --git a/src/Backend/satelemencoder.c b/src/Backend/satelemencoder.c
index 80e1489..87d19b4 100644
--- a/src/Backend/satelemencoder.c
+++ b/src/Backend/satelemencoder.c
@@ -70,14 +70,17 @@ Edge getElementValueBinaryValueConstraint(SATEncoder * This, Element* element, u
 	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 ...
-		}
+	if (elemEnc->low <= elemEnc->high) {
+		if (value < elemEnc->low || value > elemEnc->high)
+			return E_False;
+	} else {
+		//Range wraps around 0
+		if (value < elemEnc->low && value > elemEnc->high)
+			return E_False;
 	}
-	return E_BOGUS;
+	
+	uint64_t valueminusoffset=value-elemEnc->offset;
+	return generateBinaryConstraint(This->cnf, elemEnc->numVars, elemEnc->variables, valueminusoffset);
 }
 
 void allocElementConstraintVariables(ElementEncoding* This, uint numVars) {
@@ -87,7 +90,7 @@ void allocElementConstraintVariables(ElementEncoding* This, uint numVars) {
 
 void generateBinaryValueEncodingVars(SATEncoder* This, ElementEncoding* encoding){
 	ASSERT(encoding->type==BINARYVAL);
-	allocElementConstraintVariables(encoding, getMaximumBitsBinaryValueEncodingVars(encoding));
+	allocElementConstraintVariables(encoding, encoding->numBits);
 	getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
 }
 
diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c
index 01cb65a..19d3111 100644
--- a/src/Backend/sattranslator.c
+++ b/src/Backend/sattranslator.c
@@ -16,13 +16,19 @@ uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding*
 }
 
 uint64_t getElementValueBinaryValueSATTranslator(CSolver* This, ElementEncoding* elemEnc){
-	//THIS WILL PROBABLY BE WRONG SINCE THE VALUES CAN BE OFFSET
 	uint64_t value=0;
 	for(int i=elemEnc->numVars-1;i>=0;i--) {
 		value=value<<1;
 		if (This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ])
 			value |= 1;
 	}
+	if (elemEnc->isBinaryValSigned &&
+			This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[elemEnc->numVars-1])]) {
+		//Do sign extension of negative number
+		uint64_t highbits=0xffffffffffffffff - ((1 << (elemEnc->numVars)) - 1);
+		value+=highbits;
+	}
+	value+=elemEnc->offset;
 	return value;
 }
 
diff --git a/src/Encoders/elementencoding.c b/src/Encoders/elementencoding.c
index 8d01cc7..47c6ea0 100644
--- a/src/Encoders/elementencoding.c
+++ b/src/Encoders/elementencoding.c
@@ -37,12 +37,4 @@ 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 49a890f..61bdb3e 100644
--- a/src/Encoders/elementencoding.h
+++ b/src/Encoders/elementencoding.h
@@ -14,9 +14,20 @@ struct ElementEncoding {
 	ElementEncodingType type;
 	Element * element;
 	Edge * variables;/* List Variables Used To Encode Element */
-	uint64_t * encodingArray;	/* List the Variables in the appropriate order */
-	uint64_t * inUseArray;/* Bitmap to track variables in use */
-	uint encArraySize;
+	union {
+		struct {
+			uint64_t * encodingArray;	/* List the Variables in the appropriate order */
+			uint64_t * inUseArray;/* Bitmap to track variables in use */
+			uint encArraySize;
+		};
+		struct {
+			uint64_t offset;/* Value = offset + encoded number (interpretted according to isBinaryValSigned) */
+			uint64_t low;/* Lowest value to encode */
+			uint64_t high;/* High value to encode.   If low > high, we assume wrap around to include 0. */
+			uint numBits;
+			bool isBinaryValSigned;
+		};
+	};
 	uint numVars;	/* Number of variables */
 };
 
@@ -36,6 +47,4 @@ static inline void setInUseElement(ElementEncoding *This, uint offset) {
 	This->inUseArray[(offset>>6)] |= 1 << (offset & 63);
 }
 
-uint getMaximumBitsBinaryValueEncodingVars(ElementEncoding *encoding);
-
 #endif