11 const char * assertstart = "ASSERTSTART";
12 const char * assertend = "ASSERTEND";
13 const char * satstart = "SATSTART";
14 const char * satend = "SATEND";
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(string &smtProblem, long long id);
21 void renameDumpFile(const char *path, long long id);
22 void addASSERTConstraintToSMTProblem(string & smtProblem, char * assert);
23 void addSATConstraintToSMTProblem(string &smtProblem, char * sat);
24 void createSATtuneDumps (char *assert, char *sat, long long &smtID);
31 intwrapper(int _val) : value(_val) {
36 unsigned int iw_hash_function(intwrapper *i) {
40 bool iw_equals(intwrapper *key1, intwrapper *key2) {
41 return (key1->value == key2->value);
44 typedef Hashset<intwrapper *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashsetIW;
45 typedef SetIterator<intwrapper *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashsetIWIterator;
48 OrderRec() : set (NULL), value(-1), alloced(false) {
52 set->resetAndDelete();
61 typedef Hashtable<intwrapper *, OrderRec *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashtableIW;
62 typedef Hashtable<intwrapper *, Boolean *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashtableBV;
63 Vector<OrderRec*> * orderRecVector = NULL;
64 HashtableIW * ordertable = NULL;
65 HashtableBV * vartable = new HashtableBV();
66 HashsetIW * intSet = new HashsetIW();
67 HashsetIW * boolSet = new HashsetIW();
69 void cleanAndFreeOrderRecVector(){
70 for(uint i=0; i< orderRecVector->getSize(); i++){
71 delete orderRecVector->get(i);
73 orderRecVector->clear();
76 int main(int numargs, char ** argv) {
77 file = new std::ifstream(argv[1]);
80 string smtProblem = "";
82 Vector<OrderRec*> orderRecs;
83 orderRecVector = &orderRecs;
85 int retval = skipahead(assertstart, satstart);
86 printf("%d\n", retval);
94 dumpSMTproblem(smtProblem, smtID);
99 assert = readuntilend(assertend);
100 addASSERTConstraintToSMTProblem(smtProblem, assert);
101 //cout << "INFO: SMTProblem After adding ASSERT Constraints\n" << smtProblem << "\n&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&\n";
102 printf("[%s]\n", assert);
103 } else if (retval == 2) {
107 vartable->resetAndDeleteKeys();
109 cleanAndFreeOrderRecVector();
111 ordertable = new HashtableIW();
113 sat = readuntilend(satend);
114 createSATtuneDumps(assert, sat, smtID);
115 addSATConstraintToSMTProblem(smtProblem, sat);
116 //cout << "INFO: SMTProblem After adding SAT Constraints\n" << smtProblem << "\n&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&\n";
121 char trueString [] = "true";
122 ordertable = new HashtableIW();
123 createSATtuneDumps(assert, trueString, smtID);
124 addSATConstraintToSMTProblem(smtProblem, trueString);
126 dumpSMTproblem(smtProblem, smtID);
127 cleanAndFreeOrderRecVector();
128 if(ordertable != NULL){
137 vartable->resetAndDeleteKeys();
143 void createSATtuneDumps (char *assert, char *sat, long long &smtID){
144 CSolver *solver = new CSolver();
145 solver->turnoffOptimizations();
146 set = solver->createMutableSet(1);
147 order = solver->createOrder(SATC_TOTAL, (Set *) set);
149 processEquality(sat, offset);
151 processEquality(assert, offset);
153 solver->addConstraint(parseConstraint(solver, sat, offset));
155 solver->addConstraint(parseConstraint(solver, assert, offset));
156 printf("[%s]\n", sat);
157 solver->finalizeMutableSet(set);
159 solver->printConstraints();
160 smtID= getTimeNano();
161 renameDumpFile("./", smtID);
165 void doExit(const char * message){
166 printf("%s", message);
171 doExit("Parse Error\n");
174 void renameDumpFile(const char *path, long long id) {
175 struct dirent *entry;
176 DIR *dir = opendir(path);
180 char newname[128] ={0};
181 sprintf(newname, "%lld.dump", id);
182 bool duplicate = false;
183 while ((entry = readdir(dir)) != NULL) {
184 if(strstr(entry->d_name, "DUMP") != NULL){
186 doExit("Multiplle DUMP file exists. Make sure to clean them all before running the program");
188 int result= rename( entry->d_name , newname );
190 printf ( "File successfully renamed to %s\n" , newname);
192 doExit( "Error renaming file" );
198 template <class MyType>
199 string to_string(MyType value){
201 std::stringstream strstream;
207 void dumpDeclarations(std::ofstream& smtfile){
208 HashsetIWIterator* iterator = intSet->iterator();
209 smtfile << "(set-logic QF_LRA)" << endl;
210 while(iterator->hasNext()){
211 intwrapper * iw = iterator->next();
212 string declare = "(declare-const O!"+ to_string<uint32_t>(iw->value) + " Real)\n";
217 iterator = boolSet->iterator();
218 while(iterator->hasNext()){
219 intwrapper * iw = iterator->next();
220 string declare = "(declare-const S!" + to_string<uint32_t>(iw->value) + " Bool)\n";
226 void addASSERTConstraintToSMTProblem(string & smtProblem, char * assert){
228 string assertStatement = "(assert "+ ssat + "\n)\n";
229 smtProblem += assertStatement;
232 void addSATConstraintToSMTProblem(string &smtProblem, char * sat){
234 string satStatement = "(push)\n(assert "+ ssat + "\n)\n(check-sat)\n(get-model)\n(pop)\n";
235 smtProblem += satStatement;
239 void dumpSMTproblem(string &smtProblem, long long id){
240 std::ofstream smtfile;
241 string smtfilename = to_string<long long>(id) + ".smt";
242 smtfile.open (smtfilename.c_str());
243 if(!smtfile.is_open())
245 doExit("Unable to create file.\n");
247 dumpDeclarations(smtfile);
248 smtfile << smtProblem;
250 cout <<"************here is the SMT file*********" << endl << smtProblem <<endl << "****************************" << endl;;
254 void skipwhitespace(char * constraint, int & offset) {
256 while (constraint[offset] == ' ' || constraint[offset] == '\n')
260 int32_t getOrderVar(char *constraint, int & offset) {
261 if (constraint[offset++] != 'O' || constraint[offset++] != '!' ) {
266 char next = constraint[offset];
267 if (next >= '0' && next <= '9') {
268 num = (num * 10) + (next - '0');
275 int32_t getBooleanVar(char *constraint, int & offset) {
276 if (constraint[offset++] != 'S' || constraint[offset++] != '!' ) {
277 cout << "Constraint= " << constraint << "\toffset=" << constraint[offset - 1] << " ******\n";
282 char next = constraint[offset];
283 if (next >= '0' && next <= '9') {
284 num = (num * 10) + (next - '0');
291 BooleanEdge checkBooleanVar(CSolver *solver, int32_t value) {
293 if (vartable->contains(&v)) {
294 return BooleanEdge(vartable->get(&v));
296 Boolean* ve = solver->getBooleanVar(2).getBoolean();
297 vartable->put(new intwrapper(value), ve);
298 return BooleanEdge(ve);
302 void mergeVars(int32_t value1, int32_t value2) {
303 intwrapper v1(value1);
304 intwrapper v2(value2);
305 OrderRec *r1 = ordertable->get(&v1);
306 OrderRec *r2 = ordertable->get(&v2);
309 OrderRec * r = new OrderRec();
310 orderRecVector->push(r);
312 r->set = new HashsetIW();
313 intwrapper * k1 = new intwrapper(v1);
314 intwrapper * k2 = new intwrapper(v2);
317 ordertable->put(k1, r);
318 ordertable->put(k2, r);
320 } else if (r1 == NULL) {
321 intwrapper * k = new intwrapper(v1);
322 ordertable->put(k, r2);
324 } else if (r2 == NULL) {
325 intwrapper * k = new intwrapper(v2);
326 ordertable->put(k, r1);
329 SetIterator<intwrapper *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> * it1 = r1->set->iterator();
330 while (it1->hasNext()) {
331 intwrapper * k = it1->next();
332 ordertable->put(k, r2);
342 int32_t checkordervar(CSolver * solver, int32_t value) {
344 OrderRec * rec = ordertable->get(&v);
346 intwrapper * k = new intwrapper(value);
347 rec = new OrderRec();
348 orderRecVector->push(rec);
350 rec->set = new HashsetIW();
352 ordertable->put(k, rec);
355 solver->addItem(set, rec->value);
361 void processEquality(char * constraint, int &offset) {
362 skipwhitespace(constraint, offset);
363 if (strncmp(&constraint[offset], "(and",4) == 0) {
365 Vector<BooleanEdge> vec;
367 skipwhitespace(constraint, offset);
368 if (constraint[offset] == ')') {
372 processEquality(constraint, offset);
374 } else if (strncmp(&constraint[offset], "(<", 2) == 0) {
376 skipwhitespace(constraint, offset);
377 getOrderVar(constraint, offset);
378 skipwhitespace(constraint, offset);
379 getOrderVar(constraint, offset);
380 skipwhitespace(constraint, offset);
381 if (constraint[offset++] != ')'){
385 } else if (strncmp(&constraint[offset], "(=", 2) == 0) {
387 skipwhitespace(constraint, offset);
388 int v1=getOrderVar(constraint, offset);
390 if(intSet->get(&iwv1) == NULL){
391 intSet->add(new intwrapper(v1));
393 skipwhitespace(constraint, offset);
394 int v2=getOrderVar(constraint, offset);
396 if(intSet->get(&iwv2) == NULL){
397 intSet->add(new intwrapper(v2));
399 skipwhitespace(constraint, offset);
400 if (constraint[offset++] != ')')
404 } else if (strncmp(&constraint[offset], "tr", 2) == 0){
406 skipwhitespace(constraint, offset);
410 int32_t b1 = getBooleanVar(constraint, offset);
412 if(boolSet->get(&iwb1) == NULL){
413 boolSet->add(new intwrapper(b1));
415 skipwhitespace(constraint, offset);
420 BooleanEdge parseConstraint(CSolver * solver, char * constraint, int & offset) {
421 skipwhitespace(constraint, offset);
422 if (strncmp(&constraint[offset], "(and", 4) == 0) {
424 Vector<BooleanEdge> vec;
426 skipwhitespace(constraint, offset);
427 if (constraint[offset] == ')') {
429 return solver->applyLogicalOperation(SATC_AND, vec.expose(), vec.getSize());
431 vec.push(parseConstraint(solver, constraint, offset));
433 } else if (strncmp(&constraint[offset], "(<", 2) == 0) {
435 skipwhitespace(constraint, offset);
436 int32_t v1 = getOrderVar(constraint, offset);
438 if(intSet->get(&iwv1) == NULL){
439 intSet->add(new intwrapper(v1));
441 skipwhitespace(constraint, offset);
442 int32_t v2 = getOrderVar(constraint, offset);
444 if(intSet->get(&iwv2) == NULL){
445 intSet->add(new intwrapper(v2));
447 skipwhitespace(constraint, offset);
448 if (constraint[offset++] != ')')
450 return solver->orderConstraint(order, checkordervar(solver, v1), checkordervar(solver, v2));
451 } else if (strncmp(&constraint[offset], "(=", 2) == 0) {
453 skipwhitespace(constraint, offset);
454 getOrderVar(constraint, offset);
455 skipwhitespace(constraint, offset);
456 getOrderVar(constraint, offset);
457 skipwhitespace(constraint, offset);
458 if (constraint[offset++] != ')')
460 return solver->getBooleanTrue();
461 }else if (strncmp(&constraint[offset], "tr", 2) == 0){
463 skipwhitespace(constraint, offset);
464 return solver->getBooleanTrue();
467 int32_t v = getBooleanVar(constraint, offset);
469 if(boolSet->get(&iwb1) == NULL){
470 boolSet->add(new intwrapper(v));
472 skipwhitespace(constraint, offset);
473 return checkBooleanVar(solver, v);
477 int skipahead(const char * token1, const char * token2) {
478 int index1 = 0, index2 = 0;
481 if (token1[index1] == 0)
483 if (token2[index2] == 0)
487 file->read(buffer, 1);
488 if (buffer[0] == token1[index1])
492 if (buffer[0] == token2[index2])
499 char * readuntilend(const char * token) {
504 char * outbuffer = (char *) malloc(length);
506 if (token[index] == 0) {
507 outbuffer[offset - index] = 0;
515 file->read(buffer, 1);
516 outbuffer[offset++] = buffer[0];
517 if (offset == length) {
519 outbuffer = (char *) realloc(outbuffer, length);
521 if (buffer[0] == token[index])