From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Wed, 23 Jan 2019 00:59:57 +0000 (-0800)
Subject: Bug Fix: defining the scope of integer for Alloy
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=c8012458e3e2777c72ed1d9b217dfa3d69422a4d;ds=sidebyside

Bug Fix: defining the scope of integer for Alloy
---

diff --git a/src/AlloyEnc/alloyenc.cc b/src/AlloyEnc/alloyenc.cc
index c7acf23..033985a 100644
--- 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 94d991e..dd93eb0 100644
--- 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 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();
 }
diff --git a/src/AlloyEnc/signatureenc.h b/src/AlloyEnc/signatureenc.h
index d98a636..7648195 100644
--- 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