enum PredicateType {TABLEPRED, OPERATORPRED};
typedef enum PredicateType PredicateType;
-enum ASTNodeType {ORDERCONST, BOOLEANVAR, LOGICOP, PREDICATEOP, BOOLCONST, ELEMSET, ELEMFUNCRETURN, ELEMCONST};
+enum ASTNodeType {ORDERCONST, BOOLEANVAR, LOGICOP, PREDICATEOP, BOOLCONST, ELEMSET, ELEMFUNCRETURN, ELEMCONST, BOOLEANEDGE};
typedef enum ASTNodeType ASTNodeType;
enum Polarity {P_UNDEFINED=0, P_TRUE=1, P_FALSE=2, P_BOTHTRUEFALSE=3};
MKDIR_P = mkdir -p
OBJ_DIR = bin
-CPP_SOURCES := $(wildcard *.cc) $(wildcard AST/*.cc) $(wildcard ASTTransform/*.cc) $(wildcard Translator/*.cc) $(wildcard ASTAnalyses/*.cc) $(wildcard Tuner/*.cc) $(wildcard Collections/*.cc) $(wildcard Backend/*.cc) $(wildcard Encoders/*.cc)
+CPP_SOURCES := $(wildcard *.cc) $(wildcard AST/*.cc) $(wildcard ASTTransform/*.cc) $(wildcard Translator/*.cc) $(wildcard ASTAnalyses/*.cc) $(wildcard Tuner/*.cc) $(wildcard Collections/*.cc) $(wildcard Backend/*.cc) $(wildcard Encoders/*.cc) $(wildcard Serialize/*.cc)
-C_SOURCES := $(wildcard *.c) $(wildcard AST/*.c) $(wildcard ASTTransform/*.c) $(wildcard Translator/*.c) $(wildcard ASTAnalyses/*.c) $(wildcard Tuner/*.c) $(wildcard Collections/*.c) $(wildcard Backend/*.c) $(wildcard Encoders/*.c)
+C_SOURCES := $(wildcard *.c) $(wildcard AST/*.c) $(wildcard ASTTransform/*.c) $(wildcard Translator/*.c) $(wildcard ASTAnalyses/*.c) $(wildcard Tuner/*.c) $(wildcard Collections/*.c) $(wildcard Backend/*.c) $(wildcard Encoders/*.c) $(wildcard Serialize/*.c)
-HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard ASTTransform/*.h) $(wildcard Translator/*.h) $(wildcard ASTAnalyses/*.h) $(wildcard Tuner/*.h) $(wildcard Collections/*.h) $(wildcard Backend/*.h) $(wildcard Encoders/*.h)
+HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard ASTTransform/*.h) $(wildcard Translator/*.h) $(wildcard ASTAnalyses/*.h) $(wildcard Tuner/*.h) $(wildcard Collections/*.h) $(wildcard Backend/*.h) $(wildcard Encoders/*.h) $(wildcard Serialize/*.h)
OBJECTS := $(CPP_SOURCES:%.cc=$(OBJ_DIR)/%.o) $(C_SOURCES:%.c=$(OBJ_DIR)/%.o)
CFLAGS := -Wall -g -O0
-CFLAGS += -IAST -IASTTransform -IASTAnalyses -ITranslator -ICollections -IBackend -I. -IEncoders -ITuner
+CFLAGS += -IAST -IASTTransform -IASTAnalyses -ITranslator -ICollections -IBackend -I. -IEncoders -ITuner -ISerialize
LDFLAGS := -ldl -lrt -rdynamic
SHARED := -shared
${MKDIR_P} ${OBJ_DIR}/Collections
${MKDIR_P} ${OBJ_DIR}/Backend
${MKDIR_P} ${OBJ_DIR}/Encoders
+ ${MKDIR_P} ${OBJ_DIR}/Serialize
debug: CFLAGS += -DCONFIG_DEBUG
debug: all
--- /dev/null
+
+/*
+ * File: deserializer.cc
+ * Author: hamed
+ *
+ * Created on September 7, 2017, 6:08 PM
+ */
+
+#include "deserializer.h"
+#include "csolver.h"
+#include "unistd.h"
+#include "fcntl.h"
+
+Deserializer::Deserializer(const char* file):
+ solver(new CSolver())
+{
+ filedesc = open(file, O_RDONLY);
+
+ if (filedesc < 0) {
+ exit(-1);
+ }
+}
+
+Deserializer::~Deserializer() {
+ delete solver;
+}
+
+ssize_t Deserializer::myread(void* __buf, size_t __nbytes){
+ ssize_t t = read (filedesc, __buf, __nbytes);
+ write (1, __buf, __nbytes);
+ model_print("read\n");
+ return t;
+}
+
+CSolver * Deserializer::deserialize(){
+ ASTNodeType nodeType;
+ while(myread(&nodeType, sizeof(ASTNodeType) ) >0){
+ switch(nodeType){
+ case BOOLEANEDGE:
+ deserializeBooleanEdge();
+ break;
+ default:
+ ASSERT(0);
+ }
+ }
+ return solver;
+}
+
+void Deserializer::deserializeBooleanEdge(){
+ Boolean *b;
+ myread(&b, sizeof(Boolean*));
+ BooleanEdge tmp(b);
+ bool isNegated = tmp.isNegated();
+ ASSERT(map.contains(tmp.getBoolean()));
+ b = (Boolean*) map.get(tmp.getBoolean());
+ BooleanEdge res(b);
+ solver->addConstraint(isNegated?res.negate():res);
+}
--- /dev/null
+
+/*
+ * File: deserializer.h
+ * Author: hamed
+ *
+ * Created on September 7, 2017, 6:07 PM
+ */
+
+#ifndef DESERIALIZER_H
+#define DESERIALIZER_H
+#include "classlist.h"
+#include "mymemory.h"
+#include "structs.h"
+/**
+ * Style of serialized file:
+ * ASTNodeType#Pointer#ObjectDATA
+ *
+ * @param file
+ */
+class Deserializer {
+public:
+ Deserializer(const char* file);
+ CSolver *deserialize();
+ virtual ~Deserializer();
+private:
+ ssize_t myread (void *__buf, size_t __nbytes);
+ void deserializeBooleanEdge();
+ CSolver *solver;
+ int filedesc;
+ CloneMap map;
+};
+
+#endif /* DESERIALIZER_H */
+
--- /dev/null
+
+/*
+ * File: serializable.h
+ * Author: hamed
+ *
+ * Created on September 7, 2017, 3:39 PM
+ */
+
+#ifndef SERIALIZABLE_H
+#define SERIALIZABLE_H
+#include "classlist.h"
+
+class Serializable{
+ virtual void serialize(Serializer* ) = 0;
+};
+
+#endif /* SERIALIZABLE_H */
+
--- /dev/null
+
+/*
+ * File: serializer.cc
+ * Author: hamed
+ *
+ * Created on September 7, 2017, 3:38 PM
+ */
+
+#include "serializer.h"
+#include "unistd.h"
+#include "fcntl.h"
+
+Serializer::Serializer(const char *file) {
+ filedesc = open(file, O_WRONLY | O_CREAT, 0666);
+
+ if (filedesc < 0) {
+ exit(-1);
+ }
+}
+
+Serializer::~Serializer() {
+ if (-1 == close(filedesc)){
+ exit(-1);
+ }
+}
+
+void Serializer::mywrite(const void *__buf, size_t __n){
+ write (1, __buf, __n);
+ model_print("\n");
+ write (filedesc, __buf, __n);
+}
+
+
+void serializeBooleanEdge(Serializer* serializer, BooleanEdge& be){
+ if(serializer->isSerialized(be.getRaw()))
+ return;
+ serializer->addObject(be.getRaw());
+// b->seralize(serializer);
+ ASTNodeType type = BOOLEANEDGE;
+ serializer->mywrite(&type, sizeof(ASTNodeType));
+ serializer->mywrite(be.getRaw(), sizeof(Boolean*));
+}
\ No newline at end of file
--- /dev/null
+
+/*
+ * File: serializer.h
+ * Author: hamed
+ *
+ * Created on September 7, 2017, 3:38 PM
+ */
+
+#ifndef SERIALIZER_H
+#define SERIALIZER_H
+#include "mymemory.h"
+#include "structs.h"
+
+class Serializer {
+public:
+ Serializer(const char *file);
+ void mywrite(const void *__buf, size_t __n);
+ inline bool isSerialized(void *obj);
+ inline void addObject(void *obj) { map.put(obj, obj);}
+ virtual ~Serializer();
+ CMEMALLOC;
+private:
+ int filedesc;
+ CloneMap map;
+};
+
+inline bool Serializer::isSerialized(void* obj){
+ return map.contains(obj);
+}
+
+
+
+
+void serializeBooleanEdge(Serializer* serializer, BooleanEdge& be);
+
+#endif /* SERIALIZER_H */
+
Element *inputs2 [] = {e4, e3};
BooleanEdge pred = solver->applyPredicate(equal2, inputs2, 2);
solver->addConstraint(pred);
-
+ solver->serialize();
if (solver->solve() == 1)
printf("e1=%" PRIu64 " e2=%" PRIu64 " \n", solver->getElementValue(e1), solver->getElementValue(e2));
else
class Transformer;
class Set;
class BooleanLogic;
+class Serializer;
+
typedef uint64_t VarType;
typedef unsigned int uint;
#include "integerencoding.h"
#include "qsort.h"
#include "preprocess.h"
+#include "serializer.h"
+#include "deserializer.h"
CSolver::CSolver() :
boolTrue(BooleanEdge(new BooleanConst(true))),
return copy;
}
+void CSolver::serialize() {
+ {
+ Serializer serializer("dump");
+ SetIteratorBooleanEdge *it = getConstraints();
+ while (it->hasNext()) {
+ BooleanEdge b = it->next();
+ serializeBooleanEdge(&serializer, b);
+ }
+ delete it;
+ }
+ model_print("deserializing ...\n");
+ {
+ Deserializer deserializer("dump");
+ deserializer.deserialize();
+ }
+
+}
+
Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) {
Set *set = new Set(type, elements, numelements);
allSets.push(set);
void replaceBooleanWithFalse(BooleanEdge bexpr);
void replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb);
CSolver *clone();
+ void serialize();
void autoTune(uint budget);
void setTuner(Tuner *_tuner) { tuner = _tuner; }