fixing alloy performance bugs

diff --git a/src/AlloyEnc/alloyenc.cc b/src/AlloyEnc/alloyenc.cc
index 35ecd45ca50366ee232f690fb24430c298a7d403..6a84180ee88f91edee8ecb3ea23cd7f29960811f 100644 (file)
--- a/src/AlloyEnc/alloyenc.cc
+++ b/src/AlloyEnc/alloyenc.cc
@@ -56,6 +56,18 @@ void AlloyEnc::encode(){
        delete iterator;
 }
 
+void tokenize(string const &str, const char delim, vector<std::string> &out)
+{
+       size_t start;
+       size_t end = 0;
+
+       while ((start = str.find_first_not_of(delim, end)) != string::npos)
+       {
+               end = str.find(delim, start);
+               out.push_back(str.substr(start, end - start));
+       }
+}
+
 int AlloyEnc::getResult(){
        ifstream input(solutionFile, ios::in);
        string line;
@@ -63,14 +75,17 @@ int AlloyEnc::getResult(){
                if(regex_match(line, regex("Unsatisfiable."))){
                        return IS_UNSAT;
                }
-               if(regex_match(line, regex(".*Element\\d+.*value=.*Element\\d+.*->\\d+.*"))){
-                       int tmp=0, index=0, value=0;
-                       const char* s = line.c_str();
-                       uint i1, i2, i3;
-                       uint64_t i4;
-                       if (4 == sscanf(s,"%*[^0123456789]%u%*[^0123456789]%d%*[^0123456789]%d%*[^0123456789]%" PRId64 "", &i1, &i2, &i3, &i4)){
-                               model_print("Element%d = %" PRId64 "\n", i1, i4);
-                               sigEnc.setValue(i1, i4);
+               if(regex_match(line, regex(".*Element.*value=.*Element\\d+.*->\\d+.*"))){
+                       vector<string> values;
+                       const char delim = ',';
+                       tokenize(line, delim, values);
+                       for (uint i=0; i<values.size(); i++){
+                               uint i1, i2;
+                               uint64_t i3;
+                               if (3 == sscanf(values[i].c_str(),"%*[^0123456789]%d%*[^0123456789]%d%*[^0123456789]%" PRId64 "", &i1, &i2, &i3)){
+                                       model_print("Element%d = %" PRId64 "\n", i1, i3);
+                                       sigEnc.setValue(i1, i3);
+                               }
                        }
                }
        }
@@ -205,7 +220,6 @@ string AlloyEnc::processElementFunction(ElementFunction* elemFunc, ElementSig *s
 }
 
 string AlloyEnc::encodeOperatorPredicate(BooleanPredicate *constraint){
-       constraint->print();
        PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
        ASSERT(constraint->inputs.getSize() == 2);
        string str;

diff --git a/src/AlloyEnc/signature.cc b/src/AlloyEnc/signature.cc
index 4b898d8230d66347a13c66f3197fc26fd6630706..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::encodeAbsSig = 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(encodeAbsSig){
-               encodeAbsSig = 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";
        
 }
 

diff --git a/src/AlloyEnc/signature.h b/src/AlloyEnc/signature.h
index b3ebf47b84bbfba798b394e865fc7ca9301b7149..e395ce3d35603ee0bab57ba0782c14bcf60b2f11 100644 (file)
--- a/src/AlloyEnc/signature.h
+++ b/src/AlloyEnc/signature.h
@@ -10,6 +10,7 @@ public:
        Signature(uint _id):id(_id){}
        string operator+(const string& s);
        virtual string toString() const = 0;
+       virtual string getAbsSignature() const =0;
        virtual string getSignature() const =0;
        virtual ~Signature(){}
 protected:
@@ -23,10 +24,11 @@ public:
        void setValue(bool v) {value = v; }
        virtual ~BooleanSig(){}
        virtual string toString() const;
+       virtual string getAbsSignature() const;
        virtual string getSignature() const;
 private:
        int value;
-       static bool encodeAbsSig;
+       static bool encodeAbs;
 };
 
 class SetSig: public Signature{
@@ -34,7 +36,9 @@ public:
        SetSig(uint id, Set *set);
        virtual ~SetSig(){}
        virtual string toString() const;
+       virtual string getAbsSignature() const;
        virtual string getSignature() const;
+       static bool encodeAbs;
 private:
        string domain;
 };
@@ -46,10 +50,12 @@ public:
        void setValue(uint64_t v){value = v;}
        virtual ~ElementSig(){}
        virtual string toString() const;
+       virtual string getAbsSignature() const;
        virtual string getSignature() const;
 private:
        SetSig *ssig;
        uint64_t value;
+       static bool encodeAbs;
 };
 
 string operator+(const string& str, const Signature& sig);