14 const char * assertstart = "ASSERTSTART";
15 const char * assertend = "ASSERTEND";
16 const char * satstart = "SATSTART";
17 const char * satend = "SATEND";
18 const char * varstart = "VARSTART";
19 const char * varend = "VAREND";
21 int skipahead(const char * token1, const char * token2, const char * token3);
22 char * readuntilend(const char * token);
23 BooleanEdge parseConstraint(CSolver * solver, char * constraint, int & offset);
24 void processEquality(char * constraint, int &offset);
25 void dumpSMTproblem(string &smtProblem, long long id);
26 void renameDumpFile(const char *path, long long id);
27 void addASSERTConstraintToSMTProblem(string & smtProblem, char * assert);
28 void addVarConstraintToSMTProblem(string & smtProblem, Vector<char *> & varconstraint);
29 void addSATConstraintToSMTProblem(string &smtProblem, char * sat);
30 void createSATtuneDumps (char *assert, char *sat, Vector<char *> & varconstraints, long long &smtID);
35 bool incremental = true;
38 intwrapper(int _val) : value(_val) {
43 unsigned int iw_hash_function(intwrapper *i) {
47 bool iw_equals(intwrapper *key1, intwrapper *key2) {
48 return (key1->value == key2->value);
51 typedef Hashset<intwrapper *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashsetIW;
52 typedef SetIterator<intwrapper *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashsetIWIterator;
55 OrderRec() : set (NULL), value(-1), alloced(false) {
59 set->resetAndDelete();
68 typedef Hashtable<intwrapper *, OrderRec *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashtableIW;
69 typedef Hashtable<intwrapper *, Boolean *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashtableBV;
70 Vector<OrderRec*> * orderRecVector = NULL;
71 HashtableIW * ordertable = NULL;
72 HashtableBV * vartable = new HashtableBV();
73 HashsetIW * intSet = new HashsetIW();
74 HashsetIW * boolSet = new HashsetIW();
76 void cleanAndFreeOrderRecVector(){
77 for(uint i=0; i< orderRecVector->getSize(); i++){
78 delete orderRecVector->get(i);
80 orderRecVector->clear();
83 int main(int numargs, char ** argv) {
84 file = new std::ifstream(argv[1]);
91 Vector<char *> varconstraints;
92 string smtProblem = "";
94 Vector<OrderRec*> orderRecs;
95 orderRecVector = &orderRecs;
97 int retval = skipahead(assertstart, satstart, varstart);
98 //printf("%d\n", retval);
106 dumpSMTproblem(smtProblem, smtID);
108 for(uint i=0; i< varconstraints.getSize(); i++){
109 free(varconstraints.get(i));
111 varconstraints.clear();
115 assert = readuntilend(assertend);
116 addASSERTConstraintToSMTProblem(smtProblem, assert);
117 //cout << "INFO: SMTProblem After adding ASSERT Constraints\n" << smtProblem << "\n&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&\n";
118 //printf("[%s]\n", assert);
119 } else if (retval == 2) {
123 vartable->resetAndDeleteKeys();
125 cleanAndFreeOrderRecVector();
127 ordertable = new HashtableIW();
128 addVarConstraintToSMTProblem(smtProblem, varconstraints);
130 sat = readuntilend(satend);
131 createSATtuneDumps(assert, sat, varconstraints, smtID);
132 addSATConstraintToSMTProblem(smtProblem, sat);
134 dumpSMTproblem(smtProblem, smtID);
136 //cout << "INFO: SMTProblem After adding SAT Constraints\n" << smtProblem << "\n&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&\n";
137 } else if (retval == 3) {
138 var = readuntilend(varend);
139 varconstraints.push(var);
144 char trueString [] = "true";
145 ordertable = new HashtableIW();
146 createSATtuneDumps(assert, trueString, varconstraints, smtID);
147 addSATConstraintToSMTProblem(smtProblem, trueString);
150 dumpSMTproblem(smtProblem, smtID);
152 cleanAndFreeOrderRecVector();
153 if(ordertable != NULL){
162 vartable->resetAndDeleteKeys();
168 void createSATtuneDumps (char *assert, char *sat, Vector<char *> & varconstraints, long long &smtID){
169 CSolver *solver = new CSolver();
170 // solver->turnoffOptimizations();
171 set = solver->createMutableSet(1);
172 order = solver->createOrder(SATC_TOTAL, (Set *) set);
174 processEquality(sat, offset);
176 processEquality(assert, offset);
178 solver->addConstraint(parseConstraint(solver, sat, offset));
180 solver->addConstraint(parseConstraint(solver, assert, offset));
181 for(uint i=0; i<varconstraints.getSize(); i++){
183 processEquality(varconstraints.get(i),offset);
185 solver->addConstraint(parseConstraint(solver, varconstraints.get(i), offset));
187 //printf("[%s]\n", sat);
188 solver->finalizeMutableSet(set);
190 //solver->printConstraints();
191 smtID= getTimeNano();
192 renameDumpFile("./", smtID);
197 void doExit(const char * message){
198 printf("%s", message);
203 doExit("Parse Error\n");
206 void renameDumpFile(const char *path, long long id) {
207 struct dirent *entry;
208 DIR *dir = opendir(path);
212 char newname[128] ={0};
213 sprintf(newname, "%lld.dump", id);
214 bool duplicate = false;
215 while ((entry = readdir(dir)) != NULL) {
216 if(strstr(entry->d_name, "DUMP") != NULL){
218 doExit("Multiplle DUMP file exists. Make sure to clean them all before running the program");
220 int result= rename( entry->d_name , newname );
222 printf ( "File successfully renamed to %s\n" , newname);
224 doExit( "Error renaming file" );
230 template <class MyType>
231 string to_string(MyType value){
233 std::stringstream strstream;
239 void dumpDeclarations(std::ofstream& smtfile){
240 HashsetIWIterator* iterator = intSet->iterator();
241 smtfile << "(set-logic QF_LRA)" << endl;
242 while(iterator->hasNext()){
243 intwrapper * iw = iterator->next();
244 string declare = "(declare-const O!"+ to_string<uint32_t>(iw->value) + " Real)\n";
249 iterator = boolSet->iterator();
250 while(iterator->hasNext()){
251 intwrapper * iw = iterator->next();
252 string declare = "(declare-const S!" + to_string<uint32_t>(iw->value) + " Bool)\n";
259 void addVarConstraintToSMTProblem(string & smtProblem, Vector<char *> & varconstraints){
260 for(uint i=0; i<varconstraints.getSize(); i++){
261 //cout << "[ " << varconstraints.get(i) << " ]" << endl;
262 smtProblem += "(assert "+ string(varconstraints.get(i)) +")\n";
266 void addASSERTConstraintToSMTProblem(string & smtProblem, char * assert){
268 string assertStatement = "(assert "+ ssat + "\n)\n";
269 smtProblem += assertStatement;
272 void addSATConstraintToSMTProblem(string &smtProblem, char * sat){
276 satStatement = "(push)\n(assert "+ ssat + "\n)\n(check-sat)\n(pop)\n";
278 satStatement = "(assert "+ ssat + "\n)\n(check-sat)\n";
280 smtProblem += satStatement;
284 void dumpSMTproblem(string &smtProblem, long long id){
285 std::ofstream smtfile;
286 string smtfilename = to_string<long long>(id) + ".smt";
287 smtfile.open (smtfilename.c_str());
288 if(!smtfile.is_open())
290 doExit("Unable to create file.\n");
292 dumpDeclarations(smtfile);
293 smtfile << smtProblem;
295 cout <<"************here is the SMT file*********" << endl << smtProblem <<endl << "****************************" << endl;;
299 void skipwhitespace(char * constraint, int & offset) {
301 while (constraint[offset] == ' ' || constraint[offset] == '\n')
305 int32_t getOrderVar(char *constraint, int & offset) {
306 if (constraint[offset++] != 'O' || constraint[offset++] != '!' ) {
311 char next = constraint[offset];
312 if (next >= '0' && next <= '9') {
313 num = (num * 10) + (next - '0');
320 int32_t getBooleanVar(char *constraint, int & offset) {
321 if (constraint[offset++] != 'S' || constraint[offset++] != '!' ) {
322 cout << "Constraint= " << constraint << "\tconstraint[offset=" << offset - 1 << "]" << &constraint[offset -1] <<"\n";
327 char next = constraint[offset];
328 if (next >= '0' && next <= '9') {
329 num = (num * 10) + (next - '0');
336 BooleanEdge checkBooleanVar(CSolver *solver, int32_t value) {
338 if (vartable->contains(&v)) {
339 return BooleanEdge(vartable->get(&v));
341 Boolean* ve = solver->getBooleanVar(2).getBoolean();
342 vartable->put(new intwrapper(value), ve);
343 return BooleanEdge(ve);
347 void mergeVars(int32_t value1, int32_t value2) {
348 intwrapper v1(value1);
349 intwrapper v2(value2);
350 OrderRec *r1 = ordertable->get(&v1);
351 OrderRec *r2 = ordertable->get(&v2);
354 OrderRec * r = new OrderRec();
355 orderRecVector->push(r);
357 r->set = new HashsetIW();
358 intwrapper * k1 = new intwrapper(v1);
359 intwrapper * k2 = new intwrapper(v2);
362 ordertable->put(k1, r);
363 ordertable->put(k2, r);
365 } else if (r1 == NULL) {
366 intwrapper * k = new intwrapper(v1);
367 ordertable->put(k, r2);
369 } else if (r2 == NULL) {
370 intwrapper * k = new intwrapper(v2);
371 ordertable->put(k, r1);
374 SetIterator<intwrapper *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> * it1 = r1->set->iterator();
375 while (it1->hasNext()) {
376 intwrapper * k = it1->next();
377 ordertable->put(k, r2);
387 int32_t checkordervar(CSolver * solver, int32_t value) {
389 OrderRec * rec = ordertable->get(&v);
391 intwrapper * k = new intwrapper(value);
392 rec = new OrderRec();
393 orderRecVector->push(rec);
395 rec->set = new HashsetIW();
397 ordertable->put(k, rec);
400 solver->addItem(set, rec->value);
406 void processLetExpression (char * constraint){
407 int constrSize = strlen(constraint);
408 char * replace = (char *) malloc(constrSize);
409 for (int i=0; i< constrSize; i++){
414 skipwhitespace(constraint, offset);
415 ASSERT(strncmp(&constraint[offset], "((a!1",5) == 0);
417 skipwhitespace(constraint, offset);
418 int startOffset = offset;
419 processEquality(constraint, offset);
420 strncpy(replace, &constraint[startOffset], offset-startOffset);
421 while(constraint[offset] == ')')
423 skipwhitespace(constraint, offset);
424 string modified = "";
425 while(offset < constrSize){
427 while(strncmp(&constraint[offset], "a!1",3) != 0){
428 modified += constraint[offset++];
429 if(offset >= constrSize -2){ //Not considering ) and \n ...
430 ASSERT(constraint[constrSize-1] == '\n');
431 ASSERT(constraint[constrSize-2] == ')');
442 strcpy(constraint, modified.c_str());
443 cout << "modified:*****" << modified << "****\n";
447 void processEquality(char * constraint, int &offset) {
448 skipwhitespace(constraint, offset);
449 if (strncmp(&constraint[offset], "(and",4) == 0) {
451 Vector<BooleanEdge> vec;
453 skipwhitespace(constraint, offset);
454 if (constraint[offset] == ')') {
458 processEquality(constraint, offset);
460 } else if (strncmp(&constraint[offset], "(or",3) == 0) {
462 Vector<BooleanEdge> vec;
464 skipwhitespace(constraint, offset);
465 if (constraint[offset] == ')') {
469 processEquality(constraint, offset);
471 } else if (strncmp(&constraint[offset], "(let",4) == 0){
473 cout << "Before: " << constraint << endl;
474 processLetExpression(constraint);
475 cout << "After: " << constraint << endl;
477 processEquality(constraint, offset);
478 } else if (strncmp(&constraint[offset], "(=>",3) == 0){
480 skipwhitespace(constraint, offset);
481 processEquality(constraint, offset);
482 skipwhitespace(constraint, offset);
483 processEquality(constraint, offset);
484 skipwhitespace(constraint, offset);
485 if (constraint[offset++] != ')'){
489 } else if (strncmp(&constraint[offset], "(<", 2) == 0) {
491 skipwhitespace(constraint, offset);
492 getOrderVar(constraint, offset);
493 skipwhitespace(constraint, offset);
494 getOrderVar(constraint, offset);
495 skipwhitespace(constraint, offset);
496 if (constraint[offset++] != ')'){
500 } else if (strncmp(&constraint[offset], "(=", 2) == 0) {
502 skipwhitespace(constraint, offset);
503 int v1=getOrderVar(constraint, offset);
505 if(intSet->get(&iwv1) == NULL){
506 intSet->add(new intwrapper(v1));
508 skipwhitespace(constraint, offset);
509 int v2=getOrderVar(constraint, offset);
511 if(intSet->get(&iwv2) == NULL){
512 intSet->add(new intwrapper(v2));
514 skipwhitespace(constraint, offset);
515 if (constraint[offset++] != ')')
519 } else if (strncmp(&constraint[offset], "tr", 2) == 0){
521 skipwhitespace(constraint, offset);
525 int32_t b1 = getBooleanVar(constraint, offset);
527 if(boolSet->get(&iwb1) == NULL){
528 boolSet->add(new intwrapper(b1));
530 skipwhitespace(constraint, offset);
535 BooleanEdge parseConstraint(CSolver * solver, char * constraint, int & offset) {
536 skipwhitespace(constraint, offset);
537 if (strncmp(&constraint[offset], "(and", 4) == 0) {
539 Vector<BooleanEdge> vec;
541 skipwhitespace(constraint, offset);
542 if (constraint[offset] == ')') {
544 return solver->applyLogicalOperation(SATC_AND, vec.expose(), vec.getSize());
546 vec.push(parseConstraint(solver, constraint, offset));
548 } else if (strncmp(&constraint[offset], "(or", 3) == 0) {
550 Vector<BooleanEdge> vec;
552 skipwhitespace(constraint, offset);
553 if (constraint[offset] == ')') {
555 return solver->applyLogicalOperation(SATC_OR, vec.expose(), vec.getSize());
557 vec.push(parseConstraint(solver, constraint, offset));
559 } else if (strncmp(&constraint[offset], "(=>", 3) == 0){
561 skipwhitespace(constraint, offset);
562 BooleanEdge b1 = parseConstraint(solver, constraint, offset);
563 skipwhitespace(constraint, offset);
564 BooleanEdge b2 = parseConstraint(solver, constraint, offset);
565 skipwhitespace(constraint, offset);
566 if (constraint[offset++] != ')')
568 return solver->applyLogicalOperation(SATC_IMPLIES, b1, b2);
569 } else if (strncmp(&constraint[offset], "(<", 2) == 0) {
571 skipwhitespace(constraint, offset);
572 int32_t v1 = getOrderVar(constraint, offset);
574 if(intSet->get(&iwv1) == NULL){
575 intSet->add(new intwrapper(v1));
577 skipwhitespace(constraint, offset);
578 int32_t v2 = getOrderVar(constraint, offset);
580 if(intSet->get(&iwv2) == NULL){
581 intSet->add(new intwrapper(v2));
583 skipwhitespace(constraint, offset);
584 if (constraint[offset++] != ')')
586 // int32_t o1 = checkordervar(solver, v1);
587 // int32_t o2 = checkordervar(solver, v2);
588 // cout << "V1=" << v1 << ",V2=" << v2 << ",O1=" << o1 << ",O2=" << o2<< endl;
589 // ASSERT( o1 != o2);
590 return solver->orderConstraint(order, checkordervar(solver, v1), checkordervar(solver, v2));
591 } else if (strncmp(&constraint[offset], "(=", 2) == 0) {
593 skipwhitespace(constraint, offset);
594 getOrderVar(constraint, offset);
595 skipwhitespace(constraint, offset);
596 getOrderVar(constraint, offset);
597 skipwhitespace(constraint, offset);
598 if (constraint[offset++] != ')')
600 return solver->getBooleanTrue();
601 }else if (strncmp(&constraint[offset], "tr", 2) == 0){
603 skipwhitespace(constraint, offset);
604 return solver->getBooleanTrue();
607 int32_t v = getBooleanVar(constraint, offset);
609 if(boolSet->get(&iwb1) == NULL){
610 boolSet->add(new intwrapper(v));
612 skipwhitespace(constraint, offset);
613 return checkBooleanVar(solver, v);
617 int skipahead(const char * token1, const char * token2, const char * token3) {
618 int index1 = 0, index2 = 0, index3 = 0;
621 if (token1[index1] == 0)
623 if (token2[index2] == 0)
625 if (token3[index3] == 0)
629 file->read(buffer, 1);
630 if (buffer[0] == token1[index1])
634 if (buffer[0] == token2[index2])
638 if (buffer[0] == token3[index3])
645 char * readuntilend(const char * token) {
650 char * outbuffer = (char *) malloc(length);
652 if (token[index] == 0) {
653 outbuffer[offset - index] = 0;
661 file->read(buffer, 1);
662 outbuffer[offset++] = buffer[0];
663 if (offset == length) {
665 outbuffer = (char *) realloc(outbuffer, length);
667 if (buffer[0] == token[index])