Merge

diff --git a/src/AST/element.h b/src/AST/element.h
index b74e582630d594d22708e1114442ed4cba3310ee..1e7b1f2899aaba7883573adab92c09b923ad5d79 100644 (file)
--- a/src/AST/element.h
+++ b/src/AST/element.h
@@ -26,6 +26,7 @@ public:
 class ElementSet : public Element {
 public:
        ElementSet(ASTNodeType type, Set *s);
+        virtual ~ElementSet(){}
        ElementSet(Set *s);
        virtual Element *clone(CSolver *solver, CloneMap *map);
        virtual void serialize(Serializer *serializer);
@@ -40,6 +41,7 @@ protected:
 class ElementConst : public ElementSet {
 public:
        ElementConst(uint64_t value, Set *_set);
+        virtual ~ElementConst(){}
        uint64_t value;
        virtual void serialize(Serializer *serializer);
        virtual void print();
@@ -49,6 +51,7 @@ public:
 
 class ElementFunction : public Element {
 public:
+        virtual ~ElementFunction(){}
        ElementFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus);
        Array<Element *> inputs;
        BooleanEdge overflowstatus;

diff --git a/src/AST/set.cc b/src/AST/set.cc
index 0a6e14f41a95dfdf439fa3ef06153083f67ccff2..52494e393ca9ef682fbd5d20bce9e52041d31665 100644 (file)
--- a/src/AST/set.cc
+++ b/src/AST/set.cc
@@ -139,16 +139,19 @@ void Set::serialize(Serializer *serializer) {
        serializer->mywrite(&This, sizeof(Set *));
        serializer->mywrite(&type, sizeof(VarType));
        serializer->mywrite(&isRange, sizeof(bool));
-       serializer->mywrite(&low, sizeof(uint64_t));
-       serializer->mywrite(&high, sizeof(uint64_t));
-       bool isMutable = isMutableSet();
+        bool isMutable = isMutableSet();
        serializer->mywrite(&isMutable, sizeof(bool));
-       uint size = members->getSize();
-       serializer->mywrite(&size, sizeof(uint));
-       for (uint i = 0; i < size; i++) {
-               uint64_t mem = members->get(i);
-               serializer->mywrite(&mem, sizeof(uint64_t));
-       }
+        if(isRange){
+                serializer->mywrite(&low, sizeof(uint64_t));
+                serializer->mywrite(&high, sizeof(uint64_t));
+        }else {
+                uint size = members->getSize();
+                serializer->mywrite(&size, sizeof(uint));
+                for(uint i=0; i<size; i++){
+                        uint64_t mem = members->get(i);
+                        serializer->mywrite(&mem, sizeof(uint64_t));
+                }
+        }
 }
 
 void Set::print() {

diff --git a/src/Serialize/deserializer.cc b/src/Serialize/deserializer.cc
index cd1e1a232fca290d3401e140e96854bbaf1dfbbb..c0b8bf4fcddbcc9e6a5c655df31fdf1e3db6d6ca 100644 (file)
--- a/src/Serialize/deserializer.cc
+++ b/src/Serialize/deserializer.cc
@@ -26,8 +26,6 @@ Deserializer::Deserializer(const char *file) :
 }
 
 Deserializer::~Deserializer() {
-       delete solver;
-
        if (-1 == close(filedesc)) {
                exit(-1);
        }
@@ -94,14 +92,18 @@ CSolver *Deserializer::deserialize() {
 }
 
 void Deserializer::deserializeBooleanEdge() {
-       Boolean *b;
-       myread(&b, sizeof(Boolean *));
-       BooleanEdge tmp(b);
+       Boolean *b_ptr;
+       myread(&b_ptr, sizeof(Boolean *));
+       BooleanEdge tmp(b_ptr);
        bool isNegated = tmp.isNegated();
        ASSERT(map.contains(tmp.getBoolean()));
-       b = (Boolean *) map.get(tmp.getBoolean());
-       BooleanEdge res(b);
-       solver->addConstraint(isNegated ? res.negate() : res);
+       b_ptr = (Boolean *) map.get(tmp.getBoolean());
+       BooleanEdge res(b_ptr);
+        bool isTopLevel;
+        myread(&isTopLevel, sizeof(bool));
+        if(isTopLevel){
+                solver->addConstraint(isNegated ? res.negate() : res);
+        }
 }
 
 void Deserializer::deserializeBooleanVar() {
@@ -145,33 +147,36 @@ void Deserializer::deserializeSet() {
        myread(&type, sizeof(VarType));
        bool isRange;
        myread(&isRange, sizeof(bool));
-       uint64_t low;
-       myread(&low, sizeof(uint64_t));
-       uint64_t high;
-       myread(&high, sizeof(uint64_t));
-       bool isMutable;
+        bool isMutable;
        myread(&isMutable, sizeof(bool));
-       Set *set;
-       if (isMutable) {
-               set = new MutableSet(type);
-       }
-       uint size;
-       myread(&size, sizeof(uint));
-       Vector<uint64_t> members;
-       for (uint i = 0; i < size; i++) {
-               uint64_t mem;
-               myread(&mem, sizeof(uint64_t));
-               if (isMutable) {
-                       ((MutableSet *) set)->addElementMSet(mem);
-               } else {
-                       members.push(mem);
-               }
-       }
-       if (!isMutable) {
-               set = isRange ? solver->createRangeSet(type, low, high) :
-                                       solver->createSet(type, members.expose(), size);
-       }
-       map.put(s_ptr, set);
+        if(isRange){
+                uint64_t low;
+                myread(&low, sizeof(uint64_t));
+                uint64_t high;
+                myread(&high, sizeof(uint64_t));
+                map.put(s_ptr, new Set(type, low, high));
+        } else{
+                Set *set;
+                if(isMutable){
+                        set = new MutableSet(type);
+                }
+                uint size;
+                myread(&size, sizeof(uint));
+                Vector<uint64_t> members;
+                for(uint i=0; i<size; i++){
+                        uint64_t mem;
+                        myread(&mem, sizeof(uint64_t));
+                        if(isMutable) {
+                                ((MutableSet*) set)->addElementMSet(mem);
+                        }else {
+                                members.push(mem);
+                        }
+                }
+                if(!isMutable){
+                        set = solver->createSet(type, members.expose(), size);
+                }
+                map.put(s_ptr, set);
+        }
 }
 
 void Deserializer::deserializeBooleanLogic() {
@@ -343,7 +348,6 @@ void Deserializer::deserializeElementFunction() {
        overflowstatus = (Boolean *) map.get(tmp.getBoolean());
        BooleanEdge res(overflowstatus);
        BooleanEdge undefStatus = isNegated ? res.negate() : res;
-
        map.put(ef_ptr, solver->applyFunction(function, members.expose(), size, undefStatus));
 }
 
@@ -383,4 +387,4 @@ void Deserializer::deserializeFunctionTable() {
        myread(&undefinedbehavior, sizeof(UndefinedBehavior));
 
        map.put(ft_ptr, solver->completeTable(table, undefinedbehavior));
-}
\ No newline at end of file
+}

diff --git a/src/Serialize/serializer.cc b/src/Serialize/serializer.cc
index 810ece81237929aed77dba5d43c2764d42f7f8c8..118cf867296a2c680b3b1e55831affaa2a553baf 100644 (file)
--- a/src/Serialize/serializer.cc
+++ b/src/Serialize/serializer.cc
@@ -30,12 +30,14 @@ void Serializer::mywrite(const void *__buf, size_t __n) {
 }
 
 
-void serializeBooleanEdge(Serializer *serializer, BooleanEdge be) {
-       if (be == BooleanEdge(NULL))
-               return;
+void serializeBooleanEdge(Serializer *serializer, BooleanEdge be, bool isTopLevel) {
+       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

diff --git a/src/Serialize/serializer.h b/src/Serialize/serializer.h
index f147773f5ebf9fae2533ebd38da5d4130d0ab9c3..cf30a55e952494cd6b480aca694a6dcf1797e444 100644 (file)
--- a/src/Serialize/serializer.h
+++ b/src/Serialize/serializer.h
@@ -33,7 +33,7 @@ inline bool Serializer::isSerialized(void *obj) {
 
 
 
-void serializeBooleanEdge(Serializer *serializer, BooleanEdge be);
+void serializeBooleanEdge(Serializer *serializer, BooleanEdge be, bool isTopLevel=false);
 
 #endif/* SERIALIZER_H */
 

diff --git a/src/Test/deserializertest.cc b/src/Test/deserializertest.cc
new file mode 100644 (file)
index 0000000..bbef427
--- /dev/null
+++ b/src/Test/deserializertest.cc
@@ -0,0 +1,14 @@
+#include "csolver.h"
+
+
+int main(int argc, char ** argv){
+       if(argc != 2){
+               printf("You only specify the name of the file ...");
+               exit(-1);       
+       }
+       CSolver* solver = CSolver::deserialize(argv[1]);
+       solver->printConstraints();
+        delete solver;
+       return 1;
+               
+}

diff --git a/src/common.h b/src/common.h
index fb4d7bacb1028c752f58dc62e947e214f4c05793..3d3adba8cb5df9e6956731cef0d6227cdb795f72 100644 (file)
--- a/src/common.h
+++ b/src/common.h
@@ -19,17 +19,21 @@
 #include "time.h"
 
 
-#if 1
+#ifdef SATCHECK_CONFIG
 extern int model_out;
 extern int model_err;
 extern int switch_alloc;
 
 #define model_dprintf(fd, fmt, ...) do { switch_alloc = 1; dprintf(fd, fmt, ## __VA_ARGS__); switch_alloc = 0; } while (0)
+
 #define model_print(fmt, ...) do { model_dprintf(model_out, fmt, ## __VA_ARGS__); } while (0)
 #define model_print_err(fmt, ...) do { model_dprintf(model_err, fmt, ## __VA_ARGS__); } while (0)
 #else
-#define model_print printf
+    #define model_print printf
 #endif
+#define model_println(fmt, ...) do { model_print(fmt, ## __VA_ARGS__); model_print("\n");} while(0)
+
+
 
 #define NEXTPOW2(x) ((x == 1) ? 1 : (1 << (sizeof(uint) * 8 - __builtin_clz(x - 1))))
 #define NUMBITS(x) ((x == 0) ? 0 : 8 * sizeof(x) - __builtin_clz(x))

diff --git a/src/config.h b/src/config.h
index db02014b5f128ab4262b83f69f1ec7ae5a12dfc9..0c53dd6dbab21bb3a45e2955f0110b322a1614c3 100644 (file)
--- a/src/config.h
+++ b/src/config.h
@@ -19,7 +19,7 @@
 //#define CONFIG_DEBUG
 #define TRACE_DEBUG
 #endif
-
+//#define SATCHECK_CONFIG
 #ifndef CONFIG_ASSERT
 #define CONFIG_ASSERT
 #endif

diff --git a/src/csolver.cc b/src/csolver.cc
index a2163a0c839103179fc6a31df3608ea71651d8a9..71205f68aab557baf933689510435ee4f312d328 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -48,7 +48,8 @@ CSolver::~CSolver() {
 
        size = allElements.getSize();
        for (uint i = 0; i < size; i++) {
-               delete allElements.get(i);
+                Element* el = allElements.get(i);
+               delete el;
        }
 
        size = allTables.getSize();
@@ -86,22 +87,22 @@ CSolver *CSolver::clone() {
        return copy;
 }
 
+CSolver* CSolver::deserialize(const char * file){
+       model_print("deserializing ...\n");
+       Deserializer deserializer(file);
+       return deserializer.deserialize();
+}
+
 void CSolver::serialize() {
        model_print("serializing ...\n");
-       {
-               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();
+        printConstraints();
+       Serializer serializer("dump");
+       SetIteratorBooleanEdge *it = getConstraints();
+       while (it->hasNext()) {
+               BooleanEdge b = it->next();
+               serializeBooleanEdge(&serializer, b, true);
        }
+       delete it;
 }
 
 Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) {
@@ -411,6 +412,12 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
 }
 
 void CSolver::addConstraint(BooleanEdge constraint) {
+#ifdef TRACE_DEBUG
+        model_println("****New Constraint******");
+#endif
+        if(constraint.isNegated())
+                model_print("!");
+        constraint.getBoolean()->print();
        if (isTrue(constraint))
                return;
        else if (isFalse(constraint)) {
@@ -471,10 +478,10 @@ int CSolver::solve() {
        //IntegerEncodingTransform iet(this);
        //iet.doTransform();
 
-       //EncodingGraph eg(this);
-       //eg.buildGraph();
-       //eg.encode();
-       //printConstraints();
+       EncodingGraph eg(this);
+       eg.buildGraph();
+       eg.encode();
+//     printConstraints();
        naiveEncodingDecision(this);
        satEncoder->encodeAllSATEncoder(this);
        model_print("Is problem UNSAT after encoding: %d\n", unsat);
@@ -499,7 +506,6 @@ void CSolver::printConstraints() {
                model_print("\n");
        }
        delete it;
-
 }
 
 void CSolver::printConstraint(BooleanEdge b) {

diff --git a/src/csolver.h b/src/csolver.h
index 2730a934164a7d267bdf26d47f78576671c8c52a..16396f9b389fb933168fdf1c7740a735a1579218 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -152,6 +152,7 @@ public:
        void replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb);
        CSolver *clone();
        void serialize();
+       static CSolver* deserialize(const char * file);
        void autoTune(uint budget);
 
        void setTuner(Tuner *_tuner) { tuner = _tuner; }

diff --git a/src/mymemory.h b/src/mymemory.h
index 92fb0fed609057c3fd40132bcf507986489133cd..700fb4f72553957a33259b9e7707e209b797367d 100644 (file)
--- a/src/mymemory.h
+++ b/src/mymemory.h
@@ -26,7 +26,7 @@
    void * ourrealloc(void *ptr, size_t size);
  */
 
-#if 1
+#ifdef SATCHECK_CONFIG
 void *model_malloc(size_t size);
 void model_free(void *ptr);
 void *model_calloc(size_t count, size_t size);