renaming alloyenc to alloy interpreter
authorHamed Gorjiara <hgorjiar@uci.edu>
Tue, 19 Feb 2019 20:27:43 +0000 (12:27 -0800)
committerHamed Gorjiara <hgorjiar@uci.edu>
Tue, 19 Feb 2019 20:27:43 +0000 (12:27 -0800)
src/Interpreter/alloyenc.cc [deleted file]
src/Interpreter/alloyenc.h [deleted file]
src/Interpreter/alloyinterpreter.cc [new file with mode: 0644]
src/Interpreter/alloyinterpreter.h [new file with mode: 0644]
src/Interpreter/signatureenc.cc
src/csolver.cc

diff --git a/src/Interpreter/alloyenc.cc b/src/Interpreter/alloyenc.cc
deleted file mode 100644 (file)
index 66e0ef5..0000000
+++ /dev/null
@@ -1,194 +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 "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
deleted file mode 100644 (file)
index f3e0f1b..0000000
+++ /dev/null
@@ -1,28 +0,0 @@
-#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/alloyinterpreter.cc b/src/Interpreter/alloyinterpreter.cc
new file mode 100644 (file)
index 0000000..f910ac6
--- /dev/null
@@ -0,0 +1,194 @@
+#include "alloyinterpreter.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 ALLOYSOLUTIONFILE "solution.sol"
+
+AlloyInterpreter::AlloyInterpreter(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);
+       }
+}
+
+AlloyInterpreter::~AlloyInterpreter(){
+       if(output.is_open()){
+               output.close();
+       }
+}
+
+void AlloyInterpreter::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 AlloyInterpreter::getResult(){
+       ifstream input(ALLOYSOLUTIONFILE, 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 AlloyInterpreter::dumpFooter(){
+       output << "pred show {}" << endl;
+       output << "run show for " << sigEnc.getAlloyIntScope() << " int" << endl;
+}
+
+void AlloyInterpreter::dumpHeader(){
+       output << "open util/integer" << endl;
+}
+
+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 AlloyInterpreter::negateConstraint(string constr){
+       return "not ( " + constr + " )";
+}
+
+string AlloyInterpreter::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 AlloyInterpreter::encodeBooleanVar( BooleanVar *bv){
+       BooleanSig * boolSig = sigEnc.getBooleanSignature(bv);
+       return *boolSig + " = 1";
+}
+
+string AlloyInterpreter::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 AlloyInterpreter::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/alloyinterpreter.h b/src/Interpreter/alloyinterpreter.h
new file mode 100644 (file)
index 0000000..ec2e4a3
--- /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 AlloyInterpreter: public Interpreter{
+public:
+       AlloyInterpreter(CSolver *solver);
+       virtual ~AlloyInterpreter();
+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
index 888efe2..5e0a900 100644 (file)
@@ -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): 
index 14f902b..fd44646 100644 (file)
@@ -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);
        }
 }