Interpreter abstraction and memory bug fixes
authorHamed Gorjiara <hgorjiar@uci.edu>
Tue, 19 Feb 2019 20:11:31 +0000 (12:11 -0800)
committerHamed Gorjiara <hgorjiar@uci.edu>
Tue, 19 Feb 2019 20:11:31 +0000 (12:11 -0800)
18 files changed:
src/AlloyEnc/alloyenc.cc [deleted file]
src/AlloyEnc/alloyenc.h [deleted file]
src/AlloyEnc/signature.cc [deleted file]
src/AlloyEnc/signature.h [deleted file]
src/AlloyEnc/signatureenc.cc [deleted file]
src/AlloyEnc/signatureenc.h [deleted file]
src/Interpreter/alloyenc.cc [new file with mode: 0644]
src/Interpreter/alloyenc.h [new file with mode: 0644]
src/Interpreter/interpreter.cc [new file with mode: 0644]
src/Interpreter/interpreter.h [new file with mode: 0644]
src/Interpreter/signature.cc [new file with mode: 0644]
src/Interpreter/signature.h [new file with mode: 0644]
src/Interpreter/signatureenc.cc [new file with mode: 0644]
src/Interpreter/signatureenc.h [new file with mode: 0644]
src/Makefile
src/classes.h
src/csolver.cc
src/csolver.h

diff --git a/src/AlloyEnc/alloyenc.cc b/src/AlloyEnc/alloyenc.cc
deleted file mode 100644 (file)
index cad0529..0000000
+++ /dev/null
@@ -1,294 +0,0 @@
-#include "alloyenc.h"
-#include <string>
-#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 <fstream>
-#include <vector>
-
-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<char *> 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<std::string> &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<string> values;
-                       const char delim = ',';
-                       tokenize(line, delim, values);
-                       for (uint i=0; i<values.size(); i++){
-                               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);
-                               }
-                       }
-               }
-       }
-       return IS_SAT;
-}
-
-void AlloyEnc::dumpAlloyFooter(){
-       output << "pred show {}" << endl;
-       output << "run show for " << sigEnc.getAlloyIntScope() << " int" << endl;
-}
-
-uint AlloyEnc::getTimeout(){
-       uint timeout =csolver->getSatSolverTimeout(); 
-       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 (file)
index 3edfdbf..0000000
+++ /dev/null
@@ -1,37 +0,0 @@
-#ifndef ALLOYENC_H
-#define ALLOYENC_H
-
-#include "classlist.h"
-#include "signatureenc.h"
-#include <iostream>
-#include <fstream>
-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 (file)
index ad7d2e7..0000000
+++ /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 (file)
index 1b321a6..0000000
+++ /dev/null
@@ -1,66 +0,0 @@
-#ifndef ELEMENTSIG_H
-#define ELEMENTSIG_H
-#include <string>
-#include <iostream>
-#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 (file)
index 92fb03f..0000000
+++ /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; i<signatures.getSize(); i++){
-               Signature *s = signatures.get(i);
-               delete s;
-       }
-}
-
-int SignatureEnc::getAlloyIntScope(){
-       double mylog = log2(maxValue + 1);
-       return floor(mylog) == mylog ? (int)mylog + 1: (int)mylog + 2;
-}
-
-void SignatureEnc::updateMaxValue(Set *set){
-       for(uint i=0; i< set->getSize(); 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 (file)
index 636c2b3..0000000
+++ /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<Signature*> signatures;
-       AlloyEnc *alloyEncoder;
-       uint64_t maxValue;
-};
-#endif
diff --git a/src/Interpreter/alloyenc.cc b/src/Interpreter/alloyenc.cc
new file mode 100644 (file)
index 0000000..66e0ef5
--- /dev/null
@@ -0,0 +1,194 @@
+#include "alloyenc.h"
+#include <string>
+#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 <fstream>
+#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<char *> &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 (file)
index 0000000..f3e0f1b
--- /dev/null
@@ -0,0 +1,28 @@
+#ifndef ALLOYENC_H
+#define ALLOYENC_H
+
+#include "classlist.h"
+#include "signatureenc.h"
+#include "interpreter.h"
+#include <iostream>
+#include <fstream>
+
+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<char *> &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 (file)
index 0000000..bab92b4
--- /dev/null
@@ -0,0 +1,133 @@
+#include "interpreter.h"
+#include <string>
+#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 <fstream>
+
+using namespace std;
+
+Interpreter::Interpreter(CSolver *_solver): 
+       csolver(_solver),
+       sigEnc(this)
+{
+}
+
+Interpreter::~Interpreter(){
+}
+
+void Interpreter::encode(){
+       dumpHeader();
+       SetIteratorBooleanEdge *iterator = csolver->getConstraints();
+       Vector<char *> 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 (file)
index 0000000..814511b
--- /dev/null
@@ -0,0 +1,39 @@
+#ifndef INTERPRETER_H
+#define INTERPRETER_H
+
+#include "classlist.h"
+#include "signatureenc.h"
+#include <iostream>
+#include <fstream>
+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<char *> &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 (file)
index 0000000..ad7d2e7
--- /dev/null
@@ -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 (file)
index 0000000..1b321a6
--- /dev/null
@@ -0,0 +1,66 @@
+#ifndef ELEMENTSIG_H
+#define ELEMENTSIG_H
+#include <string>
+#include <iostream>
+#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 (file)
index 0000000..888efe2
--- /dev/null
@@ -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; i<signatures.getSize(); i++){
+               Signature *s = signatures.get(i);
+               delete s;
+       }
+}
+
+int SignatureEnc::getAlloyIntScope(){
+       double mylog = log2(maxValue + 1);
+       return floor(mylog) == mylog ? (int)mylog + 1: (int)mylog + 2;
+}
+
+void SignatureEnc::updateMaxValue(Set *set){
+       for(uint i=0; i< set->getSize(); 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 (file)
index 0000000..b195d03
--- /dev/null
@@ -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<Signature*> signatures;
+       Interpreter *interpreter;
+       uint64_t maxValue;
+};
+#endif
index 457ca9a..29627f4 100644 (file)
@@ -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
index 6f476ee..5369a05 100644 (file)
@@ -28,7 +28,7 @@ class Set;
 class BooleanLogic;
 class Serializer;
 class ElementFunction;
-class AlloyEnc;
+class Interpreter;
 
 typedef uint64_t VarType;
 typedef unsigned int uint;
index c81e2f3..14f902b 100644 (file)
@@ -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);
index 6fea9ee..7da50c5 100644 (file)
@@ -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;
 };