src/AlloyEnc/alloyenc.cc

   1 #include "alloyenc.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 <fstream>
  13 #include <regex>
  14
  15 using namespace std;
  16
  17 const char * AlloyEnc::alloyFileName = "satune.als";
  18 const char * AlloyEnc::solutionFile = "solution.sol";
  19
  20 AlloyEnc::AlloyEnc(CSolver *_solver):
  21         csolver(_solver),
  22         sigEnc(this)
  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 AlloyEnc::~AlloyEnc(){
  32         if(output.is_open()){
  33                 output.close();
  34         }
  35 }
  36
  37 void AlloyEnc::encode(){
  38         dumpAlloyHeader();
  39         SetIteratorBooleanEdge *iterator = csolver->getConstraints();
  40         Vector<char *> facts;
  41         while(iterator->hasNext()){
  42                 BooleanEdge constraint = iterator->next();
  43                 string constr = encodeConstraint(constraint);
  44                 //model_print("constr=%s\n", constr.c_str());
  45                 char *cstr = new char [constr.length()+1];
  46                 strcpy (cstr, constr.c_str());
  47                 facts.push(cstr);
  48         }
  49         output << "fact {" << endl;
  50         for(uint i=0; i< facts.getSize(); i++){
  51                 char *cstr = facts.get(i);
  52                 writeToFile(cstr);
  53                 delete[] cstr;
  54         }
  55         output << "}" << endl;
  56         delete iterator;
  57 }
  58
  59 int AlloyEnc::getResult(){
  60         ifstream input(solutionFile, ios::in);
  61         string line;
  62         while(getline(input, line)){
  63                 if(regex_match(line, regex("Unsatisfiable."))){
  64                         return IS_UNSAT;
  65                 }
  66                 if(regex_match(line, regex(".*Element\\d+.*value=.*Element\\d+.*->\\d+.*"))){
  67                         int tmp=0, index=0, value=0;
  68                         const char* s = line.c_str();
  69                         uint i1, i2, i3;
  70                         uint64_t i4;
  71                         if (4 == sscanf(s,"%*[^0123456789]%u%*[^0123456789]%d%*[^0123456789]%d%*[^0123456789]%" PRId64 "", &i1, &i2, &i3, &i4)){
  72                                 model_print("Element%d = %" PRId64 "\n", i1, i4);
  73                                 sigEnc.setValue(i1, i4);
  74                         }
  75                 }
  76         }
  77         return IS_SAT;
  78 }
  79
  80 void AlloyEnc::dumpAlloyFooter(){
  81         output << "pred show {}" << endl;
  82         output << "run show for " << sigEnc.getAlloyIntScope() << " int" << endl;
  83 }
  84
  85 void AlloyEnc::dumpAlloyHeader(){
  86         output << "open util/integer" << endl;
  87 }
  88
  89 int AlloyEnc::solve(){
  90         dumpAlloyFooter();
  91         int result = IS_INDETER;
  92         char buffer [512];
  93         if( output.is_open()){
  94                 output.close();
  95         }
  96         snprintf(buffer, sizeof(buffer), "./run.sh java -Xmx10000m edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", alloyFileName, solutionFile);
  97         int status = system(buffer);
  98         if (status == 0) {
  99                 //Read data in from results file
 100                 result = getResult();
 101         }
 102         return result;
 103 }
 104
 105 string AlloyEnc::encodeConstraint(BooleanEdge c){
 106         Boolean *constraint = c.getBoolean();
 107         string res;
 108         switch(constraint->type){
 109                 case LOGICOP:{
 110                         res = encodeBooleanLogic((BooleanLogic *) constraint);
 111                         break;
 112                 }
 113                 case PREDICATEOP:{
 114                         res = encodePredicate((BooleanPredicate *) constraint);
 115                         break;
 116                 }
 117                 case BOOLEANVAR:{
 118                         res = encodeBooleanVar( (BooleanVar *) constraint);
 119                         break;
 120                 }
 121                 default:
 122                         ASSERT(0);
 123         }
 124         if(c.isNegated()){
 125                 return "not ( " + res + " )";
 126         }
 127         return res;
 128 }
 129
 130 string AlloyEnc::encodeBooleanLogic( BooleanLogic *bl){
 131         uint size = bl->inputs.getSize();
 132         string array[size];
 133         for (uint i = 0; i < size; i++)
 134                 array[i] = encodeConstraint(bl->inputs.get(i));
 135         switch (bl->op) {
 136                 case SATC_AND:{
 137                         ASSERT(size >= 2);
 138                         string res = "";
 139                         res += array[0];
 140                         for( uint i=1; i< size; i++){
 141                                 res += " and " + array[i];
 142                         }
 143                         return res;
 144                 }
 145                 case SATC_NOT:{
 146                         return "not " + array[0];
 147                 }
 148                 case SATC_IFF:
 149                         return array[0] + " iff " + array[1];
 150                 case SATC_OR:
 151                 case SATC_XOR:
 152                 case SATC_IMPLIES:
 153                 default:
 154                         ASSERT(0);
 155
 156         }
 157 }
 158
 159 string AlloyEnc::encodePredicate( BooleanPredicate *bp){
 160         switch (bp->predicate->type) {
 161                 case TABLEPRED:
 162                         ASSERT(0);
 163                 case OPERATORPRED:
 164                         return encodeOperatorPredicate(bp);
 165                 default:
 166                         ASSERT(0);
 167         }
 168 }
 169
 170 string AlloyEnc::encodeBooleanVar( BooleanVar *bv){
 171         BooleanSig * boolSig = sigEnc.getBooleanSignature(bv);
 172         return *boolSig + " = 1";
 173 }
 174
 175 string AlloyEnc::processElementFunction(ElementFunction* elemFunc, ElementSig *signature){
 176         FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
 177         uint numDomains = elemFunc->inputs.getSize();
 178         ASSERT(numDomains > 1);
 179         ElementSig *inputs[numDomains];
 180         string result;
 181         for (uint i = 0; i < numDomains; i++) {
 182                 Element *elem = elemFunc->inputs.get(i);
 183                 inputs[i] = sigEnc.getElementSignature(elem);
 184                 if(elem->type == ELEMFUNCRETURN){
 185                         result += processElementFunction((ElementFunction *) elem, inputs[i]);
 186                 }
 187         }
 188         string op;
 189         switch(function->op){
 190                 case SATC_ADD:
 191                         op = ".add";
 192                         break;
 193                 case SATC_SUB:
 194                         op = ".sub";
 195                         break;
 196                 default:
 197                         ASSERT(0);
 198         }
 199         result += *signature + " = " + *inputs[0];
 200         for (uint i = 1; i < numDomains; i++) {
 201                 result += op + "["+ *inputs[i] +"]";
 202         }
 203         result += "\n";
 204         return result;
 205 }
 206
 207 string AlloyEnc::encodeOperatorPredicate(BooleanPredicate *constraint){
 208         constraint->print();
 209         PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
 210         ASSERT(constraint->inputs.getSize() == 2);
 211         string str;
 212         Element *elem0 = constraint->inputs.get(0);
 213         ASSERT(elem0->type == ELEMSET || elem0->type == ELEMFUNCRETURN || elem0->type == ELEMCONST);
 214         ElementSig *elemSig1 = sigEnc.getElementSignature(elem0);
 215         if(elem0->type == ELEMFUNCRETURN){
 216                 str += processElementFunction((ElementFunction *) elem0, elemSig1);
 217         }
 218         Element *elem1 = constraint->inputs.get(1);
 219         ASSERT(elem1->type == ELEMSET || elem1->type == ELEMFUNCRETURN || elem1->type == ELEMCONST);
 220         ElementSig *elemSig2 = sigEnc.getElementSignature(elem1);
 221         if(elem1->type == ELEMFUNCRETURN){
 222                 str += processElementFunction((ElementFunction *) elem1, elemSig2);
 223         }
 224         switch (predicate->getOp()) {
 225                 case SATC_EQUALS:
 226                         str += *elemSig1 + " = " + *elemSig2;
 227                         break;
 228                 case SATC_LT:
 229                         str += *elemSig1 + " < " + *elemSig2;
 230                         break;
 231                 case SATC_GT:
 232                         str += *elemSig1 + " > " + *elemSig2;
 233                         break;
 234                 default:
 235                         ASSERT(0);
 236         }
 237         return str;
 238 }
 239
 240 void AlloyEnc::writeToFile(string str){
 241         output << str << endl;
 242 }
 243
 244 bool AlloyEnc::getBooleanValue(Boolean *b){
 245         if (b->boolVal == BV_MUSTBETRUE)
 246                 return true;
 247         else if (b->boolVal == BV_MUSTBEFALSE)
 248                 return false;
 249         return sigEnc.getBooleanSignature(b);
 250 }
 251
 252 uint64_t AlloyEnc::getValue(Element * element){
 253         ElementEncoding *elemEnc = element->getElementEncoding();
 254         if (elemEnc->numVars == 0)//case when the set has only one item
 255                 return element->getRange()->getElement(0);
 256         return sigEnc.getValue(element);
 257 }
 258