From 3267d387309bb4d2aa130a940f386b419652a956 Mon Sep 17 00:00:00 2001 From: Hamed Gorjiara Date: Tue, 19 Feb 2019 12:11:31 -0800 Subject: [PATCH 1/1] Interpreter abstraction and memory bug fixes --- src/AlloyEnc/alloyenc.cc | 294 ------------------ src/AlloyEnc/alloyenc.h | 37 --- src/Interpreter/alloyenc.cc | 194 ++++++++++++ src/Interpreter/alloyenc.h | 28 ++ src/Interpreter/interpreter.cc | 133 ++++++++ src/Interpreter/interpreter.h | 39 +++ src/{AlloyEnc => Interpreter}/signature.cc | 0 src/{AlloyEnc => Interpreter}/signature.h | 0 src/{AlloyEnc => Interpreter}/signatureenc.cc | 10 +- src/{AlloyEnc => Interpreter}/signatureenc.h | 4 +- src/Makefile | 10 +- src/classes.h | 2 +- src/csolver.cc | 18 +- src/csolver.h | 4 +- 14 files changed, 420 insertions(+), 353 deletions(-) delete mode 100644 src/AlloyEnc/alloyenc.cc delete mode 100644 src/AlloyEnc/alloyenc.h create mode 100644 src/Interpreter/alloyenc.cc create mode 100644 src/Interpreter/alloyenc.h create mode 100644 src/Interpreter/interpreter.cc create mode 100644 src/Interpreter/interpreter.h rename src/{AlloyEnc => Interpreter}/signature.cc (100%) rename src/{AlloyEnc => Interpreter}/signature.h (100%) rename src/{AlloyEnc => Interpreter}/signatureenc.cc (88%) rename src/{AlloyEnc => Interpreter}/signatureenc.h (90%) 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/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/AlloyEnc/signature.cc b/src/Interpreter/signature.cc similarity index 100% rename from src/AlloyEnc/signature.cc rename to src/Interpreter/signature.cc diff --git a/src/AlloyEnc/signature.h b/src/Interpreter/signature.h similarity index 100% rename from src/AlloyEnc/signature.h rename to src/Interpreter/signature.h diff --git a/src/AlloyEnc/signatureenc.cc b/src/Interpreter/signatureenc.cc similarity index 88% rename from src/AlloyEnc/signatureenc.cc rename to src/Interpreter/signatureenc.cc index 92fb03f..888efe2 100644 --- a/src/AlloyEnc/signatureenc.cc +++ b/src/Interpreter/signatureenc.cc @@ -5,8 +5,8 @@ #include "alloyenc.h" #include "math.h" -SignatureEnc::SignatureEnc(AlloyEnc *ae): - alloyEncoder(ae), +SignatureEnc::SignatureEnc(Interpreter *inter): + interpreter(inter), maxValue(0) { } @@ -37,7 +37,7 @@ BooleanSig *SignatureEnc::getBooleanSignature(Boolean *bvar){ bsig = new BooleanSig(getUniqueSigID()); encoded.put(bvar, bsig); signatures.push(bsig); - alloyEncoder->writeToFile(bsig->getSignature()); + interpreter->writeToFile(bsig->getSignature()); } return bsig; } @@ -51,13 +51,13 @@ ElementSig *SignatureEnc::getElementSignature(Element *element){ ssig = new SetSig(getUniqueSigID(), set); encoded.put(set, ssig); signatures.push(ssig); - alloyEncoder->writeToFile(ssig->getSignature()); + interpreter->writeToFile(ssig->getSignature()); updateMaxValue(set); } esig = new ElementSig(getUniqueSigID(), ssig); encoded.put(element, esig); signatures.push(esig); - alloyEncoder->writeToFile(esig->getSignature()); + interpreter->writeToFile(esig->getSignature()); } return esig; diff --git a/src/AlloyEnc/signatureenc.h b/src/Interpreter/signatureenc.h similarity index 90% rename from src/AlloyEnc/signatureenc.h rename to src/Interpreter/signatureenc.h index 636c2b3..b195d03 100644 --- a/src/AlloyEnc/signatureenc.h +++ b/src/Interpreter/signatureenc.h @@ -7,7 +7,7 @@ class SignatureEnc { public: - SignatureEnc(AlloyEnc *_alloyEncoder); + SignatureEnc(Interpreter *_alloyEncoder); ~SignatureEnc(); void setValue(uint id, uint value); ElementSig *getElementSignature(Element *element); @@ -20,7 +20,7 @@ private: void updateMaxValue(Set *set); CloneMap encoded; Vector signatures; - AlloyEnc *alloyEncoder; + 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; }; -- 2.34.1