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 "inc_solver.h"
  13 #include <fstream>
  14 #include <vector>
  15
  16 using namespace std;
  17
  18 const char * AlloyEnc::alloyFileName = "satune.als";
  19 const char * AlloyEnc::solutionFile = "solution.sol";
  20
  21 AlloyEnc::AlloyEnc(CSolver *_solver):
  22         csolver(_solver),
  23         sigEnc(this)
  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 AlloyEnc::~AlloyEnc(){
  33         if(output.is_open()){
  34                 output.close();
  35         }
  36 }
  37
  38 void AlloyEnc::encode(){
  39         dumpAlloyHeader();
  40         SetIteratorBooleanEdge *iterator = csolver->getConstraints();
  41         Vector<char *> facts;
  42         while(iterator->hasNext()){
  43                 BooleanEdge constraint = iterator->next();
  44                 string constr = encodeConstraint(constraint);
  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(line.find("Unsatisfiable.")== 0){
  76                         return IS_UNSAT;
  77                 }
  78                 if(line.find("univ") == 0){
  79                         continue;
  80                 }
  81                 if(line.find("this/AbsBool<:value") == 0 || line.find("this/AbsElement<:value=") == 0){
  82                         vector<string> values;
  83                         const char delim = ',';
  84                         tokenize(line, delim, values);
  85                         for (uint i=0; i<values.size(); i++){
  86                                 uint i1, i2, i3;
  87                                 if (3 == sscanf(values[i].c_str(),"%*[^0123456789]%u%*[^0123456789]%d%*[^0123456789]%u", &i1, &i2, &i3)){
  88                                         model_print("Signature%u = %u\n", i1, i3);
  89                                         sigEnc.setValue(i1, i3);
  90                                 }
  91                         }
  92                 }
  93         }
  94         return IS_SAT;
  95 }
  96
  97 void AlloyEnc::dumpAlloyFooter(){
  98         output << "pred show {}" << endl;
  99         output << "run show for " << sigEnc.getAlloyIntScope() << " int" << endl;
 100 }
 101
 102 uint AlloyEnc::getTimeout(){
 103         uint timeout =csolver->getSatSolverTimeout();
 104         return timeout == (uint)NOTIMEOUT? 1000: timeout;
 105 }
 106
 107 void AlloyEnc::dumpAlloyHeader(){
 108         output << "open util/integer" << endl;
 109 }
 110
 111 int AlloyEnc::solve(){
 112         dumpAlloyFooter();
 113         int result = IS_INDETER;
 114         char buffer [512];
 115         if( output.is_open()){
 116                 output.close();
 117         }
 118         snprintf(buffer, sizeof(buffer), "./run.sh timeout %u java -Xmx10000m edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", getTimeout(), alloyFileName, solutionFile);
 119         int status = system(buffer);
 120         if (status == 0) {
 121                 //Read data in from results file
 122                 result = getResult();
 123         }
 124         return result;
 125 }
 126
 127 string AlloyEnc::encodeConstraint(BooleanEdge c){
 128         Boolean *constraint = c.getBoolean();
 129         string res;
 130         switch(constraint->type){
 131                 case LOGICOP:{
 132                         res = encodeBooleanLogic((BooleanLogic *) constraint);
 133                         break;
 134                 }
 135                 case PREDICATEOP:{
 136                         res = encodePredicate((BooleanPredicate *) constraint);
 137                         break;
 138                 }
 139                 case BOOLEANVAR:{
 140                         res = encodeBooleanVar( (BooleanVar *) constraint);
 141                         break;
 142                 }
 143                 default:
 144                         ASSERT(0);
 145         }
 146         if(c.isNegated()){
 147                 return "not ( " + res + " )";
 148         }
 149         return res;
 150 }
 151
 152 string AlloyEnc::encodeBooleanLogic( BooleanLogic *bl){
 153         uint size = bl->inputs.getSize();
 154         string array[size];
 155         for (uint i = 0; i < size; i++)
 156                 array[i] = encodeConstraint(bl->inputs.get(i));
 157         string op;
 158         switch (bl->op){
 159                 case SATC_OR:
 160                         op = " or ";
 161                         break;
 162                 case SATC_AND:
 163                         op = " and ";
 164                         break;
 165                 case SATC_NOT:
 166                         op = " not ";
 167                         break;
 168                 case SATC_IFF:
 169                         op = " iff ";
 170                         break;
 171                 case SATC_IMPLIES:
 172                         op = " implies ";
 173                         break;
 174                 case SATC_XOR:
 175                 default:
 176                         ASSERT(0);
 177         }
 178         switch (bl->op) {
 179                 case SATC_OR:
 180                 case SATC_AND:{
 181                         ASSERT(size >= 2);
 182                         string res = "( ";
 183                         res += array[0];
 184                         for( uint i=1; i< size; i++){
 185                                 res += op + array[i];
 186                         }
 187                         res += " )";
 188                         return res;
 189                 }
 190                 case SATC_NOT:{
 191                         return "not ( " + array[0] + " )";
 192                 }
 193                 case SATC_IMPLIES:
 194                 case SATC_IFF:
 195                         return "( " + array[0] + op + array[1] + " )";
 196                 case SATC_XOR:
 197                 default:
 198                         ASSERT(0);
 199
 200         }
 201 }
 202
 203 string AlloyEnc::encodePredicate( BooleanPredicate *bp){
 204         switch (bp->predicate->type) {
 205                 case TABLEPRED:
 206                         ASSERT(0);
 207                 case OPERATORPRED:
 208                         return encodeOperatorPredicate(bp);
 209                 default:
 210                         ASSERT(0);
 211         }
 212 }
 213
 214 string AlloyEnc::encodeBooleanVar( BooleanVar *bv){
 215         BooleanSig * boolSig = sigEnc.getBooleanSignature(bv);
 216         return *boolSig + " = 1";
 217 }
 218
 219 string AlloyEnc::processElementFunction(ElementFunction* elemFunc, ElementSig *signature){
 220         FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
 221         uint numDomains = elemFunc->inputs.getSize();
 222         ASSERT(numDomains > 1);
 223         ElementSig *inputs[numDomains];
 224         string result;
 225         for (uint i = 0; i < numDomains; i++) {
 226                 Element *elem = elemFunc->inputs.get(i);
 227                 inputs[i] = sigEnc.getElementSignature(elem);
 228                 if(elem->type == ELEMFUNCRETURN){
 229                         result += processElementFunction((ElementFunction *) elem, inputs[i]);
 230                 }
 231         }
 232         string op;
 233         switch(function->op){
 234                 case SATC_ADD:
 235                         op = ".add";
 236                         break;
 237                 case SATC_SUB:
 238                         op = ".sub";
 239                         break;
 240                 default:
 241                         ASSERT(0);
 242         }
 243         result += *signature + " = " + *inputs[0];
 244         for (uint i = 1; i < numDomains; i++) {
 245                 result += op + "["+ *inputs[i] +"]";
 246         }
 247         result += "\n";
 248         return result;
 249 }
 250
 251 string AlloyEnc::encodeOperatorPredicate(BooleanPredicate *constraint){
 252         PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
 253         ASSERT(constraint->inputs.getSize() == 2);
 254         string str;
 255         Element *elem0 = constraint->inputs.get(0);
 256         ASSERT(elem0->type == ELEMSET || elem0->type == ELEMFUNCRETURN || elem0->type == ELEMCONST);
 257         ElementSig *elemSig1 = sigEnc.getElementSignature(elem0);
 258         if(elem0->type == ELEMFUNCRETURN){
 259                 str += processElementFunction((ElementFunction *) elem0, elemSig1);
 260         }
 261         Element *elem1 = constraint->inputs.get(1);
 262         ASSERT(elem1->type == ELEMSET || elem1->type == ELEMFUNCRETURN || elem1->type == ELEMCONST);
 263         ElementSig *elemSig2 = sigEnc.getElementSignature(elem1);
 264         if(elem1->type == ELEMFUNCRETURN){
 265                 str += processElementFunction((ElementFunction *) elem1, elemSig2);
 266         }
 267         switch (predicate->getOp()) {
 268                 case SATC_EQUALS:
 269                         str += *elemSig1 + " = " + *elemSig2;
 270                         break;
 271                 case SATC_LT:
 272                         str += *elemSig1 + " < " + *elemSig2;
 273                         break;
 274                 case SATC_GT:
 275                         str += *elemSig1 + " > " + *elemSig2;
 276                         break;
 277                 default:
 278                         ASSERT(0);
 279         }
 280         return str;
 281 }
 282
 283 void AlloyEnc::writeToFile(string str){
 284         output << str << endl;
 285 }
 286
 287 bool AlloyEnc::getBooleanValue(Boolean *b){
 288         return (bool)sigEnc.getValue(b);
 289 }
 290
 291 uint64_t AlloyEnc::getValue(Element * element){
 292         return (uint64_t)sigEnc.getValue(element);
 293 }
 294