Dump Inceremental SMT + Using Real logic instead of Int

diff --git a/src/Test/dirkreader.cc b/src/Test/dirkreader.cc
index 7daa46bd15e0fdd10a5bd7291a296aa98369d45e..e5414b0aea5d78b007be3769e6c399dd5c38cf48 100644 (file)
--- a/src/Test/dirkreader.cc
+++ b/src/Test/dirkreader.cc
@@ -17,7 +17,11 @@ int skipahead(const char * token1, const char * token2);
 char * readuntilend(const char * token);
 BooleanEdge parseConstraint(CSolver * solver, char * constraint, int & offset);
 void processEquality(char * constraint, int &offset);
 char * readuntilend(const char * token);
 BooleanEdge parseConstraint(CSolver * solver, char * constraint, int & offset);
 void processEquality(char * constraint, int &offset);

-void dumpSMTproblem(char * sat, char * assert);
+void dumpSMTproblem(string &smtProblem, long long id);
+void renameDumpFile(const char *path, long long id);
+void addASSERTConstraintToSMTProblem(string & smtProblem, char * assert);
+void addSATConstraintToSMTProblem(string &smtProblem, char * sat);
+void createSATtuneDumps (char *assert, char *sat, long long &smtID);

 
 std::ifstream * file;
 Order * order;
 
 std::ifstream * file;
 Order * order;


