After resolving conflicts

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..6f14484c95646b2da6752ef9cb77e8d2fa27b437 100644 (file)
--- a/src/Serialize/deserializer.cc
+++ b/src/Serialize/deserializer.cc
@@ -145,33 +145,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() {
@@ -383,4 +386,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/common.h b/src/common.h
index 52c0b5f7ebd85b9e0830bafee33367b18bc19123..0efebf8152d581e20066ca2e32222b5be37e9717 100644 (file)
--- a/src/common.h
+++ b/src/common.h
@@ -18,21 +18,22 @@
 #include "config.h"
 #include "time.h"
 
-/*
-   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 { printf(fmt, ## __VA_ARGS__); } while (0)
- #define model_println(fmt, ...) do { model_print(fmt, ## __VA_ARGS__); model_print("\n");} while(0)
+#if 1
+extern int model_out;
+extern int model_err;
+extern int switch_alloc;
 
- #define model_print(fmt, ...) do { model_dprintf(model_out, fmt, ## __VA_ARGS__); } while (0)
+#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
+#endif
+#define model_println(fmt, ...) do { model_print(fmt, ## __VA_ARGS__); model_print("\n");} while(0)
 
- #define model_print_err(fmt, ...) do { model_dprintf(model_err, fmt, ## __VA_ARGS__); } while (0)
- */
 
-#define model_print printf
 
 #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/csolver.cc b/src/csolver.cc
index 311ad0f5052ac00ac29ff03cbdbc1082912fcd94..81329914c80acea519b310c0bad122328876aff8 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -48,7 +48,10 @@ CSolver::~CSolver() {
 
        size = allElements.getSize();
        for (uint i = 0; i < size; i++) {
-               delete allElements.get(i);
+                Element* el = allElements.get(i);
+                model_print("deleting ...%u", i);
+                ASSERT(el != NULL);
+               delete el;
        }
 
        size = allTables.getSize();
@@ -98,12 +101,11 @@ void CSolver::serialize() {
                }
                delete it;
        }
-       model_print("deserializing ...\n");
-       {
-               Deserializer deserializer("dump");
-               deserializer.deserialize();
-       }
-
+//     model_print("deserializing ...\n");
+//     {
+//             Deserializer deserializer("dump");
+//             deserializer.deserialize();
+//     }
 }
 
 Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) {
@@ -149,6 +151,7 @@ void CSolver::finalizeMutableSet(MutableSet *set) {
 
 Element *CSolver::getElementVar(Set *set) {
        Element *element = new ElementSet(set);
+        model_println("%%%%ElementVar:%u", allElements.getSize());
        allElements.push(element);
        return element;
 }
@@ -165,6 +168,7 @@ Element *CSolver::getElementConst(VarType type, uint64_t value) {
        Element *e = elemMap.get(element);
        if (e == NULL) {
                allSets.push(set);
+                model_println("%%%%ElementConst:%u", allElements.getSize());
                allElements.push(element);
                elemMap.put(element, element);
                return element;
@@ -180,6 +184,7 @@ Element *CSolver::applyFunction(Function *function, Element **array, uint numArr
        Element *e = elemMap.get(element);
        if (e == NULL) {
                element->updateParents();
+                model_println("%%%%ElementFunction:%u", allElements.getSize());
                allElements.push(element);
                elemMap.put(element, element);
                return element;
@@ -393,6 +398,9 @@ 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 (isTrue(constraint))
                return;
        else if (isFalse(constraint)) {