X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FAlloyEnc%2Fsignatureenc.cc;h=f0ed880fb33a6c8b8836dea2b37f5f81a24016b2;hp=4c11957b31069354e1af1bbaa0c875a030d438d9;hb=c8012458e3e2777c72ed1d9b217dfa3d69422a4d;hpb=b18182d3220c63bdd7b4810ee5752413f317c28f

diff --git a/src/AlloyEnc/signatureenc.cc b/src/AlloyEnc/signatureenc.cc
index 4c11957..f0ed880 100644
--- a/src/AlloyEnc/signatureenc.cc
+++ b/src/AlloyEnc/signatureenc.cc
@@ -3,8 +3,12 @@
 #include "set.h"
 #include "signature.h"
 #include "alloyenc.h"
+#include "math.h"
 
-SignatureEnc::SignatureEnc(AlloyEnc *ae): alloyEncoder(ae){
+SignatureEnc::SignatureEnc(AlloyEnc *ae): 
+	alloyEncoder(ae),
+	maxValue(0)
+{
 }
 
 SignatureEnc::~SignatureEnc(){
@@ -14,6 +18,19 @@ SignatureEnc::~SignatureEnc(){
 	}
 }
 
+int SignatureEnc::getAlloyIntScope(){
+	double mylog = log2(maxValue + 1);
+	return floor(mylog) == mylog ? (int)mylog + 1: (int)mylog + 2;
+}
+
+void SignatureEnc::updateMaxValue(Set *set){
+	for(uint i=0; i< set->getSize(); i++){
+		if(set->getElement(i) > maxValue){
+			maxValue = set->getElement(i);
+		}
+	}
+}
+
 ElementSig *SignatureEnc::getElementSignature(Element *element){
 	ElementSig *esig = (ElementSig *)encoded.get((void *)element);
 	if(esig == NULL){
@@ -24,8 +41,11 @@ ElementSig *SignatureEnc::getElementSignature(Element *element){
 			encoded.put(set, ssig);
 			signatures.push(ssig);
 			alloyEncoder->writeToFile(ssig->getSignature());
+			updateMaxValue(set);
 		}
 		esig = new ElementSig(signatures.getSize(), ssig);
+		element->print();
+		model_print(" = Element%u\n", signatures.getSize());
 		encoded.put(element, esig);
 		signatures.push(esig);
 		alloyEncoder->writeToFile(esig->getSignature());
@@ -42,5 +62,8 @@ void SignatureEnc::setValue(uint id, uint64_t value){
 uint64_t SignatureEnc::getValue(Element *element){
 	ElementSig *sig = (ElementSig *)encoded.get((void *) element);
 	ASSERT(sig != NULL);
+	model_print("******************\n");
+	element->print();
+	model_print("Value = %" PRId64 "\n", sig->getValue());
 	return sig->getValue();
 }