Adding an API for finalizing MutableSet

diff --git a/src/AST/mutableset.cc b/src/AST/mutableset.cc
index d6657c550df8432f4cfd577fea379450243396a0..3d9db49b2ab6e4a117bcf1f3f4ab16e8fcb1aa20 100644 (file)
--- a/src/AST/mutableset.cc
+++ b/src/AST/mutableset.cc
@@ -1,5 +1,6 @@
 #include "mutableset.h"
 #include "csolver.h"
 #include "mutableset.h"
 #include "csolver.h"

+#include "qsort.h"

 
 MutableSet::MutableSet(VarType t) : Set(t) {
 }
 
 MutableSet::MutableSet(VarType t) : Set(t) {
 }


@@ -15,8 +16,13 @@ Set *MutableSet::clone(CSolver *solver, CloneMap *map) {
        s = solver->createMutableSet(type);
        for (uint i = 0; i < members->getSize(); i++) {
                ((MutableSet *)s)->addElementMSet(members->get(i));
        s = solver->createMutableSet(type);
        for (uint i = 0; i < members->getSize(); i++) {
                ((MutableSet *)s)->addElementMSet(members->get(i));

-               //              solver->addItem((MutableSet *) s, members->get(i));
+                               solver->addItem((MutableSet *) s, members->get(i));

        }
        }

+       ((MutableSet*)s)->finalize();

        map->put(this, s);
        return s;
 }
        map->put(this, s);
        return s;
 }

+
+void MutableSet::finalize(){
+       bsdqsort(members->expose(), members->getSize(), sizeof(uint64_t), intcompare);
+}
\ No newline at end of file

diff --git a/src/AST/mutableset.h b/src/AST/mutableset.h
index c608f3fd6f1c2f0794bd634260dda1cd81247d87..9cfa9e6a5acce23e4aab7360c43d72abaf4b2177 100644 (file)
--- a/src/AST/mutableset.h
+++ b/src/AST/mutableset.h
@@ -8,6 +8,7 @@ public:
        void addElementMSet(uint64_t element);
        Set *clone(CSolver *solver, CloneMap *map);
        bool isMutableSet() {return true;}
        void addElementMSet(uint64_t element);
        Set *clone(CSolver *solver, CloneMap *map);
        bool isMutableSet() {return true;}

+       void finalize();

        CMEMALLOC;
 };
 #endif
        CMEMALLOC;
 };
 #endif

diff --git a/src/AST/set.cc b/src/AST/set.cc
index fc8bf150f0bd3433caa3798eb8d0c0196fede809..66f8461ace3a070975749dfccd479f4a5b98b55a 100644 (file)
--- a/src/AST/set.cc
+++ b/src/AST/set.cc
@@ -4,10 +4,6 @@
 #include "serializer.h"
 #include "qsort.h"
 
 #include "serializer.h"
 #include "qsort.h"
 

-Set::Set(VarType t) : type(t), isRange(false), low(0), high(0) {
-       members = new Vector<uint64_t>();
-}
-

 int intcompare(const void *p1, const void *p2) {
        uint64_t a=*(uint64_t const *) p1;
        uint64_t b=*(uint64_t const *) p2;
 int intcompare(const void *p1, const void *p2) {
        uint64_t a=*(uint64_t const *) p1;
        uint64_t b=*(uint64_t const *) p2;


@@ -19,6 +15,11 @@ int intcompare(const void *p1, const void *p2) {
                return 1;
 }
 
                return 1;
 }
 

+Set::Set(VarType t) : type(t), isRange(false), low(0), high(0) {
+       members = new Vector<uint64_t>();
+}
+
+

 Set::Set(VarType t, uint64_t *elements, uint num) : type(t), isRange(false), low(0), high(0) {
        members = new Vector<uint64_t>(num, elements);
        bsdqsort(members->expose(), members->getSize(), sizeof(uint64_t), intcompare);
 Set::Set(VarType t, uint64_t *elements, uint num) : type(t), isRange(false), low(0), high(0) {
        members = new Vector<uint64_t>(num, elements);
        bsdqsort(members->expose(), members->getSize(), sizeof(uint64_t), intcompare);

diff --git a/src/AST/set.h b/src/AST/set.h
index efd281d77ae7effdd59ef2a38c570a380a4c821b..ef10b39bdaf3dc75830dde6d980a0a155b1293eb 100644 (file)
--- a/src/AST/set.h
+++ b/src/AST/set.h
@@ -37,5 +37,6 @@ protected:
 
 };
 
 
 };
 

+int intcompare(const void *p1, const void *p2);

 #endif/* SET_H */
 
 #endif/* SET_H */
 

diff --git a/src/csolver.cc b/src/csolver.cc
index 0eebb1759e8fde28ae529b403e853ad8e0f3202d..575a12b6f347714e5711eccd08c6131ec381de81 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -138,6 +138,10 @@ uint64_t CSolver::createUniqueItem(MutableSet *set) {
        return element;
 }
 
        return element;
 }
 

+void CSolver::finalizeMutableSet(MutableSet* set){
+       set->finalize();
+}
+

 Element *CSolver::getElementVar(Set *set) {
        Element *element = new ElementSet(set);
        allElements.push(element);
 Element *CSolver::getElementVar(Set *set) {
        Element *element = new ElementSet(set);
        allElements.push(element);

diff --git a/src/csolver.h b/src/csolver.h
index 42a62160b8eaf59fd4e9c8df9cf82f1d932a2e87..e49278116f5a00119ee9f8091b3aaa21b2ee80e9 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -34,6 +34,11 @@ public:
            items to the set. */
 
        uint64_t createUniqueItem(MutableSet *set);
            items to the set. */
 
        uint64_t createUniqueItem(MutableSet *set);

+       
+       /**
+        * Freeze and finalize the mutableSet ...
+        */
+       void finalizeMutableSet(MutableSet* set);

 
        /** This function creates an element variable over a set. */
 
 
        /** This function creates an element variable over a set. */