From: Hamed Gorjiara Date: Tue, 19 Feb 2019 20:11:31 +0000 (-0800) Subject: Interpreter abstraction and memory bug fixes X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=3267d387309bb4d2aa130a940f386b419652a956 Interpreter abstraction and memory bug fixes --- diff --git a/src/AlloyEnc/alloyenc.cc b/src/AlloyEnc/alloyenc.cc deleted file mode 100644 index cad0529..0000000 --- a/src/AlloyEnc/alloyenc.cc +++ /dev/null @@ -1,294 +0,0 @@ -#include "alloyenc.h" -#include -#include "signatureenc.h" -#include "structs.h" -#include "csolver.h" -#include "boolean.h" -#include "predicate.h" -#include "element.h" -#include "signature.h" -#include "set.h" -#include "function.h" -#include "inc_solver.h" -#include -#include - -using namespace std; - -const char * AlloyEnc::alloyFileName = "satune.als"; -const char * AlloyEnc::solutionFile = "solution.sol"; - -AlloyEnc::AlloyEnc(CSolver *_solver): - csolver(_solver), - sigEnc(this) -{ - output.open(alloyFileName); - if(!output.is_open()){ - model_print("AlloyEnc:Error in opening the dump file satune.als\n"); - exit(-1); - } -} - -AlloyEnc::~AlloyEnc(){ - if(output.is_open()){ - output.close(); - } -} - -void AlloyEnc::encode(){ - dumpAlloyHeader(); - SetIteratorBooleanEdge *iterator = csolver->getConstraints(); - Vector facts; - while(iterator->hasNext()){ - BooleanEdge constraint = iterator->next(); - string constr = encodeConstraint(constraint); - char *cstr = new char [constr.length()+1]; - strcpy (cstr, constr.c_str()); - facts.push(cstr); - } - output << "fact {" << endl; - for(uint i=0; i< facts.getSize(); i++){ - char *cstr = facts.get(i); - writeToFile(cstr); - delete[] cstr; - } - output << "}" << endl; - 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; - while(getline(input, line)){ - if(line.find("Unsatisfiable.")== 0){ - return IS_UNSAT; - } - 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; igetSatSolverTimeout(); - return timeout == (uint)NOTIMEOUT? 1000: timeout; -} - -void AlloyEnc::dumpAlloyHeader(){ - output << "open util/integer" << endl; -} - -int AlloyEnc::solve(){ - dumpAlloyFooter(); - int result = IS_INDETER; - char buffer [512]; - if( output.is_open()){ - output.close(); - } - snprintf(buffer, sizeof(buffer), "./run.sh timeout %u java -Xmx10000m edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", getTimeout(), alloyFileName, solutionFile); - int status = system(buffer); - if (status == 0) { - //Read data in from results file - result = getResult(); - } - return result; -} - -string AlloyEnc::encodeConstraint(BooleanEdge c){ - Boolean *constraint = c.getBoolean(); - string res; - switch(constraint->type){ - case LOGICOP:{ - res = encodeBooleanLogic((BooleanLogic *) constraint); - break; - } - case PREDICATEOP:{ - res = encodePredicate((BooleanPredicate *) constraint); - break; - } - case BOOLEANVAR:{ - res = encodeBooleanVar( (BooleanVar *) constraint); - break; - } - default: - ASSERT(0); - } - if(c.isNegated()){ - return "not ( " + res + " )"; - } - return res; -} - -string AlloyEnc::encodeBooleanLogic( BooleanLogic *bl){ - uint size = bl->inputs.getSize(); - 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 = "( "; - res += array[0]; - for( uint i=1; i< size; i++){ - res += op + array[i]; - } - res += " )"; - return res; - } - case SATC_NOT:{ - return "not ( " + array[0] + " )"; - } - case SATC_IMPLIES: - case SATC_IFF: - return "( " + array[0] + op + array[1] + " )"; - case SATC_XOR: - default: - ASSERT(0); - - } -} - -string AlloyEnc::encodePredicate( BooleanPredicate *bp){ - switch (bp->predicate->type) { - case TABLEPRED: - ASSERT(0); - case OPERATORPRED: - return encodeOperatorPredicate(bp); - default: - ASSERT(0); - } -} - -string AlloyEnc::encodeBooleanVar( BooleanVar *bv){ - BooleanSig * boolSig = sigEnc.getBooleanSignature(bv); - return *boolSig + " = 1"; -} - -string AlloyEnc::processElementFunction(ElementFunction* elemFunc, ElementSig *signature){ - FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction(); - uint numDomains = elemFunc->inputs.getSize(); - ASSERT(numDomains > 1); - ElementSig *inputs[numDomains]; - string result; - for (uint i = 0; i < numDomains; i++) { - Element *elem = elemFunc->inputs.get(i); - inputs[i] = sigEnc.getElementSignature(elem); - if(elem->type == ELEMFUNCRETURN){ - result += processElementFunction((ElementFunction *) elem, inputs[i]); - } - } - string op; - switch(function->op){ - case SATC_ADD: - op = ".add"; - break; - case SATC_SUB: - op = ".sub"; - break; - default: - ASSERT(0); - } - result += *signature + " = " + *inputs[0]; - for (uint i = 1; i < numDomains; i++) { - result += op + "["+ *inputs[i] +"]"; - } - result += "\n"; - return result; -} - -string AlloyEnc::encodeOperatorPredicate(BooleanPredicate *constraint){ - PredicateOperator *predicate = (PredicateOperator *) constraint->predicate; - ASSERT(constraint->inputs.getSize() == 2); - string str; - Element *elem0 = constraint->inputs.get(0); - ASSERT(elem0->type == ELEMSET || elem0->type == ELEMFUNCRETURN || elem0->type == ELEMCONST); - ElementSig *elemSig1 = sigEnc.getElementSignature(elem0); - if(elem0->type == ELEMFUNCRETURN){ - str += processElementFunction((ElementFunction *) elem0, elemSig1); - } - Element *elem1 = constraint->inputs.get(1); - ASSERT(elem1->type == ELEMSET || elem1->type == ELEMFUNCRETURN || elem1->type == ELEMCONST); - ElementSig *elemSig2 = sigEnc.getElementSignature(elem1); - if(elem1->type == ELEMFUNCRETURN){ - str += processElementFunction((ElementFunction *) elem1, elemSig2); - } - switch (predicate->getOp()) { - case SATC_EQUALS: - str += *elemSig1 + " = " + *elemSig2; - break; - case SATC_LT: - str += *elemSig1 + " < " + *elemSig2; - break; - case SATC_GT: - str += *elemSig1 + " > " + *elemSig2; - break; - default: - ASSERT(0); - } - return str; -} - -void AlloyEnc::writeToFile(string str){ - output << str << endl; -} - -bool AlloyEnc::getBooleanValue(Boolean *b){ - return (bool)sigEnc.getValue(b); -} - -uint64_t AlloyEnc::getValue(Element * element){ - return (uint64_t)sigEnc.getValue(element); -} - diff --git a/src/AlloyEnc/alloyenc.h b/src/AlloyEnc/alloyenc.h deleted file mode 100644 index 3edfdbf..0000000 --- a/src/AlloyEnc/alloyenc.h +++ /dev/null @@ -1,37 +0,0 @@ -#ifndef ALLOYENC_H -#define ALLOYENC_H - -#include "classlist.h" -#include "signatureenc.h" -#include -#include -using namespace std; - -class AlloyEnc{ -public: - AlloyEnc(CSolver *solver); - void encode(); - int solve(); - void writeToFile(string str); - uint64_t getValue(Element *element); - bool getBooleanValue(Boolean *element); - ~AlloyEnc(); -private: - void dumpAlloyFooter(); - void dumpAlloyHeader(); - inline uint getTimeout(); - string encodeConstraint(BooleanEdge constraint); - int getResult(); - string encodeBooleanLogic( BooleanLogic *bl); - string encodeBooleanVar( BooleanVar *bv); - string encodePredicate( BooleanPredicate *bp); - string encodeOperatorPredicate(BooleanPredicate *constraint); - string processElementFunction(ElementFunction *element, ElementSig *signature); - CSolver *csolver; - SignatureEnc sigEnc; - ofstream output; - static const char * alloyFileName; - static const char * solutionFile; -}; - -#endif diff --git a/src/AlloyEnc/signature.cc b/src/AlloyEnc/signature.cc deleted file mode 100644 index ad7d2e7..0000000 --- a/src/AlloyEnc/signature.cc +++ /dev/null @@ -1,123 +0,0 @@ -#include "signature.h" -#include "set.h" - -bool BooleanSig::encodeAbs = true; -bool SetSig::encodeAbs = true; -bool ElementSig::encodeAbs = true; - -ValuedSignature::ValuedSignature(uint id): - Signature(id), - value(-1) -{ -} - -int ValuedSignature::getValue(){ - ASSERT(value != -1); - return value; -} - -BooleanSig::BooleanSig(uint id): - ValuedSignature(id) -{ -} - -string BooleanSig::toString() const{ - return "Boolean" + to_string(id) + ".value"; -} - -string BooleanSig::getSignature() const{ - string str; - 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 BooleanSet extends AbsSet {}{\n\ - domain = 0 + 1 \n\ - }\n\ - abstract sig AbsBool {\ - value: Int\ - }{\n\ - value in BooleanSet.domain\n\ - }\n"; - return str; -} - -ElementSig::ElementSig(uint id, SetSig *_ssig): - ValuedSignature(id), - ssig(_ssig) -{ -} - -string ElementSig::toString() const{ - return "Element" + to_string(id) + ".value"; -} - -string ElementSig::getSignature() const{ - 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"; - -} - -SetSig::SetSig(uint id, Set *set): Signature(id){ - ASSERT(set->getSize() > 0); - domain = to_string(set->getElement(0)); - for(uint i=1; i< set->getSize(); i++){ - domain += " + " + to_string(set->getElement(i)); - } -} - -string SetSig::toString() const{ - return "Set" + to_string(id) + ".domain"; -} - -string SetSig::getSignature() const{ - 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"; - -} - -string Signature::operator+(const string& str){ - return toString() + str; -} - -string operator+(const string& str, const Signature& sig){ - return str + sig.toString(); -} diff --git a/src/AlloyEnc/signature.h b/src/AlloyEnc/signature.h deleted file mode 100644 index 1b321a6..0000000 --- a/src/AlloyEnc/signature.h +++ /dev/null @@ -1,66 +0,0 @@ -#ifndef ELEMENTSIG_H -#define ELEMENTSIG_H -#include -#include -#include "classlist.h" -using namespace std; - -class Signature{ -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: - uint id; -}; - -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); - virtual ~BooleanSig(){} - virtual string toString() const; - virtual string getAbsSignature() const; - virtual string getSignature() const; -private: - static bool encodeAbs; -}; - -class SetSig: public Signature{ -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; -}; - -class ElementSig: public ValuedSignature{ -public: - ElementSig(uint id, SetSig *ssig); - virtual ~ElementSig(){} - virtual string toString() const; - virtual string getAbsSignature() const; - virtual string getSignature() const; -private: - SetSig *ssig; - static bool encodeAbs; -}; - -string operator+(const string& str, const Signature& sig); - -#endif diff --git a/src/AlloyEnc/signatureenc.cc b/src/AlloyEnc/signatureenc.cc deleted file mode 100644 index 92fb03f..0000000 --- a/src/AlloyEnc/signatureenc.cc +++ /dev/null @@ -1,76 +0,0 @@ -#include "signatureenc.h" -#include "element.h" -#include "set.h" -#include "signature.h" -#include "alloyenc.h" -#include "math.h" - -SignatureEnc::SignatureEnc(AlloyEnc *ae): - alloyEncoder(ae), - maxValue(0) -{ -} - -SignatureEnc::~SignatureEnc(){ - for(uint i=0; igetSize(); i++){ - if(set->getElement(i) > maxValue){ - maxValue = set->getElement(i); - } - } -} - -BooleanSig *SignatureEnc::getBooleanSignature(Boolean *bvar){ - BooleanSig *bsig = (BooleanSig *)encoded.get((void *)bvar); - if(bsig == NULL){ - bsig = new BooleanSig(getUniqueSigID()); - encoded.put(bvar, bsig); - signatures.push(bsig); - alloyEncoder->writeToFile(bsig->getSignature()); - } - return bsig; -} - -ElementSig *SignatureEnc::getElementSignature(Element *element){ - ElementSig *esig = (ElementSig *)encoded.get((void *)element); - if(esig == NULL){ - Set *set = element->getRange(); - SetSig *ssig = (SetSig *)encoded.get((void *)set); - if(ssig == NULL){ - ssig = new SetSig(getUniqueSigID(), set); - encoded.put(set, ssig); - signatures.push(ssig); - alloyEncoder->writeToFile(ssig->getSignature()); - updateMaxValue(set); - } - esig = new ElementSig(getUniqueSigID(), ssig); - encoded.put(element, esig); - signatures.push(esig); - alloyEncoder->writeToFile(esig->getSignature()); - - } - return esig; -} - -void SignatureEnc::setValue(uint id, uint value){ - ValuedSignature *sig = getValuedSignature(id); - ASSERT(sig != NULL); - sig->setValue(value); -} - -int SignatureEnc::getValue(void *astnode){ - ValuedSignature *sig = (ValuedSignature *)encoded.get(astnode); - ASSERT(sig != NULL); - return sig->getValue(); -} diff --git a/src/AlloyEnc/signatureenc.h b/src/AlloyEnc/signatureenc.h deleted file mode 100644 index 636c2b3..0000000 --- a/src/AlloyEnc/signatureenc.h +++ /dev/null @@ -1,26 +0,0 @@ -#ifndef SIGNATUREENC_H -#define SIGNATUREENC_H - -#include "classlist.h" -#include "structs.h" -#include "cppvector.h" - -class SignatureEnc { -public: - SignatureEnc(AlloyEnc *_alloyEncoder); - ~SignatureEnc(); - void setValue(uint id, uint value); - ElementSig *getElementSignature(Element *element); - BooleanSig *getBooleanSignature(Boolean *bvar); - int getAlloyIntScope(); - 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; - AlloyEnc *alloyEncoder; - uint64_t maxValue; -}; -#endif diff --git a/src/Interpreter/alloyenc.cc b/src/Interpreter/alloyenc.cc new file mode 100644 index 0000000..66e0ef5 --- /dev/null +++ b/src/Interpreter/alloyenc.cc @@ -0,0 +1,194 @@ +#include "alloyenc.h" +#include +#include "signatureenc.h" +#include "structs.h" +#include "csolver.h" +#include "boolean.h" +#include "predicate.h" +#include "element.h" +#include "signature.h" +#include "set.h" +#include "function.h" +#include "inc_solver.h" +#include +#include "cppvector.h" + +using namespace std; + +#define alloyFileName "satune.als" +#define solutionFile "solution.sol" + +AlloyEnc::AlloyEnc(CSolver *_solver): + Interpreter(_solver) +{ + output.open(alloyFileName); + if(!output.is_open()){ + model_print("AlloyEnc:Error in opening the dump file satune.als\n"); + exit(-1); + } +} + +AlloyEnc::~AlloyEnc(){ + if(output.is_open()){ + output.close(); + } +} + +void AlloyEnc::dumpAllConstraints(Vector &facts){ + output << "fact {" << endl; + for(uint i=0; i< facts.getSize(); i++){ + char *cstr = facts.get(i); + writeToFile(cstr); + } + output << "}" << endl; +} + + +int AlloyEnc::getResult(){ + ifstream input(solutionFile, ios::in); + string line; + while(getline(input, line)){ + if(line.find("Unsatisfiable.")== 0){ + return IS_UNSAT; + } + if(line.find("univ") == 0){ + continue; + } + if(line.find("this/AbsBool<:value") == 0 || line.find("this/AbsElement<:value=") == 0){ + const char delim [2] = ","; + char cline [line.size()+1]; + strcpy ( cline, line.c_str() ); + char *token = strtok(cline, delim); + while( token != NULL ) { + printf( " %s\n", token ); + uint i1, i2, i3; + if (3 == sscanf(token,"%*[^0123456789]%u%*[^0123456789]%d%*[^0123456789]%u", &i1, &i2, &i3)){ + model_print("Signature%u = %u\n", i1, i3); + sigEnc.setValue(i1, i3); + } + token = strtok(NULL, delim); + } + } + } + return IS_SAT; +} + +void AlloyEnc::dumpFooter(){ + output << "pred show {}" << endl; + output << "run show for " << sigEnc.getAlloyIntScope() << " int" << endl; +} + +void AlloyEnc::dumpHeader(){ + output << "open util/integer" << endl; +} + +void AlloyEnc::compileRunCommand(char * command, size_t size){ + snprintf(command, size, "./run.sh timeout %u java -Xmx10000m edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", getTimeout(), alloyFileName, solutionFile); +} + +string AlloyEnc::negateConstraint(string constr){ + return "not ( " + constr + " )"; +} + +string AlloyEnc::encodeBooleanLogic( BooleanLogic *bl){ + uint size = bl->inputs.getSize(); + 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 = "( "; + res += array[0]; + for( uint i=1; i< size; i++){ + res += op + array[i]; + } + res += " )"; + return res; + } + case SATC_NOT:{ + return "not ( " + array[0] + " )"; + } + case SATC_IMPLIES: + case SATC_IFF: + return "( " + array[0] + op + array[1] + " )"; + case SATC_XOR: + default: + ASSERT(0); + + } +} + +string AlloyEnc::encodeBooleanVar( BooleanVar *bv){ + BooleanSig * boolSig = sigEnc.getBooleanSignature(bv); + return *boolSig + " = 1"; +} + +string AlloyEnc::processElementFunction(ElementFunction* elemFunc, ElementSig *signature){ + FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction(); + uint numDomains = elemFunc->inputs.getSize(); + ASSERT(numDomains > 1); + ElementSig *inputs[numDomains]; + string result; + for (uint i = 0; i < numDomains; i++) { + Element *elem = elemFunc->inputs.get(i); + inputs[i] = sigEnc.getElementSignature(elem); + if(elem->type == ELEMFUNCRETURN){ + result += processElementFunction((ElementFunction *) elem, inputs[i]); + } + } + string op; + switch(function->op){ + case SATC_ADD: + op = ".add"; + break; + case SATC_SUB: + op = ".sub"; + break; + default: + ASSERT(0); + } + result += *signature + " = " + *inputs[0]; + for (uint i = 1; i < numDomains; i++) { + result += op + "["+ *inputs[i] +"]"; + } + result += "\n"; + return result; +} + +string AlloyEnc::operatorPredicateConstraint(CompOp op, ElementSig *elemSig1, ElementSig *elemSig2){ + switch (op) { + case SATC_EQUALS: + return *elemSig1 + " = " + *elemSig2; + case SATC_LT: + return *elemSig1 + " < " + *elemSig2; + case SATC_GT: + return *elemSig1 + " > " + *elemSig2; + default: + ASSERT(0); + } +} + + diff --git a/src/Interpreter/alloyenc.h b/src/Interpreter/alloyenc.h new file mode 100644 index 0000000..f3e0f1b --- /dev/null +++ b/src/Interpreter/alloyenc.h @@ -0,0 +1,28 @@ +#ifndef ALLOYENC_H +#define ALLOYENC_H + +#include "classlist.h" +#include "signatureenc.h" +#include "interpreter.h" +#include +#include + +class AlloyEnc: public Interpreter{ +public: + AlloyEnc(CSolver *solver); + virtual ~AlloyEnc(); +protected: + virtual void dumpFooter(); + virtual void dumpHeader(); + virtual void compileRunCommand(char * command , size_t size); + virtual int getResult(); + virtual void dumpAllConstraints(Vector &facts); + virtual string negateConstraint(string constr); + virtual string encodeBooleanLogic( BooleanLogic *bl); + virtual string encodeBooleanVar( BooleanVar *bv); + string encodeOperatorPredicate(BooleanPredicate *constraint); + virtual string processElementFunction(ElementFunction *element, ElementSig *signature); + virtual string operatorPredicateConstraint(CompOp op, ElementSig *elemSig1, ElementSig *elemSig2); +}; + +#endif diff --git a/src/Interpreter/interpreter.cc b/src/Interpreter/interpreter.cc new file mode 100644 index 0000000..bab92b4 --- /dev/null +++ b/src/Interpreter/interpreter.cc @@ -0,0 +1,133 @@ +#include "interpreter.h" +#include +#include "signatureenc.h" +#include "structs.h" +#include "csolver.h" +#include "boolean.h" +#include "predicate.h" +#include "element.h" +#include "signature.h" +#include "set.h" +#include "function.h" +#include "inc_solver.h" +#include + +using namespace std; + +Interpreter::Interpreter(CSolver *_solver): + csolver(_solver), + sigEnc(this) +{ +} + +Interpreter::~Interpreter(){ +} + +void Interpreter::encode(){ + dumpHeader(); + SetIteratorBooleanEdge *iterator = csolver->getConstraints(); + Vector facts; + while(iterator->hasNext()){ + BooleanEdge constraint = iterator->next(); + string constr = encodeConstraint(constraint); + char *cstr = new char [constr.length()+1]; + strcpy (cstr, constr.c_str()); + facts.push(cstr); + } + dumpAllConstraints(facts); + for(uint i=0; i< facts.getSize(); i++){ + char *cstr = facts.get(i); + delete[] cstr; + } + delete iterator; +} + +uint Interpreter::getTimeout(){ + uint timeout =csolver->getSatSolverTimeout(); + return timeout == (uint)NOTIMEOUT? 1000: timeout; +} + +int Interpreter::solve(){ + dumpFooter(); + int result = IS_INDETER; + char buffer [512]; + if( output.is_open()){ + output.close(); + } + compileRunCommand(buffer, sizeof(buffer)); + int status = system(buffer); + if (status == 0) { + //Read data in from results file + result = getResult(); + } + return result; +} + +string Interpreter::encodeConstraint(BooleanEdge c){ + Boolean *constraint = c.getBoolean(); + string res; + switch(constraint->type){ + case LOGICOP:{ + res = encodeBooleanLogic((BooleanLogic *) constraint); + break; + } + case PREDICATEOP:{ + res = encodePredicate((BooleanPredicate *) constraint); + break; + } + case BOOLEANVAR:{ + res = encodeBooleanVar( (BooleanVar *) constraint); + break; + } + default: + ASSERT(0); + } + if(c.isNegated()){ + return negateConstraint(res); + } + return res; +} + +string Interpreter::encodePredicate( BooleanPredicate *bp){ + switch (bp->predicate->type) { + case TABLEPRED: + ASSERT(0); + case OPERATORPRED: + return encodeOperatorPredicate(bp); + default: + ASSERT(0); + } +} + +string Interpreter::encodeOperatorPredicate(BooleanPredicate *constraint){ + PredicateOperator *predicate = (PredicateOperator *) constraint->predicate; + ASSERT(constraint->inputs.getSize() == 2); + string str; + Element *elem0 = constraint->inputs.get(0); + ASSERT(elem0->type == ELEMSET || elem0->type == ELEMFUNCRETURN || elem0->type == ELEMCONST); + ElementSig *elemSig1 = sigEnc.getElementSignature(elem0); + if(elem0->type == ELEMFUNCRETURN){ + str += processElementFunction((ElementFunction *) elem0, elemSig1); + } + Element *elem1 = constraint->inputs.get(1); + ASSERT(elem1->type == ELEMSET || elem1->type == ELEMFUNCRETURN || elem1->type == ELEMCONST); + ElementSig *elemSig2 = sigEnc.getElementSignature(elem1); + if(elem1->type == ELEMFUNCRETURN){ + str += processElementFunction((ElementFunction *) elem1, elemSig2); + } + str += operatorPredicateConstraint(predicate->getOp(), elemSig1, elemSig2); + return str; +} + +void Interpreter::writeToFile(string str){ + output << str << endl; +} + +bool Interpreter::getBooleanValue(Boolean *b){ + return (bool)sigEnc.getValue(b); +} + +uint64_t Interpreter::getValue(Element * element){ + return (uint64_t)sigEnc.getValue(element); +} + diff --git a/src/Interpreter/interpreter.h b/src/Interpreter/interpreter.h new file mode 100644 index 0000000..814511b --- /dev/null +++ b/src/Interpreter/interpreter.h @@ -0,0 +1,39 @@ +#ifndef INTERPRETER_H +#define INTERPRETER_H + +#include "classlist.h" +#include "signatureenc.h" +#include +#include +using namespace std; + +class Interpreter{ +public: + Interpreter(CSolver *solver); + void encode(); + int solve(); + void writeToFile(string str); + uint64_t getValue(Element *element); + bool getBooleanValue(Boolean *element); + virtual ~Interpreter(); +protected: + virtual void dumpFooter() = 0; + virtual void dumpHeader() = 0; + uint getTimeout(); + virtual void compileRunCommand(char * command, size_t size) = 0; + string encodeConstraint(BooleanEdge constraint); + virtual int getResult() = 0; + virtual string negateConstraint(string constr) = 0; + virtual void dumpAllConstraints(Vector &facts) = 0; + virtual string encodeBooleanLogic( BooleanLogic *bl) = 0; + virtual string encodeBooleanVar( BooleanVar *bv) = 0; + string encodePredicate( BooleanPredicate *bp); + string encodeOperatorPredicate(BooleanPredicate *constraint); + virtual string processElementFunction(ElementFunction *element, ElementSig *signature) = 0; + virtual string operatorPredicateConstraint(CompOp op, ElementSig *elemSig1, ElementSig *elemSig2) = 0; + CSolver *csolver; + SignatureEnc sigEnc; + ofstream output; +}; + +#endif diff --git a/src/Interpreter/signature.cc b/src/Interpreter/signature.cc new file mode 100644 index 0000000..ad7d2e7 --- /dev/null +++ b/src/Interpreter/signature.cc @@ -0,0 +1,123 @@ +#include "signature.h" +#include "set.h" + +bool BooleanSig::encodeAbs = true; +bool SetSig::encodeAbs = true; +bool ElementSig::encodeAbs = true; + +ValuedSignature::ValuedSignature(uint id): + Signature(id), + value(-1) +{ +} + +int ValuedSignature::getValue(){ + ASSERT(value != -1); + return value; +} + +BooleanSig::BooleanSig(uint id): + ValuedSignature(id) +{ +} + +string BooleanSig::toString() const{ + return "Boolean" + to_string(id) + ".value"; +} + +string BooleanSig::getSignature() const{ + string str; + 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 BooleanSet extends AbsSet {}{\n\ + domain = 0 + 1 \n\ + }\n\ + abstract sig AbsBool {\ + value: Int\ + }{\n\ + value in BooleanSet.domain\n\ + }\n"; + return str; +} + +ElementSig::ElementSig(uint id, SetSig *_ssig): + ValuedSignature(id), + ssig(_ssig) +{ +} + +string ElementSig::toString() const{ + return "Element" + to_string(id) + ".value"; +} + +string ElementSig::getSignature() const{ + 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"; + +} + +SetSig::SetSig(uint id, Set *set): Signature(id){ + ASSERT(set->getSize() > 0); + domain = to_string(set->getElement(0)); + for(uint i=1; i< set->getSize(); i++){ + domain += " + " + to_string(set->getElement(i)); + } +} + +string SetSig::toString() const{ + return "Set" + to_string(id) + ".domain"; +} + +string SetSig::getSignature() const{ + 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"; + +} + +string Signature::operator+(const string& str){ + return toString() + str; +} + +string operator+(const string& str, const Signature& sig){ + return str + sig.toString(); +} diff --git a/src/Interpreter/signature.h b/src/Interpreter/signature.h new file mode 100644 index 0000000..1b321a6 --- /dev/null +++ b/src/Interpreter/signature.h @@ -0,0 +1,66 @@ +#ifndef ELEMENTSIG_H +#define ELEMENTSIG_H +#include +#include +#include "classlist.h" +using namespace std; + +class Signature{ +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: + uint id; +}; + +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); + virtual ~BooleanSig(){} + virtual string toString() const; + virtual string getAbsSignature() const; + virtual string getSignature() const; +private: + static bool encodeAbs; +}; + +class SetSig: public Signature{ +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; +}; + +class ElementSig: public ValuedSignature{ +public: + ElementSig(uint id, SetSig *ssig); + virtual ~ElementSig(){} + virtual string toString() const; + virtual string getAbsSignature() const; + virtual string getSignature() const; +private: + SetSig *ssig; + static bool encodeAbs; +}; + +string operator+(const string& str, const Signature& sig); + +#endif diff --git a/src/Interpreter/signatureenc.cc b/src/Interpreter/signatureenc.cc new file mode 100644 index 0000000..888efe2 --- /dev/null +++ b/src/Interpreter/signatureenc.cc @@ -0,0 +1,76 @@ +#include "signatureenc.h" +#include "element.h" +#include "set.h" +#include "signature.h" +#include "alloyenc.h" +#include "math.h" + +SignatureEnc::SignatureEnc(Interpreter *inter): + interpreter(inter), + maxValue(0) +{ +} + +SignatureEnc::~SignatureEnc(){ + for(uint i=0; igetSize(); i++){ + if(set->getElement(i) > maxValue){ + maxValue = set->getElement(i); + } + } +} + +BooleanSig *SignatureEnc::getBooleanSignature(Boolean *bvar){ + BooleanSig *bsig = (BooleanSig *)encoded.get((void *)bvar); + if(bsig == NULL){ + bsig = new BooleanSig(getUniqueSigID()); + encoded.put(bvar, bsig); + signatures.push(bsig); + interpreter->writeToFile(bsig->getSignature()); + } + return bsig; +} + +ElementSig *SignatureEnc::getElementSignature(Element *element){ + ElementSig *esig = (ElementSig *)encoded.get((void *)element); + if(esig == NULL){ + Set *set = element->getRange(); + SetSig *ssig = (SetSig *)encoded.get((void *)set); + if(ssig == NULL){ + ssig = new SetSig(getUniqueSigID(), set); + encoded.put(set, ssig); + signatures.push(ssig); + interpreter->writeToFile(ssig->getSignature()); + updateMaxValue(set); + } + esig = new ElementSig(getUniqueSigID(), ssig); + encoded.put(element, esig); + signatures.push(esig); + interpreter->writeToFile(esig->getSignature()); + + } + return esig; +} + +void SignatureEnc::setValue(uint id, uint value){ + ValuedSignature *sig = getValuedSignature(id); + ASSERT(sig != NULL); + sig->setValue(value); +} + +int SignatureEnc::getValue(void *astnode){ + ValuedSignature *sig = (ValuedSignature *)encoded.get(astnode); + ASSERT(sig != NULL); + return sig->getValue(); +} diff --git a/src/Interpreter/signatureenc.h b/src/Interpreter/signatureenc.h new file mode 100644 index 0000000..b195d03 --- /dev/null +++ b/src/Interpreter/signatureenc.h @@ -0,0 +1,26 @@ +#ifndef SIGNATUREENC_H +#define SIGNATUREENC_H + +#include "classlist.h" +#include "structs.h" +#include "cppvector.h" + +class SignatureEnc { +public: + SignatureEnc(Interpreter *_alloyEncoder); + ~SignatureEnc(); + void setValue(uint id, uint value); + ElementSig *getElementSignature(Element *element); + BooleanSig *getBooleanSignature(Boolean *bvar); + int getAlloyIntScope(); + 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; + Interpreter *interpreter; + uint64_t maxValue; +}; +#endif diff --git a/src/Makefile b/src/Makefile index 457ca9a..29627f4 100644 --- a/src/Makefile +++ b/src/Makefile @@ -4,17 +4,17 @@ PHONY += directories MKDIR_P = mkdir -p OBJ_DIR = bin -CPP_SOURCES := $(wildcard *.cc) $(wildcard AST/*.cc) $(wildcard ASTTransform/*.cc) $(wildcard Translator/*.cc) $(wildcard ASTAnalyses/*.cc) $(wildcard ASTAnalyses/Order/*.cc) $(wildcard ASTAnalyses/Encoding/*.cc) $(wildcard ASTAnalyses/Polarity/*.cc) $(wildcard Tuner/*.cc) $(wildcard Collections/*.cc) $(wildcard Backend/*.cc) $(wildcard Encoders/*.cc) $(wildcard Serialize/*.cc) $(wildcard AlloyEnc/*.cc) +CPP_SOURCES := $(wildcard *.cc) $(wildcard AST/*.cc) $(wildcard ASTTransform/*.cc) $(wildcard Translator/*.cc) $(wildcard ASTAnalyses/*.cc) $(wildcard ASTAnalyses/Order/*.cc) $(wildcard ASTAnalyses/Encoding/*.cc) $(wildcard ASTAnalyses/Polarity/*.cc) $(wildcard Tuner/*.cc) $(wildcard Collections/*.cc) $(wildcard Backend/*.cc) $(wildcard Encoders/*.cc) $(wildcard Serialize/*.cc) $(wildcard Interpreter/*.cc) -C_SOURCES := $(wildcard *.c) $(wildcard AST/*.c) $(wildcard ASTTransform/*.c) $(wildcard Translator/*.c) $(wildcard ASTAnalyses/*.c) $(wildcard ASTAnalyses/Order/*.c) $(wildcard ASTAnalyses/Encoding/*.c) $(wildcard ASTAnalyses/Polarity/*.c) $(wildcard Tuner/*.c) $(wildcard Collections/*.c) $(wildcard Backend/*.c) $(wildcard Encoders/*.c) $(wildcard Serialize/*.c) $(wildcard AlloyEnc/*.c) +C_SOURCES := $(wildcard *.c) $(wildcard AST/*.c) $(wildcard ASTTransform/*.c) $(wildcard Translator/*.c) $(wildcard ASTAnalyses/*.c) $(wildcard ASTAnalyses/Order/*.c) $(wildcard ASTAnalyses/Encoding/*.c) $(wildcard ASTAnalyses/Polarity/*.c) $(wildcard Tuner/*.c) $(wildcard Collections/*.c) $(wildcard Backend/*.c) $(wildcard Encoders/*.c) $(wildcard Serialize/*.c) $(wildcard Interpreter/*.c) -HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard ASTTransform/*.h) $(wildcard Translator/*.h) $(wildcard ASTAnalyses/*.h) $(wildcard ASTAnalyses/Order/*.h) $(wildcard ASTAnalyses/Encoding/*.h) $(wildcard ASTAnalyses/Polarity/*.h) $(wildcard Tuner/*.h) $(wildcard Collections/*.h) $(wildcard Backend/*.h) $(wildcard Encoders/*.h) $(wildcard Serialize/*.h) $(wildcard AlloyEnc/*.h) +HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard ASTTransform/*.h) $(wildcard Translator/*.h) $(wildcard ASTAnalyses/*.h) $(wildcard ASTAnalyses/Order/*.h) $(wildcard ASTAnalyses/Encoding/*.h) $(wildcard ASTAnalyses/Polarity/*.h) $(wildcard Tuner/*.h) $(wildcard Collections/*.h) $(wildcard Backend/*.h) $(wildcard Encoders/*.h) $(wildcard Serialize/*.h) $(wildcard Interpreter/*.h) OBJECTS := $(CPP_SOURCES:%.cc=$(OBJ_DIR)/%.o) $(C_SOURCES:%.c=$(OBJ_DIR)/%.o) CFLAGS := -Wall -O0 -g CXXFLAGS := -std=c++1y -pthread -CFLAGS += -IAST -IASTTransform -IASTAnalyses -IASTAnalyses/Polarity -IASTAnalyses/Order -IASTAnalyses/Encoding -ITranslator -ICollections -IBackend -I. -IEncoders -ITuner -ISerialize -IAlloyEnc +CFLAGS += -IAST -IASTTransform -IASTAnalyses -IASTAnalyses/Polarity -IASTAnalyses/Order -IASTAnalyses/Encoding -ITranslator -ICollections -IBackend -I. -IEncoders -ITuner -ISerialize -IInterpreter LDFLAGS := -ldl -lrt -rdynamic -g SHARED := -shared @@ -44,7 +44,7 @@ ${OBJ_DIR}: ${MKDIR_P} ${OBJ_DIR}/Backend ${MKDIR_P} ${OBJ_DIR}/Encoders ${MKDIR_P} ${OBJ_DIR}/Serialize - ${MKDIR_P} ${OBJ_DIR}/AlloyEnc + ${MKDIR_P} ${OBJ_DIR}/Interpreter debug: CFLAGS += -DCONFIG_DEBUG debug: all diff --git a/src/classes.h b/src/classes.h index 6f476ee..5369a05 100644 --- a/src/classes.h +++ b/src/classes.h @@ -28,7 +28,7 @@ class Set; class BooleanLogic; class Serializer; class ElementFunction; -class AlloyEnc; +class Interpreter; typedef uint64_t VarType; typedef unsigned int uint; diff --git a/src/csolver.cc b/src/csolver.cc index c81e2f3..14f902b 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -39,7 +39,7 @@ CSolver::CSolver() : tuner(NULL), elapsedTime(0), satsolverTimeout(NOTIMEOUT), - alloyEncoder(NULL) + interpreter(NULL) { satEncoder = new SATEncoder(this); } @@ -82,6 +82,10 @@ CSolver::~CSolver() { for (uint i = 0; i < size; i++) { delete allFunctions.get(i); } + + if(interpreter != NULL){ + delete interpreter; + } delete boolTrue.getBoolean(); delete satEncoder; @@ -606,9 +610,9 @@ int CSolver::solve() { } int result = IS_INDETER; if(useAlloyCompiler()){ - alloyEncoder->encode(); + interpreter->encode(); model_print("Problem encoded in Alloy\n"); - result = alloyEncoder->solve(); + result = interpreter->solve(); model_print("Problem solved by Alloy\n"); } else{ @@ -676,8 +680,8 @@ int CSolver::solve() { } void CSolver::setAlloyEncoder(){ - if(alloyEncoder == NULL){ - alloyEncoder = new AlloyEnc(this); + if(interpreter == NULL){ + interpreter = new AlloyEnc(this); } } @@ -699,7 +703,7 @@ uint64_t CSolver::getElementValue(Element *element) { case ELEMSET: case ELEMCONST: case ELEMFUNCRETURN: - return useAlloyCompiler()? alloyEncoder->getValue(element): + return useAlloyCompiler()? interpreter->getValue(element): getElementValueSATTranslator(this, element); default: ASSERT(0); @@ -711,7 +715,7 @@ bool CSolver::getBooleanValue(BooleanEdge bedge) { Boolean *boolean = bedge.getBoolean(); switch (boolean->type) { case BOOLEANVAR: - return useAlloyCompiler()? alloyEncoder->getBooleanValue(boolean): + return useAlloyCompiler()? interpreter->getBooleanValue(boolean): getBooleanVariableValueSATTranslator(this, boolean); default: ASSERT(0); diff --git a/src/csolver.h b/src/csolver.h index 6fea9ee..7da50c5 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -166,7 +166,7 @@ public: void inferFixedOrders(); void inferFixedOrder(Order *order); void setAlloyEncoder(); - bool useAlloyCompiler() {return alloyEncoder != NULL;} + bool useAlloyCompiler() {return interpreter != NULL;} void setTuner(Tuner *_tuner) { tuner = _tuner; } long long getElapsedTime() { return elapsedTime; } long long getEncodeTime(); @@ -223,7 +223,7 @@ private: Tuner *tuner; long long elapsedTime; long satsolverTimeout; - AlloyEnc *alloyEncoder; + Interpreter *interpreter; friend class ElementOpt; friend class VarOrderingOpt; };