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 void tokenize(string const &str, const char delim, vector<std::string> &out)
  60 {
  61         size_t start;
  62         size_t end = 0;
  63
  64         while ((start = str.find_first_not_of(delim, end)) != string::npos)
  65         {
  66                 end = str.find(delim, start);
  67                 out.push_back(str.substr(start, end - start));
  68         }
  69 }
  70
  71 int AlloyEnc::getResult(){
  72         ifstream input(solutionFile, ios::in);
  73         string line;
  74         while(getline(input, line)){
  75                 if(regex_match(line, regex("Unsatisfiable."))){
  76                         return IS_UNSAT;
  77                 }
  78                 if(regex_match(line, regex(".*Element.*value=.*Element\\d+.*->\\d+.*"))){
  79                         vector<string> values;
  80                         const char delim = ',';
  81                         tokenize(line, delim, values);
  82                         for (uint i=0; i<values.size(); i++){
  83                                 uint i1, i2;
  84                                 uint64_t i3;
  85                                 if (3 == sscanf(values[i].c_str(),"%*[^0123456789]%d%*[^0123456789]%d%*[^0123456789]%" PRId64 "", &i1, &i2, &i3)){
  86                                         model_print("Element%d = %" PRId64 "\n", i1, i3);
  87                                         sigEnc.setValue(i1, i3);
  88                                 }
  89                         }
  90                 }
  91         }
  92         return IS_SAT;
  93 }
  94
  95 void AlloyEnc::dumpAlloyFooter(){
  96         output << "pred show {}" << endl;
  97         output << "run show for " << sigEnc.getAlloyIntScope() << " int" << endl;
  98 }
  99
 100 void AlloyEnc::dumpAlloyHeader(){
 101         output << "open util/integer" << endl;
 102 }
 103
 104 int AlloyEnc::solve(){
 105         dumpAlloyFooter();
 106         int result = IS_INDETER;
 107         char buffer [512];
 108         if( output.is_open()){
 109                 output.close();
 110         }
 111         snprintf(buffer, sizeof(buffer), "./run.sh java -Xmx10000m edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", alloyFileName, solutionFile);
 112         int status = system(buffer);
 113         if (status == 0) {
 114                 //Read data in from results file
 115                 result = getResult();
 116         }
 117         return result;
 118 }
 119
 120 string AlloyEnc::encodeConstraint(BooleanEdge c){
 121         Boolean *constraint = c.getBoolean();
 122         string res;
 123         switch(constraint->type){
 124                 case LOGICOP:{
 125                         res = encodeBooleanLogic((BooleanLogic *) constraint);
 126                         break;
 127                 }
 128                 case PREDICATEOP:{
 129                         res = encodePredicate((BooleanPredicate *) constraint);
 130                         break;
 131                 }
 132                 case BOOLEANVAR:{
 133                         res = encodeBooleanVar( (BooleanVar *) constraint);
 134                         break;
 135                 }
 136                 default:
 137                         ASSERT(0);
 138         }
 139         if(c.isNegated()){
 140                 return "not ( " + res + " )";
 141         }
 142         return res;
 143 }
 144
 145 string AlloyEnc::encodeBooleanLogic( BooleanLogic *bl){
 146         uint size = bl->inputs.getSize();
 147         string array[size];
 148         for (uint i = 0; i < size; i++)
 149                 array[i] = encodeConstraint(bl->inputs.get(i));
 150         switch (bl->op) {
 151                 case SATC_AND:{
 152                         ASSERT(size >= 2);
 153                         string res = "";
 154                         res += array[0];
 155                         for( uint i=1; i< size; i++){
 156                                 res += " and " + array[i];
 157                         }
 158                         return res;
 159                 }
 160                 case SATC_NOT:{
 161                         return "not " + array[0];
 162                 }
 163                 case SATC_IFF:
 164                         return array[0] + " iff " + array[1];
 165                 case SATC_OR:
 166                 case SATC_XOR:
 167                 case SATC_IMPLIES:
 168                 default:
 169                         ASSERT(0);
 170
 171         }
 172 }
 173
 174 string AlloyEnc::encodePredicate( BooleanPredicate *bp){
 175         switch (bp->predicate->type) {
 176                 case TABLEPRED:
 177                         ASSERT(0);
 178                 case OPERATORPRED:
 179                         return encodeOperatorPredicate(bp);
 180                 default:
 181                         ASSERT(0);
 182         }
 183 }
 184
 185 string AlloyEnc::encodeBooleanVar( BooleanVar *bv){
 186         BooleanSig * boolSig = sigEnc.getBooleanSignature(bv);
 187         return *boolSig + " = 1";
 188 }
 189
 190 string AlloyEnc::processElementFunction(ElementFunction* elemFunc, ElementSig *signature){
 191         FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
 192         uint numDomains = elemFunc->inputs.getSize();
 193         ASSERT(numDomains > 1);
 194         ElementSig *inputs[numDomains];
 195         string result;
 196         for (uint i = 0; i < numDomains; i++) {
 197                 Element *elem = elemFunc->inputs.get(i);
 198                 inputs[i] = sigEnc.getElementSignature(elem);
 199                 if(elem->type == ELEMFUNCRETURN){
 200                         result += processElementFunction((ElementFunction *) elem, inputs[i]);
 201                 }
 202         }
 203         string op;
 204         switch(function->op){
 205                 case SATC_ADD:
 206                         op = ".add";
 207                         break;
 208                 case SATC_SUB:
 209                         op = ".sub";
 210                         break;
 211                 default:
 212                         ASSERT(0);
 213         }
 214         result += *signature + " = " + *inputs[0];
 215         for (uint i = 1; i < numDomains; i++) {
 216                 result += op + "["+ *inputs[i] +"]";
 217         }
 218         result += "\n";
 219         return result;
 220 }
 221
 222 string AlloyEnc::encodeOperatorPredicate(BooleanPredicate *constraint){
 223         PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
 224         ASSERT(constraint->inputs.getSize() == 2);
 225         string str;
 226         Element *elem0 = constraint->inputs.get(0);
 227         ASSERT(elem0->type == ELEMSET || elem0->type == ELEMFUNCRETURN || elem0->type == ELEMCONST);
 228         ElementSig *elemSig1 = sigEnc.getElementSignature(elem0);
 229         if(elem0->type == ELEMFUNCRETURN){
 230                 str += processElementFunction((ElementFunction *) elem0, elemSig1);
 231         }
 232         Element *elem1 = constraint->inputs.get(1);
 233         ASSERT(elem1->type == ELEMSET || elem1->type == ELEMFUNCRETURN || elem1->type == ELEMCONST);
 234         ElementSig *elemSig2 = sigEnc.getElementSignature(elem1);
 235         if(elem1->type == ELEMFUNCRETURN){
 236                 str += processElementFunction((ElementFunction *) elem1, elemSig2);
 237         }
 238         switch (predicate->getOp()) {
 239                 case SATC_EQUALS:
 240                         str += *elemSig1 + " = " + *elemSig2;
 241                         break;
 242                 case SATC_LT:
 243                         str += *elemSig1 + " < " + *elemSig2;
 244                         break;
 245                 case SATC_GT:
 246                         str += *elemSig1 + " > " + *elemSig2;
 247                         break;
 248                 default:
 249                         ASSERT(0);
 250         }
 251         return str;
 252 }
 253
 254 void AlloyEnc::writeToFile(string str){
 255         output << str << endl;
 256 }
 257
 258 bool AlloyEnc::getBooleanValue(Boolean *b){
 259         if (b->boolVal == BV_MUSTBETRUE)
 260                 return true;
 261         else if (b->boolVal == BV_MUSTBEFALSE)
 262                 return false;
 263         return sigEnc.getBooleanSignature(b);
 264 }
 265
 266 uint64_t AlloyEnc::getValue(Element * element){
 267         ElementEncoding *elemEnc = element->getElementEncoding();
 268         if (elemEnc->numVars == 0)//case when the set has only one item
 269                 return element->getRange()->getElement(0);
 270         return sigEnc.getValue(element);
 271 }
 272