fixing alloy performance bugs

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

diff --git a/src/AlloyEnc/signature.cc b/src/AlloyEnc/signature.cc
index 4237fd6e25e042a976986013141a7dbdf657ec18..7201dc2a9a996155bb68b573314b2111ece598ed 100644 (file)
--- a/src/AlloyEnc/signature.cc
+++ b/src/AlloyEnc/signature.cc
@@ -1,7 +1,9 @@
 #include "signature.h"
 #include "set.h"
 
-bool BooleanSig::encodeSet = true;
+bool BooleanSig::encodeAbs = true;
+bool SetSig::encodeAbs = true;
+bool ElementSig::encodeAbs = true;
 
 BooleanSig::BooleanSig(uint id):
        Signature(id),
@@ -20,19 +22,30 @@ string BooleanSig::toString() const{
 
 string BooleanSig::getSignature() const{
        string str;
-       if(encodeSet){
-               encodeSet = false;
-               str += "one sig BooleanSet {\n\
-               domain: set Int\n\
-               }{\n\
-               domain = 0 + 1 \n\
+       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 Boolean" + to_string(id) + " {\n\
-       value: 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;
 }
 
@@ -48,11 +61,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";
        
 }
 
@@ -69,11 +92,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";
        
 }