From: Hamed Gorjiara Date: Thu, 7 Feb 2019 00:21:09 +0000 (-0800) Subject: 1)core dump in regex for big strings 2) Boolean Var bugs 3) adding support for other... X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=51799c65144abda2e95b5bab5a0af868b3378714;hp=829b44197d915859a76704b501ebe14105b7585e 1)core dump in regex for big strings 2) Boolean Var bugs 3) adding support for other logical operations --- diff --git a/src/AlloyEnc/alloyenc.cc b/src/AlloyEnc/alloyenc.cc index 6a84180..6a8dcdf 100644 --- a/src/AlloyEnc/alloyenc.cc +++ b/src/AlloyEnc/alloyenc.cc @@ -10,7 +10,7 @@ #include "set.h" #include "function.h" #include -#include +#include 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 values; const char delim = ','; tokenize(line, delim, values); for (uint i=0; iinputs.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 7201dc2..ad7d2e7 100644 --- 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 e395ce3..1b321a6 100644 --- 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 6971a5e..92fb03f 100644 --- 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 f1756df..636c2b3 100644 --- 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 signatures; diff --git a/src/classlist.h b/src/classlist.h index 55ead29..d81b9bc 100644 --- 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;