src/Test/dirkreader.cc

   1 #include <iostream>
   2 #include <fstream>
   3 #include "csolver.h"
   4 #include "hashset.h"
   5 #include "cppvector.h"
   6
   7 const char * assertstart = "ASSERTSTART";
   8 const char * assertend = "ASSERTEND";
   9 const char * satstart = "SATSTART";
  10 const char * satend = "SATEND";
  11
  12 int skipahead(const char * token1, const char * token2);
  13 char * readuntilend(const char * token);
  14 BooleanEdge parseConstraint(CSolver * solver, char * constraint, int & offset);
  15 void processEquality(char * constraint, int &offset);
  16
  17 std::ifstream * file;
  18 Order * order;
  19 MutableSet * set;
  20 class intwrapper {
  21 public:
  22   intwrapper(int _val) : value(_val) {
  23   }
  24   int32_t value;
  25 };
  26
  27 unsigned int iw_hash_function(intwrapper *i) {
  28   return i->value;
  29 }
  30
  31 bool iw_equals(intwrapper *key1, intwrapper *key2) {
  32   return (key1->value == key2->value);
  33 }
  34
  35 typedef Hashset<intwrapper *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashsetIW;
  36
  37 class OrderRec {
  38 public:
  39   OrderRec() : set (NULL), value(-1), alloced(false) {
  40   }
  41   ~OrderRec() {
  42     if (set != NULL) {
  43       set->resetAndDelete();
  44       delete set;
  45     }
  46   }
  47   HashsetIW * set;
  48   int32_t value;
  49   bool alloced;
  50 };
  51
  52 typedef Hashtable<intwrapper *, OrderRec *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashtableIW;
  53 typedef Hashtable<intwrapper *, Boolean *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashtableBV;
  54 Vector<OrderRec*> * orderRecVector = NULL;
  55 HashtableIW * ordertable = NULL;
  56 HashtableBV * vartable = new HashtableBV();
  57
  58 void cleanAndFreeOrderRecVector(){
  59         for(uint i=0; i< orderRecVector->getSize(); i++){
  60                 delete orderRecVector->get(i);
  61         }
  62         orderRecVector->clear();
  63 }
  64
  65 int main(int numargs, char ** argv) {
  66   file = new std::ifstream(argv[1]);
  67   char * assert = NULL;
  68   char * sat = NULL;
  69   Vector<OrderRec*> orderRecs;
  70   orderRecVector = &orderRecs;
  71   while(true) {
  72     int retval = skipahead(assertstart, satstart);
  73     printf("%d\n", retval);
  74     if (retval == 0){
  75       break;
  76     }
  77     if (retval == 1) {
  78       if (assert != NULL){
  79         free(assert);
  80         assert = NULL;
  81       }
  82       assert = readuntilend(assertend);
  83       printf("[%s]\n", assert);
  84     } else if (retval == 2) {
  85       if (sat != NULL) {
  86         free(sat);
  87         sat = NULL;
  88         vartable->resetAndDeleteKeys();
  89         ordertable->reset();
  90         cleanAndFreeOrderRecVector();
  91       } else {
  92         ordertable = new HashtableIW();
  93       }
  94       sat = readuntilend(satend);
  95       CSolver *solver = new CSolver();
  96       solver->turnoffOptimizations();
  97       set = solver->createMutableSet(1);
  98       order = solver->createOrder(SATC_TOTAL, (Set *) set);
  99       int offset = 0;
 100       processEquality(sat, offset);
 101       offset = 0;
 102       processEquality(assert, offset);
 103       offset = 0;
 104       solver->addConstraint(parseConstraint(solver, sat, offset));
 105       offset = 0;
 106       solver->addConstraint(parseConstraint(solver, assert, offset));
 107       printf("[%s]\n", sat);
 108       solver->finalizeMutableSet(set);
 109       solver->serialize();
 110       solver->printConstraints();
 111       delete solver;
 112     }
 113   }
 114
 115   cleanAndFreeOrderRecVector();
 116   if(ordertable != NULL){
 117         delete ordertable;
 118   }
 119   if(assert != NULL){
 120         free(assert);
 121   }
 122   if(sat != NULL){
 123         free(sat);
 124   }
 125   vartable->resetAndDeleteKeys();
 126   delete vartable;
 127   file->close();
 128   delete file;
 129 }
 130
 131 void skipwhitespace(char * constraint, int & offset) {
 132   //skip whitespace
 133   while (constraint[offset] == ' ' || constraint[offset] == '\n')
 134     offset++;
 135 }
 136
 137 void doExit() {
 138   printf("PARSE ERROR\n");
 139   exit(-1);
 140 }
 141
 142 int32_t getOrderVar(char *constraint, int & offset) {
 143   if (constraint[offset++] != 'O' || constraint[offset++] != '!' ) {
 144     doExit();
 145   }
 146   int32_t num = 0;
 147   while(true) {
 148     char next = constraint[offset];
 149     if (next >= '0' && next <= '9') {
 150       num = (num * 10) + (next - '0');
 151       offset++;
 152     } else
 153       return num;
 154   }
 155 }
 156
 157 int32_t getBooleanVar(char *constraint, int & offset) {
 158   if (constraint[offset++] != 'S' || constraint[offset++] != '!' ) {
 159     doExit();
 160   }
 161   int32_t num = 0;
 162   while(true) {
 163     char next = constraint[offset];
 164     if (next >= '0' && next <= '9') {
 165       num = (num * 10) + (next - '0');
 166       offset++;
 167     } else
 168       return num;
 169   }
 170 }
 171
 172 BooleanEdge checkBooleanVar(CSolver *solver, int32_t value) {
 173   intwrapper v(value);
 174   if (vartable->contains(&v)) {
 175     return BooleanEdge(vartable->get(&v));
 176   } else {
 177     Boolean* ve = solver->getBooleanVar(2).getBoolean();
 178     vartable->put(new intwrapper(value), ve);
 179     return BooleanEdge(ve);
 180   }
 181 }
 182
 183 void mergeVars(int32_t value1, int32_t value2) {
 184   intwrapper v1(value1);
 185   intwrapper v2(value2);
 186   OrderRec *r1 = ordertable->get(&v1);
 187   OrderRec *r2 = ordertable->get(&v2);
 188   if (r1 == r2) {
 189     if (r1 == NULL) {
 190       OrderRec * r = new OrderRec();
 191       orderRecVector->push(r);
 192       r->value = value1;
 193       r->set = new HashsetIW();
 194       intwrapper * k1 = new intwrapper(v1);
 195       intwrapper * k2 = new intwrapper(v2);
 196       r->set->add(k1);
 197       r->set->add(k2);
 198       ordertable->put(k1, r);
 199       ordertable->put(k2, r);
 200     }
 201   } else if (r1 == NULL) {
 202     intwrapper * k = new intwrapper(v1);
 203     ordertable->put(k, r2);
 204     r2->set->add(k);
 205   } else if (r2 == NULL) {
 206     intwrapper * k = new intwrapper(v2);
 207     ordertable->put(k, r1);
 208     r1->set->add(k);
 209   } else {
 210     SetIterator<intwrapper *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> * it1 = r1->set->iterator();
 211     while (it1->hasNext()) {
 212       intwrapper * k = it1->next();
 213       ordertable->put(k, r2);
 214       r2->set->add(k);
 215     }
 216     delete r2->set;
 217     r2->set = NULL;
 218     delete r2;
 219     delete it1;
 220   }
 221 }
 222
 223 int32_t checkordervar(CSolver * solver, int32_t value) {
 224   intwrapper v(value);
 225   OrderRec * rec = ordertable->get(&v);
 226   if (rec == NULL) {
 227     intwrapper * k = new intwrapper(value);
 228     rec = new OrderRec();
 229     orderRecVector->push(rec);
 230     rec->value = value;
 231     rec->set = new HashsetIW();
 232     rec->set->add(k);
 233     ordertable->put(k, rec);
 234   }
 235   if (!rec->alloced) {
 236     solver->addItem(set, rec->value);
 237     rec->alloced = true;
 238   }
 239   return rec->value;
 240 }
 241
 242 void processEquality(char * constraint, int &offset) {
 243   skipwhitespace(constraint, offset);
 244   if (strncmp(&constraint[offset], "(and",4) == 0) {
 245     offset +=4;
 246     Vector<BooleanEdge> vec;
 247     while(true) {
 248       skipwhitespace(constraint, offset);
 249       if (constraint[offset] == ')') {
 250         offset++;
 251         return;
 252       }
 253       processEquality(constraint, offset);
 254     }
 255   } else if (strncmp(&constraint[offset], "(<", 2) == 0) {
 256     offset+=2;
 257     skipwhitespace(constraint, offset);
 258     getOrderVar(constraint, offset);
 259     skipwhitespace(constraint, offset);
 260     getOrderVar(constraint, offset);
 261     skipwhitespace(constraint, offset);
 262     if (constraint[offset++] != ')')
 263       doExit();
 264     return;
 265   } else if (strncmp(&constraint[offset], "(=", 2) == 0) {
 266     offset+=2;
 267     skipwhitespace(constraint, offset);
 268     int v1=getOrderVar(constraint, offset);
 269     skipwhitespace(constraint, offset);
 270     int v2=getOrderVar(constraint, offset);
 271     skipwhitespace(constraint, offset);
 272     if (constraint[offset++] != ')')
 273       doExit();
 274     mergeVars(v1, v2);
 275     return;
 276   } else {
 277     getBooleanVar(constraint, offset);
 278     skipwhitespace(constraint, offset);
 279     return;
 280   }
 281 }
 282
 283 BooleanEdge parseConstraint(CSolver * solver, char * constraint, int & offset) {
 284   skipwhitespace(constraint, offset);
 285   if (strncmp(&constraint[offset], "(and", 4) == 0) {
 286     offset +=4;
 287     Vector<BooleanEdge> vec;
 288     while(true) {
 289       skipwhitespace(constraint, offset);
 290       if (constraint[offset] == ')') {
 291         offset++;
 292         return solver->applyLogicalOperation(SATC_AND, vec.expose(), vec.getSize());
 293       }
 294       vec.push(parseConstraint(solver, constraint, offset));
 295     }
 296   } else if (strncmp(&constraint[offset], "(<", 2) == 0) {
 297     offset+=2;
 298     skipwhitespace(constraint, offset);
 299     int32_t v1 = getOrderVar(constraint, offset);
 300     skipwhitespace(constraint, offset);
 301     int32_t v2 = getOrderVar(constraint, offset);
 302     skipwhitespace(constraint, offset);
 303     if (constraint[offset++] != ')')
 304       doExit();
 305     return solver->orderConstraint(order, checkordervar(solver, v1), checkordervar(solver, v2));
 306   } else if (strncmp(&constraint[offset], "(=", 2) == 0) {
 307     offset+=2;
 308     skipwhitespace(constraint, offset);
 309     getOrderVar(constraint, offset);
 310     skipwhitespace(constraint, offset);
 311     getOrderVar(constraint, offset);
 312     skipwhitespace(constraint, offset);
 313     if (constraint[offset++] != ')')
 314       doExit();
 315     return solver->getBooleanTrue();
 316   } else {
 317     int32_t v = getBooleanVar(constraint, offset);
 318     skipwhitespace(constraint, offset);
 319     return checkBooleanVar(solver, v);
 320   }
 321 }
 322
 323 int skipahead(const char * token1, const char * token2) {
 324   int index1 = 0, index2 = 0;
 325   char buffer[256];
 326   while(true) {
 327     if (token1[index1] == 0)
 328       return 1;
 329     if (token2[index2] == 0)
 330       return 2;
 331     if (file->eof())
 332       return 0;
 333     file->read(buffer, 1);
 334     if (buffer[0] == token1[index1])
 335       index1++;
 336     else
 337       index1 = 0;
 338     if (buffer[0] == token2[index2])
 339       index2++;
 340     else
 341       index2 = 0;
 342   }
 343 }
 344
 345 char * readuntilend(const char * token) {
 346   int index = 0;
 347   char buffer[256];
 348   int length = 256;
 349   int offset = 0;
 350   char * outbuffer = (char *) malloc(length);
 351   while(true) {
 352     if (token[index] == 0) {
 353       outbuffer[offset - index] = 0;
 354       return outbuffer;
 355     }
 356     if (file->eof()) {
 357       free(outbuffer);
 358       return NULL;
 359     }
 360
 361     file->read(buffer, 1);
 362     outbuffer[offset++] = buffer[0];
 363     if (offset == length) {
 364       length = length * 2;
 365       outbuffer = (char *) realloc(outbuffer, length);
 366     }
 367     if (buffer[0] == token[index])
 368       index++;
 369     else
 370       index=0;
 371   }
 372 }