Bug Fix: defining the scope of integer for Alloy

diff --git a/src/AlloyEnc/alloyenc.cc b/src/AlloyEnc/alloyenc.cc
index c7acf23e140c691b1da8e8a067f2d04da497bb9a..033985a5a576868c6a9ef31da3005531d74d7b8a 100644 (file)
--- a/src/AlloyEnc/alloyenc.cc
+++ b/src/AlloyEnc/alloyenc.cc
@@ -7,6 +7,7 @@
 #include "predicate.h"
 #include "element.h"
 #include "signature.h"
+#include "set.h"
 #include <fstream>
 #include <regex>
 
@@ -74,7 +75,13 @@ int AlloyEnc::getResult(){
        return IS_SAT;
 }
 
+void AlloyEnc::dumpAlloyIntScope(){
+       output << "pred show {}" << endl;
+       output << "run show for " << sigEnc.getAlloyIntScope() << " int" << endl;
+}
+
 int AlloyEnc::solve(){
+       dumpAlloyIntScope();
        int result = IS_INDETER;
        char buffer [512];
        if( output.is_open()){
@@ -177,6 +184,9 @@ void AlloyEnc::writeToFile(string str){
 }
 
 uint64_t AlloyEnc::getValue(Element * element){
+       ElementEncoding *elemEnc = element->getElementEncoding();
+       if (elemEnc->numVars == 0)//case when the set has only one item
+               return element->getRange()->getElement(0);
        return sigEnc.getValue(element);
 }
 

diff --git a/src/AlloyEnc/alloyenc.h b/src/AlloyEnc/alloyenc.h
index 94d991e726548bf96f2988f66ecfae57731c8beb..dd93eb039f7d65e22f3359bfe5a90403687bce7b 100644 (file)
--- a/src/AlloyEnc/alloyenc.h
+++ b/src/AlloyEnc/alloyenc.h
@@ -16,6 +16,7 @@ public:
        uint64_t getValue(Element * element);
        ~AlloyEnc();
 private:
+       void dumpAlloyIntScope();
        string encodeConstraint(BooleanEdge constraint);
        int getResult();
        string encodeBooleanLogic( BooleanLogic *bl);

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 "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();
 }

diff --git a/src/AlloyEnc/signatureenc.h b/src/AlloyEnc/signatureenc.h
index d98a636075df3135eca4a4c988232d6a793d1904..76481954bd380bc3728c5f108b41dd3a0d690e20 100644 (file)
--- a/src/AlloyEnc/signatureenc.h
+++ b/src/AlloyEnc/signatureenc.h
@@ -11,10 +11,13 @@ public:
        ~SignatureEnc();
        void setValue(uint id, uint64_t value);
        ElementSig *getElementSignature(Element *element);
+       int getAlloyIntScope();
        uint64_t getValue(Element *element);
 private:
+       void updateMaxValue(Set *set);
        CloneMap encoded;
        Vector<Signature*> signatures;
        AlloyEnc *alloyEncoder;
+       uint64_t maxValue;
 };
 #endif