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
  55 HashtableIW * ordertable = NULL;
  56 HashtableBV * vartable = new HashtableBV();
  57
  58 int main(int numargs, char ** argv) {
  59   file = new std::ifstream(argv[1]);
  60   char * assert = NULL;
  61   char * sat = NULL;
  62   while(true) {
  63     int retval = skipahead(assertstart, satstart);
  64     printf("%d\n", retval);
  65     if (retval == 0)
  66       break;
  67     if (retval == 1) {
  68       if (assert != NULL)
  69         free(assert);
  70       assert = readuntilend(assertend);
  71       printf("[%s]\n", assert);
  72     } else if (retval == 2) {
  73       if (sat != NULL) {
  74         free(sat);
  75         vartable->resetAndDeleteKeys();
  76         ordertable->resetAndDeleteVals();
  77       } else {
  78         ordertable = new HashtableIW();
  79       }
  80       sat = readuntilend(satend);
  81       CSolver *solver = new CSolver();
  82       set = solver->createMutableSet(1);
  83       order = solver->createOrder(SATC_TOTAL, (Set *) set);
  84       int offset = 0;
  85       processEquality(sat, offset);
  86       offset = 0;
  87       processEquality(assert, offset);
  88       offset = 0;
  89       solver->addConstraint(parseConstraint(solver, sat, offset));
  90       offset = 0;
  91       solver->addConstraint(parseConstraint(solver, assert, offset));
  92       printf("[%s]\n", sat);
  93       solver->finalizeMutableSet(set);
  94       solver->serialize();
  95       solver->printConstraints();
  96       delete solver;
  97     }
  98   }
  99
 100   file->close();
 101 }
 102
 103 void skipwhitespace(char * constraint, int & offset) {
 104   //skip whitespace
 105   while (constraint[offset] == ' ' || constraint[offset] == '\n')
 106     offset++;
 107 }
 108
 109 void doExit() {
 110   printf("PARSE ERROR\n");
 111   exit(-1);
 112 }
 113
 114 int32_t getOrderVar(char *constraint, int & offset) {
 115   if (constraint[offset++] != 'O' || constraint[offset++] != '!' ) {
 116     doExit();
 117   }
 118   int32_t num = 0;
 119   while(true) {
 120     char next = constraint[offset];
 121     if (next >= '0' && next <= '9') {
 122       num = (num * 10) + (next - '0');
 123       offset++;
 124     } else
 125       return num;
 126   }
 127 }
 128
 129 int32_t getBooleanVar(char *constraint, int & offset) {
 130   if (constraint[offset++] != 'S' || constraint[offset++] != '!' ) {
 131     doExit();
 132   }
 133   int32_t num = 0;
 134   while(true) {
 135     char next = constraint[offset];
 136     if (next >= '0' && next <= '9') {
 137       num = (num * 10) + (next - '0');
 138       offset++;
 139     } else
 140       return num;
 141   }
 142 }
 143
 144 BooleanEdge checkBooleanVar(CSolver *solver, int32_t value) {
 145   intwrapper v(value);
 146   if (vartable->contains(&v)) {
 147     return BooleanEdge(vartable->get(&v));
 148   } else {
 149     Boolean* ve = solver->getBooleanVar(2).getBoolean();
 150     vartable->put(new intwrapper(value), ve);
 151     return BooleanEdge(ve);
 152   }
 153 }
 154
 155 void mergeVars(int32_t value1, int32_t value2) {
 156   intwrapper v1(value1);
 157   intwrapper v2(value2);
 158   OrderRec *r1 = ordertable->get(&v1);
 159   OrderRec *r2 = ordertable->get(&v2);
 160   if (r1 == r2) {
 161     if (r1 == NULL) {
 162       OrderRec * r = new OrderRec();
 163       r->value = value1;
 164       r->set = new HashsetIW();
 165       intwrapper * k1 = new intwrapper(v1);
 166       intwrapper * k2 = new intwrapper(v2);
 167       r->set->add(k1);
 168       r->set->add(k2);
 169       ordertable->put(k1, r);
 170       ordertable->put(k2, r);
 171     }
 172   } else if (r1 == NULL) {
 173     intwrapper * k = new intwrapper(v1);
 174     ordertable->put(k, r2);
 175     r2->set->add(k);
 176   } else if (r2 == NULL) {
 177     intwrapper * k = new intwrapper(v2);
 178     ordertable->put(k, r1);
 179     r1->set->add(k);
 180   } else {
 181     SetIterator<intwrapper *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> * it1 = r1->set->iterator();
 182     while (it1->hasNext()) {
 183       intwrapper * k = it1->next();
 184       ordertable->put(k, r2);
 185       r2->set->add(k);
 186     }
 187     delete r2->set;
 188     r2->set = NULL;
 189     delete r2;
 190     delete it1;
 191   }
 192 }
 193
 194 int32_t checkordervar(CSolver * solver, int32_t value) {
 195   intwrapper v(value);
 196   OrderRec * rec = ordertable->get(&v);
 197   if (rec == NULL) {
 198     intwrapper * k = new intwrapper(value);
 199     rec = new OrderRec();
 200     rec->value = value;
 201     ordertable->put(k, rec);
 202   }
 203   if (!rec->alloced) {
 204     solver->addItem(set, rec->value);
 205     rec->alloced = true;
 206   }
 207   return rec->value;
 208 }
 209
 210 void processEquality(char * constraint, int &offset) {
 211   skipwhitespace(constraint, offset);
 212   if (strncmp(&constraint[offset], "(and",4) == 0) {
 213     offset +=4;
 214     Vector<BooleanEdge> vec;
 215     while(true) {
 216       skipwhitespace(constraint, offset);
 217       if (constraint[offset] == ')') {
 218         offset++;
 219         return;
 220       }
 221       processEquality(constraint, offset);
 222     }
 223   } else if (strncmp(&constraint[offset], "(<", 2) == 0) {
 224     offset+=2;
 225     skipwhitespace(constraint, offset);
 226     getOrderVar(constraint, offset);
 227     skipwhitespace(constraint, offset);
 228     getOrderVar(constraint, offset);
 229     skipwhitespace(constraint, offset);
 230     if (constraint[offset++] != ')')
 231       doExit();
 232     return;
 233   } else if (strncmp(&constraint[offset], "(=", 2) == 0) {
 234     offset+=2;
 235     skipwhitespace(constraint, offset);
 236     int v1=getOrderVar(constraint, offset);
 237     skipwhitespace(constraint, offset);
 238     int v2=getOrderVar(constraint, offset);
 239     skipwhitespace(constraint, offset);
 240     if (constraint[offset++] != ')')
 241       doExit();
 242     mergeVars(v1, v2);
 243     return;
 244   } else {
 245     getBooleanVar(constraint, offset);
 246     skipwhitespace(constraint, offset);
 247     return;
 248   }
 249 }
 250
 251 BooleanEdge parseConstraint(CSolver * solver, char * constraint, int & offset) {
 252   skipwhitespace(constraint, offset);
 253   if (strncmp(&constraint[offset], "(and", 4) == 0) {
 254     offset +=4;
 255     Vector<BooleanEdge> vec;
 256     while(true) {
 257       skipwhitespace(constraint, offset);
 258       if (constraint[offset] == ')') {
 259         offset++;
 260         return solver->applyLogicalOperation(SATC_AND, vec.expose(), vec.getSize());
 261       }
 262       vec.push(parseConstraint(solver, constraint, offset));
 263     }
 264   } else if (strncmp(&constraint[offset], "(<", 2) == 0) {
 265     offset+=2;
 266     skipwhitespace(constraint, offset);
 267     int32_t v1 = getOrderVar(constraint, offset);
 268     skipwhitespace(constraint, offset);
 269     int32_t v2 = getOrderVar(constraint, offset);
 270     skipwhitespace(constraint, offset);
 271     if (constraint[offset++] != ')')
 272       doExit();
 273     return solver->orderConstraint(order, checkordervar(solver, v1), checkordervar(solver, v2));
 274   } else if (strncmp(&constraint[offset], "(=", 2) == 0) {
 275     offset+=2;
 276     skipwhitespace(constraint, offset);
 277     getOrderVar(constraint, offset);
 278     skipwhitespace(constraint, offset);
 279     getOrderVar(constraint, offset);
 280     skipwhitespace(constraint, offset);
 281     if (constraint[offset++] != ')')
 282       doExit();
 283     return solver->getBooleanTrue();
 284   } else {
 285     int32_t v = getBooleanVar(constraint, offset);
 286     skipwhitespace(constraint, offset);
 287     return checkBooleanVar(solver, v);
 288   }
 289 }
 290
 291 int skipahead(const char * token1, const char * token2) {
 292   int index1 = 0, index2 = 0;
 293   char buffer[256];
 294   while(true) {
 295     if (token1[index1] == 0)
 296       return 1;
 297     if (token2[index2] == 0)
 298       return 2;
 299     if (file->eof())
 300       return 0;
 301     file->read(buffer, 1);
 302     if (buffer[0] == token1[index1])
 303       index1++;
 304     else
 305       index1 = 0;
 306     if (buffer[0] == token2[index2])
 307       index2++;
 308     else
 309       index2 = 0;
 310   }
 311 }
 312
 313 char * readuntilend(const char * token) {
 314   int index = 0;
 315   char buffer[256];
 316   int length = 256;
 317   int offset = 0;
 318   char * outbuffer = (char *) malloc(length);
 319   while(true) {
 320     if (token[index] == 0) {
 321       outbuffer[offset - index] = 0;
 322       return outbuffer;
 323     }
 324     if (file->eof()) {
 325       free(outbuffer);
 326       return NULL;
 327     }
 328
 329     file->read(buffer, 1);
 330     outbuffer[offset++] = buffer[0];
 331     if (offset == length) {
 332       length = length * 2;
 333       outbuffer = (char *) realloc(outbuffer, length);
 334     }
 335     if (buffer[0] == token[index])
 336       index++;
 337     else
 338       index=0;
 339   }
 340 }