Add new test cases plus buffer serialization code
authorbdemsky <bdemsky@uci.edu>
Tue, 24 Oct 2017 01:23:20 +0000 (18:23 -0700)
committerbdemsky <bdemsky@uci.edu>
Tue, 24 Oct 2017 01:23:20 +0000 (18:23 -0700)
src/Serialize/deserializer.cc
src/Serialize/deserializer.h
src/Serialize/serializer.cc
src/Serialize/serializer.h
src/Test/deserializersolveprint.cc [new file with mode: 0755]
src/Test/deserializersolveprintopt.cc [new file with mode: 0755]
src/Test/deserializersolvetest.cc [new file with mode: 0755]
src/config.h
src/csolver.cc

index c0b8bf4..47de8b1 100644 (file)
 #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() {
index 6335c89..c56911d 100644 (file)
@@ -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;
index 118cf86..fe41a39 100644 (file)
 #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));
+}
index cf30a55..7030438 100644 (file)
@@ -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
@@ -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
@@ -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
@@ -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;
+}
index 6eafa57..0c73cae 100644 (file)
@@ -20,7 +20,7 @@
 #define TRACE_DEBUG
 #endif
 
-#define SATCHECK_CONFIG
+//#define SATCHECK_CONFIG
 
 #ifndef CONFIG_ASSERT
 #define CONFIG_ASSERT
index 25c9b1e..95c06f8 100644 (file)
@@ -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);