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