From 3267d387309bb4d2aa130a940f386b419652a956 Mon Sep 17 00:00:00 2001
From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Tue, 19 Feb 2019 12:11:31 -0800
Subject: [PATCH] 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 <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
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 <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/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 <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
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 <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
index 0000000..bab92b4
--- /dev/null
+++ b/src/Interpreter/interpreter.cc
@@ -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
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 <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/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<Signature*> 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