X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FAlloyEnc%2Fsignature.cc;h=ad7d2e700fe9b81bbf2f3268c5340e07718c66bf;hb=51799c65144abda2e95b5bab5a0af868b3378714;hp=62c1c1a9972dfcc8dd657066275d43fa54b6e759;hpb=b18182d3220c63bdd7b4810ee5752413f317c28f;p=satune.git

diff --git a/src/AlloyEnc/signature.cc b/src/AlloyEnc/signature.cc
index 62c1c1a..ad7d2e7 100644
--- a/src/AlloyEnc/signature.cc
+++ b/src/AlloyEnc/signature.cc
@@ -1,12 +1,63 @@
 #include "signature.h"
 #include "set.h"
 
+bool BooleanSig::encodeAbs = true;
+bool SetSig::encodeAbs = true;
+bool ElementSig::encodeAbs = true;
+
+ValuedSignature::ValuedSignature(uint id): 
+	Signature(id), 
+	value(-1) 
+{
+}
+
+int ValuedSignature::getValue(){
+	ASSERT(value != -1);
+	return value;
+}
+
+BooleanSig::BooleanSig(uint id):
+	ValuedSignature(id)
+{
+}
+
+string BooleanSig::toString() const{
+	return "Boolean" + to_string(id) + ".value";
+}
+
+string BooleanSig::getSignature() const{
+	string str;
+	if(encodeAbs){
+		encodeAbs = false;
+		str += getAbsSignature();
+	}
+	str += "one sig Boolean" + to_string(id) + " extends AbsBool {}";
+	return str;
+}
+
+string BooleanSig::getAbsSignature() const{
+	string str;
+	if(SetSig::encodeAbs){
+		SetSig::encodeAbs = false;
+		str += "abstract sig AbsSet {\
+		domain: set Int\
+		}\n";
+	}
+	str +="one sig BooleanSet extends AbsSet {}{\n\
+	domain = 0 + 1 \n\
+	}\n\
+	abstract sig AbsBool {\
+	value: Int\
+	}{\n\
+	value in BooleanSet.domain\n\
+	}\n";
+	return str;
+}
+
 ElementSig::ElementSig(uint id, SetSig *_ssig): 
-	Signature(id),
-	ssig(_ssig),
-	value(0)
+	ValuedSignature(id),
+	ssig(_ssig)
 {
-	
 }
 
 string ElementSig::toString() const{
@@ -14,11 +65,21 @@ string ElementSig::toString() const{
 }
 
 string ElementSig::getSignature() const{
-	return "one sig Element" + to_string(id) + " {\n\
-		value: Int\n\
-		}{\n\
+	string str;
+	if(encodeAbs){
+		encodeAbs = false;
+		str += getAbsSignature();
+	}
+	str += "one sig Element" + to_string(id) + " extends AbsElement {}{\n\
 		value in " + *ssig + "\n\
 		}";
+	return str;
+}
+
+string ElementSig::getAbsSignature() const{
+	return "abstract sig AbsElement {\n\
+		value: Int\n\
+		}\n";
 	
 }
 
@@ -35,11 +96,21 @@ string SetSig::toString() const{
 }
 
 string SetSig::getSignature() const{
-	return "one sig Set" + to_string(id) + " {\n\
-		domain: set Int\n\
-		}{\n\
+	string str;
+	if(encodeAbs){
+		encodeAbs = false;
+		str += getAbsSignature();
+	}
+	str += "one sig Set" + to_string(id) + " extends AbsSet {}{\n\
 		domain = " + domain + "\n\
 		}";
+	return str;
+}
+
+string SetSig::getAbsSignature() const{
+	return "abstract sig AbsSet {\n\
+		domain: set Int\n\
+		}\n";
 	
 }