From 829b44197d915859a76704b501ebe14105b7585e Mon Sep 17 00:00:00 2001 From: Hamed Gorjiara Date: Mon, 28 Jan 2019 16:23:33 -0800 Subject: [PATCH 1/1] fixing alloy performance bugs --- src/AlloyEnc/alloyenc.cc | 32 +++++++++++++------ src/AlloyEnc/signature.cc | 65 +++++++++++++++++++++++++++++---------- src/AlloyEnc/signature.h | 8 ++++- 3 files changed, 79 insertions(+), 26 deletions(-) diff --git a/src/AlloyEnc/alloyenc.cc b/src/AlloyEnc/alloyenc.cc index 35ecd45..6a84180 100644 --- 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 &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 values; + const char delim = ','; + tokenize(line, delim, values); + for (uint i=0; iprint(); 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 4b898d8..7201dc2 100644 --- 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 b3ebf47..e395ce3 100644 --- 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); -- 2.34.1