Add new test cases plus buffer serialization code

diff --git a/src/Serialize/deserializer.cc b/src/Serialize/deserializer.cc
index c0b8bf4fcddbcc9e6a5c655df31fdf1e3db6d6ca..47de8b1595f2189162fe23fb9ff9c330517617ec 100644 (file)
--- a/src/Serialize/deserializer.cc
+++ b/src/Serialize/deserializer.cc
@@ -15,11 +15,17 @@
 #include "element.h"
 #include "mutableset.h"
 
+#define READBUFFERSIZE 16384
+
 Deserializer::Deserializer(const char *file) :
+       buffer((char *)ourmalloc(READBUFFERSIZE)),
+       bufferindex(0),
+       bufferbytes(0),
+       buffercap(READBUFFERSIZE),
        solver(new CSolver())
 {
        filedesc = open(file, O_RDONLY);
-
+       
        if (filedesc < 0) {
                exit(-1);
        }
@@ -29,10 +35,35 @@ Deserializer::~Deserializer() {
        if (-1 == close(filedesc)) {
                exit(-1);
        }
+       ourfree(buffer);
 }
 
-ssize_t Deserializer::myread(void *__buf, size_t __nbytes) {
-       return read (filedesc, __buf, __nbytes);
+ssize_t Deserializer::myread(void *__buf, size_t bytestoread) {
+       char * out = (char * ) __buf;
+       size_t totalbytesread = 0;
+       while (bytestoread) {
+               if (bufferbytes != 0) {
+                       uint bytestocopy = (bufferbytes > bytestoread) ? bytestoread : bufferbytes;
+                       memcpy(out, &buffer[bufferindex], bytestocopy);
+                       //update local buffer
+                       bufferbytes -= bytestocopy;
+                       bufferindex += bytestocopy;
+                       totalbytesread += bytestocopy;
+                       //update request pointers
+                       out += bytestocopy;
+                       bytestoread -= bytestocopy;
+               } else {
+                       size_t bytesread=read (filedesc, buffer, buffercap);
+                       bufferindex = 0;
+                       bufferbytes = bytesread;
+                       if (bytesread == 0) {
+                               break;
+                       } else if (bytesread < 0) {
+                               exit(-1);
+                       }
+               }
+       }
+       return totalbytesread;
 }
 
 CSolver *Deserializer::deserialize() {

diff --git a/src/Serialize/deserializer.h b/src/Serialize/deserializer.h
index 6335c897c42270ba115a8dc87b5f57f67e4e1b8a..c56911db614d9a065249d02eeb59c32716fb4845 100644 (file)
--- a/src/Serialize/deserializer.h
+++ b/src/Serialize/deserializer.h
@@ -39,6 +39,11 @@ private:
        void deserializeElementFunction();
        void deserializeFunctionOperator();
        void deserializeFunctionTable();
+       char *buffer;
+       uint bufferindex;
+       uint bufferbytes;
+       uint buffercap;
+
        CSolver *solver;
        int filedesc;
        CloneMap map;

diff --git a/src/Serialize/serializer.cc b/src/Serialize/serializer.cc
index 118cf867296a2c680b3b1e55831affaa2a553baf..fe41a39fae91964300180684b02b20e9029e521f 100644 (file)
--- a/src/Serialize/serializer.cc
+++ b/src/Serialize/serializer.cc
@@ -11,33 +11,74 @@
 #include "fcntl.h"
 #include "boolean.h"
 
-Serializer::Serializer(const char *file) {
-       filedesc = open(file, O_WRONLY | O_CREAT | O_TRUNC, 0666);
+#define SERIALBUFFERLENGTH 4096
 
+Serializer::Serializer(const char *file) :
+       buffer((char *) ourmalloc(SERIALBUFFERLENGTH)),
+       bufferoffset(0),
+       bufferlength(SERIALBUFFERLENGTH) {
+       filedesc = open(file, O_WRONLY | O_CREAT | O_TRUNC, 0666);
        if (filedesc < 0) {
                exit(-1);
        }
 }
 
+void Serializer::flushBuffer() {
+       ssize_t datatowrite = bufferoffset;
+       ssize_t index = 0;
+       while(datatowrite) {
+               ssize_t byteswritten = write(filedesc, &buffer[index], datatowrite);
+               if (byteswritten == -1)
+                       exit(-1);
+               datatowrite -= byteswritten;
+               index += byteswritten;
+       }
+       bufferoffset=0;
+}
+
 Serializer::~Serializer() {
+       flushBuffer();
        if (-1 == close(filedesc)) {
                exit(-1);
        }
+       ourfree(buffer);
 }
 
 void Serializer::mywrite(const void *__buf, size_t __n) {
-       write (filedesc, __buf, __n);
+       if (__n > SERIALBUFFERLENGTH *2) {
+               if (bufferoffset != 0)
+                       flushBuffer();
+               write(filedesc, __buf, __n);
+       } else {
+               char *towrite=(char *) __buf;
+               do  {
+                       uint spacefree = bufferlength-bufferoffset;
+                       uint datatowrite = spacefree > __n ? __n : spacefree;
+                       memcpy(&buffer[bufferoffset], towrite, datatowrite);
+                       bufferoffset += datatowrite;
+
+                       if (spacefree < __n) {
+                               flushBuffer();
+                               towrite += datatowrite;
+                       } else if (spacefree == __n) {
+                               flushBuffer();
+                               return;
+                       } else {
+                               return;
+                       }
+               } while(true);
+       }
 }
 
 
 void serializeBooleanEdge(Serializer *serializer, BooleanEdge be, bool isTopLevel) {
-       if (be == BooleanEdge(NULL)){
-                return;
-        }
+       if (be == BooleanEdge(NULL)) {
+               return;
+       }
        be.getBoolean()->serialize(serializer);
        ASTNodeType type = BOOLEANEDGE;
        serializer->mywrite(&type, sizeof(ASTNodeType));
        Boolean *boolean = be.getRaw();
        serializer->mywrite(&boolean, sizeof(Boolean *));
-        serializer->mywrite(&isTopLevel, sizeof(bool));
-}
\ No newline at end of file
+       serializer->mywrite(&isTopLevel, sizeof(bool));
+}

diff --git a/src/Serialize/serializer.h b/src/Serialize/serializer.h
index cf30a55e952494cd6b480aca694a6dcf1797e444..7030438e76c2fb1f3c58a2db712161a1c4f9b09f 100644 (file)
--- a/src/Serialize/serializer.h
+++ b/src/Serialize/serializer.h
@@ -22,6 +22,10 @@ public:
        virtual ~Serializer();
        CMEMALLOC;
 private:
+       void flushBuffer();
+       char * buffer;
+       uint bufferoffset;
+       uint bufferlength;
        int filedesc;
        CloneMap map;
 };

diff --git a/src/Test/deserializersolveprint.cc b/src/Test/deserializersolveprint.cc
new file mode 100755 (executable)
index 0000000..1d1148b
--- /dev/null
+++ b/src/Test/deserializersolveprint.cc
@@ -0,0 +1,21 @@
+#include "csolver.h"
+
+
+int main(int argc, char ** argv){
+       if(argc < 2){
+               printf("You should specify file names ...");
+               exit(-1);       
+       }
+       for(int i = 1; i < argc; i++) {
+               CSolver* solver = CSolver::deserialize(argv[i]);
+               solver->printConstraints();
+               int value=solver->solve();
+               if (value ==1) {
+                       printf("%s is SAT\n", argv[i]);
+               } else {
+                       printf("%s is UNSAT\n", argv[i]);
+               }
+               delete solver;
+       }
+       return 1;
+}

diff --git a/src/Test/deserializersolveprintopt.cc b/src/Test/deserializersolveprintopt.cc
new file mode 100755 (executable)
index 0000000..4e9637d
--- /dev/null
+++ b/src/Test/deserializersolveprintopt.cc
@@ -0,0 +1,22 @@
+#include "csolver.h"
+
+
+int main(int argc, char ** argv){
+       if(argc < 2){
+               printf("You should specify file names ...");
+               exit(-1);       
+       }
+       for(int i = 1; i < argc; i++) {
+               CSolver* solver = CSolver::deserialize(argv[i]);
+               int value=solver->solve();
+               if (value ==1) {
+                       printf("%s is SAT\n", argv[i]);
+               } else {
+                       printf("%s is UNSAT\n", argv[i]);
+               }
+               solver->printConstraints();
+
+               delete solver;
+       }
+       return 1;
+}

diff --git a/src/Test/deserializersolvetest.cc b/src/Test/deserializersolvetest.cc
new file mode 100755 (executable)
index 0000000..7a938cf
--- /dev/null
+++ b/src/Test/deserializersolvetest.cc
@@ -0,0 +1,20 @@
+#include "csolver.h"
+
+
+int main(int argc, char ** argv){
+       if(argc < 2){
+               printf("You should specify file names ...");
+               exit(-1);       
+       }
+       for(int i = 1; i < argc; i++) {
+               CSolver* solver = CSolver::deserialize(argv[i]);
+               int value=solver->solve();
+               if (value ==1) {
+                       printf("%s is SAT\n", argv[i]);
+               } else {
+                       printf("%s is UNSAT\n", argv[i]);
+               }
+               delete solver;
+       }
+       return 1;
+}

diff --git a/src/config.h b/src/config.h
index 6eafa57c3aa598c399b0c8df4ffac5bf7c9951dc..0c73caed3505242452efe2d4048eb1108e99837f 100644 (file)
--- a/src/config.h
+++ b/src/config.h
@@ -20,7 +20,7 @@
 #define TRACE_DEBUG
 #endif
 
-#define SATCHECK_CONFIG
+//#define SATCHECK_CONFIG
 
 #ifndef CONFIG_ASSERT
 #define CONFIG_ASSERT

diff --git a/src/csolver.cc b/src/csolver.cc
index 25c9b1e0ffc130b8851ac8a6d118083b332f4c8f..95c06f8568ec9e4da27e2704a9f1348c85baf51a 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -22,6 +22,7 @@
 #include "serializer.h"
 #include "deserializer.h"
 #include "encodinggraph.h"
+#include <time.h>
 
 CSolver::CSolver() :
        boolTrue(BooleanEdge(new BooleanConst(true))),
@@ -95,8 +96,13 @@ CSolver* CSolver::deserialize(const char * file){
 
 void CSolver::serialize() {
        model_print("serializing ...\n");
-       printConstraints();
-       Serializer serializer("dump");
+       char buffer[255];
+       struct timespec t;
+       clock_gettime(CLOCK_REALTIME, &t);
+
+       unsigned long long nanotime=t.tv_sec*1000000000+t.tv_nsec;
+       int numchars=sprintf(buffer, "DUMP%llu", nanotime);
+       Serializer serializer(buffer);
        SetIteratorBooleanEdge *it = getConstraints();
        while (it->hasNext()) {
                BooleanEdge b = it->next();
@@ -459,7 +465,8 @@ int CSolver::solve() {
                tuner = new DefaultTuner();
                deleteTuner = true;
        }
-
+       serialize();
+       
        long long startTime = getTimeNano();
        computePolarities(this);