Bug Fix: defining the scope of integer for Alloy

[satune.git] / src / AlloyEnc / signatureenc.cc

diff --git a/src/AlloyEnc/signatureenc.cc b/src/AlloyEnc/signatureenc.cc
index 4c11957b31069354e1af1bbaa0c875a030d438d9..f0ed880fb33a6c8b8836dea2b37f5f81a24016b2 100644 (file)
--- a/src/AlloyEnc/signatureenc.cc
+++ b/src/AlloyEnc/signatureenc.cc
@@ -3,8 +3,12 @@
 #include "set.h"
 #include "signature.h"
 #include "alloyenc.h"
 #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(){
 }
 
 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){
 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());
                        encoded.put(set, ssig);
                        signatures.push(ssig);
                        alloyEncoder->writeToFile(ssig->getSignature());

+                       updateMaxValue(set);

                }
                esig = new ElementSig(signatures.getSize(), ssig);
                }
                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());
                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);
 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();
 }
        return sig->getValue();
 }