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(char * sat, char * assert);
27 intwrapper(int _val) : value(_val) {
32 unsigned int iw_hash_function(intwrapper *i) {
36 bool iw_equals(intwrapper *key1, intwrapper *key2) {
37 return (key1->value == key2->value);
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;
44 OrderRec() : set (NULL), value(-1), alloced(false) {
48 set->resetAndDelete();
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();
65 void cleanAndFreeOrderRecVector(){
66 for(uint i=0; i< orderRecVector->getSize(); i++){
67 delete orderRecVector->get(i);
69 orderRecVector->clear();
72 int main(int numargs, char ** argv) {
73 file = new std::ifstream(argv[1]);
76 Vector<OrderRec*> orderRecs;
77 orderRecVector = &orderRecs;
79 int retval = skipahead(assertstart, satstart);
80 printf("%d\n", retval);
89 assert = readuntilend(assertend);
90 printf("[%s]\n", assert);
91 } else if (retval == 2) {
95 vartable->resetAndDeleteKeys();
97 cleanAndFreeOrderRecVector();
99 ordertable = new HashtableIW();
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);
107 processEquality(sat, offset);
109 processEquality(assert, offset);
111 solver->addConstraint(parseConstraint(solver, sat, offset));
113 solver->addConstraint(parseConstraint(solver, assert, offset));
114 printf("[%s]\n", sat);
115 solver->finalizeMutableSet(set);
117 solver->printConstraints();
118 dumpSMTproblem(sat, assert);
123 cleanAndFreeOrderRecVector();
124 if(ordertable != NULL){
133 vartable->resetAndDeleteKeys();
139 void doExit(const char * message){
140 printf("%s", message);
145 doExit("Parse Error\n");
148 void renameDumpFile(const char *path, long long id) {
149 struct dirent *entry;
150 DIR *dir = opendir(path);
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){
160 doExit("Multiplle DUMP file exists. Make sure to clean them all before running the program");
162 int result= rename( entry->d_name , newname );
164 printf ( "File successfully renamed to %s\n" , newname);
166 doExit( "Error renaming file" );
172 template <class MyType>
173 string to_string(MyType value){
175 std::stringstream strstream;
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";
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";
199 void dumpFooter(std::ofstream& smtfile){
200 smtfile << "(check-sat)" << endl;
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())
215 doExit("Unable to create file.\n");
217 dumpDeclarations(smtfile);
219 string satStatement = "(assert "+ ssat + "\n)\n";
220 smtfile << satStatement;
221 string sassert(assert);
222 string assertStatement = "(assert " + sassert + "\n)\n";
223 smtfile << assertStatement;
228 void skipwhitespace(char * constraint, int & offset) {
230 while (constraint[offset] == ' ' || constraint[offset] == '\n')
234 int32_t getOrderVar(char *constraint, int & offset) {
235 if (constraint[offset++] != 'O' || constraint[offset++] != '!' ) {
240 char next = constraint[offset];
241 if (next >= '0' && next <= '9') {
242 num = (num * 10) + (next - '0');
249 int32_t getBooleanVar(char *constraint, int & offset) {
250 if (constraint[offset++] != 'S' || constraint[offset++] != '!' ) {
251 cout << "Constraint= " << constraint << "\toffset=" << constraint[offset - 1] << " ******\n";
256 char next = constraint[offset];
257 if (next >= '0' && next <= '9') {
258 num = (num * 10) + (next - '0');
265 BooleanEdge checkBooleanVar(CSolver *solver, int32_t value) {
267 if (vartable->contains(&v)) {
268 return BooleanEdge(vartable->get(&v));
270 Boolean* ve = solver->getBooleanVar(2).getBoolean();
271 vartable->put(new intwrapper(value), ve);
272 return BooleanEdge(ve);
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);
283 OrderRec * r = new OrderRec();
284 orderRecVector->push(r);
286 r->set = new HashsetIW();
287 intwrapper * k1 = new intwrapper(v1);
288 intwrapper * k2 = new intwrapper(v2);
291 ordertable->put(k1, r);
292 ordertable->put(k2, r);
294 } else if (r1 == NULL) {
295 intwrapper * k = new intwrapper(v1);
296 ordertable->put(k, r2);
298 } else if (r2 == NULL) {
299 intwrapper * k = new intwrapper(v2);
300 ordertable->put(k, r1);
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);
316 int32_t checkordervar(CSolver * solver, int32_t value) {
318 OrderRec * rec = ordertable->get(&v);
320 intwrapper * k = new intwrapper(value);
321 rec = new OrderRec();
322 orderRecVector->push(rec);
324 rec->set = new HashsetIW();
326 ordertable->put(k, rec);
329 solver->addItem(set, rec->value);
335 void processEquality(char * constraint, int &offset) {
336 skipwhitespace(constraint, offset);
337 if (strncmp(&constraint[offset], "(and",4) == 0) {
339 Vector<BooleanEdge> vec;
341 skipwhitespace(constraint, offset);
342 if (constraint[offset] == ')') {
346 processEquality(constraint, offset);
348 } else if (strncmp(&constraint[offset], "(<", 2) == 0) {
350 skipwhitespace(constraint, offset);
351 getOrderVar(constraint, offset);
352 skipwhitespace(constraint, offset);
353 getOrderVar(constraint, offset);
354 skipwhitespace(constraint, offset);
355 if (constraint[offset++] != ')'){
359 } else if (strncmp(&constraint[offset], "(=", 2) == 0) {
361 skipwhitespace(constraint, offset);
362 int v1=getOrderVar(constraint, offset);
364 if(intSet->get(&iwv1) == NULL){
365 intSet->add(new intwrapper(v1));
367 skipwhitespace(constraint, offset);
368 int v2=getOrderVar(constraint, offset);
370 if(intSet->get(&iwv2) == NULL){
371 intSet->add(new intwrapper(v2));
373 skipwhitespace(constraint, offset);
374 if (constraint[offset++] != ')')
378 } else if (strncmp(&constraint[offset], "tr", 2) == 0){
380 skipwhitespace(constraint, offset);
384 int32_t b1 = getBooleanVar(constraint, offset);
386 if(boolSet->get(&iwb1) == NULL){
387 boolSet->add(new intwrapper(b1));
389 skipwhitespace(constraint, offset);
394 BooleanEdge parseConstraint(CSolver * solver, char * constraint, int & offset) {
395 skipwhitespace(constraint, offset);
396 if (strncmp(&constraint[offset], "(and", 4) == 0) {
398 Vector<BooleanEdge> vec;
400 skipwhitespace(constraint, offset);
401 if (constraint[offset] == ')') {
403 return solver->applyLogicalOperation(SATC_AND, vec.expose(), vec.getSize());
405 vec.push(parseConstraint(solver, constraint, offset));
407 } else if (strncmp(&constraint[offset], "(<", 2) == 0) {
409 skipwhitespace(constraint, offset);
410 int32_t v1 = getOrderVar(constraint, offset);
412 if(intSet->get(&iwv1) == NULL){
413 intSet->add(new intwrapper(v1));
415 skipwhitespace(constraint, offset);
416 int32_t v2 = getOrderVar(constraint, offset);
418 if(intSet->get(&iwv2) == NULL){
419 intSet->add(new intwrapper(v2));
421 skipwhitespace(constraint, offset);
422 if (constraint[offset++] != ')')
424 return solver->orderConstraint(order, checkordervar(solver, v1), checkordervar(solver, v2));
425 } else if (strncmp(&constraint[offset], "(=", 2) == 0) {
427 skipwhitespace(constraint, offset);
428 getOrderVar(constraint, offset);
429 skipwhitespace(constraint, offset);
430 getOrderVar(constraint, offset);
431 skipwhitespace(constraint, offset);
432 if (constraint[offset++] != ')')
434 return solver->getBooleanTrue();
435 }else if (strncmp(&constraint[offset], "tr", 2) == 0){
437 skipwhitespace(constraint, offset);
438 return solver->getBooleanTrue();
441 int32_t v = getBooleanVar(constraint, offset);
443 if(boolSet->get(&iwb1) == NULL){
444 boolSet->add(new intwrapper(v));
446 skipwhitespace(constraint, offset);
447 return checkBooleanVar(solver, v);
451 int skipahead(const char * token1, const char * token2) {
452 int index1 = 0, index2 = 0;
455 if (token1[index1] == 0)
457 if (token2[index2] == 0)
461 file->read(buffer, 1);
462 if (buffer[0] == token1[index1])
466 if (buffer[0] == token2[index2])
473 char * readuntilend(const char * token) {
478 char * outbuffer = (char *) malloc(length);
480 if (token[index] == 0) {
481 outbuffer[offset - index] = 0;
489 file->read(buffer, 1);
490 outbuffer[offset++] = buffer[0];
491 if (offset == length) {
493 outbuffer = (char *) realloc(outbuffer, length);
495 if (buffer[0] == token[index])