src/Test/dirkreader.cc

   1 #include <iostream>
   2 #include <fstream>
   3 #include "csolver.h"
   4 #include "hashset.h"
   5 #include "cppvector.h"
   6 #include <dirent.h>
   7 #include <string>
   8 #include <sstream>
   9 #include "common.h"
  10 using namespace std;
  11 const char * assertstart = "ASSERTSTART";
  12 const char * assertend = "ASSERTEND";
  13 const char * satstart = "SATSTART";
  14 const char * satend = "SATEND";
  15
  16 int skipahead(const char * token1, const char * token2);
  17 char * readuntilend(const char * token);
  18 BooleanEdge parseConstraint(CSolver * solver, char * constraint, int & offset);
  19 void processEquality(char * constraint, int &offset);
  20 void dumpSMTproblem(char * sat, char * assert);
  21
  22 std::ifstream * file;
  23 Order * order;
  24 MutableSet * set;
  25 class intwrapper {
  26 public:
  27   intwrapper(int _val) : value(_val) {
  28   }
  29   int32_t value;
  30 };
  31
  32 unsigned int iw_hash_function(intwrapper *i) {
  33   return i->value;
  34 }
  35
  36 bool iw_equals(intwrapper *key1, intwrapper *key2) {
  37   return (key1->value == key2->value);
  38 }
  39
  40 typedef Hashset<intwrapper *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashsetIW;
  41 typedef SetIterator<intwrapper *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashsetIWIterator;
  42 class OrderRec {
  43 public:
  44   OrderRec() : set (NULL), value(-1), alloced(false) {
  45   }
  46   ~OrderRec() {
  47     if (set != NULL) {
  48       set->resetAndDelete();
  49       delete set;
  50     }
  51   }
  52   HashsetIW * set;
  53   int32_t value;
  54   bool alloced;
  55 };
  56
  57 typedef Hashtable<intwrapper *, OrderRec *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashtableIW;
  58 typedef Hashtable<intwrapper *, Boolean *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashtableBV;
  59 Vector<OrderRec*> * orderRecVector = NULL;
  60 HashtableIW * ordertable = NULL;
  61 HashtableBV * vartable = new HashtableBV();
  62 HashsetIW * intSet = new HashsetIW();
  63 HashsetIW * boolSet = new HashsetIW();
  64
  65 void cleanAndFreeOrderRecVector(){
  66         for(uint i=0; i< orderRecVector->getSize(); i++){
  67                 delete orderRecVector->get(i);
  68         }
  69         orderRecVector->clear();
  70 }
  71
  72 int main(int numargs, char ** argv) {
  73   file = new std::ifstream(argv[1]);
  74   char * assert = NULL;
  75   char * sat = NULL;
  76   Vector<OrderRec*> orderRecs;
  77   orderRecVector = &orderRecs;
  78   while(true) {
  79     int retval = skipahead(assertstart, satstart);
  80     printf("%d\n", retval);
  81     if (retval == 0){
  82       break;
  83     }
  84     if (retval == 1) {
  85       if (assert != NULL){
  86         free(assert);
  87         assert = NULL;
  88       }
  89       assert = readuntilend(assertend);
  90       printf("[%s]\n", assert);
  91     } else if (retval == 2) {
  92       if (sat != NULL) {
  93         free(sat);
  94         sat = NULL;
  95         vartable->resetAndDeleteKeys();
  96         ordertable->reset();
  97         cleanAndFreeOrderRecVector();
  98       } else {
  99         ordertable = new HashtableIW();
 100       }
 101       sat = readuntilend(satend);
 102       CSolver *solver = new CSolver();
 103       solver->turnoffOptimizations();
 104       set = solver->createMutableSet(1);
 105       order = solver->createOrder(SATC_TOTAL, (Set *) set);
 106       int offset = 0;
 107       processEquality(sat, offset);
 108       offset = 0;
 109       processEquality(assert, offset);
 110       offset = 0;
 111       solver->addConstraint(parseConstraint(solver, sat, offset));
 112       offset = 0;
 113       solver->addConstraint(parseConstraint(solver, assert, offset));
 114       printf("[%s]\n", sat);
 115       solver->finalizeMutableSet(set);
 116       solver->serialize();
 117       solver->printConstraints();
 118       dumpSMTproblem(sat, assert);
 119       delete solver;
 120     }
 121   }
 122
 123   cleanAndFreeOrderRecVector();
 124   if(ordertable != NULL){
 125         delete ordertable;
 126   }
 127   if(assert != NULL){
 128         free(assert);
 129   }
 130   if(sat != NULL){
 131         free(sat);
 132   }
 133   vartable->resetAndDeleteKeys();
 134   delete vartable;
 135   file->close();
 136   delete file;
 137 }
 138
 139 void doExit(const char * message){
 140         printf("%s", message);
 141         exit(-1);
 142 }
 143
 144 void doExit() {
 145         doExit("Parse Error\n");
 146 }
 147
 148 void renameDumpFile(const char *path, long long id) {
 149         struct dirent *entry;
 150         DIR *dir = opendir(path);
 151         if (dir == NULL) {
 152                 return;
 153         }
 154         char newname[128] ={0};
 155         sprintf(newname, "%lld.dump", id);
 156         bool duplicate = false;
 157         while ((entry = readdir(dir)) != NULL) {
 158                  if(strstr(entry->d_name, "DUMP") != NULL){
 159                         if(duplicate){
 160                                 doExit("Multiplle DUMP file exists. Make sure to clean them all before running the program");
 161                         }
 162                         int result= rename( entry->d_name , newname );
 163                         if ( result == 0 )
 164                                 printf ( "File successfully renamed to %s\n" , newname);
 165                         else
 166                                 doExit( "Error renaming file" );
 167                         duplicate = true;
 168                  }
 169         }
 170         closedir(dir);
 171 }
 172 template <class MyType>
 173 string to_string(MyType value){
 174         string number;
 175         std::stringstream strstream;
 176         strstream << value;
 177         strstream >> number;
 178         return number;
 179 }
 180
 181 void dumpDeclarations(std::ofstream& smtfile){
 182         HashsetIWIterator* iterator = intSet->iterator();
 183         while(iterator->hasNext()){
 184                 intwrapper * iw = iterator->next();
 185                 string declare = "(declare-const O!"+ to_string<uint32_t>(iw->value) + " Int)\n";
 186                 smtfile << declare;
 187         }
 188         delete iterator;
 189
 190         iterator = boolSet->iterator();
 191         while(iterator->hasNext()){
 192                 intwrapper * iw = iterator->next();
 193                 string declare = "(declare-const S!" + to_string<uint32_t>(iw->value) + " Bool)\n";
 194                 smtfile << declare;
 195         }
 196         delete iterator;
 197 }
 198
 199 void dumpFooter(std::ofstream& smtfile){
 200         smtfile << "(check-sat)" << endl;
 201 }
 202
 203
 204
 205 void dumpSMTproblem(char * sat, char * assert){
 206         long long id = getTimeNano();
 207         cout << "Here's the ID= " << id << endl;
 208         cout <<"************here is the SMT file*********" << endl << sat << endl << assert <<endl << "****************************" << endl;;
 209         renameDumpFile("./", id);
 210         string smtfilename = to_string<long long>(id) + ".smt";
 211         std::ofstream smtfile;
 212         smtfile.open (smtfilename.c_str());
 213         if(!smtfile.is_open())
 214         {
 215                 doExit("Unable to create file.\n");
 216         }
 217         dumpDeclarations(smtfile);
 218         string ssat(sat);
 219         string satStatement = "(assert "+ ssat + "\n)\n";
 220         smtfile << satStatement;
 221         string sassert(assert);
 222         string assertStatement = "(assert " + sassert + "\n)\n";
 223         smtfile << assertStatement;
 224         dumpFooter(smtfile);
 225         smtfile.close();
 226 }
 227
 228 void skipwhitespace(char * constraint, int & offset) {
 229   //skip whitespace
 230   while (constraint[offset] == ' ' || constraint[offset] == '\n')
 231     offset++;
 232 }
 233
 234 int32_t getOrderVar(char *constraint, int & offset) {
 235   if (constraint[offset++] != 'O' || constraint[offset++] != '!' ) {
 236     doExit();
 237   }
 238   int32_t num = 0;
 239   while(true) {
 240     char next = constraint[offset];
 241     if (next >= '0' && next <= '9') {
 242       num = (num * 10) + (next - '0');
 243       offset++;
 244     } else
 245       return num;
 246   }
 247 }
 248
 249 int32_t getBooleanVar(char *constraint, int & offset) {
 250         if (constraint[offset++] != 'S' || constraint[offset++] != '!' ) {
 251                 cout << "Constraint= " << constraint << "\toffset=" << constraint[offset - 1] << " ******\n";
 252                 doExit();
 253         }
 254   int32_t num = 0;
 255   while(true) {
 256     char next = constraint[offset];
 257     if (next >= '0' && next <= '9') {
 258       num = (num * 10) + (next - '0');
 259       offset++;
 260     } else
 261       return num;
 262   }
 263 }
 264
 265 BooleanEdge checkBooleanVar(CSolver *solver, int32_t value) {
 266   intwrapper v(value);
 267   if (vartable->contains(&v)) {
 268     return BooleanEdge(vartable->get(&v));
 269   } else {
 270     Boolean* ve = solver->getBooleanVar(2).getBoolean();
 271     vartable->put(new intwrapper(value), ve);
 272     return BooleanEdge(ve);
 273   }
 274 }
 275
 276 void mergeVars(int32_t value1, int32_t value2) {
 277   intwrapper v1(value1);
 278   intwrapper v2(value2);
 279   OrderRec *r1 = ordertable->get(&v1);
 280   OrderRec *r2 = ordertable->get(&v2);
 281   if (r1 == r2) {
 282     if (r1 == NULL) {
 283       OrderRec * r = new OrderRec();
 284       orderRecVector->push(r);
 285       r->value = value1;
 286       r->set = new HashsetIW();
 287       intwrapper * k1 = new intwrapper(v1);
 288       intwrapper * k2 = new intwrapper(v2);
 289       r->set->add(k1);
 290       r->set->add(k2);
 291       ordertable->put(k1, r);
 292       ordertable->put(k2, r);
 293     }
 294   } else if (r1 == NULL) {
 295     intwrapper * k = new intwrapper(v1);
 296     ordertable->put(k, r2);
 297     r2->set->add(k);
 298   } else if (r2 == NULL) {
 299     intwrapper * k = new intwrapper(v2);
 300     ordertable->put(k, r1);
 301     r1->set->add(k);
 302   } else {
 303     SetIterator<intwrapper *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> * it1 = r1->set->iterator();
 304     while (it1->hasNext()) {
 305       intwrapper * k = it1->next();
 306       ordertable->put(k, r2);
 307       r2->set->add(k);
 308     }
 309     delete r2->set;
 310     r2->set = NULL;
 311     delete r2;
 312     delete it1;
 313   }
 314 }
 315
 316 int32_t checkordervar(CSolver * solver, int32_t value) {
 317   intwrapper v(value);
 318   OrderRec * rec = ordertable->get(&v);
 319   if (rec == NULL) {
 320     intwrapper * k = new intwrapper(value);
 321     rec = new OrderRec();
 322     orderRecVector->push(rec);
 323     rec->value = value;
 324     rec->set = new HashsetIW();
 325     rec->set->add(k);
 326     ordertable->put(k, rec);
 327   }
 328   if (!rec->alloced) {
 329     solver->addItem(set, rec->value);
 330     rec->alloced = true;
 331   }
 332   return rec->value;
 333 }
 334
 335 void processEquality(char * constraint, int &offset) {
 336   skipwhitespace(constraint, offset);
 337   if (strncmp(&constraint[offset], "(and",4) == 0) {
 338     offset +=4;
 339     Vector<BooleanEdge> vec;
 340     while(true) {
 341       skipwhitespace(constraint, offset);
 342       if (constraint[offset] == ')') {
 343         offset++;
 344         return;
 345       }
 346       processEquality(constraint, offset);
 347     }
 348   } else if (strncmp(&constraint[offset], "(<", 2) == 0) {
 349     offset+=2;
 350     skipwhitespace(constraint, offset);
 351     getOrderVar(constraint, offset);
 352     skipwhitespace(constraint, offset);
 353     getOrderVar(constraint, offset);
 354     skipwhitespace(constraint, offset);
 355     if (constraint[offset++] != ')'){
 356             doExit();
 357     }
 358     return;
 359   } else if (strncmp(&constraint[offset], "(=", 2) == 0) {
 360     offset+=2;
 361     skipwhitespace(constraint, offset);
 362     int v1=getOrderVar(constraint, offset);
 363     intwrapper iwv1(v1);
 364     if(intSet->get(&iwv1) == NULL){
 365         intSet->add(new intwrapper(v1));
 366     }
 367     skipwhitespace(constraint, offset);
 368     int v2=getOrderVar(constraint, offset);
 369     intwrapper iwv2(v2);
 370     if(intSet->get(&iwv2) == NULL){
 371         intSet->add(new intwrapper(v2));
 372     }
 373     skipwhitespace(constraint, offset);
 374     if (constraint[offset++] != ')')
 375       doExit();
 376     mergeVars(v1, v2);
 377     return;
 378   } else if (strncmp(&constraint[offset], "tr", 2) == 0){
 379         offset+=4;
 380         skipwhitespace(constraint, offset);
 381         return;
 382   }
 383   else{
 384         int32_t b1 = getBooleanVar(constraint, offset);
 385         intwrapper iwb1(b1);
 386         if(boolSet->get(&iwb1) == NULL){
 387             boolSet->add(new intwrapper(b1));
 388         }
 389         skipwhitespace(constraint, offset);
 390 return;
 391   }
 392 }
 393
 394 BooleanEdge parseConstraint(CSolver * solver, char * constraint, int & offset) {
 395   skipwhitespace(constraint, offset);
 396   if (strncmp(&constraint[offset], "(and", 4) == 0) {
 397     offset +=4;
 398     Vector<BooleanEdge> vec;
 399     while(true) {
 400       skipwhitespace(constraint, offset);
 401       if (constraint[offset] == ')') {
 402         offset++;
 403         return solver->applyLogicalOperation(SATC_AND, vec.expose(), vec.getSize());
 404       }
 405       vec.push(parseConstraint(solver, constraint, offset));
 406     }
 407   } else if (strncmp(&constraint[offset], "(<", 2) == 0) {
 408     offset+=2;
 409     skipwhitespace(constraint, offset);
 410     int32_t v1 = getOrderVar(constraint, offset);
 411     intwrapper iwv1(v1);
 412     if(intSet->get(&iwv1) == NULL){
 413         intSet->add(new intwrapper(v1));
 414     }
 415     skipwhitespace(constraint, offset);
 416     int32_t v2 = getOrderVar(constraint, offset);
 417     intwrapper iwv2(v2);
 418     if(intSet->get(&iwv2) == NULL){
 419         intSet->add(new intwrapper(v2));
 420     }
 421     skipwhitespace(constraint, offset);
 422     if (constraint[offset++] != ')')
 423       doExit();
 424     return solver->orderConstraint(order, checkordervar(solver, v1), checkordervar(solver, v2));
 425   } else if (strncmp(&constraint[offset], "(=", 2) == 0) {
 426     offset+=2;
 427     skipwhitespace(constraint, offset);
 428     getOrderVar(constraint, offset);
 429     skipwhitespace(constraint, offset);
 430     getOrderVar(constraint, offset);
 431     skipwhitespace(constraint, offset);
 432     if (constraint[offset++] != ')')
 433       doExit();
 434     return solver->getBooleanTrue();
 435   }else if (strncmp(&constraint[offset], "tr", 2) == 0){
 436         offset+=4;
 437         skipwhitespace(constraint, offset);
 438         return solver->getBooleanTrue();
 439   }
 440   else {
 441     int32_t v = getBooleanVar(constraint, offset);
 442     intwrapper iwb1(v);
 443     if(boolSet->get(&iwb1) == NULL){
 444         boolSet->add(new intwrapper(v));
 445     }
 446     skipwhitespace(constraint, offset);
 447     return checkBooleanVar(solver, v);
 448   }
 449 }
 450
 451 int skipahead(const char * token1, const char * token2) {
 452   int index1 = 0, index2 = 0;
 453   char buffer[256];
 454   while(true) {
 455     if (token1[index1] == 0)
 456       return 1;
 457     if (token2[index2] == 0)
 458       return 2;
 459     if (file->eof())
 460       return 0;
 461     file->read(buffer, 1);
 462     if (buffer[0] == token1[index1])
 463       index1++;
 464     else
 465       index1 = 0;
 466     if (buffer[0] == token2[index2])
 467       index2++;
 468     else
 469       index2 = 0;
 470   }
 471 }
 472
 473 char * readuntilend(const char * token) {
 474   int index = 0;
 475   char buffer[256];
 476   int length = 256;
 477   int offset = 0;
 478   char * outbuffer = (char *) malloc(length);
 479   while(true) {
 480     if (token[index] == 0) {
 481       outbuffer[offset - index] = 0;
 482       return outbuffer;
 483     }
 484     if (file->eof()) {
 485       free(outbuffer);
 486       return NULL;
 487     }
 488
 489     file->read(buffer, 1);
 490     outbuffer[offset++] = buffer[0];
 491     if (offset == length) {
 492       length = length * 2;
 493       outbuffer = (char *) realloc(outbuffer, length);
 494     }
 495     if (buffer[0] == token[index])
 496       index++;
 497     else
 498       index=0;
 499   }
 500 }