src/Interpreter/alloyinterpreter.cc

   1 #include "alloyinterpreter.h"
   2 #include <string>
   3 #include "signatureenc.h"
   4 #include "structs.h"
   5 #include "csolver.h"
   6 #include "boolean.h"
   7 #include "predicate.h"
   8 #include "element.h"
   9 #include "signature.h"
  10 #include "set.h"
  11 #include "function.h"
  12 #include "inc_solver.h"
  13 #include <fstream>
  14 #include "cppvector.h"
  15
  16 using namespace std;
  17
  18 #define ALLOYFILENAME "satune.als"
  19 #define ALLOYSOLUTIONFILE "solution.sol"
  20
  21 AlloyInterpreter::AlloyInterpreter(CSolver *_solver):
  22         Interpreter(_solver)
  23 {
  24         output.open(ALLOYFILENAME);
  25         if(!output.is_open()){
  26                 model_print("AlloyEnc:Error in opening the dump file satune.als\n");
  27                 exit(-1);
  28         }
  29 }
  30
  31 AlloyInterpreter::~AlloyInterpreter(){
  32         if(output.is_open()){
  33                 output.close();
  34         }
  35 }
  36
  37 void AlloyInterpreter::dumpAllConstraints(Vector<char *> &facts){
  38         output << "fact {" << endl;
  39         for(uint i=0; i< facts.getSize(); i++){
  40                 char *cstr = facts.get(i);
  41                 writeToFile(cstr);
  42         }
  43         output << "}" << endl;
  44 }
  45
  46
  47 int AlloyInterpreter::getResult(){
  48         ifstream input(ALLOYSOLUTIONFILE, ios::in);
  49         string line;
  50         while(getline(input, line)){
  51                 if(line.find("Unsatisfiable.")== 0){
  52                         return IS_UNSAT;
  53                 }
  54                 if(line.find("univ") == 0){
  55                         continue;
  56                 }
  57                 if(line.find("this/AbsBool<:value") == 0 || line.find("this/AbsElement<:value=") == 0){
  58                         const char delim [2] = ",";
  59                         char cline [line.size()+1];
  60                         strcpy ( cline, line.c_str() );
  61                         char *token = strtok(cline, delim);
  62                         while( token != NULL ) {
  63                                 printf( " %s\n", token );
  64                                 uint i1, i2, i3;
  65                                 if (3 == sscanf(token,"%*[^0123456789]%u%*[^0123456789]%d%*[^0123456789]%u", &i1, &i2, &i3)){
  66                                         model_print("Signature%u = %u\n", i1, i3);
  67                                         sigEnc.setValue(i1, i3);
  68                                 }
  69                                 token = strtok(NULL, delim);
  70                         }
  71                 }
  72         }
  73         return IS_SAT;
  74 }
  75
  76 void AlloyInterpreter::dumpFooter(){
  77         output << "pred show {}" << endl;
  78         output << "run show for " << sigEnc.getAlloyIntScope() << " int" << endl;
  79 }
  80
  81 void AlloyInterpreter::dumpHeader(){
  82         output << "open util/integer" << endl;
  83 }
  84
  85 void AlloyInterpreter::compileRunCommand(char * command, size_t size){
  86         snprintf(command, size, "./run.sh timeout %u java -Xmx10000m edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", getTimeout(), ALLOYFILENAME, ALLOYSOLUTIONFILE);
  87 }
  88
  89 string AlloyInterpreter::negateConstraint(string constr){
  90         return "not ( " + constr + " )";
  91 }
  92
  93 string AlloyInterpreter::encodeBooleanLogic( BooleanLogic *bl){
  94         uint size = bl->inputs.getSize();
  95         string array[size];
  96         for (uint i = 0; i < size; i++)
  97                 array[i] = encodeConstraint(bl->inputs.get(i));
  98         string op;
  99         switch (bl->op){
 100                 case SATC_OR:
 101                         op = " or ";
 102                         break;
 103                 case SATC_AND:
 104                         op = " and ";
 105                         break;
 106                 case SATC_NOT:
 107                         op = " not ";
 108                         break;
 109                 case SATC_IFF:
 110                         op = " iff ";
 111                         break;
 112                 case SATC_IMPLIES:
 113                         op = " implies ";
 114                         break;
 115                 case SATC_XOR:
 116                 default:
 117                         ASSERT(0);
 118         }
 119         switch (bl->op) {
 120                 case SATC_OR:
 121                 case SATC_AND:{
 122                         ASSERT(size >= 2);
 123                         string res = "( ";
 124                         res += array[0];
 125                         for( uint i=1; i< size; i++){
 126                                 res += op + array[i];
 127                         }
 128                         res += " )";
 129                         return res;
 130                 }
 131                 case SATC_NOT:{
 132                         return "not ( " + array[0] + " )";
 133                 }
 134                 case SATC_IMPLIES:
 135                 case SATC_IFF:
 136                         return "( " + array[0] + op + array[1] + " )";
 137                 case SATC_XOR:
 138                 default:
 139                         ASSERT(0);
 140
 141         }
 142 }
 143
 144 string AlloyInterpreter::encodeBooleanVar( BooleanVar *bv){
 145         BooleanSig * boolSig = sigEnc.getBooleanSignature(bv);
 146         return *boolSig + " = 1";
 147 }
 148
 149 string AlloyInterpreter::processElementFunction(ElementFunction* elemFunc, ElementSig *signature){
 150         FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
 151         uint numDomains = elemFunc->inputs.getSize();
 152         ASSERT(numDomains > 1);
 153         ElementSig *inputs[numDomains];
 154         string result;
 155         for (uint i = 0; i < numDomains; i++) {
 156                 Element *elem = elemFunc->inputs.get(i);
 157                 inputs[i] = sigEnc.getElementSignature(elem);
 158                 if(elem->type == ELEMFUNCRETURN){
 159                         result += processElementFunction((ElementFunction *) elem, inputs[i]);
 160                 }
 161         }
 162         string op;
 163         switch(function->op){
 164                 case SATC_ADD:
 165                         op = ".add";
 166                         break;
 167                 case SATC_SUB:
 168                         op = ".sub";
 169                         break;
 170                 default:
 171                         ASSERT(0);
 172         }
 173         result += *signature + " = " + *inputs[0];
 174         for (uint i = 1; i < numDomains; i++) {
 175                 result += op + "["+ *inputs[i] +"]";
 176         }
 177         result += "\n";
 178         return result;
 179 }
 180
 181 string AlloyInterpreter::operatorPredicateConstraint(CompOp op, ElementSig *elemSig1, ElementSig *elemSig2){
 182         switch (op) {
 183                 case SATC_EQUALS:
 184                         return *elemSig1 + " = " + *elemSig2;
 185                 case SATC_LT:
 186                         return *elemSig1 + " < " + *elemSig2;
 187                 case SATC_GT:
 188                         return *elemSig1 + " > " + *elemSig2;
 189                 default:
 190                         ASSERT(0);
 191         }
 192 }
 193
 194