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