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