From: bdemsky Date: Tue, 24 Oct 2017 01:23:20 +0000 (-0700) Subject: Add new test cases plus buffer serialization code X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=da1157817f232a4c2b6b6e7947ef169e119c91e7 Add new test cases plus buffer serialization code --- diff --git a/src/Serialize/deserializer.cc b/src/Serialize/deserializer.cc index c0b8bf4..47de8b1 100644 --- 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 6335c89..c56911d 100644 --- 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 118cf86..fe41a39 100644 --- 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 cf30a55..7030438 100644 --- 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 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 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 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 6eafa57..0c73cae 100644 --- 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 25c9b1e..95c06f8 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -22,6 +22,7 @@ #include "serializer.h" #include "deserializer.h" #include "encodinggraph.h" +#include 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);