1)core dump in regex for big strings 2) Boolean Var bugs 3) adding support for other...

diff --git a/src/AlloyEnc/alloyenc.cc b/src/AlloyEnc/alloyenc.cc
index 6a84180ee88f91edee8ecb3ea23cd7f29960811f..6a8dcdfe1a122af005f6abd8e99f87521299ddf6 100644 (file)
--- a/src/AlloyEnc/alloyenc.cc
+++ b/src/AlloyEnc/alloyenc.cc
@@ -10,7 +10,7 @@
 #include "set.h"
 #include "function.h"
 #include <fstream>
-#include <regex>
+#include <vector>
 
 using namespace std;
 
@@ -41,7 +41,6 @@ void AlloyEnc::encode(){
        while(iterator->hasNext()){
                BooleanEdge constraint = iterator->next();
                string constr = encodeConstraint(constraint);
-               //model_print("constr=%s\n", constr.c_str());
                char *cstr = new char [constr.length()+1];
                strcpy (cstr, constr.c_str());
                facts.push(cstr);
@@ -72,18 +71,20 @@ int AlloyEnc::getResult(){
        ifstream input(solutionFile, ios::in);
        string line;
        while(getline(input, line)){
-               if(regex_match(line, regex("Unsatisfiable."))){
+               if(line.find("Unsatisfiable.")== 0){
                        return IS_UNSAT;
                }
-               if(regex_match(line, regex(".*Element.*value=.*Element\\d+.*->\\d+.*"))){
+               if(line.find("univ") == 0){
+                       continue;
+               }
+               if(line.find("this/AbsBool<:value") == 0 || line.find("this/AbsElement<:value=") == 0){
                        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);
+                               uint i1, i2, i3;
+                               if (3 == sscanf(values[i].c_str(),"%*[^0123456789]%u%*[^0123456789]%d%*[^0123456789]%u", &i1, &i2, &i3)){
+                                       model_print("Signature%u = %u\n", i1, i3);
                                        sigEnc.setValue(i1, i3);
                                }
                        }
@@ -147,24 +148,46 @@ string AlloyEnc::encodeBooleanLogic( BooleanLogic *bl){
        string array[size];
        for (uint i = 0; i < size; i++)
                array[i] = encodeConstraint(bl->inputs.get(i));
+       string op;
+       switch (bl->op){
+               case SATC_OR:
+                       op = " or ";
+                       break;
+               case SATC_AND:
+                       op = " and ";
+                       break;
+               case SATC_NOT:
+                       op = " not ";
+                       break;
+               case SATC_IFF:
+                       op = " iff ";
+                       break;
+               case SATC_IMPLIES:
+                       op = " implies ";
+                       break;
+               case SATC_XOR:
+               default:
+                       ASSERT(0);
+       }
        switch (bl->op) {
+               case SATC_OR:
                case SATC_AND:{
                        ASSERT(size >= 2);
-                       string res = "";
+                       string res = "( ";
                        res += array[0];
                        for( uint i=1; i< size; i++){
-                               res += " and " + array[i];
+                               res += op + array[i];
                        }
+                       res += " )";
                        return res;
                }
                case SATC_NOT:{
-                       return "not " + array[0];
+                       return "not ( " + array[0] + " )";
                }
+               case SATC_IMPLIES:
                case SATC_IFF:
-                       return array[0] + " iff " + array[1];
-               case SATC_OR:
+                       return "( " + array[0] + op + array[1] + " )";
                case SATC_XOR:
-               case SATC_IMPLIES:
                default:
                        ASSERT(0);
 
@@ -256,17 +279,10 @@ void AlloyEnc::writeToFile(string str){
 }
 
 bool AlloyEnc::getBooleanValue(Boolean *b){
-       if (b->boolVal == BV_MUSTBETRUE)
-               return true;
-       else if (b->boolVal == BV_MUSTBEFALSE)
-               return false;
-       return sigEnc.getBooleanSignature(b);
+       return (bool)sigEnc.getValue(b);
 }
 
 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);
+       return (uint64_t)sigEnc.getValue(element);
 }
 

diff --git a/src/AlloyEnc/signature.cc b/src/AlloyEnc/signature.cc
index 7201dc2a9a996155bb68b573314b2111ece598ed..ad7d2e700fe9b81bbf2f3268c5340e07718c66bf 100644 (file)
--- a/src/AlloyEnc/signature.cc
+++ b/src/AlloyEnc/signature.cc
@@ -5,15 +5,20 @@ bool BooleanSig::encodeAbs = true;
 bool SetSig::encodeAbs = true;
 bool ElementSig::encodeAbs = true;
 
-BooleanSig::BooleanSig(uint id):
-       Signature(id),
-       value(-1)
+ValuedSignature::ValuedSignature(uint id): 
+       Signature(id), 
+       value(-1) 
 {
 }
 
-bool BooleanSig::getValue(){
+int ValuedSignature::getValue(){
        ASSERT(value != -1);
-       return (bool) value;
+       return value;
+}
+
+BooleanSig::BooleanSig(uint id):
+       ValuedSignature(id)
+{
 }
 
 string BooleanSig::toString() const{
@@ -50,9 +55,8 @@ string BooleanSig::getAbsSignature() const{
 }
 
 ElementSig::ElementSig(uint id, SetSig *_ssig): 
-       Signature(id),
-       ssig(_ssig),
-       value(0)
+       ValuedSignature(id),
+       ssig(_ssig)
 {
 }
 

diff --git a/src/AlloyEnc/signature.h b/src/AlloyEnc/signature.h
index e395ce3d35603ee0bab57ba0782c14bcf60b2f11..1b321a6f134590f8d7bbac8fbcece632119d9861 100644 (file)
--- a/src/AlloyEnc/signature.h
+++ b/src/AlloyEnc/signature.h
@@ -17,17 +17,23 @@ protected:
        uint id;
 };
 
-class BooleanSig: public Signature{
+class ValuedSignature: public Signature{
+public:
+       ValuedSignature(uint id);
+       int getValue();
+       void setValue(int v){value = v;}
+protected:
+       int value;
+};
+
+class BooleanSig: public ValuedSignature{
 public:
        BooleanSig(uint id);
-       bool getValue();
-       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 encodeAbs;
 };
 
@@ -43,18 +49,15 @@ private:
        string domain;
 };
 
-class ElementSig: public Signature{
+class ElementSig: public ValuedSignature{
 public:
        ElementSig(uint id, SetSig *ssig);
-       uint64_t getValue() { return value;}
-       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;
 };
 

diff --git a/src/AlloyEnc/signatureenc.cc b/src/AlloyEnc/signatureenc.cc
index 6971a5edcda4978f700531735ba3d81e934d5a35..92fb03fecd8af4e999ec52e9e48da5190325fbf4 100644 (file)
--- a/src/AlloyEnc/signatureenc.cc
+++ b/src/AlloyEnc/signatureenc.cc
@@ -34,7 +34,7 @@ void SignatureEnc::updateMaxValue(Set *set){
 BooleanSig *SignatureEnc::getBooleanSignature(Boolean *bvar){
        BooleanSig *bsig = (BooleanSig *)encoded.get((void *)bvar);
        if(bsig == NULL){
-               bsig = new BooleanSig(signatures.getSize());
+               bsig = new BooleanSig(getUniqueSigID());
                encoded.put(bvar, bsig);
                signatures.push(bsig);
                alloyEncoder->writeToFile(bsig->getSignature());
@@ -48,13 +48,13 @@ ElementSig *SignatureEnc::getElementSignature(Element *element){
                Set *set = element->getRange();
                SetSig *ssig = (SetSig *)encoded.get((void *)set);
                if(ssig == NULL){
-                       ssig = new SetSig(signatures.getSize(), set);
+                       ssig = new SetSig(getUniqueSigID(), set);
                        encoded.put(set, ssig);
                        signatures.push(ssig);
                        alloyEncoder->writeToFile(ssig->getSignature());
                        updateMaxValue(set);
                }
-               esig = new ElementSig(signatures.getSize(), ssig);
+               esig = new ElementSig(getUniqueSigID(), ssig);
                encoded.put(element, esig);
                signatures.push(esig);
                alloyEncoder->writeToFile(esig->getSignature());
@@ -63,16 +63,14 @@ ElementSig *SignatureEnc::getElementSignature(Element *element){
        return esig;
 }
 
-void SignatureEnc::setValue(uint id, uint64_t value){
-       ElementSig *sig = (ElementSig *)signatures.get(id);
+void SignatureEnc::setValue(uint id, uint value){
+       ValuedSignature *sig = getValuedSignature(id);
+       ASSERT(sig != NULL);
        sig->setValue(value);
 }
 
-uint64_t SignatureEnc::getValue(Element *element){
-       ElementSig *sig = (ElementSig *)encoded.get((void *) element);
+int SignatureEnc::getValue(void *astnode){
+       ValuedSignature *sig = (ValuedSignature *)encoded.get(astnode);
        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 f1756df7913c061b84f9936485d05b60d4b97022..636c2b3e500a0cbf2feeb28c4f8e8d0621274bdd 100644 (file)
--- a/src/AlloyEnc/signatureenc.h
+++ b/src/AlloyEnc/signatureenc.h
@@ -9,12 +9,14 @@ class SignatureEnc {
 public:
        SignatureEnc(AlloyEnc *_alloyEncoder);
        ~SignatureEnc();
-       void setValue(uint id, uint64_t value);
+       void setValue(uint id, uint value);
        ElementSig *getElementSignature(Element *element);
        BooleanSig *getBooleanSignature(Boolean *bvar);
        int getAlloyIntScope();
-       uint64_t getValue(Element *element);
+       int getValue(void *astnode);
 private:
+       ValuedSignature *getValuedSignature(uint uniqueID){return (ValuedSignature*)signatures.get(uniqueID-1);}
+       uint getUniqueSigID(){return signatures.getSize() +1;}
        void updateMaxValue(Set *set);
        CloneMap encoded;
        Vector<Signature*> signatures;

diff --git a/src/classlist.h b/src/classlist.h
index 55ead2954e92ea34cbd6a30f4bd7f625f1748f27..d81b9bc9c6e683e8f45d8cc67df45f73dd392b45 100644 (file)
--- a/src/classlist.h
+++ b/src/classlist.h
@@ -74,6 +74,7 @@ class EncodingEdge;
 class EncodingSubGraph;
 class SignatureEnc;
 class Signature;
+class ValuedSignature;
 class ElementSig;
 class SetSig;
 class BooleanSig;