@@ -73,6 +77,8 @@ int main(int numargs, char ** argv) {
   file = new std::ifstream(argv[1]);
   char * assert = NULL;
   char * sat = NULL;
   file = new std::ifstream(argv[1]);
   char * assert = NULL;
   char * sat = NULL;

+  string smtProblem = "";
+  long long smtID=0L;

   Vector<OrderRec*> orderRecs;
   orderRecVector = &orderRecs;
   while(true) {
   Vector<OrderRec*> orderRecs;
   orderRecVector = &orderRecs;
   while(true) {


@@ -85,8 +91,14 @@ int main(int numargs, char ** argv) {
       if (assert != NULL){
        free(assert);
        assert = NULL;
       if (assert != NULL){
        free(assert);
        assert = NULL;

+       dumpSMTproblem(smtProblem, smtID);
+       smtProblem = "";
+       intSet->reset();
+       boolSet->reset();

       }
       assert = readuntilend(assertend);
       }
       assert = readuntilend(assertend);

+      addASSERTConstraintToSMTProblem(smtProblem, assert);
+      //cout << "INFO: SMTProblem After adding ASSERT Constraints\n" << smtProblem << "\n&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&\n";

       printf("[%s]\n", assert);
     } else if (retval == 2) {
       if (sat != NULL) {
       printf("[%s]\n", assert);
     } else if (retval == 2) {
       if (sat != NULL) {


@@ -99,27 +111,19 @@ int main(int numargs, char ** argv) {
        ordertable = new HashtableIW();
       }
       sat = readuntilend(satend);
        ordertable = new HashtableIW();
       }
       sat = readuntilend(satend);

-      CSolver *solver = new CSolver();
-      solver->turnoffOptimizations();
-      set = solver->createMutableSet(1);
-      order = solver->createOrder(SATC_TOTAL, (Set *) set);
-      int offset = 0;
-      processEquality(sat, offset);
-      offset = 0;
-      processEquality(assert, offset);
-      offset = 0;
-      solver->addConstraint(parseConstraint(solver, sat, offset));
-      offset = 0;
-      solver->addConstraint(parseConstraint(solver, assert, offset));
-      printf("[%s]\n", sat);
-      solver->finalizeMutableSet(set);
-      solver->serialize();
-      solver->printConstraints();
-      dumpSMTproblem(sat, assert);
-      delete solver;
+      createSATtuneDumps(assert, sat, smtID);
+      addSATConstraintToSMTProblem(smtProblem, sat);
+      //cout << "INFO: SMTProblem After adding SAT Constraints\n" << smtProblem << "\n&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&\n";

     }
   }
     }
   }

-
+  
+  if(smtID == 0L){
+       char trueString [] = "true";
+       ordertable = new HashtableIW();
+       createSATtuneDumps(assert, trueString, smtID);
+       addSATConstraintToSMTProblem(smtProblem, trueString);
+  }
+  dumpSMTproblem(smtProblem, smtID);

   cleanAndFreeOrderRecVector();
   if(ordertable != NULL){
        delete ordertable;
   cleanAndFreeOrderRecVector();
   if(ordertable != NULL){
        delete ordertable;


@@ -136,6 +140,28 @@ int main(int numargs, char ** argv) {
   delete file;
 }
 
   delete file;
 }
 

+void createSATtuneDumps (char *assert, char *sat, long long &smtID){
+       CSolver *solver = new CSolver();
+       solver->turnoffOptimizations();
+       set = solver->createMutableSet(1);
+       order = solver->createOrder(SATC_TOTAL, (Set *) set);
+       int offset = 0;
+       processEquality(sat, offset);
+       offset = 0;
+       processEquality(assert, offset);
+       offset = 0;
+       solver->addConstraint(parseConstraint(solver, sat, offset));
+       offset = 0;
+       solver->addConstraint(parseConstraint(solver, assert, offset));
+       printf("[%s]\n", sat);
+       solver->finalizeMutableSet(set);
+       solver->serialize();
+       solver->printConstraints();
+       smtID= getTimeNano();
+       renameDumpFile("./", smtID);
+       delete solver;
+}
+

 void doExit(const char * message){
        printf("%s", message);
        exit(-1);
 void doExit(const char * message){
        printf("%s", message);
        exit(-1);


@@ -180,9 +206,10 @@ string to_string(MyType value){
 
 void dumpDeclarations(std::ofstream& smtfile){
        HashsetIWIterator* iterator = intSet->iterator();
 
 void dumpDeclarations(std::ofstream& smtfile){
        HashsetIWIterator* iterator = intSet->iterator();

+       smtfile << "(set-logic QF_LRA)" << endl;

        while(iterator->hasNext()){
                intwrapper * iw = iterator->next();
        while(iterator->hasNext()){
                intwrapper * iw = iterator->next();

-               string declare = "(declare-const O!"+ to_string<uint32_t>(iw->value) + " Int)\n";
+               string declare = "(declare-const O!"+ to_string<uint32_t>(iw->value) + " Real)\n";

                smtfile << declare;
        }
        delete iterator;
                smtfile << declare;
        }
        delete iterator;


@@ -196,35 +223,34 @@ void dumpDeclarations(std::ofstream& smtfile){
         delete iterator;
 }
 
         delete iterator;
 }
 

-void dumpFooter(std::ofstream& smtfile){
-       smtfile << "(check-sat)" << endl;
+void addASSERTConstraintToSMTProblem(string & smtProblem, char * assert){
+       string ssat(assert);
+       string assertStatement = "(assert "+ ssat + "\n)\n";
+       smtProblem += assertStatement;

 }
 
 }
 

+void addSATConstraintToSMTProblem(string &smtProblem, char * sat){
+       string ssat(sat);
+        string satStatement = "(push)\n(assert "+ ssat + "\n)\n(check-sat)\n(get-model)\n(pop)\n";
+        smtProblem += satStatement;
+}

 
 
 
 

-void dumpSMTproblem(char * sat, char * assert){
-       long long id = getTimeNano();
-       cout << "Here's the ID= " << id << endl;
-       cout <<"************here is the SMT file*********" << endl << sat << endl << assert <<endl << "****************************" << endl;;
-       renameDumpFile("./", id);
-       string smtfilename = to_string<long long>(id) + ".smt";
+void dumpSMTproblem(string &smtProblem, long long id){

        std::ofstream smtfile;
        std::ofstream smtfile;

-       smtfile.open (smtfilename.c_str());
-       if(!smtfile.is_open())
-       {
-               doExit("Unable to create file.\n");
-       }
+       string smtfilename = to_string<long long>(id) + ".smt";
+        smtfile.open (smtfilename.c_str());
+        if(!smtfile.is_open())
+        {
+                doExit("Unable to create file.\n");
+        }

        dumpDeclarations(smtfile);
        dumpDeclarations(smtfile);

-       string ssat(sat);
-       string satStatement = "(assert "+ ssat + "\n)\n";
-       smtfile << satStatement;
-       string sassert(assert);
-       string assertStatement = "(assert " + sassert + "\n)\n";
-       smtfile << assertStatement;
-       dumpFooter(smtfile);
+       smtfile << smtProblem;

        smtfile.close();
        smtfile.close();

+       cout <<"************here is the SMT file*********" << endl << smtProblem  <<endl << "****************************" << endl;;

 }
 
 }
 

+

 void skipwhitespace(char * constraint, int & offset) {
   //skip whitespace
   while (constraint[offset] == ' ' || constraint[offset] == '\n')
 void skipwhitespace(char * constraint, int & offset) {
   //skip whitespace
   while (constraint[offset] == ' ' || constraint[offset] == '\n')