From 917bc08fb2d0ea78f6492323d52a4465b517809a Mon Sep 17 00:00:00 2001
From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Tue, 19 Feb 2019 12:27:43 -0800
Subject: [PATCH] renaming alloyenc to alloy interpreter

---
 .../{alloyenc.cc => alloyinterpreter.cc}      | 36 +++++++++----------
 .../{alloyenc.h => alloyinterpreter.h}        |  6 ++--
 src/Interpreter/signatureenc.cc               |  2 +-
 src/csolver.cc                                |  4 +--
 4 files changed, 24 insertions(+), 24 deletions(-)
 rename src/Interpreter/{alloyenc.cc => alloyinterpreter.cc} (78%)
 rename src/Interpreter/{alloyenc.h => alloyinterpreter.h} (87%)

diff --git a/src/Interpreter/alloyenc.cc b/src/Interpreter/alloyinterpreter.cc
similarity index 78%
rename from src/Interpreter/alloyenc.cc
rename to src/Interpreter/alloyinterpreter.cc
index 66e0ef5..f910ac6 100644
--- a/src/Interpreter/alloyenc.cc
+++ b/src/Interpreter/alloyinterpreter.cc
@@ -1,4 +1,4 @@
-#include "alloyenc.h"
+#include "alloyinterpreter.h"
 #include <string>
 #include "signatureenc.h"
 #include "structs.h"
@@ -15,26 +15,26 @@
 
 using namespace std;
 
-#define alloyFileName "satune.als"
-#define solutionFile "solution.sol"
+#define ALLOYFILENAME "satune.als"
+#define ALLOYSOLUTIONFILE "solution.sol"
 
-AlloyEnc::AlloyEnc(CSolver *_solver): 
+AlloyInterpreter::AlloyInterpreter(CSolver *_solver): 
 	Interpreter(_solver) 
 {
-	output.open(alloyFileName);
+	output.open(ALLOYFILENAME);
 	if(!output.is_open()){
 		model_print("AlloyEnc:Error in opening the dump file satune.als\n");
 		exit(-1);
 	}
 }
 
-AlloyEnc::~AlloyEnc(){
+AlloyInterpreter::~AlloyInterpreter(){
 	if(output.is_open()){
 		output.close();
 	}
 }
 
-void AlloyEnc::dumpAllConstraints(Vector<char *> &facts){
+void AlloyInterpreter::dumpAllConstraints(Vector<char *> &facts){
 	output << "fact {" << endl;
 	for(uint i=0; i< facts.getSize(); i++){
 		char *cstr = facts.get(i);
@@ -44,8 +44,8 @@ void AlloyEnc::dumpAllConstraints(Vector<char *> &facts){
 }
 
 
-int AlloyEnc::getResult(){
-	ifstream input(solutionFile, ios::in);
+int AlloyInterpreter::getResult(){
+	ifstream input(ALLOYSOLUTIONFILE, ios::in);
 	string line;
 	while(getline(input, line)){
 		if(line.find("Unsatisfiable.")== 0){
@@ -73,24 +73,24 @@ int AlloyEnc::getResult(){
 	return IS_SAT;
 }
 
-void AlloyEnc::dumpFooter(){
+void AlloyInterpreter::dumpFooter(){
 	output << "pred show {}" << endl;
 	output << "run show for " << sigEnc.getAlloyIntScope() << " int" << endl;
 }
 
-void AlloyEnc::dumpHeader(){
+void AlloyInterpreter::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);
+void AlloyInterpreter::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, ALLOYSOLUTIONFILE);
 }
 
-string AlloyEnc::negateConstraint(string constr){
+string AlloyInterpreter::negateConstraint(string constr){
 	return "not ( " + constr + " )";
 }
 
-string AlloyEnc::encodeBooleanLogic( BooleanLogic *bl){
+string AlloyInterpreter::encodeBooleanLogic( BooleanLogic *bl){
 	uint size = bl->inputs.getSize();
 	string array[size];
 	for (uint i = 0; i < size; i++)
@@ -141,12 +141,12 @@ string AlloyEnc::encodeBooleanLogic( BooleanLogic *bl){
 	}
 }
 
-string AlloyEnc::encodeBooleanVar( BooleanVar *bv){
+string AlloyInterpreter::encodeBooleanVar( BooleanVar *bv){
 	BooleanSig * boolSig = sigEnc.getBooleanSignature(bv);
 	return *boolSig + " = 1";
 }
 
-string AlloyEnc::processElementFunction(ElementFunction* elemFunc, ElementSig *signature){
+string AlloyInterpreter::processElementFunction(ElementFunction* elemFunc, ElementSig *signature){
 	FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
 	uint numDomains = elemFunc->inputs.getSize();
 	ASSERT(numDomains > 1);
@@ -178,7 +178,7 @@ string AlloyEnc::processElementFunction(ElementFunction* elemFunc, ElementSig *s
 	return result;
 }
 
-string AlloyEnc::operatorPredicateConstraint(CompOp op, ElementSig *elemSig1, ElementSig *elemSig2){
+string AlloyInterpreter::operatorPredicateConstraint(CompOp op, ElementSig *elemSig1, ElementSig *elemSig2){
 	switch (op) {
 		case SATC_EQUALS:
 			return *elemSig1 + " = " + *elemSig2;
diff --git a/src/Interpreter/alloyenc.h b/src/Interpreter/alloyinterpreter.h
similarity index 87%
rename from src/Interpreter/alloyenc.h
rename to src/Interpreter/alloyinterpreter.h
index f3e0f1b..ec2e4a3 100644
--- a/src/Interpreter/alloyenc.h
+++ b/src/Interpreter/alloyinterpreter.h
@@ -7,10 +7,10 @@
 #include <iostream>
 #include <fstream>
 
-class AlloyEnc: public Interpreter{
+class AlloyInterpreter: public Interpreter{
 public:
-	AlloyEnc(CSolver *solver);
-	virtual ~AlloyEnc();
+	AlloyInterpreter(CSolver *solver);
+	virtual ~AlloyInterpreter();
 protected:
 	virtual void dumpFooter();
 	virtual void dumpHeader();
diff --git a/src/Interpreter/signatureenc.cc b/src/Interpreter/signatureenc.cc
index 888efe2..5e0a900 100644
--- a/src/Interpreter/signatureenc.cc
+++ b/src/Interpreter/signatureenc.cc
@@ -2,7 +2,7 @@
 #include "element.h"
 #include "set.h"
 #include "signature.h"
-#include "alloyenc.h"
+#include "alloyinterpreter.h"
 #include "math.h"
 
 SignatureEnc::SignatureEnc(Interpreter *inter): 
diff --git a/src/csolver.cc b/src/csolver.cc
index 14f902b..fd44646 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -29,7 +29,7 @@
 #include "varorderingopt.h"
 #include <time.h>
 #include <stdarg.h>
-#include "alloyenc.h"
+#include "alloyinterpreter.h"
 
 CSolver::CSolver() :
 	boolTrue(BooleanEdge(new BooleanConst(true))),
@@ -681,7 +681,7 @@ int CSolver::solve() {
 
 void CSolver::setAlloyEncoder(){
 	if(interpreter == NULL){
-		interpreter = new AlloyEnc(this);
+		interpreter = new AlloyInterpreter(this);
 	}
 }
 
-- 
2.34.1